Imparare a Riparare Dimostrazioni Lean dal Feedback del Compilatore
Learning to Repair Lean Proofs from Compiler Feedback
February 3, 2026
Autori: Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Vasily Ilin
cs.AI
Abstract
Man mano che i dimostratori di teoremi neurali diventano sempre più agentici, la capacità di interpretare e agire in base al feedback del compilatore è fondamentale. Tuttavia, i dataset esistenti per Lean sono composti quasi esclusivamente da dimostrazioni corrette, offrendo poca supervisione per comprendere e riparare i fallimenti. Studiamo la riparazione di dimostrazioni in Lean come un problema di apprendimento supervisionato: data una dimostrazione errata e il feedback del compilatore, prevedere sia una dimostrazione corretta sia una diagnosi in linguaggio naturale basata sullo stesso feedback. Introduciamo APRIL (Automated Proof Repair in Lean), un dataset di 260.000 tuple supervisionate che associano fallimenti dimostrativi generati sistematicamente a diagnosi del compilatore e a target allineati di riparazione e spiegazione. L'addestramento di modelli linguistici su APRIL migliora sostanzialmente l'accuratezza della riparazione e il ragionamento condizionato dal feedback; nella nostra impostazione di valutazione della riparazione in singolo tentativo, un modello da 4 miliardi di parametri fine-tunato supera la baseline open-source più robusta. Consideriamo la supervisione condizionata dalla diagnosi come un segnale di addestramento complementare per i dimostratori che utilizzano il feedback. Il nostro dataset è disponibile all'indirizzo https://huggingface.co/datasets/uw-math-ai/APRIL{questo link}.
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}.