通过预测证明进度提升大模型在Lean中的定理证明效率。
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
- 构建模型预测定理证明的进展与剩余步骤数。
- 在Mathlib4上实现75.8%的预测准确率，长证明提升3.8%成功率。
- 适合需要高效辅助证明的数学形式化项目使用者。
数学推理对大型语言模型（LLM）仍是重大挑战，因存在幻觉问题。结合形式化证明助手Lean后，可通过严格验证消除幻觉，使定理证明更可靠。然而，即使有形式化验证，LLM在长证明和复杂形式化中仍表现不佳。尽管Lean+LLM可协助检索引理、生成策略或完整证明，但缺乏对证明进度的感知能力，严重影响大型形式化项目的开发效率。本文提出LeanProgress，一种基于大规模Lean证明语料（来自Lean Workbook Plus和Mathlib4）训练的证明进度预测方法。通过数据预处理与分布平衡技术应对证明长度的偏斜问题。实验表明，该方法在预测证明进度与剩余步骤方面达到75.8%的准确率；集成至Reprover的最佳优先搜索框架后，在Mathlib4上较基线41.4%的性能提升3.8%，尤其在长证明中效果显著。结果表明，证明进度预测能有效提升自动与交互式定理证明的效率，帮助用户优化策略决策。代码已合并至LeanDojo-v2库。
原文摘要 · Abstract (English)
Mathematical reasoning remains a significant challenge for Large Language Models (LLMs) due to hallucinations. When combined with formal proof assistants like Lean, these hallucinations can be eliminated through rigorous verification, making theorem proving reliable. However, even with formal verification, LLMs still struggle with long proofs and complex mathematical formalizations. While Lean with LLMs offers valuable assistance with retrieving lemmas, generating tactics, or even complete proofs, it lacks a crucial capability: providing a sense of proof progress. This limitation particularly impacts the overall development efficiency in large formalization projects. We introduce LeanProgress, a method that predicts the progress in the proof. Training and evaluating our models made on a large corpus of Lean proofs from Lean Workbook Plus and Mathlib4 and how many steps remain to complete it, we employ data preprocessing and balancing techniques to handle the skewed distribution of proof lengths. Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.8% in predicting the amount of progress and, hence, the remaining number of steps. When integrated into a best-first search framework using Reprover, our method shows a 3.8% improvement on Mathlib4 compared to baseline performances of 41.4%, particularly for longer proofs. These results demonstrate how proof progress prediction can enhance both automated and interactive theorem proving, enabling users to make more informed decisions about proof strategies. Our code is merged in this library here https://github.com/lean-dojo/LeanDojo-v2.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。