DeepSeek-Prover-V1.5

TL;DR#

• What was built: DeepSeek-Prover-V1.5, a 7B Lean 4 prover trained in three stages. It starts with continued pre-training of DeepSeekMath-Base on formal-math data, then supervised fine-tuning (SFT) on 9.6M proof sequences, then reinforcement learning (RL) with GRPO where Lean's verdict is the reward (§2).
• Two training tricks: proofs are annotated with natural-language reasoning written as Lean comments by DeepSeek-Coder-V2 236B. The model is also trained to predict Lean's intermediate tactic state, inserted as a /- tactic state: ... -/ comment (§2.2).
• Key inference idea: truncate-and-resume. The model generates a whole proof, and Lean finds the first error. The model keeps the valid prefix and continues from there, with the current tactic state shown as a comment. Organizing these restarts as a Monte-Carlo tree search gives RMaxTS, which rewards the search for reaching new tactic states, since actual success is too rare to guide it (§3).
• Headline: miniF2F-test goes from 50.0% (V1) to 60.2% with single-pass sampling and 63.5% with RMaxTS. ProofNet-test reaches 25.3% (Tables 1–2).
• Ablations: RL improves results at every sample budget, CoT and non-CoT prompting complement each other, and RMaxTS stops helping if either the intrinsic reward or the discounted UCB is removed (Table 3, Figure 5).

Why it matters#

DeepSeek-Prover showed that a 7B model writing whole proofs, trained on a large set of verified synthetic proofs, could beat tree-search provers on miniF2F. But whole-proof generation is open loop. The model writes 20 tactics without ever seeing the proof state that Lean would show after tactic 3. One wrong belief about an intermediate goal and every later line is wasted. Proof-step provers avoid this by calling Lean after every tactic, at the cost of many round trips and a large search.

V1.5 tries to get both. It keeps whole-proof generation, which is cheap, parallel, and lets the model plan a whole proof, but uses Lean's error location to cut the proof at the first failure and resume from the last good point, now with the true tactic state in view. Treat every such cut point as a node and you have a search tree. Proof search gives no reward until the very end, so the tree search is driven by curiosity: an expansion that reaches a tactic state never seen before counts as a success.

Key idea Truncate-and-resume turns a whole-proof generator into a tree searcher with no new model. Each failed proof's valid prefix becomes a node, Lean's tactic state at that node becomes part of the prompt, and an exploration bonus for reaching new states replaces the missing reward signal.

In the DeepSeek arc, this paper combines three earlier pieces. The data comes from DeepSeek-Prover. GRPO and the base model come from DeepSeekMath. DeepSeek-Coder-V2 writes the reasoning annotations. RL from a rule-based, verifiable reward (here, "did Lean accept it?") is the approach DeepSeek later scaled up for general reasoning. The paper itself calls its framework a step toward "an AlphaZero-like pipeline for formal theorem proving" (§5).

Background you need#

• Lean 4, tactics and tactic states. A Lean proof in tactic mode is a sequence of commands, each of which transforms the proof state: the hypotheses plus the remaining goal, written ⊢ goal. Lean can report the state before and after every tactic, and the location of the first error. See the DeepSeek-Prover page for a gentler introduction.
• Whole-proof vs. proof-step generation. Whole-proof: generate the entire proof, then verify it. Proof-step: generate one tactic, get the new state from Lean, repeat, usually inside a best-first or tree search (GPT-f, HTPS, InternLM2-StepProver).
• GRPO. Group Relative Policy Optimization, from DeepSeekMath. For each prompt, sample a group of outputs, score them, and use each output's reward relative to the group mean as its advantage. Unlike PPO, it needs no separate value (critic) network.
• Monte-Carlo Tree Search (MCTS). A search that repeats four steps: select a node by trading off value against an exploration bonus, expand it, simulate a rollout, and backpropagate the result up the path. The exploration bonus is usually UCB, an upper confidence bound that shrinks as an action is tried more.
• Intrinsic rewards / RMax. When real rewards are rare, the agent can reward itself for discovering something new. RMax (Brafman & Tennenholtz, 2002) gives maximal reward to unvisited states, which pushes the agent to cover the state space.
• Benchmarks. miniF2F: 244 validation and 244 test problems, high-school competition level (AMC, AIME, IMO). ProofNet: 185 validation and 186 test problems from undergraduate textbooks covering analysis, linear and abstract algebra, and topology. Both were ported to Lean 4.9.0 (§2.4).

The core ideas#

1. Continued pre-training (DeepSeek-Prover-V1.5-Base)#

DeepSeekMath-Base 7B is pre-trained further on "high-quality mathematics and code data", with a focus on formal languages: Lean, Isabelle and Metamath (§2.1). The paper gives no token count or data mixture for this stage. The resulting Base model already reaches 29.7% on miniF2F-test with 3-shot prompting at pass@128 (Figure 3).

2. Supervised fine-tuning with thoughts and tactic states#

Data (§2.2). Theorems come from Mathlib4, V1's synthetic statements, Lean Workbook, and the miniF2F and ProofNet validation sets. Proofs are grown by expert iteration: generate, verify, retrain, repeat. Between iterations, DeepSeek-Coder-V2 236B annotates the proofs. The final set has 9,645k sequences.

