note_sync/大模型/deepseek/_digest/2408.08152.txt

TITLE: DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
ARXIV: 2408.08152
AUTHORS: 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
DATE: [Submitted on 15 Aug 2024]

=== SECTION HEADINGS ===
## Report GitHub Issue
## DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback
## Abstract
## 1 Introduction
## 1.1 Contributions
## 1.2 Summary of Evaluations and Metrics
## 2 Model Training
## 2.1 Pre-training
## 2.2 Supervised Fine-tuning
## Data Curation.
## Thought-augmented Proof Generation.
## Prompt Augmentation with Tactic State Information.
## Training Setting.
## 2.3 Reinforcement Learning from Proof Assistant Feedback
## Prompts.
## Rewards.
## Reinforcement Learning Algorithm.
## Training Setting.
## 2.4 Evaluation
## Benchmarks.
## Prompting Configurations.
## Metric.
## Comparison across Training Stages.
## Comparison between CoT and non-CoT.
## 3 Exploration-oriented Monte-Carlo Tree Search
## 3.1 Tactic-level Tree Abstraction
## Truncate: Proof Decomposition into Tree Nodes.
## Resume: Proof Generation from a Tree Node.
## 3.2 Interactive Theorem Proving via Monte-Carlo Tree Search
## Selection.
## Expansion.
## Backpropagation.
## 3.3 Intrinsic Rewards for Monte-Carlo Tree Search
## RMax applied to MCTS.
## UCB for Non-stationary Rewards.
## 3.4 Parallelization of Monte-Carlo Tree Search
## 3.5 Comparison with Existing Methods
## 4 Experimental Results
## 4.1 Main Results
## Metric.
## Results on miniF2F.
## Results on ProofNet.
## 4.2 Re-Examining the Effectiveness of Training Strategies on Large-scale Sampling
## General Enhancement of Reinforcement Learning.
## CoT, non-CoT, and Mixture Strategy.
## 4.3 Ablation Studies on RMaxTS
## Intrinsic Rewards and Discounted UCB.
## Guidance of Tactic State Information.
## 5 Conclusion, Limitation, and Future Work

