Leren Lean-bewijzen te repareren op basis van compilerfeedback
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
Samenvatting
Naarmate neurale theoreem-bewijzers steeds meer agentisch worden, is het vermogen om compiler-feedback te interpreteren en ernaar te handelen cruciaal. Bestaande Lean-datasets bestaan echter vrijwel uitsluitend uit correcte bewijzen, waardoor er weinig supervisie is voor het begrijpen en repareren van fouten. Wij bestuderen Lean-bewijsreparatie als een supervised learning-probleem: gegeven een foutief bewijs en compiler-feedback, voorspel zowel een gecorrigeerd bewijs als een diagnose in natuurlijke taal die gebaseerd is op dezelfde feedback. Wij introduceren APRIL (Automated Proof Repair in Lean), een dataset van 260.000 gesuperviseerde tuples die systematisch gegenereerde bewijsfouten koppelen aan compiler-diagnostiek en uitgelijnde reparatie- en uitlegdoelen. Het trainen van taalmodellen op APRIL verbetert de reparatienauwkeurigheid en feedback-gestuurd redeneren aanzienlijk; in onze single-shot reparatie-evaluatieomgeving presteert een gefinetuned model met 4B parameters beter dan de sterkste open-source baseline. Wij zien diagnostiek-gestuurde supervisie als een complementair trainingssignaal voor feedback-gebruikende bewijzers. Onze dataset is beschikbaar op https://huggingface.co/datasets/uw-math-ai/APRIL{deze 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}.