Thought-augmented proofs. V1's proofs tended to call a few heavy automated tactics such as nlinarith or simp_all, with no visible reasoning. V1.5 inserts natural language as Lean comments in two places: a full informal solution at the top of the proof block, and a short plan before each tactic. Two different instructions select the mode at inference time: CoT ("Complete the following Lean 4 code with explanatory comments preceding each line of code") and non-CoT ("Complete the following Lean 4 code"). This is similar in spirit to Lean-STaR, but here the reasoning is part of the code itself, not separate from it.

Tactic-state prediction. Using the Lean REPL and LeanDojo extraction tools, the authors record each tactic's position along with the state before and after it. For a valid proof, they insert the state as a comment after a tactic:

rw [le_div_iff h1]
/- tactic state:
x : ℝ
h0 : 0 < x ∧ x < π
h1 : 0 < x * x.sin
⊢ 12 * (x * x.sin) ≤ 9 * (x ^ 2 * x.sin ^ 2) + 4
-/

Training uses everything up to /- tactic state: as the prompt, with no loss on it, and all tokens after it as the target. So the model learns two things: to predict the tactic state, an auxiliary objective, and to continue the proof from it, the main objective (Figure 2). At inference, the state is supplied by Lean, not predicted, which is exactly what truncate-and-resume needs.

Settings: 9B training tokens, batch size 2,048, constant LR 1e-4, 100 warm-up steps, sequences packed to 4,096 tokens (§2.2).

3. RL from proof assistant feedback (RLPAF)#

The reward needs no learned reward model. It is simply

This reward is exact but sparse. If the SFT model never solves a theorem, all 32 samples score 0, and GRPO's group-relative advantage is zero for every sample, so there is nothing to learn. The authors therefore keep only theorems where the SFT model has a moderate success rate across several attempts. That leaves about 4.5k theorems (§2.3), each used with both the CoT and the non-CoT instruction.

GRPO settings: SFT model as both the initial policy and the KL reference; LR 5e-6; KL coefficient 0.02; group size 32; max length 2,048; batch 512.

A notable claim (§2.4): in DeepSeekMath, RL mainly made correct answers that were already in the top-K more likely, so it helped pass@1 more than pass@K. Here RL improves pass@K at every budget up to 128, and the gap holds at much larger budgets (Table 3). The authors read this as a real gain in capability, not only a sharper distribution.

4. Truncate-and-resume as a tree#

Here is how one whole proof becomes a search tree (§3.1, Figure 4):

1. Generate a full proof from some prefix.
2. Verify it with Lean. If it is correct, stop.
3. Truncate at the first error and discard everything after it.
4. Parse the valid part into tactics. Each tactic, together with its preceding CoT comment, becomes one tree edge, and the tactic state after it becomes a node. One generation can therefore add a whole path of nodes, not just one child.
5. Resume from any node. The prompt is the file header, the theorem, the tactics on the path to that node, and the node's tactic state as a comment.

Different tactic code can lead to the same Lean state, so a node stores a set of equivalent tactic codes and picks one at random when resuming. Merging equal states this way is what makes "reached a new state" a meaningful signal.

5. RMaxTS: MCTS driven by curiosity#

Selection. At node \(s\), choose

where \(\oslash\) is a virtual child that means "expand \(s\) itself". The model can always produce new continuations from any node, so interior nodes stay expandable, not only leaves.

Expansion and simulation are merged into one step. Expanding a node is one whole-proof rollout.

Reward. The real reward, "proof complete", almost never arrives. So the search uses only an intrinsic reward, in the style of ZeroRMax:

where \(\tau\) is the latest selection trajectory, the path from the root to the expanded node, and \(\mathbb{I}\) is 1 if the condition holds and 0 otherwise. Nodes whose expansions keep reaching new tactic states look valuable. Nodes that keep producing proofs equivalent to ones already seen do not.

Discounted UCB. This reward is non-stationary: new states get harder to find as the tree grows, so old successes overstate a node's current value. Standard UCB1 weights all history equally. RMaxTS uses discounted UCB:

where \(N(s,a)\) is the number of past trajectories through \((s,a)\), \(\tau_t\) is the \(t\)-th of them in time order, and \(\gamma = 0.99\). Recent outcomes count more. For example, if a node's last 100 visits found nothing new, the weight of an early burst of discoveries has decayed by about \(0.99^{100} \approx 0.37\). Note that the discount runs over search iterations, not over steps within a trajectory as in an MDP.

Parallelism (§3.4). Root parallelization: 256 MCTS runners per node, one model per GPU, batch size 512 for generation, and Lean checks running asynchronously on thousands of CPU cores, each in a sandboxed process. Tree parallelization: 32 worker threads per tree. Virtual loss: an in-flight expansion is temporarily counted as reward 0, so concurrent workers spread out across nodes.

