DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
Stop throwing away the compiler's complaints. Truncate a failed proof at its first error, resume from there, and use the Lean verifier as the reward signal for both GRPO and tree search.
arXiv:2408.08152Where this sits
The first prover generated independent full proofs and had to redo everything after any early mistake. V1.5 asks what changes if the model can read the verifier's intermediate feedback and, more importantly, if the verifier's verdict itself becomes the learning signal.
- Adds online RL from proof assistant feedback (RLPAF) on top of SFT, using GRPO with binary accept/reject rewards from Lean.
- Raises miniF2F-test whole-proof accuracy to 60.2% from Prover-V1's 50.0%, and 63.5% when combined with RMaxTS search.
- Introduces truncate-and-resume, which turns a failed proof into a tree prefix and makes whole-proof generation compatible with MCTS.
- Adds an intrinsic new-node reward with discounted UCB so search keeps exploring sparse-reward proof states instead of stalling.
- Lifts ProofNet-test (undergraduate level) to 25.3% with RMaxTS, ahead of ReProver's 13.8% and InternLM2-StepProver's 18.1%.
What it is
Prover-V1.5 upgrades the whole-proof approach in two ways. It trains the model with reinforcement learning where the reward is simply whether Lean accepts the proof, and it adds RMaxTS, a Monte-Carlo tree search (MCTS) that treats the tactic state after each successful tactic as a tree node. Failed attempts are chopped at the first error and reused as prefixes, so every verification message becomes useful information instead of a discarded sample.
1Theory from first principles
The feedback the first version ignored
Lean does not just say 'no'. When a tactic script fails, the prover reports the first tactic that could not be applied and the state of the goal at that point. A whole-proof model never sees this during generation, so it writes blind past its own mistakes. V1.5 changes the loop: generate a proof, let Lean check it, and if it fails, keep everything before the first error and continue from the current goal state. The paper calls this truncate-and-resume, and it works because a partially correct proof is still a correct prefix.
From prefix to tree
Once prefixes are reusable, the natural structure is a tree. Each node is a tactic state; each valid tactic is an edge; the model can expand any node, not just the deepest one. Expansion works like this: take a node, resume the proof from there with the tactic-state comment appended, let the model generate a continuation, verify it, and truncate at the next error. Because whole-proof generation emits a whole continuation, one expansion can add an entire path of nodes to the tree, unlike the single child added in game-playing MCTS.
RL where the environment is the reward model
The supervised model is further trained with GRPO: for each theorem prompt, sample a group of proofs, score each 1 if Lean verifies it and 0 otherwise, and update toward the proofs that beat their group's average. The paper keeps only theorem prompts where the SFT model succeeds sometimes but not always: 4.5k statements survive filtering. This fixes the sparse-reward problem on the training side, because prompts the model can never solve give a group of all-zero rewards and therefore no gradient. The RL stage uses 32 samples per theorem with a KL coefficient of 0.02 against the SFT reference model.
Intrinsic reward and discounted UCB
R_intrinsic(tau) = 1[at least one new node is added to the search tree]
Q_DUCB(s, a) = W_gamma(s, a) / N_gamma(s, a) + sqrt( 2 * ln( sum_{a'} N_gamma(s, a') ) / N_gamma(s, a) )The extrinsic reward is 1 only for a finished proof, which makes deep trees hopeless to explore by value alone. R_intrinsic pays the search for reaching a tactic state it has not seen, and Q_DUCB is the selection rule for a state s and tactic a: the first term exploits (discounted wins, W_gamma, over discounted visits, N_gamma), the second explores (a bonus that shrinks as a state-action pair is reused). The discount gamma = 0.99 keeps old feedback from dominating, because the intrinsic reward naturally fades as the tree fills up and the signal is non-stationary.
import math
GAMMA = 0.99
def d_ucb(rewards, visits, parent_visits):
# rewards: past R(tau) values for this edge; visits: times it was chosen
discounted_w = sum(GAMMA ** (len(rewards) - 1 - t) * r
for t, r in enumerate(rewards))
discounted_n = sum(GAMMA ** t for t in range(visits))
if discounted_n == 0:
return float("inf") # unseen edge: try it first
exploit = discounted_w / discounted_n
explore = math.sqrt(2.0 * math.log(parent_visits) / discounted_n)
return exploit + explore
def intrinsic_reward(new_nodes_added):
return 1.0 if new_nodes_added > 0 else 0.0- Unseen edges get an infinite score so the search tries them first.
- The caller supplies parent_visits from the sibling set, which is what the exploration bonus is measured against.
- The intrinsic reward is deliberately binary: any new node counts once, no matter how many were added.
What the results actually show
RL helps at every sample budget, not just the lucky tail. At 128 attempts the RL model proves 51.6% of miniF2F-test, and the improvement persists as the budget grows to 60.2%, which the authors contrast with DeepSeekMath's finding that RL mostly reshuffles which correct answer is found first. Adding RMaxTS on top reaches 62.7% at 16x6400 and 63.5% at 32x6400. ProofNet-test, which is undergraduate level, goes to 25.3% with search. SFT alone with RMaxTS also reaches 60.2%, so the search machinery and the RL policy each contribute, and they compose.
The honest limits
More samples and more search cost more money, and the paper's best numbers use large generation budgets. The model is still 7B and English-to-Lean fidelity issues remain: Lean certifies the formal statement. Finally, the intrinsic reward is a heuristic, not a proof of optimal exploration; it is chosen because sparse-reward proof search is a hard-exploration problem, and the ablations are empirical.
2Inside the paper
Problem the paper sets out to solve
Whole-proof generation without mid-proof feedback compounds errors, and the first prover's verification results were used only to filter data. Can the verifier be used online, both to guide training and to organize search?
Key idea to look for while reading
Truncate-and-resume as a state-action abstraction. Section 3.1 defines the nodes and edges, Section 3.2 describes selection and backpropagation, Section 3.3 motivates the intrinsic reward and discounted UCB. Section 2.3 specifies the RL setup: GRPO, binary rewards, prompt filtering.
Evidence the paper musters
Training stages on miniF2F-test pass@128: base 29.7%, SFT (CoT) 50.4%, RL (CoT) 51.6%. At larger budgets, RL single-pass reaches 60.2% (against V1's 50.0%), and RL plus RMaxTS reaches 63.5%. ProofNet-test: 22.6% single-pass, 25.3% with RMaxTS. The best comparison lines are ReProver at 13.8% and InternLM2-StepProver at 18.1% on ProofNet. RL with only 3200 raw samples beats InternLM2-StepProver's much larger 64x3200 tree search (54.9% versus 54.5% on miniF2F-test).
Limits the authors admit
The paper labels RMaxTS a heuristic exploration strategy and keeps the evaluation to two benchmarks. Statement fidelity and the 7B capacity ceiling remain. Search results depend on parallel infrastructure (256 runners, 32 threads per tree), so reproducing the headline accuracy requires serious compute.
Practitioner takeaway
When an environment gives you partial feedback, stop discarding it. Truncating failures into reusable prefixes converts one expensive sample into a tree of information, and a cheap intrinsic bonus for novelty keeps exploration alive when the real reward is rare. The GRPO-with-binary-rewards setup here is the same machinery R1 later scales up in natural language.
3Implementation check
0 of 5 questions answered
1.Why does MCTS need the proof assistant's feedback signal in this system?
2.What problem does the intrinsic new-node reward solve?
3.Why does the RL stage use only theorems where the SFT model sometimes succeeds?
4.In truncate-and-resume, why truncate a failed proof at its first error rather than at the end of the generated text?
5.Why does the discounted UCB rule (gamma = 0.99) fit the intrinsic reward better than plain UCB1?
4Build it yourself
RMaxTS: Verifier-Guided Proof Tree Search
Intermediate4-6 hoursKeep the verified prefix of a failed tactic script and resume from there. Build a proof tree over a toy proof assistant, select nodes with discounted UCB, pay a reward for each newly verified node, and compare expansions against whole-proof sampling.
Milestones
- Define the toy assistant: depth-10 goals, three tactics per state, and a hidden accept rule the verifier exposes.
- Implement whole-proof sampling, which draws all ten tactics and checks them only at the end.
- Implement the discounted UCB score with an exploration bonus measured against parent visits.
- Implement the search loop: select a frontier node, resume a random continuation, attach only tactics the verifier accepts.
- Reward each newly attached node and backpropagate visits and rewards to the root.
- Run both methods on 20 hidden proofs and compare mean samples or expansions.
Success criteria
- Tree search finds a proof in under 10 expansions on average while whole-proof sampling needs dozens of samples.
- No unverified tactic appears in the tree: every attached node passed the verifier call.
- Removing the exploration bonus makes selection greedy and increases expansions, showing UCB is doing work.
Stretch goals
- Make some verified prefixes dead ends so the search must backtrack, and check that UCB still beats sampling.
- Decay the exploration constant as the tree fills and measure the effect on expansions.
- Compare at an equal verifier-call budget rather than an equal attempt count.