Source-linked AI summary
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, Chong Ruan
TL;DR
Formal theorem proving requires models to produce Lean proofs that satisfy strict verifier specifications, while whole-proof generation lacks intermediate tactic-state feedback. DeepSeek-Prover-V1.5 combines augmented training, reinforcement learning from Lean verification, and RMaxTS tree search, achieving new state-of-the-art results of 63.5% on miniF2F test and 25.3% on ProofNet test.
Problem
Formal theorem proving remains challenging because models must align mathematical reasoning with rigorous formal specifications, while whole-proof generation lacks intermediate tactic-state feedback.
Method
DeepSeek-Prover-V1.5 uses augmented formal-data training, reinforcement learning from Lean verification feedback, and RMaxTS Monte-Carlo tree search for diverse proof exploration.
Results
63.5% on miniF2F test and 25.3% on ProofNet test are reported as new state-of-the-art pass rates after tree-search enhancement.
Takeaways & Limitations
The framework improves formal theorem-proving performance across high-school and undergraduate benchmarks while integrating proof-assistant feedback into training and search.
Takeaways & Limitations
The exploration aspect of reinforcement learning is addressed, but exploitation through proof search remains unexplored; critic models for incomplete proofs are proposed as future work.
Abstract
from arXiv · showhide
We introduce DeepSeek-Prover-V1.5, an open-source language model designed for theorem proving in Lean 4, which enhances DeepSeek-Prover-V1 by optimizing both training and inference processes. Pre-trained on DeepSeekMath-Base with specialization in formal mathematical languages, the model undergoes supervised fine-tuning using an enhanced formal theorem proving dataset derived from DeepSeek-Prover-V1. Further refinement is achieved through reinforcement learning from proof assistant feedback (RLPAF). Beyond the single-pass whole-proof generation approach of DeepSeek-Prover-V1, we propose RMaxTS, a variant of Monte-Carlo tree search that employs an intrinsic-reward-driven exploration strategy to generate diverse proof paths. DeepSeek-Prover-V1.5 demonstrates significant improvements over DeepSeek-Prover-V1, achieving new state-of-the-art results on the test set of the high school level miniF2F benchmark ($63.5\%$) and the undergraduate level ProofNet benchmark ($25.3\%$).
1. Introduction
DeepSeek-Prover-V1.5 addresses the difficulty of formal theorem proving by combining proof-assistant-aware training with whole-proof and tree-search inference. Its framework integrates formal-data preparation, reinforcement learning from Lean verification, and publicly available components.
- Formal theorem proving requires derivations that satisfy rigorous verification-system specifications, challenging language models beyond natural-language reasoning.
- Whole-proof generation is computationally efficient but requires long-horizon prediction without access to intermediate tactic states.
- DeepSeek-Prover-V1.5 combines proof-step and whole-proof generation through a truncate-and-resume mechanism that incorporates intermediate tactic states.
- The framework trains the model through pre-training, supervised fine-tuning, and reinforcement learning using Lean verification results as binary rewards.
- The project integrates mathematical pre-training, formal-mathematics data construction, online proof-assistant-feedback reinforcement learning, and Monte-Carlo tree search, with models and search code publicly available.
- Tree-search integration raises DeepSeek-Prover-V1.5’s miniF2F test pass rate from 60.2% in single-pass generation to 63.5%.
2. Model Training
Training combines continued pre-training, augmented supervised fine-tuning, and reinforcement learning from Lean prover feedback. Evaluations across training stages show improvements on miniF2F and ProofNet, with chain-of-thought prompting generally outperforming non-CoT prompting.
- Model Training: DeepSeek-Prover-V1.5-Base is further pre-trained on high-quality code and mathematical content, emphasizing formal languages including Lean, Isabelle, and Metamath.
- Supervised Fine-Tuning: The supervised fine-tuning dataset adds explanatory comments and intermediate tactic-state information, supporting natural-language alignment and truncate-and-resume search.
- Supervised Fine-Tuning: The Lean 4 completion dataset combines synthetic proofs from Mathlib4, DeepSeek-Prover-V1, Lean Workbook, miniF2F, and ProofNet, with expert-iteration augmentation.
- Reinforcement Learning: Reinforcement learning uses Lean 4 verification feedback, assigning reward 1 to correct proofs and 0 otherwise, and applies GRPO to optimize relative rewards within candidate groups.
- Evaluation: MiniF2F evaluates high-school-level formal problem solving, while ProofNet evaluates undergraduate-level formal theorem proving.
- Evaluation: Pass@128 accuracy increases by approximately two-thirds on miniF2F and doubles on ProofNet after supervised fine-tuning, with reinforcement learning improving Pass@K across all tested K values.
- Evaluation: CoT prompting consistently outperforms non-CoT prompting across most settings, with DeepSeek-Prover-V1.5-RL averaging 51.6% on miniF2F and 18.2% on ProofNet.
3. Exploration-oriented Monte-Carlo Tree Search
DeepSeek-Prover-V1.5 adapts whole-proof generation into a tactic-level proof tree for MCTS, using truncate-and-resume to incorporate verifier feedback. RMaxTS augments sparse compiler rewards with intrinsic rewards for discovering new tactic states, supporting broader proof-path exploration.
- 3.1. Tactic-level Tree Abstraction: The proof tree decomposes incomplete proofs into tactic-level nodes, with each edge representing a single tactic-state transition.The tree is built by parsing generated proofs and truncating them at the earliest Lean verification error.
- 3.1. Tactic-level Tree Abstraction: Truncate-and-resume verifies generated continuations in Lean, retains the successful prefix, and parses successful tactics into descendant nodes for further search.Expansion resumes from stored incomplete proof code and can continue until a correct proof is found or the sample budget is exhausted.
- 3.2. Interactive Theorem Proving via Monte-Carlo Tree Search: Whole-proof generation serves as the rollout during expansion, integrating simulation into expansion and proposing a sequence of tactics from the selected node.After Lean verification, each iteration backpropagates the trajectory reward through the selected path.
- 3.2. Interactive Theorem Proving via Monte-Carlo Tree Search: MCTS selection balances exploitation and exploration by choosing among child nodes and a virtual expansion action using Q_UCB(s, a).The virtual node permits expansion of non-leaf nodes, while Q_UCB combines historical action values with an exploration bonus.
- 3.3. Intrinsic Rewards for Monte-Carlo Tree Search: Intrinsic reward marks trajectories that add at least one new search-tree node, prioritizing diverse tactic states when completed-proof rewards are sparse.The resulting heuristic can reduce redundant generation because multiple Lean codes may produce the same intermediate-state transition.
- 3.3. Intrinsic Rewards for Monte-Carlo Tree Search: DUCB discounts outdated trajectory feedback because discovering unseen tactic states becomes harder as exploration expands the search tree.The discount factor addresses the non-stationary intrinsic reward signal.
4. Experimental Results
DeepSeek-Prover-V1.5 is evaluated on miniF2F and ProofNet using pass@K under whole-proof and tree-search settings. The experiments show gains from reinforcement learning, mixed prompting, and key RMaxTS components.
- Results on miniF2F: 60.2% pass rate makes DeepSeek-Prover-V1.5-RL the strongest single-pass whole-proof method on miniF2F-test, improving 10.2 percentage points over DeepSeek-Prover-V1.With 128 attempts, it proves 51.6% of problems.
- Results on miniF2F: 62.7% pass rate makes DeepSeek-Prover-V1.5-RL + RMaxTS a new state-of-the-art on miniF2F-test.At 3200 whole-proof samplings, it reaches 54.9%, exceeding InternLM2-StepProver’s 54.5% despite the latter using 64 × 3200 tree searches.
- Results on ProofNet: 25.3% pass rate with RMaxTS exceeds DeepSeek-Prover-V1.5-RL’s 22.6% single-pass result on ProofNet and prior results from ReProver and InternLM2-StepProver.At 3200 whole-proof attempts, DeepSeek-Prover-V1.5 proves 21.7% of theorems, 3.6% above InternLM2-StepProver.
- General Enhancement of Reinforcement Learning: Online reinforcement learning consistently outperforms the SFT model across generation settings, and its gains are orthogonal to those from RMaxTS.Combining CoT and RMaxTS reaches 62.7% on miniF2F-test, 3.7% above SFT.
- CoT, non-CoT, and Mixture Strategy: 63.5% pass rate results from mixing CoT and non-CoT prompts, which exploit complementary theorem-proving advantages.CoT is more systematic and proactive, whereas non-CoT efficiently uses Lean’s high-level tactics for computational problems.
- Ablation Studies on RMaxTS: Removing intrinsic rewards or replacing discounted UCB with UCB1 reduces RMaxTS performance to a level comparable to non-search methods.Without tactic-state information, tree-search gains also become moderate, especially for hard problems requiring many samples.
5. Conclusion, Limitation, and Future Work
DeepSeek-Prover-V1.5 combines specialized training, reinforcement learning, and tree search to improve formal theorem proving in Lean 4. The authors identify proof-search exploitation and multi-theorem file-level proving as directions for future work.
- Its training pipeline combines specialized pre-training, supervised fine-tuning, GRPO-based reinforcement learning from proof assistant feedback, and RMaxTS tree search.
- The framework is designed as an AlphaZero-like pipeline, using expert iteration, synthetic data, and the compiler oracle for environmental supervision.
- Limitation and Future Work: The authors focus RMaxTS on exploration and leave exploitation in proof search, including critic-guided branch pruning and temporal credit assignment, for future work.
- Limitation and Future Work: Future work will enhance file-level context understanding to support proving within complex, multi-theorem Lean files.
A. Illustrative Examples of Non-CoT and CoT Prompting for Proof Completion
The examples contrast non-CoT and CoT whole-proof prompting for Lean 4 proof completion. They illustrate how tactic-state information and algebraic normalization can guide a compact verified proof.
- The appendix presents non-CoT and CoT prompting examples for generated proofs of aime_1983_p9 from miniF2F.
- CoT Prompting: The CoT example uses Monte-Carlo tree search with truncate-and-resume, feeding an intermediate Lean tactic state back into subsequent proof generation.
- Non-CoT Prompting: For the non-CoT example, Lean verifies positivity of x * sin x before rewriting the inequality with le_div_iff.
- Non-CoT Prompting: The resulting tactic state is transformed into the polynomial inequality 9x^2 sin^2 x − 12x sin x + 4 >= 0.
- Non-CoT Prompting: The proof closes by recognizing the polynomial as (3x sin x − 2)^2 and applying non-negativity of squares through nlinarith.
B. Example Solutions to MiniF2F-test Problems
The appendix compares non-CoT and CoT prompting through examples of proof completion on miniF2F-test problems. It includes cases where either prompting mode succeeds while the other fails.
- The examples illustrate complementary advantages of non-CoT and CoT prompting for proof completion.
B.1. Problems that non-CoT outperforms CoT
This section contains example Lean solutions for problems where non-CoT prompting outperforms CoT prompting. The supplied examples include finite-product and square-root inequalities.
- One example proves a finite-product inequality by simplifying Finset.Icc expressions and combining normalization, field simplification, and linear arithmetic.
- Another example proves bounds on x from a square-root inequality using non-negativity, denominator nonzero conditions, algebraic rewriting, and nlinarith.
B.2. Problems that CoT outperforms non-CoT
The section illustrates Lean proof solutions for algebraic, number-theoretic, and inequality problems through explicit intermediate derivations and exhaustive case analysis. These examples show how formal proofs combine mathematical transformations with verifier-oriented tactics.
- Algebraic problems: Algebraic proofs solve systems of equations by substituting variables, deriving intermediate equalities, and applying `linarith` to obtain the target value.The worked example derives d from the first equation, substitutes into subsequent equations, establishes values for a, b, c, and d, and finishes with arithmetic normalization.
- Algebraic problems: The rational-number example derives a = 1 and related linear constraints before proving the final numerator–denominator sum with normalization tactics.The proof uses intermediate hypotheses and `norm_num [h7] <;> rfl` after establishing the value of d.
- Number-theoretic problems: The modular-arithmetic proof reduces x and y modulo 11, checks all residue combinations, and concludes the contradiction with `omega`.The proof enumerates residues from 0 through 10 for both variables, simplifies modular expressions, and invokes `omega` to finish.
- Inequality problems: The inequality proof bounds a, m, and c by 12, enumerates their possible values under a + m + c = 12, and checks the polynomial against 112.It uses `omega`, `interval_cases`, and exhaustive combinations to verify the required upper bound.