=== BODY (head) ===
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
## Report GitHub Issue
×
Title:
Content selection saved. Describe the issue below:
Description:
Submit without GitHub
Submit in GitHub
arXiv is now an independent nonprofit!
Learn more
×
Back to arXiv
Why HTML?
Report Issue
Back to Abstract
Download PDF
Abstract
1 Introduction
1.1 Contributions
1.2 Summary of Evaluations and Metrics
2 Model Training
2.1 Pre-training
2.2 Supervised Fine-tuning
Data Curation.
Thought-augmented Proof Generation.
Prompt Augmentation with Tactic State Information.
Training Setting.
2.3 Reinforcement Learning from Proof Assistant Feedback
Prompts.
Rewards.
Reinforcement Learning Algorithm.
Training Setting.
2.4 Evaluation
Benchmarks.
Prompting Configurations.
Metric.
Comparison across Training Stages.
Comparison between CoT and non-CoT.
3 Exploration-oriented Monte-Carlo Tree Search
3.1 Tactic-level Tree Abstraction
Truncate: Proof Decomposition into Tree Nodes.
Resume: Proof Generation from a Tree Node.
3.2 Interactive Theorem Proving via Monte-Carlo Tree Search
Selection.
Expansion.
Backpropagation.
3.3 Intrinsic Rewards for Monte-Carlo Tree Search
RMax applied to MCTS.
UCB for Non-stationary Rewards.
3.4 Parallelization of Monte-Carlo Tree Search
3.5 Comparison with Existing Methods
4 Experimental Results
4.1 Main Results
Metric.
Results on miniF2F.
Results on ProofNet.
4.2 Re-Examining the Effectiveness of Training Strategies on Large-scale Sampling
General Enhancement of Reinforcement Learning.
CoT, non-CoT, and Mixture Strategy.
4.3 Ablation Studies on RMaxTS
Intrinsic Rewards and Discounted UCB.
Guidance of Tactic State Information.
5 Conclusion, Limitation, and Future Work
References
A Illustrative Examples of Non-CoT and CoT Prompting for Proof Completion
B Example Solutions to MiniF2F-test Problems
B.1 Problems that non-CoT outperforms CoT
B.2 Problems that CoT outperforms non-CoT
License: CC BY 4.0
arXiv:2408.08152v1 [cs.CL] 15 Aug 2024
\reportnumber
001
## 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
DeepSeek-AI
https://github.com/deepseek-ai/DeepSeek-Prover-V1.5
Corresponding author: Core contributors
## Abstract
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%).
Figure 1: Pass rates of models on formal theorem proving benchmarks in Lean 4: the high school level miniF2F-test benchmark ( Zheng et al., 2022 ) and the undergraduate level ProofNet benchmark ( Azerbayev et al., 2023 ) . We compare both the pre-trained and fine-tuned versions of DeepSeek-Prover-V1.5 with strong baselines.
## 1 Introduction
Recent advancements in large language models have significantly influenced mathematical reasoning and theorem proving in artificial intelligence. Despite notable progress in natural language domains, language models still encounter substantial challenges in formal theorem proving, e.g. using Lean ( Moura and Ullrich, 2021 ) and Isabelle ( Paulson, 1994 ) , which requires rigorous derivations satisfying formal specifications of the verification system.
Even advanced models like GPT-4 ( OpenAI, 2023 ) struggle with complex formal proofs, underscoring the intricate nature of both the coding and the mathematics involved.
A formal theorem proving model must not only grasp the syntax and semantics of formal systems like the Lean theorem prover but also align abstract mathematical reasoning with precise formal representation.
Language models in formal theorem proving typically employ two strategies: proof-step generation ( Polu and Sutskever, 2020 ; Jiang et al., 2022a ; Lample et al., 2022 ; Yang et al., 2023 ; Wu et al., 2024 ) and whole-proof generation ( Jiang et al., 2022b ; Zhao et al., 2023 ; Wang et al., 2023a ) . Proof-step generation predicts each subsequent tactic and verifies it using the formal verifier to obtain updated information about the current tactic state, often utilizing tree search techniques to construct valid proofs. In contrast, whole-proof generation is computationally efficient, which produces an entire proof code based on the theorem statement, requiring less communication budget to coordinate between the prover model and the formal theorem verifier. While DeepSeek-Prover-V1 ( Xin et al., 2024 ) has achieved state-of-the-art results in Lean 4 with whole-proof generation, this paradigm presents its unique challenges. It requires long-horizon sequence prediction without access to intermediate tactic states, and future tactics depend on these hidden results. In Lean’s tactic mode, proofs are constructed through a sequence of tactics that transform the proof state. This sequential nature introduces the risk of compounding errors ( Ross et al., 2011 ) , where a single misinterpretation can lead to significant deviations from a valid proof path. More specifically, the auto-regressive model may have incorrect believes on intermediate tactic states when generating long proofs.
To seamlessly integrate intermediate tactic states in proof-step generation while maintaining the simplicity and computational efficiency of whole-proof generation, we have developed a unified approach in DeepSeek-Prover-V1.5. This method combines the strengths of both proof-step and whole-proof generation techniques through a truncate-and-resume mechanism. The process begins with standard whole-proof generation, where the language model completes the proof code following the theorem statement prefix. The Lean prover then verifies this code. If the proof is correct and complete, the procedure terminates. If an error is detected, the code is truncated at the first error message, and any subsequent code is discarded. The successfully generated proof code is then used as a prompt for the generation of next proof segment. To enhance the accuracy of the model’s new completions, we append the latest state from the Lean 4 prover as a comment at the end of the prompt. Notably, our method is not restricted to resuming from the last successfully applied tactic. We integrate the truncate-and-resume mechanism into Monte-Carlo tree search ( Coulom, 2006 , MCTS;) in which the truncation points are scheduled by the tree search policy.
In addition, we propose a novel reward-free exploration algorithm for MCTS to address the reward sparsity issue of proof search.
We assign the tree search agent intrinsic motivation, a.k.a. curiosity ( Schmidhuber, 2010 ) , to extensively explore the tactic state space.
These algorithmic modules extend the functionality of our whole-proof generation model to become a flexible tool for interactive theorem proving, which can effectively utilize the proof assistant feedback and generate diverse solution candidates.
Figure 2: Overall Framework. DeepSeek-Prover-V1.5 is trained through pre-training, supervised fine-tuning, and reinforcement learning. During supervised fine-tuning, the pre-trained model receives an incomplete theorem proof ending with a tactic state comment keyword. The model is trained to predict the content of this tactic state (auxiliary objective) and complete the subsequent proof steps (main objective). In the reinforcement learning stage, given an incomplete theorem proof and ground-truth tactic state from the Lean prover, we roll out the fine-tuned model to generate multiple proof candidates, which are then verified by the Lean prover. The verification results for these candidates are used as binary (0-1) rewards to further optimize the model and enhance its alignment with the formal specifications of the verification system. For model inference, we offer two alternatives: single-pass sampling and Monte-Carlo tree search.
## 1.1 Contributions
We present a comprehensive framework for developing a language model-based formal mathematics prover, integrating several key components: large-scale mathematical pre-training, formal mathematics corpus construction and augmentation, online reinforcement learning from proof assistant feedback, and a tree search methodology for long-term planning in theorem proving. The pre-trained model, supervised fine-tuned model, and reinforcement learning model, along with the code for the Monte-Carlo tree search algorithm, are publicly available for further research and application.
•
Pre-Training : We enhance our base model’s capabilities in formal theorem proving and mathematical reasoning by further pre-training on high-quality mathematics and code data, with a focus on formal languages such as Lean, Isabelle, and Metamath.
•
Supervised Fine-Tuning : We improve the Lean 4 code completion dataset by implementing two data augmentation techniques. First, we use DeepSeek-Coder V2 236B ( Zhu et al., 2024 ) to annotate natural language chain-of-thought comments alongside Lean 4 code, aligning formal theorem proving with natural language reasoning. Second, we insert intermediate tactic state information within the Lean 4 proof code, enabling our model to leverage compiler feedback effectively. The resulting dataset is then used to fine-tune the pre-trained model.
•
Reinforcement Learning : We employ the GRPO algorithm ( Shao et al., 2024 ) to perform reinforcement learning from proof assistant feedback (RLPAF) on the supervised fine-tuned model. Verification results from the Lean prover serve as reward supervision, enhancing the model’s alignment with the formal specifications of the verification system.
•
Monte-Carlo Tree Search : We advance the tree search method in formal theorem proving by introducing a novel abstraction and a corresponding search algorithm. Our truncate-and-resume mechanism acts as a state-action abstraction, seamlessly integrating the tree search process into the whole-proof generation framework. We present RMaxTS, an innovative Monte-Carlo tree search algorithm that leverages the RMax ( Brafman and Tennenholtz, 2002 ) strategy to tackle exploration challenges in sparse-reward proof search problems. By assigning intrinsic rewards, this algorithm encourages the prover agent to generate diverse planning paths, thereby fostering extensive exploration of the proof space.
## 1.2 Summary of Evaluations and Metrics
•
miniF2F : In the single-pass whole-proof generation setting, DeepSeek-Prover-V1.5 achieved a pass rate of 60.2% on the test set of miniF2F, marking a significant improvement of absolute 10.2 percentage points over DeepSeek-Prover-V1’s 50.0%. Incorporating tree search techniques further elevated the pass rate to a new state-of-the-art 63.5% .
•
ProofNet : DeepSeek-Prover-V1.5 also demonstrated strong performance in the single-pass whole-proof generation setting for ProofNet, with pass rates of 21.6% on the validation set and 23.7% on the test set. The integration of tree search techniques further enhanced these results, achieving new state-of-the-art pass rates of 25.4% on the validation set and 25.3% on the test set.
## 2 Model Training
## 2.1 Pre-training
To enhance our language model’s proficiency in generating formal proofs and reasoning through mathematical language, we further pre-train our base model ( Shao et al., 2024 ) . This refinement involved training on high-quality datasets that include both code and natural language mathematical content. We specifically focused on formal languages widely used in proof assistants, such as Lean, Isabelle, and Metamath. We designate this improved model as DeepSeek-Prover-V1.5-Base.
## 2.2 Supervised Fine-tuning
In this section, we explore the methodology and processes involved in the supervised fine-tuning (SFT) of DeepSeek-Prover-V1.5. Specifically, we augment the proof dataset from DeepSeek-Prover-V1 by adding detailed explanatory comments. This enhancement aims to improve the alignment between natural language descriptions and Lean 4 code, thereby facilitating better formal mathematical reasoning. Additionally, we incorporate intermediate tactic state information as an auxiliary prediction task to support the truncate-and-resume mechanism used in the Monte-Carlo Tree Search process. We refer to the resulting model as DeepSeek-Prover-V1.5-SFT.
## Data Curation.
We develop a comprehensive Lean 4 code completion dataset for the supervised fine-tuning. This dataset includes synthetic proof code derived from a wide range of formal theorems. These theorems are sourced from various projects, such as the standard Lean 4 math library Mathlib4 ( Mathlib Community, 2020 ) , synthetic theorems from DeepSeek-Prover-V1 ( Xin et al., 2024 ) and Lean Workbook ( Ying et al., 2024a ) , and validation sets from the miniF2F ( Zheng et al., 2022 ) and ProofNet ( Azerbayev et al., 2023 ) benchmarks. To augment the formal proof data, we employed an expert iteration process ( Polu and Sutskever, 2020 ) . This involves generating proofs using the language model, verifying the generated proof data, retraining the model with the verified data, and then using the optimized model to generate additional proof data. Between each iteration, we use DeepSeek-Coder V2 236B ( Zhu et al., 2024 ) to annotate the thought process before the proof code as comments. Finally, we tailor these data for the truncate-and-resume mechanism for Monte-Carlo Tree Search (details in Section 3.1 ). The resulting proof dataset consists of 9,645k sequences.
## Thought-augmented Proof Generation.
In DeepSeek-Prover-V1, we identified a significant gap between problem-solving strategies in natural language and theorem proving in Lean. In natural language, models generate detailed deduction steps to construct proofs, whereas in Lean, they often rely on a sequence of high-level tactic calls to brute-force solutions. These high-level tactics, while effective, obscure their internal workings and outcomes, hindering the model’s ability to resolve complex proof goals with structured mathematical reasoning. To address this issue, we develop an approach that incorporates natural language reasoning before generating theorem proof code. Similar to Lean-STaR ( Lin et al., 2024 ) , which performs isolated chain-of-thought reasoning ( Wei et al., 2022 ; Feng et al., 2023 ) before each proof step, our method integrates this reasoning directly as comments within the proof code. We use the DeepSeek-Coder V2 236B ( Zhu et al., 2024 ) to enhance existing data in DeepSeek-Prover-V1 in two ways: first, by inserting a complete natural language solution at the beginning of the proof block, and second, by alternately inserting specific natural language steps for corresponding Lean tactics. Training the model with this data format enforces it to propose complete mathematical reasoning at the beginning of the proof block and detailed step planning before each tactic. This approach successfully develops new behaviors, employing delicate mathematical thinking to guide the generation of tactics. In the training data, two distinct guiding prompts are used to differentiate between the CoT (Chain of Thought) mode and the non-CoT mode for proof code completion. Examples of input and output in both modes can be found in Appendix A .
## Prompt Augmentation with Tactic State Information.
To implement the truncate-and-resume mechanism for Monte-Carlo Tree Search, we needed to extract tactic information from the code generated by the model. We enhanced the Lean REPL ( Leanprover Community, 2023 , Read-Eval-Print Loop;) with data extraction tools from the LeanDojo ( Yang et al., 2023 ) project. This allowed us to extract tactic information in triples, which include the position of each tactic, as well as the tactic states before and after its application. This information helps us identify the specific tactic code that triggers verification errors (used in the expansion step for tree search, see Section 3.2 ). For each tactic in a generated valid formal proof, we insert the tactic state returned by the verifier as a comment "/- tactic state: … -/". During training, we use all tokens following "/- tactic state: " as responses to calculate the supervised fine-tuning loss, while the tokens before this comment is used as prompts and do not contribute to the training loss calculation.
## Training Setting.
We conduct supervised fine-tuning based on the pre-trained model and train for 9B tokens, using a batch size of 2,048 and a constant learning rate of 1e-4. The training process begins with 100 warm-up steps to stabilize the learning dynamics. Training examples are randomly concatenated to form sequences, with a maximum context length of 4,096 tokens.
## 2.3 Reinforcement Learning from Proof Assistant Feedback
Reinforcement learning (RL) has been proven effective in enhancing the mathematical reasoning capabilities of supervised fine-tuned language models ( Shao et al., 2024 ) . To further advance DeepSeek-Prover-V1.5-SFT, we incorporate a reinforcement learning phase, resulting in the model DeepSeek-Prover-V1.5-RL. This phase leverages RL to enhance performance based on verification feedback from the Lean 4 prover. The specifics of this RL process are detailed below.
## Prompts.
In the reinforcement learning stage, we use a subset of theorem statements from the supervised fine-tuning dataset as training prompts. We select theorems for which DeepSeek-Prover-V1.5-SFT has a moderate success rate in generating correct proofs upon multiple attempts. This ensures that the model has room for improvement while still being able to receive positive feedback. After filtering, we retain approximately 4.5k unique theorem statements. Each theorem is prefixed with both CoT and non-CoT guiding prompts to enhance the model’s proof generation capabilities in both modes.
## Rewards.
When training LLMs via RL, a trained reward model typically provides feedback signals. In contrast, formal theorem proving benefits from the rigorous verification of generated proofs by proof assistants, offering a significant advantage. Specifically, each generated proof receives a reward of 1 if verified as correct, and 0 otherwise. While this binary reward signal is accurate, it is also sparse, especially for theorems that are challenging for the supervised fine-tuned model. To mitigate this sparsity, we select training prompts that are challenging yet achievable for the supervised fine-tuned model, as described above.
## Reinforcement Learning Algorithm.
We employ the Group Relative Policy Optimization ( Shao et al., 2024 , GRPO;) as our RL algorithm, which has demonstrated superior effectiveness and efficiency compared to PPO ( Schulman et al., 2017 ) , primarily because it eliminates the necessity of training an additional critic model. Specifically, GRPO samples a group of candidate proofs for each theorem prompt and optimizes the model based on the relative rewards of the outputs within the group. Our prompt selection strategy is designed to likely include both correct and incorrect proofs among the candidates, aligning well with the group-relative nature of GRPO and thereby enhancing the training process.
## Training Setting.
We conduct RL training based on the SFT model, which serves as both the initial model and the reference model for imposing the Kullback-Leibler (KL) divergence penalty. We use a constant learning rate of 5e-6, and the KL penalty coefficient is set to 0.02. For each theorem, we sample a group of 32 candidate proofs, with maximum length set to 2,048. The training batch size is configured to 512.
## 2.4 Evaluation
## Benchmarks.
We evaluate theorem-proving performance on the following benchmarks to compare model capabilities after each training stage:
•
MiniF2F ( Zheng et al., 2022 ) focuses on formal problem-solving skills for high-school level exercises and competitions, such as AMC, AIME, and IMO, with an emphasis on algebra and number theory. The benchmark includes 244 validation and 244 test problems, originally in Lean 3 and manually converted to Lean 4.9.0, based on the version provided by Yang (2023) .
•
ProofNet ( Azerbayev et al., 2023 ) evaluates formal theorem-proving capabilities at the undergraduate level in mathematics. It comprises 185 validation and 186 test problems from widely-used undergraduate textbooks, covering real and complex analysis, linear algebra, abstract algebra, and topology. These problems were initially in Lean 3 and manually converted to Lean 4.9.0.
Model
Pass@128
miniF2F-test
ProofNet-test
Base (3-shot)
29.7 % ± 0.5 % 29.7\%\pm 0.5\%
9.7 % ± 0.7 % 9.7\%\pm 0.7\%
SFT (non-CoT)
49.8 % ± 0.3 % 49.8\%\pm 0.3\%
15.9 % ± 0.5 % 15.9\%\pm 0.5\%
SFT (CoT)
50.4 % ± 0.4 % 50.4\%\pm 0.4\%
15.9 % ± 0.6 % 15.9\%\pm 0.6\%
RL (non-CoT)
50.5 % ± 0.6 % 50.5\%\pm 0.6\%
17.5 % ± 0.5 % 17.5\%\pm 0.5\%
RL (CoT)
51.6 % ± 0.5 % 51.6\%\pm 0.5\%
18.2 % ± 0.5 % 18.2\%\pm 0.5\%
Figure 3: Comparison of model capabilities at different training stages. "CoT" and "non-CoT" refer to evaluations using two guiding prompts. The shaded region represents the range of standard deviations around the mean values. The notation μ ± σ \mu\pm\sigma indicates the average accuracy μ \mu and the standard deviation σ \sigma .
## Prompting Configurations.
For each proof attempt of DeepSeek-Prover-V1.5-Base, we independently sample three proof demonstrations from the validation set to construct the few-shot prompts. For the miniF2F benchmark, we use human-written proofs from Yang (2023) , while for the ProofNet benchmark, we use correct proofs generated by DeepSeek-Prover-V1.5-RL as few-shot demonstrations. For DeepSeek-Prover-V1.5-SFT and DeepSeek-Prover-V1.5-RL, we employ two types of guiding prompts: one that encourages chain-of-thought (CoT) reasoning before each proof step, and one that does not (non-CoT). Detailed examples are provided in Appendix A .
## Metric.
We evaluate theorem-proving performance using the pass@ K K accuracy metric, which measures the model’s success in generating a correct proof within K K attempts. Each model is deployed on a single A100-40G GPU, utilizing the vLLM framework ( Kwon et al., 2023 ) for sample generation. The sampling parameters are set with a temperature of 1, a top-p value of 0.95, and a maximum token limit of 2,048. The generated proofs are then verified using the Lean 4 theorem prover. For this verification, we import Mathlib4 ( Mathlib Community, 2020 ) and Aesop ( Limperg and From, 2023 ) to access predefined premises and tactics. The verification process is subject to a time limit of 300 seconds.
## Comparison across Training Stages.
Figure 3 presents a comparative analysis of each training stage on the miniF2F and ProofNet datasets. Our base model, DeepSeek-Prover-V1.5-Base, achieves a notable pass rate, solving nearly one-third of the problems on the test set of the miniF2F benchmark using 3-shot prompting. The supervised fine-tuning stage, resulting in DeepSeek-Prover-V1.5-SFT, significantly outperforms the base model, with Pass@128 accuracy increasing by approximately two-thirds on miniF2F and doubling on ProofNet. The subsequent reinforcement learning stage further enhances the model’s performance, improving Pass@ K K accuracy across all values of K K . In contrast to findings in natural language mathematics, such as those reported in DeepSeekMath ( Shao et al., 2024 ) , where reinforcement learning primarily boosts the correct response from TopK, we observe a genuine enhancement of fundamental capabilities in formal theorem proving. This improvement is evident not only with a small sample budget but also remains stable as the sample budget increases. This conclusion is further supported by later Monte-Carlo Tree Search experiments with larger sample budgets, as discussed in Section 4.2 .
## Comparison between CoT and non-CoT.
We compare the performance of non-CoT and CoT generation modes for both DeepSeek-Prover-V1.5-SFT and DeepSeek-Prover-V1.5-RL. The results in Figure 3 demonstrate that the CoT mode consistently outperforms the non-CoT mode across most settings. Specifically, DeepSeek-Prover-V1.5-RL, leveraging these enhanced theorem-proving patterns, achieves superior performance on both benchmarks, with an average accuracy of 51.6 % 51.6\% on miniF2F and 18.2 % 18.2\% on ProofNet. The integration of natural language reasoning in CoT mode significantly enhances the planning and execution of formal proof writing. For a detailed comparison of proof strategies with and without the use of natural language chain-of-thought, refer to the examples provided in Appendix A .
## 3 Exploration-oriented Monte-Carlo Tree Search
## 3.1 Tactic-level Tree Abstraction
To implement the tree search method in the whole-proof generation setting, we introduce a proof tree abstraction to define the tailored state and action space, leveraging a truncate-and-resume mechanism.
Roughly following the paradigm of Yao et al. (2023) , we begin by decomposing an incomplete proof into a sequence of tree nodes that correspond to individual proof steps, and then we utilize the partial content stored in these tree nodes to continue the proof generation process.
Figure 4 illustrates the process of constructing a proof search tree from whole-proof generation.
## Truncate: Proof Decomposition into Tree Nodes.
We construct the proof search tree at the tactic level, where each tree edge represents a single transition step of the tactic state. Initially, we submit the entire proof the model generated to the Lean prover to parse it into tactics. We then truncate the proof at the earliest verification error, ensuring that all subsequent tactic codes can be successfully applied to advance the proof towards the desired theorem. The tactic codes are segmented into several code fractions, each containing a valid tactic code and its associated chain-of-thought comments, corresponding to a single tree edge that represents a tactic state transition. Through this abstraction, each tactic code is converted into a series of tree nodes, forming a path from the root to a specific node.
## Resume: Proof Generation from a Tree Node.
In Lean 4, different tactics can lead to the same tactic state, meaning each node in our proof tree can correspond to various tactic codes that achieve the same outcome. To handle this, we store a set of these equivalent tactic codes at each node. When the tree search agent expands a node, it randomly selects one tactic to use as a prompt for the language model. This prompt includes the incomplete proof code ending with the chosen tactic and the tactic state information from the Lean prover as a comment block. The fine-tuned model (see Section 2.2 ) has been trained to recognize and utilize this format, using the incomplete code augmented with tactic state comments to guide subsequent proof generation.
Figure 4: Truncate-and-Resume Mechanism in the Expansion Step of MCTS. (a) After selecting a node, we trace its corresponding incomplete proof code prefix, which includes the file header, initial statement, and successfully applied tactics from the ancestor nodes. (b) The language model then generates the subsequent proof based on this prefix along with a comment block containing the current tactic state. (c) The combined proof code (prefix and newly generated code) is verified by the Lean 4 prover. If no errors are found, the tree-search procedure terminates. If errors are detected, we truncate the newly generated code at the first error message, discard the subsequent code, and parse the successful portion into tactics. (d) Each tactic is added as a new node in the search tree, extending a chain of descendants beneath the selected node. (e) Once the tree updates are complete, the next iteration of expansion begins by selecting an alternative candidate node, which is not limited to leaf nodes. This process repeats until a correct proof is found or the sample budget is exhausted.
## 3.2 Interactive Theorem Proving via Monte-Carlo Tree Search
Our proof search tree is developed using the standard Monte-Carlo Tree Search (MCTS) paradigm ( Coulom, 2006 ; Browne et al., 2012 , MCTS;) , which iteratively applies four steps: Selection , Expansion , Simulation , and Backpropagation .
We integrate the Simulation step into Expansion because our whole-proof generation model inherently performs a rollout from the expanded node.
The detailed design of the algorithm workflow is as follows.
## Selection.
The selection step, a.k.a. the tree policy, starts from the root node and traverses downward to identify a promising node for expansion.
The objective of this algorithmic step is to trade off between exploration and exploitation ( Kocsis and Szepesvári, 2006 ) .
The tree policy at a tree node s s is computed by selecting the action that maximizes the value from the set of valid operations:
T ​ r ​ e ​ e ​ P ​ o ​ l ​ i ​ c ​ y ​ ( s ) = arg ⁡ max a ∈ C ​ h ​ i ​ l ​ d ​ r ​ e ​ n ​ ( s ) ∪ { ⊘ } ⁡ Q U ​ C ​ B ​ ( s , a ) , \displaystyle TreePolicy(s)=\mathop{\arg\max}_{a\in Children(s)\cup\{\oslash\}}Q_{UCB}(s,a),
(1)
where the action a a can be either moving to a child node, denoted by a ∈ C ​ h ​ i ​ l ​ d ​ r ​ e ​ n ​ ( s ) a\in Children(s) , or expanding the current node s s , denoted by a special token a = ⊘ a=\oslash .
This approach uses a technique called virtual node ( Wang et al., 2023b ) , which assigns each node an imaginary child to represent the selection of the current node s s for expansion.
It enables the tree search agent to continually expand non-leaf nodes, as the action space is supported by a generative model whose output scope cannot be determined by a fixed number of trails.
The value estimation Q U ​ C ​ B ​ ( s , a ) Q_{UCB}(s,a) of performing action a a on node s s is composed by two components:
∀ a ∈ C ​ h ​ i ​ l ​ d ​ r ​ e ​ n ​ ( s ) ∪ { ⊘ } , Q U ​ C ​ B ​ ( s , a ) \displaystyle\forall a\in Children(s)\cup\{\oslash\},\quad Q_{UCB}(s,a)
= Q ⁡ ( s , a ) ⏟ Exploitation + U ​ C ​ B ​ ( s , a ) ⏟ Exploration , \displaystyle=\underbrace{Q(s,a)}_{\text{Exploitation}}+\penalty\ \penalty\ \penalty\ \underbrace{UCB(s,a)}_{\text{Exploration}},
(2)
where Q ⁡ ( s , a ) Q(s,a) denotes a sample-based estimation of action values derived from the selection history, functioning as the exploitation component that retrieves high-value candidates from previous trials. U ​ C ​ B ​ ( s , a ) UCB(s,a) denotes the exploration bonus computed by upper confidence bounds ( Auer, 2002 , UCB;) , which diminishes with the repeated execution of the state-action pair ( s , a ) (s,a) . More specifically, Q U ​ C ​ B ​ ( s , a ) Q_{UCB}(s,a) stands for an optimistic estimation of Q ⁡ ( s , a ) Q(s,a) and can serve as an upper bound with high probability. We defer the discussion of detailed settings of node values and UCB bonus to Section 3.3 .
## Expansion.
The next step is invoking the proof generation model to expand the node nominated by the selection phase.
Resuming the incomplete proof codes stored on the node designated for expansion, we perform whole-proof generation to propose a series of subsequent tactics and submit the generated proof to Lean prover for verification.
Such a trial of proof completion is equivalent to conducting a single rollout of simulation within the standard MCTS framework.
When the verification result indicates the proof is complete, the search procedure is ready to be terminated, having found a new proof of the desired theorem.
Otherwise, we parse the verification feedback and truncate the generated proof to the assertion of the earliest verification error.
The remaining tactics are transformed into a path of nodes to be merged into the search tree (see Figure 4 ).
It is important to note that, because we use the whole-proof generation setting—where the output is an entire proof consisting of a sequence of tactics, rather than just the next tactic—our expansion procedure may insert a path of tree nodes into the search tree during each iteration. This differs from the conventional MCTS designed for competitive games, which typically expands only one layer of children nodes per iteration ( Silver et al., 2016 ; Silver et al., 2018 ; Schrittwieser et al., 2020 ) .
## Backpropagation.
The final phase of each tree search iteration is to update value statistics along the selection trajectory from the root to the expanded node, i.e. , updating the values associated with the tree policy stated in Eq. ( 1 ).
Let τ = { ( r o o t , s ( 1 ) ) , ( s ( 1 ) , s ( 2 ) ) , ( s ( 2 ) , s ( 3 ) ) , … , ( s ( | τ | − 1 ) = s t , ⊘ ) } \tau=\{(root,s^{(1)}),(s^{(1)},s^{(2)}),(s^{(2)},s^{(3)}),\dots,(s^{(|\tau|-1)}=s_{t},\oslash)\} denote the selection trajectory of t t -th iteration that ends with s t s_{t} as the expanding node.
We update Q U ​ C ​ B ​ ( s , a ) Q_{UCB}(s,a) for all ( s , a ) ∈ τ (s,a)\in\tau by taking the most recent trajectory reward R ⁡ ( τ ) R(\tau) into account (details refer to Eq. ( 7 )).
The extrinsic source of rewards comes from the compiler feedback, specifically assigning a reward of R extrinsic ​ ( τ ) = 1 R_{\text{extrinsic}}(\tau)=1 for completed proofs and R extrinsic ​ ( τ ) = 0 R_{\text{extrinsic}}(\tau)=0 for unsolved ones.
In Section 3.3 , we will introduce an intrinsic reward mechanism to augment the reward assignment that enhances the agent’s incentive for exploration.
## 3.3 Intrinsic Rewards for Monte-Carlo Tree Search
In the search problem of formal theorem proving, the extrinsic rewards are extremely sparse, i.e. , the search agent only obtains non-zero rewards when the proof is completely solved.
More specifically, the proof search process forms a tree structure with only a narrow set of leaves delivering non-zero rewards, which matches a famous hard-exploration case ( Krishnamurthy et al., 2016 ) in the literature of statistical reinforcement learning.
To promote exploration in sparse-reward sequential decision making, one classical paradigm is constructing intrinsic rewards ( Schmidhuber, 2010 ) that encourage the agent to not only optimize extrinsic rewards but also acquire general information about the interactive environment ( Bellemare et al., 2016 ; Houthooft et al., 2016 ; Pathak et al., 2017 ; Burda et al., 2019 ) .
In this section, we present our intrinsic-reward-driven exploration algorithm, RMax applied to Tree Search (RMaxTS), to incorporate reward-free exploration in the proof search problem.
## RMax applied to MCTS.
We adopt RMax ( Brafman and Tennenholtz, 2002 ) , a classical exploration mechanism, to construct intrinsic rewards for Monte-Carlo tree search.
The core idea of RMax is to explore a broad coverage of the state space.
The agent awards itself a maximal amount of reward upon reaching an unseen state.
In the context of proof search, where no extrinsic rewards are provided until the proof is completed, our algorithmic procedure resembles ZeroRMax ( Jin et al., 2020 ) , in which the agent’s exploration is driven solely by intrinsic rewards, i.e. , setting R ​ ( τ ) = R intrinsic ​ ( τ ) R(\tau)=R_{\text{intrinsic}}(\tau) .
The intrinsic reward of a tree expansion step is determined by whether a new node is added to the search tree,
R intrinsic ​ ( τ ) = 𝕀 ⁡ [ at least one new node is added to the search tree ] , \displaystyle R_{\text{intrinsic}}(\tau)=\mathbb{I}\left[\text{at least one new node is added to the search tree}\right],
(3)
where τ \tau denotes the most recent selection trajectory that requires a reward assignment for backpropagation.
This exploration strategy prioritizes the expansion of nodes where the prover model generates tactics that lead to a diverse range of tactic states.
As multiple Lean codes can result in the same transition of intermediate states, this heuristics can potentially reduce redundant generation and improve sample efficiency.
## UCB for Non-stationary Rewards.
The common setting of UCB exploration bonus for Monte-Carlo tree search is using UCB1 ( Auer et al., 2002 ) :
Q U ​ C ​ B ​ 1 ​ ( s , a ) \displaystyle Q_{UCB1}(s,a)
= W ⁡ ( s , a ) N ⁡ ( s , a ) + 2 ​ ln ​ ∑ a ′ N ⁡ ( s , a ′ ) N ⁡ ( s , a ) , \displaystyle=\frac{W(s,a)}{N(s,a)}+\sqrt{\frac{2\ln\sum_{a^{\prime}}N(s,a^{\prime})}{N(s,a)}},
(4)
W ⁡ ( s , a ) \displaystyle W(s,a)
= ∑ τ ∈ Γ ⁡ ( s , a ) R ⁡ ( τ ) , \displaystyle=\textstyle{\sum_{\tau\in\Gamma(s,a)}}\penalty\ R(\tau),
(5)
N ⁡ ( s , a ) \displaystyle N(s,a)
= | Γ ⁡ ( s , a ) | , \displaystyle=\left|\Gamma(s,a)\right|,
(6)
where Γ ⁡ ( s , a ) = { τ ∣ ( s , a ) ∈ τ } \Gamma(s,a)=\{\tau\mid(s,a)\in\tau\} denotes the list of tree-policy trajectory τ \tau containing ( s , a ) (s,a) as an intermediate selection step.
To facilitate discussions, we organize the list Γ ⁡ ( s , a ) = { τ 1 , τ 2 , ⋯ } \Gamma(s,a)=\{\tau_{1},\tau_{2},\cdots\} such that newly collected trajectories have larger subscript indices.
In this work, we propose to use an alternative variant of UCB method.
Note that the derived intrinsic reward in Eq. ( 3 ) is a non-stationary reward signal whose expected value decays with the progress of exploration.
That is because it becomes definitely harder to discover new nodes with unseen tactic states as the search tree expands through sophisticated exploration.
To tackle the non-stationarity, we consider discounted upper confidence bounds ( Garivier and Moulines, 2011 , DUCB;) , which uses a discount factor γ ∈ ( 0 , 1 ) \gamma\in(0,1) to smoothly drop those outdated feedback records:
Q D ​ U ​ C ​ B ​ ( s , a ) \displaystyle Q_{DUCB}(s,a)
= W γ ​ ( s , a ) N γ ​ ( s , a ) + 2 ​ ln ​ ∑ a ′ N γ ​ ( s , a ′ ) N γ ​ ( s , a ) , \displaystyle=\frac{W_{\gamma}(s,a)}{N_{\gamma}(s,a)}+\sqrt{\frac{2\ln\sum_{a^{\prime}}N_{\gamma}(s,a^{\prime})}{N_{\gamma}(s,a)}},
(7)
W γ ​ ( s , a ) \displaystyle W_{\gamma}(s,a)
= ∑ t = 1 N ⁡ ( s , a ) γ N ⁡ ( s , a ) − t ​ R ​ ( τ t ) , \displaystyle=\textstyle{\sum_{t=1}^{N(s,a)}}\penalty\ \gamma^{N(s,a)-t}R(\tau_{t}),
(8)
N γ ​ ( s , a ) \displaystyle N_{\gamma}(s,a)
= ∑ t = 0 N ⁡ ( s , a ) − 1 γ t , \displaystyle=\textstyle{\sum_{t=0}^{N(s,a)-1}}\penalty\ \gamma^{t},
(9)
where newly received feedback would be assigned a larger weight in the value estimation.
In practice, we set γ = 0.99 \gamma=0.99 .
Note that the role of discount factor γ \gamma in DUCB differs from its role in value iteration for infinite-horizon MDPs.
The discounting is applied to tree search iterations rather than to the action-step horizon within a single trajectory.
## 3.4 Parallelization of Monte-Carlo Tree Search
To enhance the efficiency of Monte-Carlo Tree Search (MCTS), we implement several established parallelization techniques as described by Chaslot et al. (2008) .
•
Root Parallelization: We deploy 256 MCTS runners per node, with one language model per GPU and a batch size of 512 for proof generation. The Lean prover is invoked through REPL and executed on a cluster with thousands of CPU cores, where each proof verification task is handled by an individual process, created and terminated in a sandbox. Both proof generation by language models and verification by Lean provers are handled asynchronously. This setup allows MCTS runners to perform concurrent tree search operations, significantly accelerating the process.
•
Tree Parallelization: We manage each search tree with 32 thread workers to parallelize the tree iteration steps. This method effectively schedules and balances the tasks of proof generation and Lean verification. Each thread worker iteratively performs the tree search loop by selecting a candidate node for expansion, invoking the language model to generate the proof, verifying the generated proof with the Lean prover, and performing backpropagation.
•
Virtual Loss: To encourage diverse node selection among concurrent thread workers, we assign a virtual reward R ⁡ ( τ ) = 0 R(\tau)=0 for ongoing iterations. This involves backpropagating a reward of 0 0 temporarily and updating it to the true reward upon completion. This strategy promotes exploration of different nodes for expansion, thereby enhancing the overall search efficiency.
## 3.5 Comparison with Existing Methods
In this section, we compare our proposed proof tree search method, which introduces a novel truncate-and-resume mechanism for whole-proof generation, with existing approaches. Current methods for using language models in formal mathematics proof search generally fall into two main strategies:
•
Multi-pass proof-step generation : This strategy breaks down the proving process into multiple episodes of tactic generation and verification, typically following a tree search pattern. It involves generating and verifying one tactic at a time, repeating the process for the next tactic until no proof goals remain. Notable examples include GPT-f ( Polu and Sutskever, 2020 ; Polu et al., 2022 ) , Thor ( Jiang et al., 2022a ) , ReProver ( Yang et al., 2023 ) , Hypertree Proof Search ( Lample et al., 2022 ) , and InternLM2-StepProver ( Wu et al., 2024 ) .
•
Single-pass whole-proof generation : This approach generates and verify an entire proof in one attempt. If the proof is incorrect, the model generates a new proof in the next attempt. Methods in this category include DSP ( Jiang et al., 2022b ) , Subgoal-Prover Zhao et al. (2023) , LEGO-Prover ( Wang et al., 2023a ) , Lyra ( Zheng et al., 2023 ) , and miniCTX ( Hu et al., 2024 ) .
Our proof tree search method uniquely bridges these two strategies, offering a novel hybrid approach. It starts with whole-proof generation, similar to the single-pass approach, but extends this by implementing a sophisticated truncate-and-resume mechanism. This process involves truncating the generated proof to its successful initial segment, parsing this segment into individual tactics, and resuming the tree search from this point. This iterative process effectively implements a Monte-Carlo Tree Search, seamlessly integrating single-pass whole-proof generation with multi-pass proof-step generation. Consequently, we can train a single model with nearly identical objectives to support both strategies simultaneously. Our experimental results demonstrate that this unified approach achieves superior performance in both settings. By combining the strengths of existing methods and introducing innovative techniques, our method offers a more versatile and effective solution for formal mathematics proof search, potentially paving the way for future advancements in this field.
## 4 Experimental Results
In this section, we evaluate the theorem-proving capabilities of DeepSeek-Prover-V1.5 using two distinct benchmarks: miniF2F, which encompasses high-school level exercises and competition problems, and ProofNet, which pertains to undergraduate-level theorems. We present the results for both complete proof generation and Monte-Carlo tree search methodologies, utilizing the same trained model and inference configuration as Section 2.4 to ensure consistency.
## 4.1 Main Results
We present a comparative analysis of DeepSeek-Prover-V1.5 against previous state-of-the-art language models, highlighting its performance and advancements.
•
General-purpose Models: GPT-3.5 and GPT-4 ( OpenAI, 2023 ) are advanced generative AI models developed by OpenAI, known for their effectiveness across diverse tasks, including code generation. Despite not being specifically designed for theorem proving, their extensive parameter scales provide significant capabilities. The evaluation of these models in formal theorem proving is facilitated by COPRA ( Thakur et al., 2023 ) , an in-context learning agent that leverages these large language models to propose tactic applications. Additionally, we examine Llemma ( Azerbayev et al., 2024 ) , a series of language models trained on extensive general mathematical corpora, commonly used as the base model for formal theorem proving.
•
Specialized Models for Formal Mathematics: GPT-f ( Polu and Sutskever, 2020 ; Polu et al., 2022 ) represents an initial effort to apply Transformers ( Vaswani et al., 2017 ) to proof-step generation for theorem proving tasks, utilizing a best-first search module to construct complete proofs. Subsequent advancements include ReProver ( Yang et al., 2023 ) , LLMStep ( Welleck and Saha, 2023 ) , and Lean-STaR ( Lin et al., 2024 ) . Hypertree Proof Search ( Lample et al., 2022 ) explores the use of Monte Carlo tree search in formal theorem proving using Lean. Concurrent works, InternLM2-Math ( Ying et al., 2024b ) and InternLM2-StepProver ( Wu et al., 2024 ) , also demonstrate outstanding performance.
## Metric.
We compare the performance of DeepSeek-Prover-V1.5 with state-of-the-art models using the pass@ K K accuracy metric, which evaluates the model’s ability to generate a correct proof within K K attempts.
We display the sample budget K K according to the the following rules to align the computation budget across different generation schemes.
•
For single-pass sampling methods, we define the sample budget K K as the total number of proofs generated, with large values of K K factorized for the ease of comparison to tree search methods.
•
For best-first-search methods, following the notation of Azerbayev et al. (2024) , we present K = N × S × T K=N\times S\times T where N N denotes the number of best-first-search attempts, S S denotes the number of tactics generated for each expansion, and T T denotes the number of expansion iterations.
•
For tree search methods, e.g. , RMaxTS and HTPS ( Lample et al., 2022 ) , we present K = N × T K=N\times T where N N denotes the number of tree search attempts, and T T denotes the number of model generations invoked in tree expansions.
## Results on miniF2F.
Table 1 provides a comparative analysis of various theorem-proving methods on the miniF2F-test dataset. In the single-pass whole-proof generation setting, DeepSeek-Prover-V1.5-RL achieved the highest pass rate at 60.2%, marking a significant improvement of 10.2 percentage points over DeepSeek-Prover-V1’s 50.0%. With a sampling budget limited to 128 attempts, DeepSeek-Prover-V1.5-RL proved 51.6% of the problems, significantly outperforming other whole-proof generation methods and is comparable to the leading tree search methods. In the Tree Search Methods category, DeepSeek-Prover-V1.5-RL + RMaxTS leads with a pass rate of 62.7%, establishing a new state-of-the-art and creating a substantial gap with existing methods. Notably, DeepSeek-Prover-V1.5-RL requires only 3200 whole-proof generation samplings to achieve a pass rate of 54.9%, surpassing the previous state-of-the-art result of InternLM2-StepProver, which performs 64 × 3200 64\times 3200 tree searches to achieve 54.5%.
Method
Sample budget
miniF2F-test
Single-pass Whole-Proof Generation Methods
TheoremLlama [ 49 ]
128
33.6 % 33.6\%
DeepSeek-Prover-V1 [ 53 ]
128 128
46.1 % ± 0.5 % 46.1\%\pm 0.5\%
16 × 4096 16\times 4096
50.0 % 50.0\%
DeepSeek-Prover-V1.5-Base
128
29.7 % ± 0.5 % 29.7\%\pm 0.5\%
3200
39.2 % 39.2\%
6400
42.2 % 42.2\%
DeepSeek-Prover-V1.5-SFT
32
48.2 % ± 0.6 % 48.2\%\pm 0.6\%
64
49.6 % ± 0.7 % 49.6\%\pm 0.7\%
128 128
50.4 % ± 0.4 % 50.4\%\pm 0.4\%
3200 3200
53.3 % ± 0.5 % 53.3\%\pm 0.5\%
4 × 6400 4\times 6400
55.8 % ± 0.7 % 55.8\%\pm 0.7\%
16 × 6400 16\times 6400
57.4 % 57.4\%
DeepSeek-Prover-V1.5-RL
32
50.0 % ± 0.5 % 50.0\%\pm 0.5\%
64
50.7 % ± 0.4 % 50.7\%\pm 0.4\%
128 128
51.6 % ± 0.5 % 51.6\%\pm 0.5\%
3200 3200
54.9 % ± 0.7 % 54.9\%\pm 0.7\%
4 × 6400 4\times 6400
58.4 % ± 0.6 % 58.4\%\pm 0.6\%
16 × 6400 16\times 6400
60.2 % \mathbf{60.2\%}
Tree Search Methods
COPRA (Code Llama) [ 45 ]
1 × 500 1\times 500
5.7 % 5.7\%
COPRA (GPT-3.5) [ 45 ]
1 × 60 1\times 60
9.0 % 9.0\%
COPRA (GPT-4) [ 45 ]
1 × 60 1\times 60
26.6 % 26.6\%
Llemma-7B [ 5 ]
1 × 32 × 100 1\times 32\times 100
26.2 % 26.2\%
Llemma-34B [ 5 ]
1 × 32 × 100 1\times 32\times 100
25.8 % 25.8\%
ReProver [ 55 ]
-
26.5 % 26.5\%
LLMStep [ 51 ]
1 × 32 × 100 1\times 32\times 100
27.9 % 27.9\%
GPT-f [ 35 ]
64 × 8 × 512 64\times 8\times 512
36.6 % 36.6\%
Hypertree Proof Search [ 23 ]
64 × 5000 64\times 5000
41.0 % 41.0\%
Lean-STaR [ 26 ]
64 × 1 × 50 64\times 1\times 50
46.3 % 46.3\%
InternLM2-Math-7B [ 58 ]
1 × 32 × 100 1\times 32\times 100
30.3 % 30.3\%
InternLM2-Math-Plus-7B [ 58 ]
1 × 32 × 100 1\times 32\times 100
43.4 % 43.4\%
InternLM2-StepProver [ 52 ]
1 × 32 × 100 1\times 32\times 100
48.8 % 48.8\%
64 × 32 × 100 64\times 32\times 100
54.5 % 54.5\%
DeepSeek-Prover-V1.5-SFT + RMaxTS
1 × 3200 1\times 3200
53.5 % ± 0.4 % 53.5\%\pm 0.4\%
4 × 6400 4\times 6400
56.3 % ± 0.3 % 56.3\%\pm 0.3\%
16 × 6400 16\times 6400
59.0 % 59.0\%
32 × 6400 † 32\times 6400^{\dagger}
60.2 % 60.2\%
DeepSeek-Prover-V1.5-RL + RMaxTS
1 × 3200 1\times 3200
55.0 % ± 0.7 % 55.0\%\pm 0.7\%
4 × 6400 4\times 6400
59.6 % ± 0.6 % 59.6\%\pm 0.6\%
16 × 6400 16\times 6400
62.7 % \mathbf{62.7\%}
32 × 6400 † 32\times 6400^{\dagger}
63.5 % \mathbf{63.5\%}
Table 1:
Comparison with state-of-the-art methods on the miniF2F-test dataset. The notation μ ± σ \mu\pm\sigma denotes the average accuracy μ \mu and the standard deviation σ \sigma . Unless otherwise specified, DeepSeek-Prover-V1.5-Base results are based on 3-shot prompting, while DeepSeek-Prover-V1.5-SFT and RL employ CoT mode prompting. The symbol † {\dagger} indicates performance using a mixture strategy with two guiding prompts (see Section 4.2 for details).
## Results on ProofNet.
Table 2 presents a comparative analysis of various theorem-proving methods on the ProofNet dataset. DeepSeek-Prover-V1.5-RL achieved pass rates of 22.6% and 25.3% for the overall ProofNet dataset in the single-pass whole-proof generation setting and with the enhancement of RMaxTS, respectively. These results surpass the existing state-of-the-art methods, ReProver (13.8%) and InternLM2-StepProver (18.1%). When the number of whole-proof generation attempts is restricted to 3200, DeepSeek-Prover-V1.5 also proved 21.7% of the theorems, demonstrating a 3.6% improvement over the previous state-of-the-art, InternLM2-StepProver.
Method
Sample budget
ProofNet
valid ‡
test
all
Single-pass Whole-Proof Generation Methods
DeepSeek-Prover-V1.5-Base
128 128
6.6 % ± 0.9 % 6.6\%\pm 0.9\%
9.7 % ± 0.7 % 9.7\%\pm 0.7\%
7.5 % ± 0.7 % 7.5\%\pm 0.7\%
3200 3200
10.8 % 10.8\%
15.6 % 15.6\%
13.2 % 13.2\%
DeepSeek-Prover-V1.5-SFT
128 128
19.9 % ± 0.4 % 19.9\%\pm 0.4\%
15.9 % ± 0.6 % 15.9\%\pm 0.6\%
17.9 % ± 0.3 % 17.9\%\pm 0.3\%
3200 3200
20.7 % ± 0.7 % 20.7\%\pm 0.7\%
21.0 % ± 0.9 % 21.0\%\pm 0.9\%
20.9 % ± 0.6 % 20.9\%\pm 0.6\%
4 × 6400 4\times 6400
22.2 % 22.2\%
23.7 % 23.7\%
22.9 % 22.9\%
DeepSeek-Prover-V1.5-RL
128 128
20.1 % ± 0.5 % 20.1\%\pm 0.5\%
18.2 % ± 0.5 % 18.2\%\pm 0.5\%
19.1 % ± 0.4 % 19.1\%\pm 0.4\%
3200 3200
21.4 % ± 0.3 % 21.4\%\pm 0.3\%
22.0 % ± 0.5 % 22.0\%\pm 0.5\%
21.7 % ± 0.4 % 21.7\%\pm 0.4\%
4 × 6400 4\times 6400
21.6 % 21.6\%
23.7 % 23.7\%
22.6 % 22.6\%
Tree Search Methods
ReProver [ 55 ]
-
-
-
13.8 % 13.8\%
InternLM2-StepProver [ 52 ]
1 × 32 × 100 1\times 32\times 100
-
-
18.1 % 18.1\%
DeepSeek-Prover-V1.5-SFT + RMaxTS
1 × 3200 1\times 3200
22.2 % ± 0.7 % 22.2\%\pm 0.7\%
21.6 % ± 0.2 % 21.6\%\pm 0.2\%
21.9 % ± 0.4 % 21.9\%\pm 0.4\%
4 × 6400 4\times 6400
23.8 % 23.8\%
25.8%
24.8 % 24.8\%
DeepSeek-Prover-V1.5-RL + RMaxTS
1 × 3200 1\times 3200
22.0 % ± 0.3 % 22.0\%\pm 0.3\%
21.5 % ± 0.8 % 21.5\%\pm 0.8\%
21.8 % ± 0.4 % 21.8\%\pm 0.4\%
4 × 6400 4\times 6400
25.4 % 25.4\%
25.3%
25.3 % 25.3\%
Table 2: Comparing with state-of-the-arts on the ProofNet dataset. ‡ Note that the validation set of ProofNet is used to perform expert iteration in supervised fine-tuning.
## 4.2 Re-Examining the Effectiveness of Training Strategies on Large-scale Sampling
We revisit the effects of several training modules in n a large-scale sampling setting, focusing on both single-pass whole-proof generation and Monte-Carlo tree search. The results demonstration that the observations and findings presented in Section 2.4 generalize to sampling scenarios with a large sample size.
## General Enhancement of Reinforcement Learning.
To support the claim that online reinforcement learning from verification feedback generally enhances the model capabilities, we compare our final model to the SFT-only version using a large sample budget.
The comparison results are presented as two columns in Table 3 .
DeepSeek-Prover-V1.5-RL consistently outperforms the SFT model across all generation settings, regardless of whether the chain-of-thought strategy is applied.
The results also indicate that the improvements gained from conducting online RL is orthogonal to those achieved through RMaxTS, which can be further combined to boost the performance.
By integrating both CoT prompting and RMaxTS, DeepSeek-Prover-V1.5-RL achieves a pass rate of 62.7 % 62.7\% on miniF2F-test.
This performance shows a notable 3.7 % 3.7\% improvement over the SFT model, highlighting the critical role of reinforcement learning in enhancing the overall effectiveness of the proof completion model.
## CoT, non-CoT, and Mixture Strategy.
We compare the performance of two generation modes, i.e. , non-CoT and CoT, on miniF2F-test dataset.
The results, shown in Table 3 , indicate that the advantage of CoT over the non-CoT mode is amplified as the sample budget increases.
This suggests that the incorporation of natural language chain-of-thought can diversify the planning pathways of theorem proving, potentially leading to a broader range of reasoning strategies and more innovative solutions.
Results also show that these two modes have complementary advantages across different problems.
The model’s theorem proving strategy in the CoT mode is more systematic and proactive in mathematical thinking, while in the non-CoT mode, the model can efficiently use Lean high-level tactics to solve computational problems that can be addressed within Lean’s automation mechanisms.
To leverage these advantages, we consider a mixture strategy, denoted by non-CoT & CoT in Table 3 , allocates half of sample budget to the CoT mode and the remains to the non-CoT mode.
This simple combination of two guiding prompts shows great promise in further bootstrapping the performance of our proof completion model, achieving a pass rate of 63.5 % 63.5\% on miniF2F-test. In Appendix B , we present example problems that illustrate the different advantages of the two generation modes.
Prompt mode
Sample budget
DeepSeek-Prover-V1.5
SFT
RL
non-CoT
4 × 6400 4\times 6400
54.7 % ± 0.4 % 54.7\%\pm 0.4\%
56.5 % ± 0.5 % 56.5\%\pm 0.5\%
16 × 6400 16\times 6400
56.1 % 56.1\%
57.4 % 57.4\%
Single-Pass
CoT
4 × 6400 4\times 6400
55.8 % ± 0.7 % 55.8\%\pm 0.7\%
58.4 % ± 0.5 % 58.4\%\pm 0.5\%
Generation
16 × 6400 16\times 6400
57.4 % 57.4\%
60.2 % 60.2\%
non-CoT & CoT
( 2 + 2 ) × 6400 (2+2)\times 6400
56.1 % ± 0.8 % 56.1\%\pm 0.8\%
58.3 % ± 0.6 % 58.3\%\pm 0.6\%
( 8 + 8 ) × 6400 (8+8)\times 6400
58.2 % 58.2\%
60.7 % 60.7\%
( 16 + 16 ) × 6400 (16+16)\times 6400
58.6 % 58.6\%
61.1 % 61.1\%
RMaxTS
non-CoT
4 × 6400 4\times 6400
55.7 % ± 0.6 % 55.7\%\pm 0.6\%
58.4 % ± 0.6 % 58.4\%\pm 0.6\%
16 × 6400 16\times 6400
57.8 % 57.8\%
59.4 % 59.4\%
CoT
4 × 6400 4\times 6400
56.3 % ± 0.3 % 56.3\%\pm 0.3\%
59.6 % ± 0.6 % 59.6\%\pm 0.6\%
16 × 6400 16\times 6400
59.0 % 59.0\%
62.7 % 62.7\%
non-CoT & CoT
( 2 + 2 ) × 6400 (2+2)\times 6400
56.1 % ± 0.8 % 56.1\%\pm 0.8\%
60.0 % ± 0.8 % 60.0\%\pm 0.8\%
( 8 + 8 ) × 6400 (8+8)\times 6400
59.0 % 59.0\%
63.1 % 63.1\%
( 16 + 16 ) × 6400 (16+16)\times 6400
60.2 % 60.2\%
63.5%
Table 3: A large-scale ablation study to investigate the effectiveness of several algorithmic designs on model training. The results are evaluated on the miniF2F-test dataset.
## 4.3 Ablation Studies on RMaxTS
## Intrinsic Rewards and Discounted UCB.
We investigate the effectiveness of two core components of RMaxTS, i.e. , the intrinsic rewards defined in Eq. ( 3 ) and the discounted upper confidence bound stated in Eq. ( 7 ).
We start with a baseline implementing the standard UCT algorithm ( Kocsis and Szepesvári, 2006 ) without intrinsic rewards, in which the exploration is driven exclusively by the UCB bonus.
Note that, since no non-zero rewards are provided for this baseline, all variants of the UCB formula become equivalent, as node selection is determined solely by visitation counts.
The experimental results in Figure 5 show that, in the absence of intrinsic rewards, the performance of UCT (without R intrinsic R_{\text{intrinsic}} ) degenerates into a level comparable to that of non-search methods.
Furthermore, we consider RMaxTS using the standard UCB1 (refer to Eq. ( 4 )) instead of the discounted UCB, denoted by RMaxTS (DUCB → \rightarrow UCB1).
The results indicate that the performance of RMaxTS with UCB1 bonus is also moderate, comparable to that of UCT (without R intrinsic R_{\text{intrinsic}} ).
That is because UCB1 is designed to guarantee asymptotic performance through exhausted exploration ( Auer et al., 2002 ) assuming the sample size to be sufficiently large.
In contrast, the discounted UCB can accelerate the value propagation of non-stationary intrinsic rewards, preventing the guidance of R intrinsic R_{\text{intrinsic}} from being dominated by that of visitation counts.
This demonstrates that the discounted UCB mechanism is a crucial complement to intrinsic-reward-driven exploration.
Sample budget
miniF2F-test
Single-Pass Generation
4 × 6400 4\times 6400
58.4 % ± 0.5 % 58.4\%\pm 0.5\%
16 × 6400 16\times 6400
60.2 % 60.2\%
UCT
4 × 6400 4\times 6400
58.2 % ± 0.3 % 58.2\%\pm 0.3\%
(without R intrinsic R_{\text{intrinsic}} )
16 × 6400 16\times 6400
61.1 % 61.1\%
RMaxTS
4 × 6400 4\times 6400
58.6 % ± 0.3 % 58.6\%\pm 0.3\%
(DUCB → \rightarrow UCB1)
16 × 6400 16\times 6400
60.7 % 60.7\%
RMaxTS
4 × 6400 4\times 6400
58.4 % ± 0.3 % 58.4\%\pm 0.3\%
(without tactic state)
16 × 6400 16\times 6400
61.1 % 61.1\%
RMaxTS
4 × 6400 4\times 6400
59.6 % ± 0.6 % 59.6\%\pm 0.6\%
16 × 6400 16\times 6400
62.7 % 62.7\%
Figure 5: A modular ablation study examining the algorithmic design of RMaxTS. The experiments are conducted on the miniF2F-test dataset with DeepSeek-Prover-V1.5-RL using the CoT mode. The left panel presents the curves of Pass@K accuracy within 6400 generation samples. The results with a larger sample size are presented in the right panel.
## Guidance of Tactic State Information.
When expanding a tree node, we concatenate the intermediate tactic state information as a comment block to the incomplete code to guide the proof completion.
With the provided auxiliary information, the proof completion model can enhance its internal representation of the tactic state, offering intermediate guidance for long-horizon planning.
To demonstrate this advantage, we present experiments on RMaxTS that performs code completion directly from the raw incomplete code without accessing tactic state information, denoted by RMaxTS (without tactic state) in Figure 5 .
The results indicate that the performance gain from applying tree search becomes moderate in the absence of tactic state information, especially when tackling hard problems that require a large amount of samples.
This highlig

