Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

## Abstract

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%).

## 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, ) and Isabelle (Paulson, ), which requires rigorous derivations satisfying formal specifications of the verification system.
Even advanced models like GPT-4 (OpenAI, ) 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, ; Jiang et al., ; Lample et al., ; Yang et al., ; Wu et al., ) and whole-proof generation (Jiang et al., ; Zhao et al., ; Wang et al., ). 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., ) 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., ), 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 (MCTS; Coulom, ) 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, ), 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: 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.
Refer to caption: x2.png

### 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., ) 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., ) 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, ) 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., ). 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, ), synthetic theorems from DeepSeek-Prover-V1 (Xin et al., ) and Lean Workbook (Ying et al., ), and validation sets from the miniF2F (Zheng et al., ) and ProofNet (Azerbayev et al., ) benchmarks. To augment the formal proof data, we employed an expert iteration process (Polu and Sutskever, ). 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., ) 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., ), which performs isolated chain-of-thought reasoning (Wei et al., ; Feng et al., ) 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., ) 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 (Read-Eval-Print Loop; Leanprover Community, ) with data extraction tools from the LeanDojo (Yang et al., ) 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., ). 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 (GRPO; Shao et al., ) as our RL algorithm, which has demonstrated superior effectiveness and efficiency compared to PPO (Schulman et al., ), 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., ) 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 ().
- •
ProofNet (Azerbayev et al., ) 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.

Figure: 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$.
Refer to caption: x3.png

#### 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 (), 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$ accuracy metric, which measures the model’s success in generating a correct proof within $K$ attempts. Each model is deployed on a single A100-40G GPU, utilizing the vLLM framework (Kwon et al., ) 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, ) and Aesop (Limperg and From, ) 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$ accuracy across all values of $K$. In contrast to findings in natural language mathematics, such as those reported in DeepSeekMath (Shao et al., ), 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\%$ on miniF2F and $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. (), 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: 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.
Refer to caption: x4.png

### 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 (MCTS; Coulom, ; Browne et al., ), 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, ).
The tree policy at a tree node $s$ is computed by selecting the action that maximizes the value from the set of valid operations:

$$ $\displaystyle TreePolicy(s)=\mathop{\arg\max}_{a\in Children(s)\cup\{\oslash\} }Q_{UCB}(s,a),$ (1) $$

where the action $a$ can be either moving to a child node, denoted by $a\in Children(s)$, or expanding the current node $s$, denoted by a special token $a=\oslash$.
This approach uses a technique called virtual node (Wang et al., ), which assigns each node an imaginary child to represent the selection of the current node $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_{UCB}(s,a)$ of performing action $a$ on node $s$ is composed by two components:

$$ $\displaystyle\forall a\in Children(s)\cup\{\oslash\},\quad Q_{UCB}(s,a)$ $\displaystyle=\underbrace{Q(s,a)}_{\text{Exploitation}}+\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \underbrace{UCB(s,a)}_{\text{ Exploration}},$ (2) $$

where $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. $UCB(s,a)$ denotes the exploration bonus computed by upper confidence bounds (UCB; Auer, ), which diminishes with the repeated execution of the state-action pair $(s,a)$. More specifically, $Q_{UCB}(s,a)$ stands for an optimistic estimation of $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., , ; Schrittwieser et al., ).

#### 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 $\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$-th iteration that ends with $s_{t}$ as the expanding node.
We update $Q_{UCB}(s,a)$ for all $(s,a)\in\tau$ by taking the most recent trajectory reward $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_{\text{extrinsic}}(\tau)=1$ for completed proofs and $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., ) in the literature of statistical reinforcement learning.
To promote exploration in sparse-reward sequential decision making, one classical paradigm is constructing intrinsic rewards (Schmidhuber, ) that encourage the agent to not only optimize extrinsic rewards but also acquire general information about the interactive environment (Bellemare et al., ; Houthooft et al., ; Pathak et al., ; Burda et al., ).
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, ), 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., ), in which the agent’s exploration is driven solely by intrinsic rewards, i.e., setting $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,

