用状态转移图生成百万级形式化定理，提升自动证明性能
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
- 通过交互式Lean客户端探索状态转移路径，自动生成新证明
- 在Mathlib4上生成470万定理、10亿词元的超大规模数据集
- 训练模型超越现有最佳水平，适合形式化验证与AI推理研究者
大型语言模型在数学证明生成方面展现出巨大潜力，但偶尔出错会导致整个证明无效。证明助手如Lean可通过形式语言逐步验证证明，近年来已有研究尝试用AI生成其语言的证明。然而，缺乏大规模的Lean证明数据集限制了自动化定理证明（ATP）模型的表现。我们提出了LeanNavigator方法，通过发现已有Lean定理的新证明方式，构建大规模定理与证明数据集。借助交互式Lean客户端和高效的证明步骤生成方法，该方法高效生成新定理及其对应证明。应用于Mathlib4时，生成了470万条定理，共10亿词元，规模超过以往数据集一个数量级以上。基于此数据集训练的AI模型在定理证明任务中表现优于当前最优的ReProver模型。结果验证了我们的假设，表明大规模数据集对提升自动定理证明器性能至关重要。
原文摘要 · Abstract (English)
Large Language Models (LLMs) have demonstrated significant potential in generating mathematical proofs. However, a persistent challenge is that LLMs occasionally make mistakes, while even a minor mistake can invalidate an entire proof. Proof assistants like Lean offer a great remedy. They are designed for verifying each step of a proof in a formal language, and in recent years researchers have created AI models to generate proofs in their languages. However, the scarcity of large-scale datasets of Lean proofs restrict the performance of such Automated Theorem Proving (ATP) models. We developed LeanNavigator, a novel method for generating a large-scale dataset of Lean theorems and proofs by finding new ways to prove existing Lean theorems. By leveraging an interactive Lean client and an efficient method for proof step generation, LeanNavigator efficiently produces new theorems with corresponding proofs. Applying this approach to Mathlib4, we generated 4.7 million theorems totaling 1 billion tokens, surpassing previous datasets by more than an order of magnitude. Using this extensive dataset, we trained an AI model that outperforms the state-of-the-art ReProver model in theorem-proving tasks. These results confirm our hypothesis and demonstrate the critical role of large datasets in improving the performance of automated theorem provers.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。