Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2602.02990 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912965514493952 |
|---|---|
| author | Wang, Evan Chess, Simon Lee, Daniel Ge, Siyuan Mallavarapu, Ajit Alper, Jarod Ilin, Vasily |
| author_facet | Wang, Evan Chess, Simon Lee, Daniel Ge, Siyuan Mallavarapu, Ajit Alper, Jarod Ilin, Vasily |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_02990 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Learning to Repair Lean Proofs from Compiler Feedback Wang, Evan Chess, Simon Lee, Daniel Ge, Siyuan Mallavarapu, Ajit Alper, Jarod Ilin, Vasily Machine Learning 68T01 (Primary) 68N18 (Secondary) I.2.6; F.4.1 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. |
| title | Learning to Repair Lean Proofs from Compiler Feedback |
| topic | Machine Learning 68T01 (Primary) 68N18 (Secondary) I.2.6; F.4.1 |
| url | https://arxiv.org/abs/2602.02990 |