让AI学会根据编译器报错修复Lean定理证明。
Learning to Repair Lean Proofs from Compiler Feedback
- 用编译器反馈指导模型修复错误证明，生成正确代码和解释。
- 构建了26万条带反馈的错误证明与修复数据，提升修复准确率。
- 适合研究自动定理证明、AI辅助编程的开发者使用。
随着神经定理证明器日益具备自主性，理解并响应编译器反馈的能力变得至关重要。然而，现有的Lean数据集几乎全由正确证明构成，难以提供失败情况下的有效监督。本文将Lean证明修复视为监督学习问题：给定一个错误证明及编译器反馈，预测正确的证明和基于同一反馈的自然语言诊断。我们提出APRIL（Automated Proof Repair in Lean）数据集，包含260,000个由系统生成的证明错误及其对应的编译诊断与对齐的修复目标。在该数据集上训练语言模型显著提升了修复准确率和反馈驱动的推理能力；在单次修复评估中，微调后的40亿参数模型优于现有最强开源基线。我们认为诊断条件监督是反馈型证明器的重要补充训练信号。数据集已公开于https://huggingface.co/datasets/uw-math-ai/APRIL。
原文摘要 · Abstract (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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。