$$ $\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., ):

$$ $\displaystyle Q_{UCB1}(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) $\displaystyle W(s,a)$ $\displaystyle=\textstyle{\sum_{\tau\in\Gamma(s,a)}}\leavevmode\nobreak\ R(\tau),$ (5) $\displaystyle N(s,a)$ $\displaystyle=\left|\Gamma(s,a)\right|,$ (6) $$

where $\Gamma(s,a)=\{\tau\mid(s,a)\in\tau\}$ denotes the list of tree-policy trajectory $\tau$ containing $(s,a)$ as an intermediate selection step.
To facilitate discussions, we organize the list $\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 (DUCB; Garivier and Moulines, ), which uses a discount factor $\gamma\in(0,1)$ to smoothly drop those outdated feedback records:

$$ $\displaystyle Q_{DUCB}(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) $\displaystyle W_{\gamma}(s,a)$ $\displaystyle=\textstyle{\sum_{t=1}^{N(s,a)}}\leavevmode\nobreak\ \gamma^{N(s, a)-t}R(\tau_{t}),$ (8) $\displaystyle N_{\gamma}(s,a)$ $\displaystyle=\textstyle{\sum_{t=0}^{N(s,a)-1}}\leavevmode\nobreak\ \gamma^{t},$ (9) $$

where newly received feedback would be assigned a larger weight in the value estimation.
In practice, we set $\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. ().

- •
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(\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, ; Polu et al., ), Thor (Jiang et al., ), ReProver (Yang et al., ), Hypertree Proof Search (Lample et al., ), and InternLM2-StepProver (Wu et al., ).
- •
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., ), Subgoal-Prover Zhao et al. (), LEGO-Prover (Wang et al., ), Lyra (Zheng et al., ), and miniCTX (Hu et al., ).

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, ) 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., ), an in-context learning agent that leverages these large language models to propose tactic applications. Additionally, we examine Llemma (Azerbayev et al., ), 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, ; Polu et al., ) represents an initial effort to apply Transformers (Vaswani et al., ) 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., ), LLMStep (Welleck and Saha, ), and Lean-STaR (Lin et al., ). Hypertree Proof Search (Lample et al., ) explores the use of Monte Carlo tree search in formal theorem proving using Lean. Concurrent works, InternLM2-Math (Ying et al., ) and InternLM2-StepProver (Wu et al., ), also demonstrate outstanding performance.

#### Metric.

