Lernen, Lean-Beweise anhand von Compiler-Feedback zu reparieren
Learning to Repair Lean Proofs from Compiler Feedback
February 3, 2026
Autoren: Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Vasily Ilin
cs.AI
Zusammenfassung
Da neuronale Theorembeweiser zunehmend agentenhaft werden, ist die Fähigkeit kritisch, Compiler-Feedback zu interpretieren und danach zu handeln. Allerdings bestehen bestehende Lean-Datensätze fast ausschließlich aus korrekten Beweisen und bieten kaum Aufsicht für das Verständnis und Reparieren von Fehlschlägen. Wir untersuchen das Reparieren von Lean-Beweisen als ein überwachtes Lernproblem: Gegeben ein fehlerhafter Beweis und Compiler-Feedback, sagt man sowohl einen korrigierten Beweis als auch eine Diagnose in natürlicher Sprache vorher, die auf demselben Feedback basiert. Wir stellen APRIL (Automated Proof Repair in Lean) vor, einen Datensatz von 260.000 überwachten Tupeln, die systematisch generierte Beweis-Fehlschläge mit Compiler-Diagnosen sowie abgestimmten Reparatur- und Erklärungszielen paaren. Das Trainieren von Sprachmodellen auf APRIL verbessert die Reparaturgenauigkeit und das feedback-konditionierte Schließen erheblich; in unserem Single-Shot-Reparatur-Evaluierungssetting übertrifft ein feinabgestimmtes 4-Milliarden-Parameter-Modell die stärkste Open-Source-Baseline. Wir betrachten diagnose-konditionierte Überwachung als ein komplementäres Trainingssignal für Feedback-nutzende Beweiser. Unser Datensatz ist verfügbar unter https://huggingface.co/datasets/uw-math-ai/APRIL{diesem 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}.