Apprendre à réparer les preuves Lean à partir des retours du compilateur
Learning to Repair Lean Proofs from Compiler Feedback
February 3, 2026
Auteurs: Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Vasily Ilin
cs.AI
Résumé
À mesure que les assistants de preuve neuronaux deviennent plus agentiques, la capacité à interpréter et à agir sur les retours du compilateur devient cruciale. Cependant, les jeux de données Lean existants sont presque exclusivement constitués de preuves correctes, offrant peu de supervision pour comprendre et réparer les échecs. Nous étudions la réparation de preuves Lean comme un problème d'apprentissage supervisé : étant donné une preuve erronée et un retour du compilateur, prédire à la fois une preuve corrigée et un diagnostic en langage naturel ancré dans ce même retour. Nous présentons APRIL (Automated Proof Repair in Lean), un jeu de données de 260 000 tuples supervisés associant des échecs de preuve générés systématiquement à des diagnostics du compilateur, ainsi qu'à des cibles de réparation et d'explication alignées. L'entraînement de modèles de langage sur APRIL améliore considérablement la précision des réparations et le raisonnement conditionné par les retours ; dans notre cadre d'évaluation de réparation en une seule tentative, un modèle de 4 milliards de paramètres affiné surpasse la base de référence open-source la plus performante. Nous considérons la supervision conditionnée par les diagnostics comme un signal d'entraînement complémentaire pour les assistants de preuve utilisant les retours. Notre jeu de données est disponible à l'adresse https://huggingface.co/datasets/uw-math-ai/APRIL{ce lien}.
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}.