Source-linked AI summary
DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, Chong Ruan
TL;DR
Formal theorem proving remains difficult for LLMs because informal reasoning must be converted into precise Lean proofs. DeepSeek-Prover-V2 uses recursive subgoal decomposition, synthetic cold-start data, and reinforcement learning to bridge these forms of reasoning. The resulting model achieves strong performance across formal theorem-proving benchmarks, while evaluation remains subject to a Lean 4.9.0 user-interface bug.
Problem
Formal theorem proving remains challenging because LLMs’ natural-language reasoning is informal, whereas Lean requires precise formal proof construction.
Method
The system uses DeepSeek-V3 to decompose and formalize theorems, a 7B prover to recursively solve subgoals, and their composed proofs to initialize reinforcement learning.
Results
The model establishes state-of-the-art performance across benchmarks, including 88.9% on MiniF2F-test and 49 solved problems on PutnamBench.
Takeaways & Limitations
Combining informal proof reasoning with formal verification substantially narrows the gap between natural-language reasoning and formal theorem proving.
Takeaways & Limitations
PutnamBench evaluation was affected by a Lean 4.9.0 user-interface bug in which apply? failed to emit sorry declarations in certain corner cases.
Abstract
from arXiv · showhide
We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3's step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model. The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. In addition to standard benchmarks, we introduce ProverBench, a collection of 325 formalized problems, to enrich our evaluation, including 15 selected problems from the recent AIME competitions (years 24-25). Further evaluation on these 15 AIME problems shows that the model successfully solves 6 of them. In comparison, DeepSeek-V3 solves 8 of these problems using majority voting, highlighting that the gap between formal and informal mathematical reasoning in large language models is substantially narrowing.
1. Introduction
DeepSeek-Prover-V2 addresses the difficulty of applying informal LLM reasoning to formal theorem proving by combining natural-language proof sketches with recursively solved Lean subgoals. Its reinforcement-learning initialization supports strong performance across formal mathematics benchmarks.
- Formal theorem proving remains challenging because LLMs reason informally in natural language while Lean requires precise formal proofs.
- DeepSeek-V3 generates natural-language proof sketches while simultaneously formalizing them into Lean statements with omitted proof details.
- A 7B prover recursively solves decomposed subgoals, whose proofs are combined into a complete proof and appended to DeepSeek-V3’s chain-of-thought.
- 88.9% pass ratio on MiniF2F-test and 47 solved problems on PutnamBench demonstrate strong formal theorem-proving performance.
- ProverBench adds 325 formalized problems, including 15 recent AIME problems, of which the model solves 6.
2. Method
The method builds formal reasoning data through hierarchical subgoal decomposition, recursive proof completion, and curriculum-based training. It then combines supervised and reinforcement-learning stages with distinct proof-generation modes and model distillation.
- Recursive Proof Search via Subgoal Decomposition: DeepSeek-V3 decomposes complex theorems into smaller lemmas, providing a unified basis for subgoal decomposition and formalization.
- Recursive Proof Search via Subgoal Decomposition: Preceding subgoals are incorporated as premises so later subgoals can use earlier intermediate results during recursive solving.
- Curriculum Learning for Subgoal-based Theorem Proving: Subgoal theorems expand formal training statements and provide denser positive training signals than sparse end-to-end proof attempts.
- Cold Start by Synthetic Data: A smaller 7B prover solves subgoals generated by DeepSeek-V3, reducing computational requirements while synthesizing complete formal proofs for cold-start data.
- Two-Stage Training: The two-stage pipeline trains non-CoT and CoT proof-generation modes using expert iteration, curriculum learning, supervised fine-tuning, and reinforcement learning.
- Distillation: The extended-context 7B model is fine-tuned on reinforcement-learning rollout data to provide a cost-efficient concise proving option.
3. Experimental Results
DeepSeek-Prover-V2 is evaluated across formal theorem-proving benchmarks spanning competition mathematics, undergraduate mathematics, and curated formalized problems. Results show strong performance, benefits from larger sample budgets and CoT reasoning, and a documented evaluation caveat involving Lean tooling.
- MiniF2F Benchmark: The performance gap between the 7B and 671B variants widens as the sample budget increases from 1 to 8192, with the larger model showing greater sample efficiency.The comparison reports a steeper improvement trajectory for the 671B model.
- MiniF2F Benchmark: 89.8% success on miniF2F-valid with the subgoal-guided curriculum nearly matches the 671B model’s 90.6% validation pass rate.The curriculum combines DeepSeek-V3 with a lightweight specialized 7B prover.
- Undergraduate-level Benchmarks: 47 problems are ultimately solved on PutnamBench after excluding two misformulated statements, while the benchmark evaluation uses 649 compatible problems.The initial run solved 49 problems before the two exclusions.
- FormalMATH: 28.31% of FormalMATH-All and 56.00% of FormalMATH-Lite problems are solved with 32 samples, increasing to 61.88% on Lite with 3200 samples.FormalMATH contains 5560 problems, while the Lite subset contains 425 problems.
- ProverBench: On 15 formalized AIME 24&25 problems, DeepSeek-Prover-V2-671B constructs valid proofs for 6, compared with DeepSeek-V3 solving 8 through majority voting.This comparison evaluates formal proof generation against informal reasoning on the same selected problems.
4. Conclusion
The paper presents a recursive cold-start data pipeline that bridges informal reasoning and formal proof structures, with performance across high-school and undergraduate benchmarks.
- 4. Conclusion: The pipeline combines high-level proof sketches, formal Lean 4 steps, complete proofs, and chain-of-thought reasoning to synthesize cold-start data.DeepSeek-V3 supports subgoal decomposition and lemma formalization, while reinforcement learning strengthens the resulting reasoning connection.
- 4. Conclusion: The resulting DeepSeek-Prover-V2-671B consistently outperforms baselines across benchmarks spanning high-school competition problems and undergraduate-level mathematics.The stated evaluation scope covers both competition-level and college-level formal mathematics.
- 4. Conclusion: Future work aims to scale the paradigm toward an AlphaProof-like system for IMO-level mathematical problems.The paper identifies IMO-level problems as a frontier challenge for automated theorem proving.
A. Examples of Non-CoT and CoT Prompting for Proof Generation
The examples contrast direct Lean proof generation with a chain-of-thought strategy that first develops informal proof plans and intermediate structures before formalization. The showcased proofs use trigonometric identities, inequalities, divisibility bounds, and case analysis to reach their stated conclusions.
- A.1. Non-CoT Generation of DeepSeek-Prover-V2: Non-CoT examples ask the model to complete Lean 4 theorem code directly, including trigonometric identities and algebraic proof obligations.The examples include Mathlib, Aesop, unlimited heartbeats, and namespace declarations as implementation scaffolding.
- A.1. Non-CoT Generation of DeepSeek-Prover-V2: The trigonometric proof rewrites double- and triple-angle expressions into polynomials in cos (Real.pi / 7).It applies Real.cos_two_mul and Real.cos_three_mul, then uses normalization and nonlinear arithmetic.
- A.2. CoT Generation Strategy of DeepSeek-Prover-V2: CoT prompting requests a detailed proof plan before Lean code, with key ideas, intermediate lemmas, and proof structures guiding construction.The accompanying text says model outputs are reformulated with inline LaTeX for clarity.
- A.2. CoT Generation Strategy of DeepSeek-Prover-V2: The integer-example proof rewrites divisibility using a positive integer k and bounds k through inequalities derived from 1 < p < q < r.The displayed reasoning first obtains k ≤ 3 after bounding the ratio involving p, q, and r.
- A.2. CoT Generation Strategy of DeepSeek-Prover-V2: The CoT proof narrows the integer cases through algebraic bounds and case splits, ultimately concluding that the only triples are (2, 4, 8) and (3, 5, 15).The conclusion is stated both in the informal proof and in the formal theorem target.
B. Examples of the Buggy Proofs Generated by DeepSeek-Prover-V2-7B on PutnamBench Triggering the User Interface Bug of apply?
The examples show buggy Lean proofs for PutnamBench problems, including matrix, polynomial, and arithmetic statements, where generated code contains unresolved apply? placeholders or sorry.
- B. Examples of the Buggy Proofs Generated by DeepSeek-Prover-V2-7B on PutnamBench Triggering the User Interface Bug of apply?: One example formalizes a Hadamard-type matrix problem: an n × n matrix with ±1 entries and orthogonal rows contains an a × b all-ones submatrix with ab ≤ n.The theorem includes positivity, entry, orthogonality, submatrix, and all-ones hypotheses.
- B. Examples of the Buggy Proofs Generated by DeepSeek-Prover-V2-7B on PutnamBench Triggering the User Interface Bug of apply?: Its generated proof derives a * b ≤ n through a calc block, but leaves apply? placeholders in cardinal-to-natural conversions.The proof obtains a ≤ n and b ≤ n before attempting the product conversion.
- B. Examples of the Buggy Proofs Generated by DeepSeek-Prover-V2-7B on PutnamBench Triggering the User Interface Bug of apply?: Another example asks for the number of polynomial pairs satisfying P^2 + Q^2 = X^(2n) + 1 with deg P > deg Q, namely 2^(n + 1).The formal statement assumes n > 0 and expresses the count with a finite-set cardinality.
- B. Examples of the Buggy Proofs Generated by DeepSeek-Prover-V2-7B on PutnamBench Triggering the User Interface Bug of apply?: The polynomial proof repeats an auxiliary cardinality claim and again relies on unresolved apply? and exact-cast steps.The excerpt includes duplicated hypotheses and a conversion from cardinal quantities to natural numbers.
C. An Example of Using exfalso to Prove a Vacuously True Statement
The Lean theorem is proved vacuously by deriving a contradiction from the period assumptions, after formalizing the word and ubiquity definitions. The construction then follows from false elimination.
- Formal statement: The theorem formalizes an infinite periodic binary word with minimal period N greater than 2^n.1 and seeks n nonempty ubiquitous words.A word appears when it occurs as a contiguous segment; ubiquity requires all four one-letter extensions to appear.
- Formal statement: The Lean goal uses an injective map from Fin n into dependent pairs of word lengths and binary words, with every image nonempty and ubiquitous.The stated conditions require each mapped word to have nonzero length and satisfy ubiquitous W.
- Contradiction: The proof strategy identifies contradictory assumptions because hW forbids every smaller period, including period 0, although Function.Periodic W 0 is trivially true.The inequality hN ensures 0 < N, allowing hW to be instantiated at 0.
- Vacuous proof: After deriving false from hW 0, the proof can construct any candidate map and discharge the nonemptiness and ubiquity goals through false elimination.The proposed implementation uses the length-1 constant-zero word as the mapped value.
- Contradiction: Since n is positive, 2^n.1 is at least 2, so hN implies N is at least 3 and supplies the required proof that 0 < N.This establishes the side condition needed to apply hW at zero.
D. Revision to MiniF2F
The revision replaces malformed or incomplete MiniF2F theorem statements with corrected Lean formulations for algebra, induction, and product inequalities. These revisions clarify hypotheses and expression syntax while retaining proof placeholders.
- Algebra: The revised algebra theorem retains hypotheses defining t and s and adds n = 3 as the condition needed to prove t = 0.The displayed theorem leaves the proof as sorry.
- Induction: The odd-sum induction theorem is revised to place + 1 inside the summand, matching the identity that the sum of the first n odd numbers equals n^2.The corrected expression sums 2 * k + 1 over Finset.range n.
- Product inequality: The product inequality theorem is revised to parenthesize each factor 1 + (1 : R) / k ^ 3 within the finite product.The bound remains 3 − 1 / ↑n under the positivity hypothesis 0 < n.