Source-linked AI summary
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, Xiaodan Liang
TL;DR
Formal theorem proving needs reliable verification, but LLM progress is constrained by limited formal-proof data and the effort required to create proofs. The paper generates and filters large-scale Lean 4 theorem-proof data from competition problems, then trains DeepSeekMath 7B on it. The resulting model outperforms reported baselines on miniF2F and proves FIMO problems that GPT-4 does not.
Problem
LLM-based formal theorem proving is hindered by scarce formal training data, while writing formal proofs requires substantial effort and expertise.
Method
The method autoformalizes competition problems, filters low-quality statements, generates and verifies proofs, and iteratively trains the prover on validated data.
Results
The model achieves state-of-the-art benchmark performance, including 46.3% whole-proof accuracy with 64 samples on miniF2F-test and 5 of 148 FIMO problems proved versus none by GPT-4.
Takeaways & Limitations
Large-scale synthetic theorem-proof data is associated with stronger Lean 4 theorem-proving performance and is released with the model to support further research.
Takeaways & Limitations
The work mainly covers algebra and number theory at middle-school and undergraduate levels, and one autoformalization incorrectly imposed a universal hypothesis unsupported by the problem.
Abstract
from arXiv · showhide
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.
1 Introduction
Formal theorem proving offers reliable verification, but progress is limited by the effort of writing proofs and scarce formal training data. The paper addresses this bottleneck with large-scale synthetic Lean 4 data and reports strong benchmark results.
- Formal languages such as Lean enable computer-verifiable proofs, but creating them requires substantial effort and specialized expertise.
- Limited formal-proof data constrains LLM-based theorem proving, while search methods struggle with the large spaces of complex theorems.
- The method translates competition problems into Lean 4 statements, filters low-quality outputs, generates proofs, and verifies them in Lean 4.
- Negated statements are proved in parallel with original statements, terminating the process when either side is proved to reduce wasted search.
- 8 million formal statements with proofs are synthesized through an iterative method designed to improve synthetic-data scalability and quality.
- 46.3% whole-proof accuracy with 64 samples on Lean 4 miniF2F-test surpasses GPT-4 at 23.0% and a reinforcement-learning method at 41.0%.The model also achieves 52% cumulatively on miniF2F-test and proves 5 of 148 FIMO problems, while GPT-4 proves none.
2 Background and Related Works
Automated theorem proving has progressed from efficient first-order provers toward neural, search-guided systems for more complex formal mathematics. LLM-based methods and autoformalization address proof generation and limited formal corpora, but existing synthetic-data approaches remain constrained.
- Classical automated theorem provers are efficient for first-order logic but often struggle with complex theorems in modern proof assistants.
- Neural-guided tree-search methods combine theorem proving with reinforcement learning to improve proof-search accuracy.
- LLM-based theorem provers iteratively generate proof steps and verify them through formal verifiers.
- Autoformalization converts natural-language descriptions into formal statements that proof assistants can verify, helping address limited formal training corpora.
3 Approach
The approach builds Lean 4 proof data by autoformalizing accessible mathematical problems, filtering flawed statements, proving candidates with dual search, and iteratively retraining the prover. This pipeline targets both data quality and proof-generation scale.
- 3 Approach: The pipeline autoformalizes informal problems, filters statements, generates proofs with DeepSeek-Prover, and validates them using Lean 4.
- 3.1 Autoformalization: High-school and undergraduate competition problems are prioritized because explicit conditions and goals are easier to formalize than advanced constructions.
- 3.1 Autoformalization: The model is initialized from DeepSeekMath-Base 7B and fine-tuned on MMA data to translate natural-language problems into Lean 4 statements.
- 3.2 Quality Filtering: Model scoring removes overly simplistic statements, while hypothesis rejection excludes statements whose assumptions can prove False.
- 3.2 Quality Filtering: 712,073 high-quality formal statements remain after model scoring and hypothesis rejection.
- 3.3 Statement Proving: Dual concurrent searches prove either Γ ⊢ P or Γ ⊢ ¬P, stopping when one succeeds and establishing the other’s unprovability.
- 3.3 Statement Proving: Validated proofs for original statements and negations are aggregated as data augmentation for further training.
- 3.4 Iterative Enhancement: Each iteration fine-tunes the model on newly generated data and reuses the updated model for subsequent autoformalization.
4 Experiments
The experiments evaluate DeepSeek-Prover on Lean 4 theorem-proving benchmarks and compare it with established baselines. Additional analyses examine autoformalized data, proof-data quality, iterative enhancement, and dataset scale.
- Experimental Setup: DeepSeek-Prover is built on DeepSeekMath-Base 7B and evaluated against GPT-4 and other theorem-proving baselines.The model is a decoder-only transformer fine-tuned with synthetic data.
- Experimental Setup: The evaluation uses miniF2F’s 244 validation and 244 test problems, spanning arithmetic through competition-level mathematics.The Lean 4 version was released by LeanDojo.
- Main Results: 60.2% on miniF2F-valid and 52.0% on miniF2F-test are DeepSeek-Prover’s cumulative scores, exceeding GPT-4’s 25.41% and 22.95%.Hypertree Proof Search reaches up to 58.6% on miniF2F-valid and 41.0% on miniF2F-test.
- Main Results: 4 theorems are proved on FIMO with 100 attempts per theorem, while increasing attempts to 4,096 proves one additional theorem.GPT-4 proves none of the benchmark’s formal problems.
- Ablation Studies: Models trained with autoformalized data significantly outperform models trained solely with Lean 4 mathlib data.The comparison uses expert iteration and miniF2F pass rates at pass@128.
- Ablation Studies: High-score proof data outperforms low-score proof data by 4.5%, while successive synthesis iterations and larger synthetic-data fractions improve theorem-proving performance.These analyses support the roles of proof-data filtering, iterative enhancement, and dataset scaling.
5 Case Studies
The case studies show Lean autoformalization translating mathematical statements into verified formal proofs while detecting inconsistent hypotheses. One example formalizes a determinant identity, and another exposes an overgeneralized assumption through a counterexample.
- 5.1 Autoformalized Theorem with Complete Proof: The determinant example translates the matrix expression and determinant assertion into Lean’s formal language.
- 5.1 Autoformalized Theorem with Complete Proof: The first case study formalizes a determinant-zero problem as a specific 3 × 3 matrix over real numbers in Lean.The formalization uses Matrix.det and Lean’s ![...] notation to represent matrix rows.
- 5.2 Autoformalization of Theorem with Inconsistent Hypotheses: The second case study concerns a determinant D and a claimed conclusion D^2 = 154 under nonzero-variable assumptions.
- 5.2 Autoformalization of Theorem with Inconsistent Hypotheses: The initial formalization incorrectly universalizes D^2 = 154 over all nonzero a, b, and c, although the problem statement does not make that claim.
- 5.2 Autoformalization of Theorem with Inconsistent Hypotheses: The model identifies the inconsistency and provides a counterexample, illustrating verification and hypothesis checking in the case studies.
6 Conclusion
The paper presents large-scale synthetic Lean 4 proof data generated from mathematical competition problems and reports improved automated theorem-proving performance after training DeepSeekMath 7B on it. The authors report results on miniF2F and FIMO and release the dataset and model, while noting a current focus on algebra and number theory.
- The method creates 8 million proof data points from formalized high-school and undergraduate-level competition problems.
- The trained DeepSeekMath 7B model significantly improves automated theorem-proving performance and outperforms GPT-4 and other methods on miniF2F and FIMO.
- The authors release the dataset and model to support further research in automated theorem proving and formal mathematical reasoning.
- The current work mainly focuses on algebra and number theory at middle-school and undergraduate levels.
Broader Impact
The paper’s broader impact is framed around using large-scale synthetic proof data to advance automated theorem proving and formal mathematical reasoning. The authors also connect the work to more reliable proof verification and educational resources.
- Large-scale synthetic proof data generated from informal mathematical problems may advance automated theorem proving.
- The work may enhance large language models’ capabilities in formal theorem proving and contribute to more reliable mathematical proof verification.
- The released resources are described as potentially valuable educational resources for students and researchers.
A.1 Prompts
The prompts define a scoring framework for judging whether formal Lean4 statements are interesting to the community. It evaluates relevance, complexity, interdisciplinary potential, community needs, and innovativeness, then assigns a qualitative rating.
- The scoring process asks the evaluator to translate each formal statement into natural language and justify its scores before assessment.
- Evaluation criteria: Relevance measures whether a statement addresses a problem or concept actively researched in mathematics or related fields.
- Evaluation criteria: Complexity and depth assess whether a statement challenges existing theories or methodologies while offering significant insights or advancements.
- Evaluation criteria: Interdisciplinary potential considers connections between mathematics and fields such as computer science, physics, or biology.
- Evaluation criteria: Community needs and gaps assess whether a statement addresses an identified need within Lean4 or the broader mathematical community.
- Evaluation criteria: Innovativeness evaluates whether a statement proposes new methods, concepts, or applications, after which the evaluator selects a qualitative rating.
A.2 Case Studies of Autoformalization
The case studies show how informal competition problems are translated into Lean 4 statements and paired with complete proofs across algebra, combinatorics, and vector geometry.
- Polynomial example: The polynomial example formalizes an interval-union condition and proves that the parameter a equals 3.The condition is represented using Set.Iio (-1) ∪ Set.Ioi 1, and the proof evaluates the hypothesis at 0, 1, and −1 before using linarith.
- Combinatorial example: The binomial-coefficient example defines F and f with Nat.choose and formalizes nested existential and implication structure.The accompanying proof uses simplification and aesop to establish the conclusion.
- Vector example: The vector example represents three-dimensional vectors as Cartesian products and expands dot products into sums of componentwise products.Given dot products −3, 4, and 6, the generated Lean proof derives the target equality with linarith.
A.3 Example Lean Proofs Generated by Our Model
The generated Lean proofs cover inequalities, weighted averages, infinitude arguments, number-theoretic statements, and FIMO-style problems, with verification performed in a configured Lean 4 environment.
- Inequalities: The Bernoulli-type inequality is formalized for real x and natural n, then proved by induction using algebraic simplification and nonnegativity.The assumptions are −1 < x and 0 < n, and the conclusion is 1 + n*x ≤ (1 + x)^n.
- Weighted averages: The class-average example formalizes the 3:4 enrollment ratio and proves the combined mean is 76.The proof uses field simplification, normalization, and linear arithmetic.
- Existence arguments: The infinitude example proves that for every positive n, a larger m and positive p exist with m*p ≤ m + p.The generated proof chooses m = n + 1 and p = 1.
- FIMO examples: The FIMO examples include a square-root bounding fraction and a functional equation whose conclusion is f x = x.The proofs use explicit witnesses, induction, simplification, and linear arithmetic.
- Verification setup: The Lean code is verified with a Mathlib-heavy prefix, unlimited heartbeats, and Aesop tracing enabled.The environment imports algebraic, order, real-number, set, topology, and automation modules.