We compare the performance of DeepSeek-Prover-V1.5 with state-of-the-art models using the pass@$K$ accuracy metric, which evaluates the model’s ability to generate a correct proof within $K$ attempts.
We display the sample budget $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$ as the total number of proofs generated, with large values of $K$ factorized for the ease of comparison to tree search methods.
- •
For best-first-search methods, following the notation of Azerbayev et al. (), we present $K=N\times S\times T$ where $N$ denotes the number of best-first-search attempts, $S$ denotes the number of tactics generated for each expansion, and $T$ denotes the number of expansion iterations.
- •
For tree search methods, e.g., RMaxTS and HTPS (Lample et al., ), we present $K=N\times T$ where $N$ denotes the number of tree search attempts, and $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\times 3200$ tree searches to achieve 54.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).**
| Method | Sample budget | miniF2F-test |
| --- | --- | --- |
| Single-pass Whole-Proof Generation Methods |  |  |
| TheoremLlama [] | 128 | $33.6\%$ |
| DeepSeek-Prover-V1 [] | $128$ | $46.1\%\pm 0.5\%$ |
| $16\times 4096$ | $50.0\%$ |  |
| DeepSeek-Prover-V1.5-Base | 128 | $29.7\%\pm 0.5\%$ |
| 3200 | $39.2\%$ |  |
| 6400 | $42.2\%$ |  |
| DeepSeek-Prover-V1.5-SFT | 32 | $48.2\%\pm 0.6\%$ |
| 64 | $49.6\%\pm 0.7\%$ |  |
| $128$ | $50.4\%\pm 0.4\%$ |  |
| $3200$ | $53.3\%\pm 0.5\%$ |  |
| $4\times 6400$ | $55.8\%\pm 0.7\%$ |  |
| $16\times 6400$ | $57.4\%$ |  |
| DeepSeek-Prover-V1.5-RL | 32 | $50.0\%\pm 0.5\%$ |
| 64 | $50.7\%\pm 0.4\%$ |  |
| $128$ | $51.6\%\pm 0.5\%$ |  |
| $3200$ | $54.9\%\pm 0.7\%$ |  |
| $4\times 6400$ | $58.4\%\pm 0.6\%$ |  |
| $16\times 6400$ | $\mathbf{60.2\%}$ |  |
| Tree Search Methods |  |  |
| COPRA (Code Llama) [] | $1\times 500$ | $5.7\%$ |
| COPRA (GPT-3.5) [] | $1\times 60$ | $9.0\%$ |
| COPRA (GPT-4) [] | $1\times 60$ | $26.6\%$ |
| Llemma-7B [] | $1\times 32\times 100$ | $26.2\%$ |
| Llemma-34B [] | $1\times 32\times 100$ | $25.8\%$ |
| ReProver [] | - | $26.5\%$ |
| LLMStep [] | $1\times 32\times 100$ | $27.9\%$ |
| GPT-f [] | $64\times 8\times 512$ | $36.6\%$ |
| Hypertree Proof Search [] | $64\times 5000$ | $41.0\%$ |
| Lean-STaR [] | $64\times 1\times 50$ | $46.3\%$ |
| InternLM2-Math-7B [] | $1\times 32\times 100$ | $30.3\%$ |
| InternLM2-Math-Plus-7B [] | $1\times 32\times 100$ | $43.4\%$ |
| InternLM2-StepProver [] | $1\times 32\times 100$ | $48.8\%$ |
| $64\times 32\times 100$ | $54.5\%$ |  |
| DeepSeek-Prover-V1.5-SFT + RMaxTS | $1\times 3200$ | $53.5\%\pm 0.4\%$ |
| $4\times 6400$ | $56.3\%\pm 0.3\%$ |  |
| $16\times 6400$ | $59.0\%$ |  |
| $32\times 6400^{\dagger}$ | $60.2\%$ |  |
| DeepSeek-Prover-V1.5-RL + RMaxTS | $1\times 3200$ | $55.0\%\pm 0.7\%$ |
| $4\times 6400$ | $59.6\%\pm 0.6\%$ |  |
| $16\times 6400$ | $\mathbf{62.7\%}$ |  |
| $32\times 6400^{\dagger}$ | $\mathbf{63.5\%}$ |  |

#### 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.

**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.**
| Method | Sample budget | ProofNet |  |  |
| --- | --- | --- | --- | --- |
| valid^‡ | test | all |  |  |
| Single-pass Whole-Proof Generation Methods |  |  |  |  |
| DeepSeek-Prover-V1.5-Base | $128$ | $6.6\%\pm 0.9\%$ | $9.7\%\pm 0.7\%$ | $7.5\%\pm 0.7\%$ |
| $3200$ | $10.8\%$ | $15.6\%$ | $13.2\%$ |  |
| DeepSeek-Prover-V1.5-SFT | $128$ | $19.9\%\pm 0.4\%$ | $15.9\%\pm 0.6\%$ | $17.9\%\pm 0.3\%$ |
| $3200$ | $20.7\%\pm 0.7\%$ | $21.0\%\pm 0.9\%$ | $20.9\%\pm 0.6\%$ |  |
| $4\times 6400$ | $22.2\%$ | $23.7\%$ | $22.9\%$ |  |
| DeepSeek-Prover-V1.5-RL | $128$ | $20.1\%\pm 0.5\%$ | $18.2\%\pm 0.5\%$ | $19.1\%\pm 0.4\%$ |
| $3200$ | $21.4\%\pm 0.3\%$ | $22.0\%\pm 0.5\%$ | $21.7\%\pm 0.4\%$ |  |
| $4\times 6400$ | $21.6\%$ | $23.7\%$ | $22.6\%$ |  |
| Tree Search Methods |  |  |  |  |
| ReProver [] | - | - | - | $13.8\%$ |
| InternLM2-StepProver [] | $1\times 32\times 100$ | - | - | $18.1\%$ |
| DeepSeek-Prover-V1.5-SFT + RMaxTS | $1\times 3200$ | $22.2\%\pm 0.7\%$ | $21.6\%\pm 0.2\%$ | $21.9\%\pm 0.4\%$ |
| $4\times 6400$ | $23.8\%$ | 25.8% | $24.8\%$ |  |
| DeepSeek-Prover-V1.5-RL + RMaxTS | $1\times 3200$ | $22.0\%\pm 0.3\%$ | $21.5\%\pm 0.8\%$ | $21.8\%\pm 0.4\%$ |
| $4\times 6400$ | $25.4\%$ | 25.3% | $25.3\%$ |  |

