Aprendendo a Reparar Provas do Lean a partir de Feedback do Compilador
Learning to Repair Lean Proofs from Compiler Feedback
February 3, 2026
Autores: Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Vasily Ilin
cs.AI
Resumo
À medida que os provadores de teoremas neurais se tornam cada vez mais agentivos, a capacidade de interpretar e agir com base no feedback do compilador é crucial. No entanto, os conjuntos de dados existentes para Lean consistem quase exclusivamente em provas corretas, oferecendo pouca supervisão para compreender e reparar falhas. Estudamos o reparo de provas em Lean como um problema de aprendizagem supervisionada: dada uma prova errónea e o feedback do compilador, prever tanto uma prova corrigida quanto um diagnóstico em linguagem natural fundamentado no mesmo feedback. Apresentamos o APRIL (Automated Proof Repair in Lean), um conjunto de dados com 260.000 tuplas supervisionadas que emparelham falhas de prova geradas sistematicamente com diagnósticos do compilador e alinham os objetivos de reparo e explicação. Treinar modelos de linguagem no APRIL melhora substancialmente a precisão do reparo e o raciocínio condicionado ao feedback; em nosso cenário de avaliação de reparo em tentativa única, um modelo de 4 mil milhões de parâmetros afinado supera a linha de base de código aberto mais robusta. Consideramos a supervisão condicionada ao diagnóstico como um sinal de treinamento complementar para provadores que utilizam feedback. Nosso conjunto de dados está disponível em https://huggingface.co/datasets/uw-math-ai/APRIL.
English
As neural theorem provers become increasingly agentic, the ability to interpret and act on compiler feedback is critical. However, existing Lean datasets consist almost exclusively of correct proofs, offering little supervision for understanding and repairing failures. We study Lean proof repair as a supervised learning problem: given an erroneous proof and compiler feedback, predict both a corrected proof and a natural-language diagnosis grounded in the same feedback. We introduce APRIL (Automated Proof Repair in Lean), a dataset of 260,000 supervised tuples pairing systematically generated proof failures with compiler diagnostics and aligned repair and explanation targets. Training language models on APRIL substantially improves repair accuracy and feedback-conditioned reasoning; in our single-shot repair evaluation setting, a finetuned 4B-parameter model outperforms the strongest open-source baseline. We view diagnostic-conditioned supervision as a complementary training signal for feedback-using provers. Our dataset is available at https://huggingface.co/datasets/uw-math-ai/APRIL{this link}.