DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

Why humans prove theorems with lemmas

No one proves a hard theorem as one monolithic line of reasoning. You isolate a claim, prove it, name it, and use it. Each lemma is small enough to keep in your head, and the final argument becomes a short assembly of trusted pieces. Formal provers benefit from the same structure for the same reason: a tactic script that spans hundreds of steps compounds errors and exhausts context, while a list of named subgoals keeps each search problem local and gives the prover intermediate milestones to celebrate with the verifier.

The recursive pipeline

DeepSeek-V3 plays the planner. Given a theorem, it writes a high-level proof sketch and formalizes each lemma of the sketch into Lean, producing a sequence of subgoals. The 7B prover then attacks each subgoal independently; proof search per subgoal is cheap because the goal is small and the context is bounded. When every subgoal is closed, the subgoal proofs are composed into a proof of the original theorem. The composition is the payoff: proving the whole in one shot may be infeasible, but proving its parts is a sequence of tractable searches.

Turning the pipeline into a cold start for RL

The pipeline is also a data generator. The authors collect problems where the 7B prover cannot solve the theorem end to end but can solve every decomposed subgoal. Composing those subgoal proofs yields a full formal proof, which is paired with V3's informal step-by-step chain of thought. The result is cold-start data that shows one model both how to talk about the proof and how to write it in Lean. Supervised fine-tuning on this mixture gives a model that can generate either mode, and the longer CoT mode is noticeably stronger on the benchmark.

RL with verified rewards, at 671B

The cold start then feeds reinforcement learning: GRPO with binary rewards, where each generated Lean proof scores 1 if the kernel accepts it and 0 otherwise. The 671B model is trained from DeepSeek-V3-Base with a learning rate of 5e-6 and a 16,384-token context. The 7B model is built from Prover-V1.5-Base with the context extended from 4,096 to 32,768 tokens, fine-tuned on the 671B model's RL rollouts, and then given the same RL treatment. Curriculum learning matters here too: miniF2F-valid problems are folded into training with subgoal decomposition, while the test set stays untouched for evaluation.

What the numbers show

On miniF2F-test the 671B model reaches 88.9% overall (91.0% on the validation split), and 82.4% with only 32 samples in CoT mode; the non-CoT prompt reaches up to 78.3% at 8192 samples. The same weights generalize to college mathematics: 37.1% of ProofNet-test with Pass@1024 and 49 of 658 PutnamBench problems, compared with earlier provers stuck in the low double digits. The paper also introduces ProverBench, 325 formalized problems including 15 recent AIME problems, of which the prover solves 6 while DeepSeek-V3 solves 8 with majority voting, a gap the authors call substantially narrowed. The 7B variant reaches 82.0% on miniF2F-test with CoT prompting at 8192 samples, and the combination of the 7B prover with V3's decomposition reaches 90.2% on miniF2F-valid, nearly matching the 671B model.

The honest limits

Even here, informal reasoning is still ahead on the AIME subset (V3 solves 8 of 15, the formal model 6), so the formal-informal gap has narrowed but not closed. The headline numbers use large sample budgets, up to 8192 attempts per problem, which is only practical because Lean verification is cheap. Benchmarks remain small and competition-oriented; PutnamBench success is under 8% of problems. And the pipeline depends on DeepSeek-V3's decomposition quality: a wrong or too-hard decomposition caps what the 7B prover can assemble.

Problem the paper sets out to solve

Formal provers plateau when they must solve a hard theorem in one pass: search is expensive, errors compound, and context runs out. Human mathematics handles this with lemmas, and the paper asks whether an LLM pipeline can do the same recursively and then learn from it.

Key idea to look for while reading

Subgoal decomposition as both a search strategy and a data source. Section 2 covers the recursive pipeline and cold-start construction; Section 3 reports miniF2F, ProofNet, PutnamBench, and the new ProverBench; the RL details (GRPO, binary rewards, context lengths) are in the training section and appendix.

Evidence the paper musters

88.9% pass ratio on miniF2F-test, 82.4% at Pass@32 with CoT, 90.6% to 91.0% on miniF2F-valid, 49 of 658 PutnamBench problems, 37.1% on ProofNet-test with Pass@1024, and 6 of 15 AIME problems in ProverBench against 8 of 15 for DeepSeek-V3 with majority voting. The 7B model reaches 82.0% on miniF2F-test (CoT, Pass@8192) and the V3 plus 7B decomposition pipeline reaches 90.2% on miniF2F-valid.

Limits the authors admit

The paper notes the persistent gap with informal reasoning on AIME and that performance is measured at large sample budgets. Decomposition quality is inherited from DeepSeek-V3 and is not separately certified. Formal statement fidelity remains the standing caveat of the whole formal-proving program.

Practitioner takeaway

When a problem is too big for one search, decompose it with the strongest general model you have and solve the pieces with a specialized small one. Then instrument the pipeline: problems that fail end to end but succeed subgoal by subgoal are exactly the training data that teaches composition. Verified binary rewards plus group-relative RL remain the training backbone, now at 671B scale.

Milestones

1. 1.Model a lemma as a start and goal position on a line of nine states with plus-or-minus-one moves.
2. 2.Implement flat_search as BFS over the joint tuple of positions and count expansions.
3. 3.Implement solve_lemma with a cache keyed by the (start, goal) pair.
4. 4.Build six theorems of three lemmas drawn from a pool of five.
5. 5.Compare total expansions and count how many pool lemmas end up cached.
6. 6.Widen the line and add theorems, then confirm the flat search scales worse.

Success criteria

• Flat search uses hundreds of expansions while the decomposed search stays under 50.
• Every cache hit costs zero expansions and all five pool lemmas end cached.
• Raising the width from 9 to 15 multiplies flat expansions while decomposed expansion grows roughly linearly.

Stretch goals

• ·Let lemmas depend on earlier lemmas so solving order matters and the cache needs care.
• ·Add a budget cutoff to flat_search and record how often it fails to finish.
• ·Replace per-lemma BFS with A* using distance to the goal and compare expansions.

Problems

• GRPO Group Advantage Normalization