=== BODY (tail) ===
hts that the integration of compiler information is an essential component of the tree search algorithm, enhancing its overall effectiveness and sample efficiency.
## 5 Conclusion, Limitation, and Future Work
We present DeepSeek-Prover-V1.5, a language model with 7 billion parameters that outperforms all open-source models in formal theorem proving in Lean 4.
DeepSeek-Prover-V1.5 is initialized with DeepSeek-Prover-V1.5-Base, which extends the pre-training of DeepSeekMath-Base 7B using a specialized corpus for formal mathematical reasoning.
Supervised fine-tuning is conducted on a comprehensive Lean 4 code completion dataset, encompassing a wide range of formal theorems from various mathematical domains.
Subsequently, we employ GRPO to enhance whole-proof generation through online reinforcement learning.
Upon developing the DeepSeek-Prover-V1.5 model, we introduce RMaxTS, a variant of Monte-Carlo tree search, to improve problem-solving capabilities via large-scale search with extensive exploration.
These components form a comprehensive pipeline for training an LLM-based proof assistant, enabling DeepSeek-Prover-V1.5 to achieve significant improvements over DeepSeek-Prover-V1.
The framework of DeepSeek-Prover-V1.5 is designed to establish an AlphaZero-like pipeline for formal theorem proving.
The use of expert iteration and synthetic data mirrors the core trial-and-error loop of reinforcement learning, with the compiler oracle serving as the world model to provide environmental supervision.
Within the RL paradigm, the integrated tree search module has proven to be highly effective in advancing superhuman performance across various domains ( Silver et al., 2016 ; Fawzi et al., 2022 ; Lutz et al., 2023 ) .
In developing DeepSeek-Prover-V1.5, we focus on the exploration aspect of RL, introducing RMaxTS to diversify the generation of proof steps.
However, the exploitation aspect, specifically the problem of proof search, remains unexplored.
A promising future direction is training a critic model to assess incomplete proofs and prune search branches.
Such a partial-proof critic model would implicitly perform temporal credit assignment ( Sutton, 1984 ) , decomposing proof-level feedback into step-wise value differences ( Arjona-Medina et al., 2019 ) .
Developing critic models for assessing long planning paths and providing guidance rewards presents a crucial and challenging problem ( Ng and Russell, 2000 ; Sorg et al., 2010 ) that warrants further investigation.
Finally, recent work has progressed beyond proving individual theorems to addressing real-world theory proving within complex, multi-theorem Lean files ( Hu et al., 2024 ) . This shift is a natural extension of our whole-proof generation approach. Our observations indicate that the current model already possesses some understanding of file-level context. Moving forward, we will focus on enhancing this aspect to support cutting-edge Lean mathematical formalization developers with our language model advancements.