Counting budget. For tree search, \(K = N \times T\): \(N\) independent searches of \(T\) model generations each. So "16 × 6400" means 16 runs of 6,400 generations, which is the same number of generations as 16 × 6400 single-pass samples. That keeps the comparisons in Table 1 fair in generation count. They are not equal in Lean calls or wall-clock time.

Key numbers#

How to read the paper#

About 19 pages of main text, followed by references and two appendices of example proofs.

• Abstract, §1 Introduction, §1.1–1.2 — Read closely. §1 explains the motivation for truncate-and-resume clearly. Figure 2 shows the whole system: pre-train → SFT → RL, then single-pass sampling or MCTS.
• §2.1 Pre-training — Skim. One paragraph with no numbers.
• §2.2 Supervised Fine-tuning — Read closely. The thought annotations and the tactic-state comment format, with its loss masking, are what make §3 possible.
• §2.3 RLPAF — Read closely. Short. Note the prompt-selection argument tied to GRPO's group-relative advantage.
• §2.4 Evaluation — Read. Benchmark sizes, sampling settings, and Figure 3, which shows each training stage's contribution and CoT vs. non-CoT.
• §3.1 Tactic-level Tree Abstraction — Read closely, with Figure 4. Figure 4 is the most useful figure in the paper.
• §3.2 MCTS — Read. Standard MCTS. The unusual parts are the virtual node and path insertion.
• §3.3 Intrinsic Rewards — Read closely. Eqs. (3) and (7)–(9) define RMaxTS.
• §3.4 Parallelization — Skim unless you are building such a system.
• §3.5 Comparison with Existing Methods — Skim.
• §4.1 Main Results — Read closely. Tables 1 and 2. Read the budget-counting rules first.
• §4.2 Training strategies at scale — Read. Table 3: RL vs. SFT, CoT vs. non-CoT, and the mixture.
• §4.3 RMaxTS ablations — Read. Figure 5. The curves on the left matter more than the table on the right.
• §5 Conclusion, Limitation, Future Work — Read. Short. It names the missing critic model.
• Appendix A — Read the aime_1983_p9 example. It shows the CoT format with a tactic state comment. Appendix B — Skim.

Suggested order: §1 + Figure 2 → §2.2–2.3 → Figure 4 + §3.1 → §3.3 → Tables 1–3 → Figure 5 → Appendix A. About 1.5–2 hours.

Check your understanding#

Limitations and open questions#

• No critic model. The authors say the search covers only the exploration side. Nothing judges how promising a partial proof is, and they name a partial-proof critic for pruning and credit assignment as future work (§5).
• Single-theorem setting. Real Lean work happens in multi-theorem files with local definitions. The authors mention file-level context, as in miniCTX, as the next direction.
• Pre-training is unspecified. There is no token count, data mixture or ablation for the continued pre-training stage, so its contribution to the Base model's 29.7% can't be separated out.
• Validation sets in training. The miniF2F and ProofNet validation sets are used for expert iteration in SFT (§2.2; Table 2 footnote). So the validation numbers are not held-out. Only the test numbers are clean, and the paper reports miniF2F mainly on test.
• Compute isn't equal across methods. Budgets match in model generations, but one RMaxTS generation also needs Lean parsing and tactic-state extraction, and the systems use different model sizes and hardware. Wall-clock time and total compute are not reported.
• Small margins at large budgets. At 16 × 6400, RMaxTS adds 2.5 points over single-pass (62.7% vs. 60.2%). Most of the gain over V1 comes from training (SFT and RL), not search. Several large-budget numbers are single runs with no standard deviation.
• The 63.5% headline uses twice the budget. The mixture result is (16 + 16) × 6400, which is 32 × 6400 generations (marked † in Table 1). The 62.7% CoT-only result uses 16 × 6400. At equal budget, the mixture's 60.0% (at (2 + 2) × 6400) vs. CoT-only's 59.6% (at 4 × 6400) is a much smaller gap (Table 3).
• Easy-to-mix-up ProofNet figures. §1.2 cites single-pass ProofNet as 21.6% valid and 23.7% test. §4.1 gives 22.6% for the whole set (valid + test). These are different splits of the same Table 2 row, not an error.

Further reading#

• DeepSeek-Prover: V1, the source of the synthetic data and the whole-proof approach.
• DeepSeekMath: the base model and GRPO.
• DeepSeek-Coder-V2: the 236B model used to write the natural-language proof comments.
• DeepSeek-V3: the end of the year's arc, where RL with rule-checkable rewards becomes part of general post-training.
• Lample et al., HyperTree Proof Search: arXiv:2205.11491
• Lin et al., Lean-STaR: Learning to Interleave Thinking and Proving: arXiv:2407.10040
• Yang et al., LeanDojo: arXiv:2306.15626
• Azerbayev et al., ProofNet: arXiv:2302.12433
• Brafman & Tennenholtz, R-max: JMLR 2002; Garivier & Moulines, discounted UCB for switching bandits (ALT 2011)
• Code and models: github.com/deepseek-ai/DeepSeek-Prover-V1.5; Hugging Face: DeepSeek-Prover-V1.5-RL
• Later, outside this series: DeepSeek-Prover-V2 (2025), arXiv:2504.21801