### 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\%$ on miniF2F-test.
This performance shows a notable $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\%$ on miniF2F-test. In Appendix B, we present example problems that illustrate the different advantages of the two generation modes.

**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.**
|  | Prompt mode | Sample budget | DeepSeek-Prover-V1.5 |  |
| --- | --- | --- | --- | --- |
|  | SFT | RL |  |  |
|  | non-CoT | $4\times 6400$ | $54.7\%\pm 0.4\%$ | $56.5\%\pm 0.5\%$ |
|  | $16\times 6400$ | $56.1\%$ | $57.4\%$ |  |
| Single-Pass | CoT | $4\times 6400$ | $55.8\%\pm 0.7\%$ | $58.4\%\pm 0.5\%$ |
| Generation | $16\times 6400$ | $57.4\%$ | $60.2\%$ |  |
| non-CoT & CoT | $(2+2)\times 6400$ | $56.1\%\pm 0.8\%$ | $58.3\%\pm 0.6\%$ |  |
|  | $(8+8)\times 6400$ | $58.2\%$ | $60.7\%$ |  |
|  | $(16+16)\times 6400$ | $58.6\%$ | $61.1\%$ |  |
| RMaxTS | non-CoT | $4\times 6400$ | $55.7\%\pm 0.6\%$ | $58.4\%\pm 0.6\%$ |
| $16\times 6400$ | $57.8\%$ | $59.4\%$ |  |  |
| CoT | $4\times 6400$ | $56.3\%\pm 0.3\%$ | $59.6\%\pm 0.6\%$ |  |
| $16\times 6400$ | $59.0\%$ | $62.7\%$ |  |  |
| non-CoT & CoT | $(2+2)\times 6400$ | $56.1\%\pm 0.8\%$ | $60.0\%\pm 0.8\%$ |  |
| $(8+8)\times 6400$ | $59.0\%$ | $63.1\%$ |  |  |
| $(16+16)\times 6400$ | $60.2\%$ | 63.5% |  |  |

### 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, ) 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_{\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_{\text{intrinsic}}$).
That is because UCB1 is designed to guarantee asymptotic performance through exhausted exploration (Auer et al., ) 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_{\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.

Figure: 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.
Refer to caption: x5.png

#### 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 highlights 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., ; Fawzi et al., ; Lutz et al., ).
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, ), decomposing proof-level feedback into step-wise value differences (Arjona-Medina et al., ).
Developing critic models for assessing long planning paths and providing guidance rewards presents a crucial and challenging problem (Ng and Russell, ; Sorg et al., ) 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., ). 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.

## Appendix A Illustrative Examples of Non-CoT and CoT Prompting for Proof Completion

In this section, we present examples of non-CoT and CoT prompting and the generated proofs for $\mathtt{aime_1983_p9}$, a problem from the miniF2F benchmark (Zheng et al., ). For clarity, inline LaTeX expressions are utilized. Firstly, here is an example of whole-proof generation in non-CoT prompting mode:

Input:

Output:

Next, here is an example of whole-proof generation in CoT prompting mode. This proof was found using a Monte-Carlo tree search with a truncate-and-resume mechanism (see Section 3 for details). The model receives a prompt including a proof code in progress, ending with a comment block containing the intermediate tactic state from the Lean 4 prover. The subsequent code is generated with guidance from this annotated code prefix.

Input:

Output:

In this case, the proof completion model first extracts the goal expression from the tactic state, i.e., the inequality $12(x\sin x)\leqslant 9(x^{2}\sin^{2}x)+4$ at the last line of the comment block, and then arranges it into the form $9x^{2}\sin^{2}x-12x\sin x+4\geqslant 0$ as part of the chain-of-thought process. Finally, the left-hand side is rewritten as a square term to establish non-negativity, closing the proof.

## Appendix B Example Solutions to MiniF2F-test Problems

To illustrate the different advantages and complementary of non-CoT mode and CoT mode of prompting, we provide examples where non-CoT mode succeeds while CoT mode fails, and vice versa.

### B.1 Problems that non-CoT outperforms CoT

### B.2 Problems that CoT outperforms non-CoT

## Peer Reviews

confidence: 3
contribution: 2
initial_rating: 5
presentation: 2
questions: Some additional suggestions/questions

-I'm a little skeptical GRPO would outperform PPO on this task since it involves actual multi-step decision making and thus the value function should provide significant benefit, at least if trained as a proper multi-step MDP. Perhaps it would be worth testing both versions?

-Why generate an entire proof and then truncate to the first error? Why not generate one tactic at a time, as is standard in multi-step RL?

-Am I correct that given an equivalent sample budget the difference between the otherwise equivalent MCTS and 1-shot generation methods is simply the way candidate solutions are generated (starting from a leaf in the search tree versus fully resampled)? Does the reduced number of new tokens generated (since some are derived from the existing leaf node) result in meaningful compute savings for the MCTS algorithm?

-Figure 4 needs to define what the shaded regions are, especially since the regions are heavily overlapping, leading me to question the statistical significance of the benefits of RMaxTS over the ablations.

