Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.
核心贡献 · Key contributions
提出一种迭代方法，从非正式数学问题中合成 800 万条带证明的形式化语句。 Proposes an iterative method to synthesize 8 million formal statements with proofs from informal math problems.
在 miniF2F 上以 64 个样本实现 46.3%的整句证明生成准确率，超越 GPT-4 和强化学习方法。 Achieves state-of-the-art whole-proof generation accuracy of 46.3% on miniF2F with 64 samples, surpassing GPT-4 and RL methods.
成功证明 FIMO 基准中 148 个问题中的 5 个，而 GPT-4 未能证明任何问题。 Successfully proves 5 out of 148 FIMO problems, while GPT-4 proves none.
引入对语句及其否定进行双重并发证明搜索，以提高效率。 Introduces dual concurrent proof search for statements and their negations to improve efficiency.
证明合成数据集规模与定理证明模型性能之间存在明确相关性。 Demonstrates clear correlation between synthetic dataset size and model performance on theorem proving.
开源大规模合成数据集和模型，以促进进一步研究。 Open-sources the large-scale synthetic dataset and model to facilitate further research.
局限 · Limitations
主要关注高中和本科水平的代数和数论问题。 Focuses primarily on algebra and number theory at high school and undergraduate levels.
合成数据质量依赖于基础模型的自动形式化能力。 Synthetic data quality depends on the base model's autoformalization capability.
尽管采用双重并发方法，证明搜索仍可能计算密集。 Proof search may still be computationally intensive despite dual concurrent approach.
对需要复杂定义的高级数学主题的泛化能力有限。 Generalizability to advanced mathematical topics requiring complex definitions is limited.
在基准测试上的表现可能无法完全反映真实世界的定理证明场景。 Performance on benchmarks may not fully reflect real-world theorem proving scenarios.
论文章节 · Sections（共 16）
摘要Abstract
1 引言1 Introduction
2 背景与相关工作2 Background and Related Works
3 方法3 Approach
3.1 自动形式化3.1 Autoformalization
3.2 质量过滤3.2 Quality Filtering
3.3 命题证明3.3 Statement Proving
3.4 迭代增强3.4 Iterative Enhancement
4.1 实验设置4.1 Experimental Setup
4.2 主要结果4.2 Main Results
4.3 消融研究4.3 Ablation Studies
5 案例研究5 Case Studies
5.1 带完整证明的自动形式化定理5.1 Autoformalized Theorem with Complete Proof
5.2 假设不一致的定理自动形式化5.2 Autoformalization of Theorem with Inconsistent Hypotheses