-In tables 1 and 2, why do some accuracy numbers have +- intervals (standard deviation? I don't see these intervals defined in the caption or introductory text) and others don't?
soundness: 3
strengths: This paper is fairly well written and clear. The problem being addressed (automatic theorem proving) is important and well motivated. The experimental evaluation is reasonably conclusive. Figures 1 and 2 illustrate the method well.
summary: This paper presents a method for improving LLM performance on theorem proving tasks, using RL on feedback from a proof assistant tool Lean to finetune the model, in combination with a Monte-Carlo tree search to iterate and search the space of possible proofs.
weaknesses: First off, I will say this paper is a little outside my area of expertise, which is in traditional deep RL rather than LLM finetuning, and I'm not familiar with theorem proving as a problem domain, so take the following with that qualifier.

That said, my main concern on this paper is that it doesn't do a great job of justifying the composition of multiple standard methods as non-trivial scientifically. Finetuning LLMs using RL with automated domain-specific feedback isn't a new idea, nor is MCTS on top of RL agents generating action sequences (including for proof/program synthesis- "Program Synthesis Through Reinforcement Learning Guided Tree Search" is an earlier example, but the idea has been explored a few times in different ways I believe). There are some technical details involved in applying these ideas using an LLM (such as how to get individual tactics as atomic actions from the model), but from my perspective these don't seem like significant contributions that will be applicable outside this paper or closely related work.

All of that might be acceptable if the result was a major breakthrough in an important problem domain, but the results as presented seem incremental, honestly- compared to the supervised fine tuning baseline, the reported improvement in accuracy is around 1-3% against a baseline of ~15% or ~50% depending on the benchmark. This doesn't seem like a major improvement in the domain of theorem proving that would motivate a relatively straightforward combination of existing algorithms.

All that said, perhaps there's something I'm not seeing here, or context I lack as an outsider to the field this work comes from, so I'm open to persuasion on the above. However, as is I am inclined to recommend rejection since I don't see a significant novel contribution in this work.

---

confidence: 3
contribution: 2
initial_rating: 5
presentation: 2
questions: Additionally to the questions provided above, in the MCTS expansion phase, was the rollout a single whole-proof generation, or were there many? If the answer is the latter, how many were used? Additionally, did the Authors consider bootstrapping in the AlphaZero style?
soundness: 2
strengths: * The paper combines a proof-generating model with (a version of an) MCTS algorithm, unifying the proof-step and whole-proof generation approaches.
* The approach applies several MCTS innovations and uses the Lean prover as a verifier. 
* The paper claims that DS-Prover-V1.5-RL performs the best in single-pass and tree search categories.
summary: The paper presents a class of models named DS-Prover-V1.5 that combines the proof-step and whole-proof generation paradigms. The models come with two versions: (a) supervised fine-tuned (DS-Prover-V1.5-SFT), and (b) incorporating reinforcement learning (DS-Prover-V1.5-RL). In the SFT case, the data is augmented in two ways. First, the intermediate tactic state information extracted from Lean proof assistant (position of each tactic and the tactic states before and after its application) is added, and a corresponding prediction task is formulated. Second, the proof dataset from (Xin et al., 2024) is extended by providing a natural language solution at the beginning of the proof block and by inserting comments for Lean tactics with the help of DeepSeek-Coder V2 236B (Zhu et al., 2024). The paper considers the chain-of-thought (CoT) and non-CoT versions for proof completition. In the RL case, the model is trained on verification feedback from the Lean 4 prover using the GRPO algorithm (Shao et al., 2024), with a reward structure assigning 1 in the case of a proof verified as correct and 0 otherwise. A subset of theorem statements from the supervised fine-tuning dataset is used as training prompts. 

The paper combines both models (SFT and RL versions) with the MCTS planning algorithm. The paper follows previous work on adding the following innovations to the classical MCTS: (a) in the selection phase, a so-called virtual node option (Wang et al., 2023) which allows expanding a non-leaf node, (b) in the expansion phase, a whole-proof consisting of path of nodes, truncated at the first verification error (if any) from the Lean prover, is added to the tree during each iteration, (c) in the backpropagation stage, an RMax exploration mechanism is added (Brafman & Tennenholtz, 2002), with extrinsic and intrinsic (Jin et al., 2020) rewards, and a discounted bonus for upper confidence bound (Garivier & Moulines, 2011).

The setup is tested on two datasets: miniF2F and ProofNet. The paper claims that the DS-Prover-V1.5-RL version outperforms baselines in the single-pass and tree search categories. The following ablation studies are provided: (a) CoT vs. non-CoT versions, (b) single-pass vs. MCTS, (c) discounted vs. non-discounted UCB, and (d) presence vs. absence of tactic state information.
weaknesses: * The paper claims `The model is named DS-Prover-V1.5, as it builds upon the prior work of DeepSeek-Prover-V1(Xin et al., 2024).`, but does not provide the description of DeepSeek-Prover-V1. In particular, no details on the underlying language model were provided. 
* The paper provides no pseudo-code or loss function formulas, making understanding the approach's details difficult. 
* GRPO is not described (even in the Appendix).
* Experiments:
	* For some categories, the baselines are other versions of the same model.
	* Tables 1-4 do not include confidence bounds for the best-performing methods.
	* Some important information is missing:
		* Not all model details are disclosed for use in the MCTS algorithm.
		* No comparison is provided between the number of parameters or FLOPS used by the evaluated models.
		* No wall clock time is given.
	* The results of Tables 1-4 are not discussed in great detail other than extracting numbers from the tables. What are the key reasons/hypotheses for the performance differences? What are the qualitative and quantitative findings with respect to the difficulty of samples from the datasets? Are there any features that stand out or can be used to classify theorems?
	* The potential data leaks are not discussed.
	* No number of seeds is reported.
	* What are the $\mu$'s and $\sigma$'s (present in tables and figures and defined in the caption of Figure 3) computed over?
	* The confidence intervals are asymptotic and one-$\sigma$ (as defined in the caption to Figure 3), corresponding to $68\%$ (assuming a standard normal distribution), a rather narrow confidence level.
	* The results in Figure 4 suggest that many differences are not statistically significant.

Edit 29 Nov 24: I increased the rating 5->6.

---

confidence: 3
contribution: 3
initial_rating: 8
presentation: 3
questions: 1. During the training, is the context-length enough for all prompts? Do you have ablation studies on how context length affect the final performance?
2. Have you tried sliding window instead of discounted weight to handle non-stationarity? Sliding window is simpler and more commonly used in the bandit community.
soundness: 3
strengths: This paper studies theorem proving using LLM, which is an important direction towards artificial general intelligence. The paper is well-written. The experiment results are quite promising as it establishes new state-of-the-art results. The proposed tricks for resolving hard exploration problem is also novel (RMaxTS + discounted UCB) and insightful.
summary: This paper studies using LLM to perform theorem proving in Lean. They propose a framework that integrates supervised fine-tuning, reinforcement learning, and Monte-Carlo tree search for efficient exploration and exploitation of tactic space. Experiment results show that the propose method achieves new state-of-the-art results on both miniF2F and ProofNet benchmarks.
weaknesses: Lean is not very well-known to the community in my opinion, and the proposed method is highly tailored for Lean (for example, tactic-level tree abstraction). Some general introduction about Lean would be very helpful in understanding the design of the algorithm.

---

confidence: 3
contribution: 3
initial_rating: 6
presentation: 3
questions: 1.	Could you clarify the standard deviation formulas used in tables? Based on binomial distribution $\sigma = 1/\sqrt{npq}$, results seem to approximate $\sigma \approx 3%$ when  p = 1/2  and  n = 250 .
2.	The gains achieved with RL over Supervised Fine-Tuning (SFT) in Tables 1 and 2 are modest. What factors contribute to these limited improvements?
3.	Similar to the RL results, improvements with RMaxTS appear modest in Tables 1 and 2. Could you provide more context?
4.	What is the exact sample budget (e.g.,  16 \times 4096 )? Is it comparable between RMaxTS and other baselines? Given potential hardware utilization differences, are wall-time comparisons available?
      - It would also be interesting to see token-budget-aligned results.
5.	The improvements in Figure 3 also appear modest. Any insights?
soundness: 3
strengths: 1. The paper tackles a critical problem, merging theorem-proving and reinforcement learning with proof assistant feedback.
2. Strong empirical results demonstrate improvements in state-of-the-art theorem proving on established benchmarks.
summary: The paper introduces DS-Prover-V1.5, a model integrating proof assistant feedback to enhance theorem-proving capabilities. The authors propose using Lean’s proof assistant in reinforcement learning (RL) and Monte-Carlo Tree Search (MCTS) settings, achieving competitive results on the miniF2F and ProofNet benchmarks. Two main innovations stand out: an intrinsic reward-based exploration strategy (RMaxTS) in MCTS to encourage diverse proof paths and a truncate-and-resume mechanism to handle proof verification errors. These advances lead to state-of-the-art results, highlighting the role of proof feedback in RL training.
weaknesses: 1. I have various doubts listed in the question section.
2. I'd love to see a short technical details section in the main body, model sizes, and the number of tokens used in training. Btw. what is the number of tokens in the RL training?
3. I'd love to see more ablations (e.g., other models). I realize that such experiments are costly, still, perhaps feasible with smaller models, to study in more detail the influence of design choices.

Meta-review: This paper uses proof assistant feedback to improve the capabilities of LLMs to construct formal proofs in Lean. It casts the problem in the RL paradigm using Lean verification outcomes as the reward signal. The generation of diverse proofs is encouraged by employing a variant of MCTS designed to increase exploration of Lean tactics. The experiments show that these technique achieve competitive results on the miniF2F and ProofNet benchmarks.

Decision: Accept (Poster)