DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
Authors: Huajian Xin
Z.Z. Ren
Junxiao Song
Zhihong Shao
Wanjia Zhao
Haocheng Wang
Bo Liu
Liyue Zhang
Xuan Lu
Qiushi Du
Wenjun Gao
Haowei Zhang
Qihao Zhu
Dejian Yang
Zhibin Gou
Z.F. Wu
Fuli Luo
Chong Ruan
Venue: ICLR 2025 Poster (2025)
Keywords: Neural Theorem Proving
Formal Math
Large Language Model
Reinforcement Learning
Monte-Carlo Tree Search
Primary area: applications to computer vision, audio, language, and other modalities

Abstract: Lean is an advanced proof assistant designed to facilitate formal theorem proving by providing a variety of interactive feedback. In this paper, we explore methodologies to leverage proof assistant feedback to augment the capabilities of large language models in constructing formal proofs. First, we deploy online reinforcement learning using Lean verification outcomes as the reward signal to improve the proof completion policy. This straightforward approach shows great promise in enhancing the model's alignment with the formal verification system. In addition, we propose RMaxTS, a variant of Monte-Carlo tree search that employs an intrinsic-reward-driven exploration strategy to generate diverse proof paths. The tree structure is organized to represent the transitions of intermediate tactic states, extracted from the compilation messages given by Lean's tactic mode. The intrinsic reward is constructed to incentivize the discovery of novel tactic states, which helps to to mitigate the sparse-reward problem inherent in proof search. These techniques lead to a more efficient planning scheme for formal proof generation, achieving new state-of-the-art results on both miniF2F and ProofNet benchmarks.

Published as a conference paper at ICLR 2025
DEEPSEEK-PROVER-VE HARNESSING PROOF As- SISTANT 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
Haowei Zhang
Qihao Zhu
Dejian Yang
Zhibin Gou
Z.F. Wu
Fuli Luo
Chong Ruan
DeepSeek-AI Thee University of Edinburgh
ABSTRACT
Lean is an advanced proof assistant designed to facilitate formal theorem proving by providing a variety of interactive feedback. this paper, we explore method- ologies to leverage proof assistant feedback to augment the capabilities of large language models in constructing formal proofs. First, we deploy online reinforce- ment learning using Lean verification outcomes the reward signal to improve the proof completion policy. This straightforward approach shows great promise in enhancing the model's is alignment with the formal verification system. In addi- tion, we propose RMaxTS, a variant of Monte-Card tree search that employs an mewsssic-eewarddiiieeee exploration strategy generate diverse proof paths. The tree structure is organized to represent the transitions of intermediate tactic states, extracted from the compilation messages given by Lean's 's tactic mode. The intrin- sic reward is constructed to incentivize the discovery of novel tactic states, which helps to to mitigate the sparse-reward problem inherent in proof search. These techniques lead to a more efficient planning scheme for formal proof generation, achieving new state-of- tfrtt-rrtttttt results on both miniF2F and ProofNet benchmarks.
INTRODUCTION
Recent advancements in large language models have significantly influenced mathematical reason- ing 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. ing Lean (Moura & Ullrich 2021) and Isabelle (Paulson 1994]. which requires rigorous derivations satisfying formal specifications of the verification system. Even advanced models like GPT-4 (Ope- nAl (023)) struggle with complex formal proofs, underscoring the intricate nature of both the coding and the mathematics involved. Language models formal theorem proving typically employ two strategies: proof-step generation (Jiang et al.] 2022a Lample et al. 2022 Yang et al. 2023 Wu
jet al. 2024) and whole-proof generation (Zhao et al. 2023 Wang et al. 2023a). The proof-step generation approach is motivated by the interactive nature of Lean't s tactic mode, in which the com- piler provides the access to the tactic state, i.e., structured representation summarizing the current status of the proof, including all the relevant information such as the local context of hypotheses and pending goals. Given the intermediate tactic state, the proof-step generation approach predicts each subsequent tactic and verifies it using the formal verifier to obtain updated information about the current tactic state. This interactive process often employs tree search techniques to compose valid proofs through several iterations of tactic generation (Polu & Sutskever 2020). In contrast, the whole-proof generation approach treats the construction of formal proots as general code com- pletion task. This branch of methods aims to generate the entire proof code based on the theorem statement and perform verification only at the end of the generation process. The simplicity of the whole- generation paradigm has been proven to offer high scalability (Xin al., (024) from the perspectives of both model training and inference deployment. In addition, the whole- proof generation model trained to perform long-term planning for theorem proving, facilitating the inte- gration and utilization of the model's 'ss capabilities in natural language mathematical reasoning (Jiang et al. 2022b).
*Core contributors

---

Published as a conference paper at ICLR 2025
Model Training
seart toop
cenn tichperators Rest Not Topsleer Pat
Pre-training
Cea the it 722-o
(43)- costt, 2
1811 Iofouet 1-1
ext
Proggt
Supervised Fine-ture tunin
scates
Whote-proot
Completion
Reinforcener Learning
roliout
falled to arnthasios
Me setee
Thas gowe to
coeatracter
LAKE prinr
Model Inference
vi.9
Late
baw 12
al
Single-pase Sampling
This
soles.
tedtt
meaute
We des that ore inted rests
Mante-Car La Tree Search
Iolia
Figure 1: Overall Framework of DeepSeck-Prover-vii During supervised fine-tuning, the model receives an incomplete theorem proof ending with 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 used binary rewards to further optimize the model and enhance its alignment with the formal specifications of the verification system. For model inference, we decom- pose the generated proof into series of tree nodes, appending intermediate tactic states extracted from the Lean prover, thereby establishing an interactive proof search paradigm.
In this paper, we present a unified approach that combines the strengths of both proof-step and whole-proof generation paradigms. We begin by training whole-proof generation model, incorpo- rating several auxiliary tasks to enhance its capabilities in mathematical reasoning and long- long-horizon planning, meanwhile empowering it to recognize information from Lean's 's proof assistant feedback. The model is named DeepSeek-Prover-VV V1.5, as it builds upon the prior work of DeepSeek-Provee VI et al., 2024). We then employ truncate-and-resume mechanism to decompose the whole- proof generation into a tactic-level proof search scheme. Figure presents illustration of our approach. The process begins with standard whole-proof generation, where the language model completes the proof code following the theorem statement prefix. The Lean assistant then verifies this code. If an error is detected, the code is truncated at the first error message, and any subse- quent code is discarded. The successfully generated proof code is then used generation of next proof segment. The latest tactic state from the Lean prover is appended at the end of the prompt proofs. Notably, our method is not restricted to resuming from the last successfully applied tactic. We formalize the (MCTS; Coulom 2006) 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. curios- ity (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 interac- tive theorem proving. which can effectively utilize the proof assistant feedback and generate diverse solution candidates. In experiments, proach over baseline models, achieving new state-of of-the-art results on the test set of the high school level F2ni benchmark (63.5% and the undergraduate level ProofNet benchmark (25.3%).
prompt for the
comment block provide intermediate guidance for the construction of long
mechanism within the framework of Monte-Carde tree search
demonstrate substantial improvement of proposed ap-
2

---

Published as a conference paper at ICLR 2025
2 RELATED WORK
Reinforcement Learning for Theorem Proving. Numerous prior research efforts have explored modeling the interaction interface with the proof assistants as a Markov Decision Process (MDP), leveraging various reinforcement learning techniques, such using policy gradient (Zombori al. 2021 Crouse et al. 2021) and deep Q-learning (Fawzi et al., 2019), and involving a wide range of formal verification systems, including E (McKeown & Sutcliffe 2023), Coq (Kusumoto al.) 2018), and HOL4 (Gauthier, 2020). A common choice for the reward signal is a binary indicator denoting whether the proof has been completed. Fawzi et al. (2019) designed temporal-differene reward assignment according to problem structure of solving polynomial incquality. Aygün et al. (2022) generalized the idea of hindsight experience replay (Andrychowiez et al. (2017) from goal- reaching control to formal theorem proving, which enriches the reward supervision.
Tree Search for Theorem Proving. Integrating supervised models with search algorithms is a classical paradigm for automated theorem proving (Rawson & Reger 2019; [202] Zhang et al., 2024). For proof-step generation models, the most widely applied search strategy is best-first search (Yang et al., 2023), in which search branches are prioritized based on the cumulative log- liglliiels of the generated tactics. [ample et al. (202) developed specialized Monte-Care tree search algo- rithm tailored for the Lean theorem prover, which subgoal branches are represented as hyperedges.
The model training and tree search procedures are integrated similarly to the algorithmic framework of AlphaZero (Silver et al.] 2018). Beyond the tactic-level tree abstraction, Wang et al. (2023b) investigated the effectiveness of using a proof-level value function in proof tree search, demonstrat- ing that incorporating the entire proof as context is more effective than using a tactic-level state representation.
3 LEARNING TO UTILIZE PROOF ASSISTANT FEEDBACK
3.1 SUPERVISED FINE-TUNING
In this section, we explore the methodology and processes involved in the supervised fine-tuning (SFT) of DeepSeek-Prowe Pee---rrvvvr-.ee Specifically, we incorporate intermediate tactic state information as auxiliary prediction task to support the truncate-and tree search. addition, we augment the proof dataset from DeepSeck-Provee Prover- (Xin et al. 2024) by adding detailed explanatory comments. This enhancement aims to improve the alignment be- tween natural language descriptions and Lean 4 code, thereby facilitating better formal mathemati- cal reasoning. We refer to the resulting model as PrepSeek-Prover VL.5-SFT, which is 7B dense model trained on around 20B tokens. Details of data processing are described in Appendix A.2
mechanism used in Carlo
Prompt Augmentation with Tactic State Information. To implement the truncate-and-resume mechanism for Monte-Carlo Tree Search, needed to extract tactic information from the code generated by the model. We enhanced the Lean REPL BRead-Eval-Pare nity| 2023) with data extraction tools from the LeanDojo (Yang et al., (023) 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 4.2). For each tactic in a generated valid formal proof, we insert the tactic state returned by the veritier as a comment "/- tactic state: -f" During training, we include all tokens following the leading prompt "/- tactic state: as responses to calculate the supervised fine-tuning loss, while the tokens before this comment is used prompts and do not contribute to the training loss calculation, i.c., we construct an auxiliary task for the prover model to predict the current tactic state.
Loop: Leog:roeen Commu-
Thought-aaummntted Proof Generation. Similar to Lean-STaR (Lin al. 2024), which per- forms isolated -fthouhtt reasoning (Wei et al.] 2022, Feng et al.) 2023) before generating each proof step, we integrate this reasoning procedure directly as comments within the proof code. We use the DeepSeek-Codee V2 236B (Zhu et al. 2024) to enhance existing data in DeepSeek- Prover-W. 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 corre- sponding Lean tactics. Training the model with this data format enforces it to propose complete mathematical reasoning the beginning of the proof block and detailed step planning before each
3

---

Published as a conference paper at ICLR 2025
tactic. This approach successfully develops new behaviors, employing delicate mathematical think- ing 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 G
Discussion. The primary purpose of implementing these data processing procedures during the SFT phase is to optimize the model's performance for downstream inference-time strategy. When applying tree search for proof generation, we leverage the model's ability to utilize proof assistant feedback while performing chain-of-thougle reasoning. For an incomplete proof, we first append a comment block containing the ground truth tactic state extracted from the Lean assistant, and then the model would perform thain-offthougee based on the full context information (see Figure This procedure emulates the strategy employed by human experts when interacting with formal proof assistant, combining both real-time feedback from the assistant and logical reasoning to iteratively refine and extend the proof. The improvements on inference-timg performance are continuously fed back into SFT through expert iteration (Polu & Sutskever, 2020). The final SFT dataset is curated from challenging problems solved through tree search, aiming fundamentally enhance the model's capabilities.
3.2 REINFORCEMENT LEARNING FROM PROOF ASSISTANT FEEDBACK
Reinforcement learning (RL) has been proven effective in enhancing the mathematical reasoning capabilities of supervised finc-tuned language models (Shao et al. 2024p. To further advance SeepSeek-Prover -wtte--rrvveeee--Se-E-- V1.5-SFT, we incorporate a reinforcement learning phase, resulting in the model DeepSeck-Prover- V1.5-RL. This phase leverages RL to enhance performance based verification feedback from the Lean 4 prover. The specifics of this RL process are detailed below. Detailed training setting and hyper-parameters refer Appendix A.3
Reinforcement Learning Algorithm. We employ Group Relative Policy Optimization (GRPO; Shao et al. 2024) 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 group of candidate proofs for each theorem prompt and optimizes the model based on the relative rewards of the outputs within the group. To ensure that both correct and incorrect proofs are included in the rollout candidates, select a subset of theorem statements with appropriate difficulty from the supervised fine-tuning dataset as training prompts. These selected prompts are chosen based the rule that SeepSeek-Prover-Ve V1.5-SFF achieves a moderate success rate in generating correct proofs over multiple attempts. After filtering, we retain approximately 4.5k unique theorem statements. Each theorem is prefixed with both CoT and non-Co'T guiding prompts to enhance the model's proof generation capabilities in both modes. The reward function is naturally given by the formal verification system, iee. each generated proof receives reward of 1 if verified as correct, and 0 otherwise. The complete RL phase processes approximately 1.5B tokens.
Discussion. In Lean's 's tactic mode, proofs are constructed through a sequence of tactics that trans- form the proof state. This sequential nature introduces the risk of compounding errors (Ross al. 2011]. where single misinterpretation can lead to significant deviations from a valid proof path. More specifically, the whole-proof generation model may have incorrect believes on intermediate tactic states when generating long proofs. Online reinforcement learning has been proven to be an effective method for mitigating compounding errors in the extrapolation setting of model inference (Fujimoto et al. 2019). By continuously interacting with the environment and receiving feedback in real-time, the model is able to refine its the supervised dataset.
policy and reduce the bias inducted from
4 EXPLORATION- MONTE-CARLO TREE SEARCH
4.1 TACTIC-LEVEL TREE ABSTRACTION
To implement the tree search method in the whole-proo pooole-roooffee generation setting, we introduce a proof tree abstraction to define the tailored state and action space, leveraging truncate-an nuncate-and-resmme and-resume mecha- nism. Roughly following the paradigm of Yao et al. (2023), we begin by decomposing an incomplete proof into sequence of tree nodes that correspond to individual proof steps, and then we utilize the
4

---

Published as a conference paper at ICLR 2025
Warall Srgort A5500
ast_a2tton madleartoatss
Monte-Carlo Tree Search
Riglperstors Real Topoloogy
Conp
Srew 200 Pantape
El
(P-1) (91) coffineet 7.7
show the
patonontal are -3/2 and 091), tutuneet E-157 U.
Esetumax, turnnet sig.eeaiiggeiiic...... SACTEE
Sctuear_actll, Pinect Aoors, PArKe WAA.AA (ear)
Tactic State Extract Lon
Expansion
pase
Pantyps
(b)
Mhole-proof Completion
ietre
Thee a a 1) a is 4 x -i A] d
This ganda aa ba casda sotre,
vata 92
Jell
(e)
Liaartth
Error froe syetassies Esneandrger
Light
(c)
No check 2012
noregn chaend
Tokds]
the cun riats:
DISCARDED
Figure 2: Truncate-and-Resunl Mechanism in the Expansion Step MCTS. (a) After selecting node, we trace its corresponding incomplete proof code prefix, which includes the file header, initial statement, and successfully applied tacties 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 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 node in the search tree, extending chain of descendants beneath the selected node. (c) Once the tree updates are complete, the next iteration of expansion begins by selecting an alternative candidate node, which is limited to leaf nodes. This process repeats until a correct proof is found or the sample budget is exhausted.
parse the successful portion into tacties. (d) Each tactic is added as
partial content stored in these tree nodes to continue the proof generation process. Figure 2 iillstrrtes the process of constructing 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 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 the earliest verification error, ensuring that all subsequent tactic codes can be success- fully 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 single tree edge that represents tactic state transition. Through this abstraction, each tactic code converted into series of tree nodes, forming a path from the root to specific node.
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 these equivalent tactic codes at each node. When the tree search agent expands node, it randomly selects one tactic to use 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 comment block. The fine-tuned model (see Section 3.II) has been trained to recognize and utilize this format, using the incomplete code augmented with tactic state comments guide subsequent proof generation.
Resume:
5

---

Published as a conference paper at ICLR 2025
4.2 INTERACTIVE THEOREM PROVING VIA MONTE- CARLO TREE SEARCH
Our proof search tree is developed using the standard Monte-Cario Tree Search (MCTS) paradigm (MCTS:
2006, Browne et al., 2012), which iteratively applies four steps: Selection, Expan- sion, Simulation, and Backpropagation. We integrate the Simulation step into Expansion because our wchole-proof generation model inherently performs a rollout from the expanded node. The de- tailed design of the algorithm workflow is follows.
Selection. The selection step, a.k.a. the policy, starts from the root node and traverses down- ward to identify a promising node for expansion. The objective of this algorithmic step is to trade off between exploration and exploitation (Kocsis & Szepesvári 2006). The tree policy tree node s is computed by selecting the action that maximizes the value from the set of valid operations:
arg max TreePolicy()) (=Children(+)U(((
QucB(s,a),
(I)
where the action be either moving child node, denoted by Children(s), or expanding the current node 8, denoted by a special token a = Ø. This approach uses a technique called virtual node (Wang al. 2023b), which assigns each node 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 generative model whose output scope cannot be determined by fixed number of trails. The value estimation QuCB(s, (s, a) of performing action on node is composed by two components:
Va E Children 8) U (0). QucB(s,a)- = Q(({,a)))(((a)) + UCB(s,a).
(2)
Exploitation
Exploration
where ((x, a) denotes 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, 2002), which diminishes with the repeated execution of the state-action pair (s, as, More specifically, QuCB(s, a) stands for optimistic estimation of (s, a) and can serve high probability. We defer the discussion of detailed settings of node values and UCB bonus to Section 4.3
upper bound with
Expansion. The next step 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 verifi- cation 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 trun- cate the generated proof to the assertion of the earliest verification error. The remaining tacties transformed into path of nodes to be merged into the search tree (see Figure 2). 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 lactic-our expansion procedure may insert a path of tree nodes into the search tree during each iteration. This differs from the conven- tional MCTS designed for competitive games, which typically expands only one layer of children nodes per iteration (Silver et al. 2016 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 T = ((root, s())), (s(1) s(2)), (s(2), s ".
St, }}} denote the selection trajectory of t-th iteration that ends with s; as the expanding node. We update Quca(s, a) for all (s,a) a) E by taking the most recent trajectory reward R((r) into account (details refer to Eq. 7 The extrinsic source of rewards comes from the compiler feedback, specifically assigning reward of Rexurissi
1 for completed proofs and Rexuinse 0 for unsolved ones. In Section 4.3 we will introduce an intrinsic reward mechanism to augment the reward assignment that enhances the agent's incentive for exploration.

---

Published as a conference paper at ICLR 2025
4.3 INTRINSIC REWARDS FOR PROOF 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 tree structure with only narrow set of leaves delivering non- zero rewards, which matches 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 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 al. (2019). In this section, we present our RMax applied to Tree Search (RMaxTS), to incorporate reward-free exploration the proof search problem.
exploration algorithm,
RMax applied to MCTS. We adopt RMax (Brafman & Tennenholtz 2002). a classical explo- ration mechanism, 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 re- wards are provided until the proof is completed, our algorithmic procedure resembles ZeroRMax (Jin et al., 2020), in which the agent's s exploration is driven solely by intrinsic rewards, i.e, setting R(T) Rintrinsie (T). The intrinsic reward of tree expansion step is determined by whether new node added to the search tree,
Remrinsic (T) = II jat least one new node is added to the search tree].
where 7 denotes the most recent selection trajectory that requires a reward assignment for back- propagation. This exploration strategy prioritizes the expansion of nodes where the prover model generates tactics that lead to a diverse range 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):
a(s,a) Qs, ass.a)
21n Ee N(s,a')
(4)
N(s.a)
a(s,a)= = Ever(e,)) R(T),
(5)
as) = (s(,,a)),
(6)
where ((s, = fr (s) r) denotes the list of tree-policy trajectory 7 containing (s, a) as an intermediate selection step. To facilitate discussions, we organize the list I'ss a) [Ti, 72, ..,
such that newly collected trajectories have larger subscript indices. this work, we propose to alternative variant of UCB method. Note that the derived intrinsic reward in Eq. 33) is 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 dis- counted upper confidence bounds (DUCB: Garivier & Moulines 2011). which uses a discount factor E (0, 1) to smoothly drop those outdated feedback records:
QDuca(s, a) W,(s,a) Ns(s,a)
2ln EN No(s,a))
(8,
Ws(s,a)= NN(,,) y (R(T))
(8)
(s, -NVo,)) 74.
(9)
where newly received feedback would be assigned a larger weight in the value estimation. In prac- tice, Y 0.99. Note that the role of discount factor 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 single trajectory.
7

---

Published as a conference paper at ICLR 2025
XL (B07)
SPT (CWT)
Model
Pass @ 128
miniF2F-test
ProofNet
miniF2F-test
ProofNet-test
Base (3-shot)
29.7% + 0.5%
9.7% + 0.7%
SFT (non-CoT)
19.8% + 0.3%
15.9% + 0.5%
SFT (CoT)
50.4% + 0.4%
15.9% + 0.6%
44m
1204
RL (non-CoT))
50.5% + 0.6%
17.5% + 0.5%
Sample Budget
Sanple Budget
RL. (CoT)
51.6% + 0.5%
18.2% + 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 μ + a indicates the average accuracy μ and the standard deviation o, estimated from 16 independent runs of sampling evaluation.
EXPERIMENTAL RESULTS
In this section, we evaluate the theorem-proving capabilities of DeepSeek-Proves Prover--rrrr---ee V1.5 using two distinct benchmarks: miniF2F (Zheng et al. (022), which encompasses high-school level exercises and competition problems, and ProofNet (Azerbayev et al. 2023), which pertains to undergraduate- level theorems. We present the results for both whole-pre prooee generation and Monte-Came tree search methodologies. Detailed experiment settings are described in Appendix B.1
5.1
MAIN RESULTS
Results on miniF2F and ProofNet. Table D and provides comparative analysis of various phrovig- methods on the miniF2F and ProofNet benchmarks. In the single-pass whole- proof generation setting,
Prover-V1.5-RL achieved the highest pass rate at 60.2% on miniF2F-test and at 23.7% on ProofNet-test, significantly outperforming all advanced baselines. When combining DeepSeek-Provers V1.5-RR. with RMaxTS,, the new state-of-the-art are achieved, solving 62.7% problems from miniF2F-test and 25.3% problems from ProofNet-test.
General Enhancement of Reinforcement Learning. To support the claim that online reinforce- ment learning from verification feedback generally enhances the model capabilities, we compare our final model to the SFT-only version using large sample budget. The comparison results are presented as two columns in Table DeepSeek-Provert -roekk--roorr--...--- V1.5-RI consistently outperforms the SFT model across all generation settings, regardless whether the chain-of-the -foohuhg-tthhht 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-Prowee Brrecck--rrver--ee V V.5-RL achieves 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., con and CoT, on miniF2F-test dataset. The results, shown in Table indicate that the ad- vantage of CoT over the non-CoT mode is amplified the sample budget increases. This suggests that the incorporation of natural language of-thughhttt can diversify the planning pathways of theorem proving, potentially leading 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 more systematic and proactive in mathematical thinking, while in the non-CoTl mode, the model can efficiently use Lean high-level tacties to solve computational problems that can be addressed within Lean's 's automation mecha- nisms. To leverage these advantages, we consider a mixture strategy, denoted by non-CoT & CoT in Table[4 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 Ap- pendix HI we present example problems that illustrate the different ad adnatage of the two generation modes.
8

---

Published as a conference paper at ICLR 2025
Method
Sample budget
miniF2F-test
Single-pass Whole-Proof Generation Methods
128 16 x 4096
16.1% 0.5% 50.0%
DeepSeck-Prowe Prover- V (Xin et al.
2024
128
50.4% = 0.4%
3200
53.3% + 0.5% 57.4%
16 6400
128
51.6% + 0.5% 54.9% + 0.7% 60.2%
DeepSeck-Prover-
3200
16 6400
Tree Search Methods
GPT-f (Polu et
2022
8 x 512 64 x 5000 64 x 1 50
36.6%
Hypertree Proof Search Lample ct al.
2022
41.0%
Lean-STaR (Lin et al. 2024)
46.3%
InternLM2-Maann Math-Plus 7B Ying
2024b
1 32 100
43.4%
x 100
48.8%
Internl MeeenlMM-SteeProver
Wu et al. 2024
64 x 32 x 100
54.5%
3200
53.5% 0.4%
DeepSeck-Provee-...---85 RMaxTS
16 6400
59.0%
32 6400
60.2%
1 3200
55.0% + 0.7%
DeppSeck-rroee-...--LL- RMaxTS
16 6400
62.7%
32 x 6400
63.5%
Table 1: Comparison with state-of-the-art methods the miniF2F-test dataset. Unless otherwise specified, SeepSeck-Prover-V....
and RL employ CoT mode prompting. The notation + a indicates the average accuracy z and the standard deviation a. The symbol indicates performance using mixture strategy with two guiding prompts (see Section 5.1 for details). More baseline results are presented Table in Appendix. The detailed description of the evaluation setting is included in Appendix B.
ProofNct
Method
Sample budget
valid
test
all
Single-pass Whole-Prooy Generation Methods
128
19.9% 0.1%
15.9%
0.6%
17.9% + 0.3%
PeepSeek-Prover-VI...
3200
20.7% = 0.7%
0.9% 21.0%
20.9% + 0.6%
4 x 6400
22.2%
23.7%
22.9%
128
20.1% + 0.5%
18.2%
0.5%
19.1 1% + 0.4%
DeepSeck-Provee Prois--r-roo-e--.-II...1 V1.5-RI
3200
21 21.4% + 0.3%
22.0% + 0.5%
21.7% + 0.4%
4 x 6400
21.6%
23.7%
22.6%
Tree Search Methods
ReProver Yang al. 2023
13.8%
InternLM2 StepProver MitenLMM-SSepPPoover
al 2024
100
18.1%
1 x 3200
22.2% + 0.7%
21.6%
0.2% 21.9% + 0.4%
DeepSeek DeepSeek-Prover-VIin RMaxTS
x 6400
23.8%
25.8%
21.8%
3200
22. 22.0%
0.3%
21.5%
0.8%
21.8% + 0.4%
DeepSeek- Probeek--Pover--1155-L.L- RMaxTS
x 6400
25.4%
25.3%
25.3%
Table 2: Comparing with state-of-the-arn on the ProofNet dataset. The notation μ a indicates the average accuracy µ and the standard deviation a. : Note that the validation set ProofNet used to perform expert iteration in supervised fine-tuning.

---

Published as a conference paper at ICLR 2025
Sample budget
miniF2P-tost
57.0%
6400
58.4% +: 0.5%
Single-Pas Generation
58,096
16 6400
60.2%
Pass
55.09
UCT
x 6100
2% + 0.33
(withoul Rasttcse)
16 x 6400
61.1%
$4.09
RMaxTS
x 6100
58.6% + 0.3% 60.7%
RMaxTS swie
(DUCB UCBI)
RMaxT5 (UCBI)
UCT R
RMaxTS
x 6100
58.49 18.4%% + 0.3%
52.094
win Thee Search
(without lactic state)
16 6400
61.1%
1800
3200
6400
x 6400
59.6% + 0.6% 62.7%
Sample Budget
RMaxTS
16 6400
Figure 4: A modular ablation study on the design of RMaxTS, The experiments are conducted on the miniF2F-test dataset with DeepSeek- DeepSeek-Prover-V.e Prover- 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. The shaded regions represent one standard deviation around the mean accuracy, The notation μ + a indicates the average accuracy μ and the standard deviation
5.2 ABLATION STUDIES ON RMAXTS
Intrinsic Rewards and Discounted UCB. We investigate the effectiveness of two core compo- nents of RMaxTS, i.e. the intrinsic rewards defined in Eq. (3) and the discounted upper confidence bound stated in Eq. (7)- We start with baseline implementing the standard UCT algorithm (Koc-) sis & 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 vari- ants of the UCB formula become equivalent, as node selection is determined solely by visitation counts. The experimental results in Figure 4 show that, in the absence of intrinsic rewards, the per- formance of UCT (without R degenerates into a level comparable to that of non-search meth- ods. Furthermore, we consider RMaxTS using the standard UCB1 (refer Eq. ④ instead of the discounted UCB, denoted by RMaxTS (DUCB - UCB1). )). The results indicate that the performance of RMaxTS with UCB1 bonus also moderate, comparable to that of UCT (without Rimtrisic).. That is because UCBL I 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 accelerate the value propagation of non-stationary intrinsic rewards.
Guidance Tactic State Information. When expanding a tree node, we concatenate the in- termediate tactic state information 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 comple- tion directly from the raw incomplete code without accessing tactic state information, denoted by RMaxTS (without tactic state) in Figure 4 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.
comment block to the incomplete code to guide the proof
6 CONCLUSION
The framework of DeepSeek-Prover-VVe 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). promising future direction is training a critic model to assess incomplete proofs and prune search branches of proofs. Such a partial-proof critic model would implicitly perform temporal credit assignment (Sutton 1984). decomposing proof-level feed- back into step-wise value differences (Arjona-Medina
al. 2019). Developing critic models for assessing long planning paths and providing guidance rewards presents a crucial and challenging problem (Ng & Russell 2000; Soog al. 2010) that warrants further investigation.
10

---

Published as a conference paper at ICLR 2025
REFERENCES
Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, Picter Abbeel, and Wojciech Zaremba. Hindsight experience replay. In Proceedings of the 31st International Conference on Neural Information Processing Systems, pp- 5055-5065, 2017.
Jose A
Michael Gillhofer, Michael Widrich, Thomas Unterthiner, Johannes Brand- stetter, and Sepp Hochreiter. Rudder: Return decomposition for delayed rewards. In Proceed- ings of the 33rd International Conference on Neural Information Processing Systems, pp. 13566- 13577, 2019.
Peter Auer. Using confidence bounds for exploitation-eexllrraion trade-offs. Journal of Machine Learning Research, 3(Nov):397-422, 2002.
Peter Auer, Nicolo problem. Machine learning, 47:235-256, 2002.
and Paul Fischer. Finite-time analysis of the multiarmed bandit
Jeremy Avigad. Mathematics and the formal turn Bulletin of the American Mathematical Society, 2023. URL/Attpp://pp..eeaarr wtt.:sseaannniccchlcccaccccc icssthlarr Dtt.aaaace.rr/oooooaSD.S22...33
Eser Aygün, Ankit Anand, Laurent Orseau, Xavier Glorot, Stephen M Mcaleer, Vlad Firoiu, Lei M Zhang, Doina Precup, and Shibl Mourad. Proving theorems using incremental learning and hindsight experience replay. In International Conference on Machine Learning, pp. 1198-1210. PMLR, 2022.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate--lvel mathemat- ics. arXiv preprini arXiv:2302. 12433, 2023.
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen Marcus McAleer, Albert Q Jiang. Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. In The Twelfth International Conference Learning Representations, 2024.
Mare G Bellemare, Sriram Srinivasan, Georg Ostrovski. Tom Schaul, David Saxton, and Rémi Munos. Unifying count-based exploration and intrinsic motivation. In Proceedings of the 30th International Conference on Neural Information Processing Systems, pp. 1479-1487, 2016.
Ronen Brafman and Moshe Tennenholtz. R-max-a general polynomial time algorithm for near- optimal reinforcement learning. Journal of Machine Learning Research, 300t)):1133231 2002.
Cameron B Browne, Edward Powley, Daniel Whitehouse, Simon M Lucas, Peter I Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez, Spyridon Samothrakis, and Simon Colton. A survey of monte carlo tree search methods. IEEE Transactions on Computational Intelligence and Al in games, 4(1):1-43, 2012.
Yuri Burda, Harrison Edwards. Amos Storkey, and Oleg Klimov. Exploration by random network distillation. In Seventh International Conference on Learning Representations, pp. 1-17, 2019.
Kevin Buzzard. The fermat's last theorem project.
communitto
github.
2024.
Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fern' andez Mir, and Scott Morrison. Schemes in lean. Experimental Mathematics, 31:355 - 363, 2021. URL https:
//api. www.eeeinnnnnool..oo oot.aao.ooooooooooaa: :t: 230799877
Guillaume MJ Chaslot, Mark HM Winands, and H Jaap van Den Herik. Parallel monte-carlo tree search. In Computers and Games: 6th International Conference, CG 2008, Beijing, China, September 29-October 1, 2008. Proceedings 6, pp. 60 Springer, 2008
Coq Development Team. Coq: A proof assistant. https: http://ooq..iii..i ingii..ri.f. 2024.
Rémi Coulom. Efficient selectivity and backup operators in Monte-Cate tree search. Interna- fional conference computers and games, pp. 72-83. Springer, 2006.

---

Published as a conference paper at ICLR 2025
Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. A deep reinforcement learning approach first-order logic theorem proving. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pp. 6279-6287, 2021.
Alhussein Fawzi, Mateusz Malinowski, Hamza Fawzi, and Omar Fawzi. Learning dynamic poly- nomial proofs. In Proceedings of the 33rd International Conference on Neural Information Pro- cessing Systems, pp. 4179-4188, 2019.
Alhussein Fawzi, Matej Balog, Aja Huang. Thomas Hubert, Bernardino Romera-Paredes, Moham- madamin Barekatain, Alexander Novikov, Francisco J R Ruiz, Julian Schrittwieser, Grzegorz Swirszez, et al. Discovering faster matrix multiplication algorithms with reinforcement learning. Nature, 6 610(7930)47-53, 2022.
Guhao Feng, Bohang Zhang, Yuntian Gu, Haotian Ye, Di He, and Liwei Wang. Towards revealing the mystery behind chain of thought: A theoretical perspective. In Thirtt--eventhh Conference Neural Information Processing Systems, volume 36, 2023.
Scott Fujimoto, David Meger, and Doina Precup. Off-policy deep reinforcement learning without exploration. In International conference on machine learning, pp. 2052-2062. PMLR, 2019.
Aurélien Garivier and Eric Moulines. On upper-confidence bound policies for switching bandit problems. In International conference on algorithmic learning theory, pp. 174-188. Springer, 2011.
Thibault Gauthier. Deep reinforcement learning for synthesizing functions in higher-order logic. EPiC Series in Computing, 73:230-248, 2020.
Jesse Michael Han and Floris van Doorn. A formalization forcing and the unprovability of the continuum hypothesis. In International Conference Interactive Theorem Proving, 2019. URL
htw.:ppp..semmannccccccccoeeeooe wtt.:eescccoaaaoooorrrooeeoooeee wwt./orppcsooroCoooooooo 12994411
Rein Houthooft, Xi Chen, Yan Duan, John Schulman, Filip De Turck, and Pieter Abbeel. Vime: variational information maximizing exploration. Proceedings of the 30th International Con- ference Neural Information Processing Systems, pp. 1117- 1125, 2016.
Jiewen Hu, Thomas Zhu, and Sean Welleck. minictx: Neural theorem proving with coontexs 2024.
Albert Q Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygó2dz, Piotr Mitoš, Yuhuai Wu, and Mateja Jamnik. Thor: wielding hammers to integrate language models and automated theorem provers. In Proceedings of the 36th International Conference on Neural Information Processing Systems, pp. 8360-8373, 2022a.
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2022b.
Chi Jin, Akshay Krishnamurthy, Max Simchowitz, and Tiancheng Yu. Reward-free exploration for reinforcement learning. In International Conference Machine Learning, pp. 4870-4879. PMLR, 2020.
Levente Kocsis and Csaba Szepesvári. Bandit based Monte-Carke planning. In European conference on machine learning, pp. 282-293. Springer, 2006.
Akshay Krishnamurthy, Alekh Agarwal, and John Langford. PAC reinforcement learning with rich observations. In Proceedings of the 30th International Conference on Neural Information Pro- cessing Systems, pp. 1848-1858 2016.
Mitsuru Kusumoto, Keisuke Yahata, and Masahiro Sakai. Automated theorem proving in intuition- istic propositional logic by deep reinforcement learning. arXiv preprint arXiv: 100i::/811.000000 1.00796, 2018.
12

---

Published as a conference paper at ICLR 2025
Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng. Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large language model serving with pagedattention. In Proceedings of the ACM SIGOPS 29th Symposium Operating Systems Principles, 2023.
Guillaume Lample, Marie-Anne Lachaux. Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving- In Proceedings of the 36th International Conference on Neural Information Processing Systems, pp. 26337-26349, 2022.
Leanprover Community. A peai-loa for Lean 4. leanprover community/rep) 2023.
https://github com/
Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 253-266, 2023.
Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-star: Learning to interleave thinking and proving. arXiv preprini arXiv:2407. 10040, 2024.
Isaac D Lutz, Shunzhi Wang, Christoffer Norn, Alexis Courbet, Andrew J Borst, Yan Ting Zhao, Annie Dosey, Longxing Cao, Jinwei Xu, Flizabeth M Leaf, Top-down design of protein architectures with reinforcement learning. Science, 3806664)) 2023.
Mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference Certified Programs and Proofs, pp. 367-381, Association for Com- puting Machinery, 2020.
Jack McKeown and Geoff Sutcliffe. Reinforcement learning for guiding the e theorem prover. In The International FLAIRS Conference Proceedings, volume 36, 2023.
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction-CADD 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pp. 625-635. Springer, 2021.
Andrew Y Ng and Stuart Russell. Algorithms for inverse reinforcement learning. In Proceedings of the Seventeenth International Conference on Machine Learning, pp. 663-670, 2000.
OpenAl. Gpt-4 technical report. arXiv preprint arXiv:2303.08774 2023.
Deepak Pathak, Pulkit Agrawal, Alexei A Efros, and Trevor Darrell. Curiosity-driven exploration by self-supervised prediction. In International conference on machine learning, pp. 2778-2787 PMLR, 2017.
Lawrence C. Paulson. Isabelle Generic Theorem Prover. Springer Verlag. 1994.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03:: 0030009000339,... 2020.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
Michael Rawson and Giles Reger. A neurally-guided, parallel theorem prover. In Frontiers of Combining Systems: 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings 12, pp. 40-56. Springer, 2019.
Michael Rawson and Giles Reger. lazycop: Lazy paramodulation meets neurally guided search. In Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Confer- ence, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings 30, pp. 187-199. Springer, 2021.
13

---

Published as a conference paper at ICLR 2025
Stéphane Ross, Geoffrey Gordon, and Drew Bagnell. A reduction of imitation learning and struc- tured prediction to no-regret online learning. In Proceedings of the fourteenth international con- ference artificial intelligence and statistics, pp. 627-635. JMLR Workshop and Conference Proceedings, 2011.
Jürgen Schmidhuber.
Formal theory of creativity, fun, and intrinsic motivation (1990-2010) IEEE fransactions on outonomous mental development, 2(3):230-247, 2010..
Julian Schrittweser, loannis Antonoglou, Thomas Hubert, Karen Simonyan, Laurent Sifre, Simon Schmitt, Arthur Guez, Edward Lockhart, Demis Hassabis, Thore Graepel, et al. Mastering atari, go, chess and shogi by planning with learned model. Nature, 588(7833):604-660) 2020.
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06344 2017.
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Y Wu, and Daya Guo. DeepSeekMath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.033000 2024.
David Silver, Aja Huang, Chris Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Pannecrshelvam,, Mare Lanctot, et al. Mastering the game of go with deep neural networks and tree search. nature, 529(7587):484 489, 2016.
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Mare Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A general reinforcement learning algorithm that masters chess, shogi, and go through self-play, Science, 362(6419):1 140- 1144, 2018
Jonathan Sorg, Satinder Singh, and Richard L Lewis. Reward design via online gradient ascent. In Proceedings of the 23rd International Conference on Neural Information Processing Systems- Volume 2, pp. 2190-2198, 2010.
Richard Stuart Sutton. Temporal credit assignment in reinforcement learning. Phd thesis, University of Massachusetts, 1984.
Amitayush Thakur, Yeming Wen, and Swarat Chaudhuri. A language-agent approach to formal theorem-proving. In The 3rd Workshop on Mathematical Reasoning and Al at NeurIPS, 2023.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention all you need. Advances in neural informa- fion processing systems, 30, 2017.
Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, et al. prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, 2023a.
Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et al. DT-solver: Automated theorem proving with dynamic-tree sam- pling guided by proof-level value function. In Proceedings of the 6lst Annual Meeting of the Association for Computational Linguistics (Volume I: Long Papers), pp. 12632-12646, 2023b.
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theorem- llama: Transforming general purpose Ilms into lean4 experts. arXiv preprint arXiv:2407.03203, 2024.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H Chi, Quoe V Le, and Denny Zhou Chain-of-thought prompting elicits reasoning in large language models. In Proceedings of the 36th International Conference on Newral Information Processing Systems, pp. 24824-24837 2022.
Sean Welleck and Rahul Saha. Ilmstep: Llm proofstep suggestions in lean. In The 3rd Workshop on Mathematical Reasoning and Al at NeurlPS'23 23, 2023.
14

---

Published as a conference paper at ICLR 2025
Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. Lean- -eannggthhb:: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.1722) 2024.
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover prover: Advancing theorem proving in llms through large-seale synthetic data. arXiv preprini arXiv:2405. 14333, 2024.
Kaiyu Yang.
2023.
Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: theorem proving with retrieval- -augenel- language models. In Proceedings of the 37th International Conference Neural Information Processing Systems, pp. 21573-21612, 2023.
Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Thomas L. Griffiths, Yuan Cao, and Karthik Narasimhan. Tree of thoughts: deliberate problem solving with large language models. In Pro- ceedings of the 37th International Conference on Neural Information Processing Systems, pp- 11809-11822, 2023.
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:24066038477 2024a.
Huaiyuan Ying. Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, al. Internlm-math Open math large language models toward verifiable reasoning. arXiv preprint 202.v:2402.066332, 2024b.
Kaiyan Zhang, Biqing Qi, and Bowen Zhou. Towards building specialized generalist ai with system and system 2 fusion. arXiv preprint 2XXv:2447.008422 2024.
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal- -based demon- stration learning for formal theorem proving, arXiv preprint arXiv:2305.16366 2023.
Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309. 2002233998800 15806, 2023.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learming Representations, 2022.
Qihao Zhu, Daya Guo, Zhihong Shao, Dejian Yang, Peiyi Wang, Runxin Xu, Wu, Yukun Li, Huazuo Gao, Shirong Ma, al. DeepSeck-Coder V2: Breaking the barrier of closed-source models in code intelligence. arXiv preprint arXiv:2406.1199 11931, 2024.
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Towards finding longer proofs. In Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEEAUX 2021, Birmingham, UK, September 6-9, 2021, Pro- ceedings 30, pp. 167-186. Springer, 2021.
A IMPLEMENTATION DETAILS
A. 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 from DeepSeekMath-7BBBBa. (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-V V..5er-V
15

---

Published as a conference paper at ICLR 2025
Potential Data Leak. When constructing our SFT dataset, we ensure that all Lean statements in the training set have distinct initial states from those in the test set. The most uncontrollable potential source of data leakage stems from the pre- traininin phase. To the best of our knowledge, the leakage risk of Lean statement from miniF2F and ProofNet is limited, as these benchmarks were specifically designed for MI. research and were not gathered from arbitrary sources the internet. On the other hand, potential leakage of natural language statements from math problems may exist, but it generally considered acceptable, as the formalization of natural language proof Lean codes is one of the core challenges of formal theorem proving.
A.2 SUPERVISED FINE-TUNING
Expert Iteration. We We develop a comprehensive Lean code completion dataset for the supervised fine-tuning. This dataset includes synthetic proof code derived from wide range of formal theo- rems. These theorems are sourced from various projects, such as the standard Lean 4 math library Mathlib4 (Mathlib Community 2020). synthetic theorems from SaapSeee--Pover-... V1 (Xin et al, 2024) and Lean Workbook (Ying et al.
2024a). and validation sets from the miniF2F (Zheng et al,, 2023) benchmarks. To augment the formal proof data, employed an expert iteration process Polu & 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 itera- tion, we use DeepSeek-Coon Coder V2 236B (Zhu et al., 2024) to annotate the thought process before the proof code as comments. We then tailor these data for the truncat--andresumm mechanism for RMaxTS (details in Section 4. 4. The validated proofs generated through tree search are gathered to perform the next iteration of SFT. The final proof dataset consists of 9,645k sequences.
2022 and ProofNet (Azerbayev al.
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 le-4. The training process begins with 100 warm-up steps to stabilize the learning dynamics. Training examples are randomly concatenated form sequences, with a maximum context length of 4,096 tokens. The entire SFT phase processes 2600 steps and around 20B tokens.
A.3 REINFORCEMENT LEARNING FROM PROOF ASSISTANT FEEDBACK
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 DrepSeek-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-CoTT guiding prompts enhance the model's proof generation capabilities in both modes.
Rewards. When training LLMs via RI., trained reward model typically provides feedback sig- nals. 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 if verified as correct, and () otherwise. While this binary reward signal is accurate, is also sparse, especially for theorems that are challenging for the supervised fine-tuned model. To mit- igate this sparsity, select training prompts that 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.) 2024) as our RL algorithm, which has demonstrated superior effectiveness and efficiency compared to PPO (Schulman et al., 2017), primarily because eliminates the neces- sity of training an additional critic model. Specifically. GRPO samples group of candidate proofs for each theorem prompt and optimizes the model based on the relative rewards of the outputs within the group. Given group of outputs (o1, ,G) regarding input question q, the objective of
16

---

Published as a conference paper at ICLR 2025
GRPO is stated follows:
10:
JGRPO
clp (os: 0) -B nead
Oj
1=1
1=1
q, 08,ce) A clip
To(os, 9. 0.0))0)) The (oi q. 0r,cttt)
A hhc.l-e,++ c,14e))
Lelip(0i, 0) min
(Oi, q, ot,
where Ai, Fs 1s-mean(r) is the normalized advantage with respect to the cumpling-average baseline. r)
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 KI. penalty coefficient is set to 0.02. For each theorem, we sample group 32 candidate proofs, with maximum length set to 2,048. The training batch size is configured to 512. The entire RL phase processes 800 steps and around 1.5B tokens.
A.4 PARALLELIZZATON OF MONTE-CARLO TREE SEARCH
To enhance the efficiency of Monte-Carlo Tree Search (MCTS), we implement several established parallelization techniques described by Chaslot al. (2008).
Root Parallelization: We deploy 256 MCTS rumners per node, with one language model per GPU and a batch size of 512 for proof generation. The Lean prover invoked through cluster with thousands of CPU cores, where each proof verifica- tion task is handled by an individual process, created and terminated in a sandbox. Both proof generation by language models and verification by Lean provers handled asyn- chronously. This setup allows MCTS runners to perform concurrent tree search operations, significantly accelerating the process.
REPL and executed
Tree Parallelization: We manage each search tree with 32 thread workers 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 candidate node for expansion, invoking the language model to generate the proof, verifying the generated proof with the Lean prover, and performing backpropa- gation.
To encourage diverse node selection among concurrent thread workers, we assign virtual reward It(T) for ongoing iterations. This involves backpropagating reward of 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.
Virtual Loss:
17

---

Published as a conference paper at ICLR 2025
A.5 PSEUDO CODE OF RMAXTS
Algorithm RMax applied Tree Search (RMaxTS)
1: function MCTS(root, sample budget)
2:
for f = 1 to hannnle..bddee. do
3: node <- SELECT (roo))
4: node' EXPAND (node, t)
5: reward + BACKPROPAGATE(node. rewardd 7: end for
I[node' lime_stamp & 1
> RMax intrinsic reward (Eq.
3
6:
8: return BESTCHILD(roof)
9:
end function
10: function (ELECT(node)
11:
A A Children (node) U {0}
Z denotes the virtual node Discounted UCB (Eq. 7
12: child t arg aE QDUCH (node, a)
where Qnuce(node, a) = W3 (node a) N2 (node, a)
In Eared Ny (node, a') N₂ (node, a)
+
13:
if child = 2 then
14:
return mode
select the virtual node
else
16:
return SELECT(child)
end if
18:
end function
19:
function EXPAND(Rode,
20:
Resume the partial code stored node
21:
Generate new proof through code completion
22:
Truncate the generated proof to the first compilation error
23:
Segment the valid code into series of state transitions (node.state -> >8) for = to K do
24:
25:
if node has child with state 8ą then
existing child
26:
node + child where child e Children(node) n child.state =
else
D create new tree node
28:
create new tree node node' node' .state +- 8k node' ttim__stapp + t Children(node) + Children(node) U {node'} node +- node'
30:
31:
32:
33:
end
34:
end for
35:
return node
36:
end function
37:
function BACKPROPAGATE<NOdee reward)
38:
(node, O) N., (node, @) W. (node, 2) - 7- W, (node, 2) reward while node, is not null do child +- node node: <- node.parent
b update the virtual node
40:
42:
43:
N., (node, chvld) <- 7 -N, (node, child) 1
update the tree path
44:
W (node, child) +- 7 W,, (node child) + reward
45:
end while
46: end function
18

---

Published as a conference paper at ICLR 2025
A.6 COMPARISON WITH EXISTING METHODS
In this section, we compare our proposed proof tree search method, which introduces a novel runcate-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 tree search pattern. It involves generating and verifying one tactic at a time, repeating the process for the next tactic until proof goals remain. Notable examples include GPT-f (Polu & Suttkeverr 2020: Polu et al. 2022), Thor (Jiang et al. 2022a), ReProver (Yang et al. 2023 2024
Hypertree Proof Search (Lample al. 2022), and Intern (Wu al.
Single-pass whole-proof generation:
This approach generates and verify an entire proof in 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), Bubgoal-Prover ZZhao et al. (2023). LEGO-Proxe (Wang et al. 2023a), Lyra (Zheng et al. 2023). and miniCTX (Hu ct al. 2024).
Our proof tree search method uniquely bridges these two strategies, offering a novel hybrid ap- proach. It starts with whole-proof generation, similar to the single-pass approach, but extends this by implementing a sophisticated truncate-ande auneate-and-rrssume mechanism. This process involves truncating the generated proof its successful initial segment, parsing this segment into individual tactics, and re- suming the tree search from this point. This iterative process effectively implements a Monte-Catt 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 more versatile and effective solution for formal mathematics proof search, potentially paving the way for future advancements in this field.
B EXPERIMENT SETTINGS
B.1 EVALUATION
Formal Verification Environment. The Lean theorem prover is a state-of-the-art proof assistant and functional programming language, primarily designed for formalizing mathematics. Developed by Leonardo de Moura at Microsoft Research (Moura & Ullrich 202T), Lean combines dependent type theory with versatile poota-progrmminngg framework, facilitating the creation of proofs and the development of Nomainnsspccio ecosystem such as mathl ib (Mathlib Community) 2020), has established Lean as cornerstone of modern mathematical formalization (Avigad) (023). Lean has hosted some of the world's most sophisticated formalizations, including scheme theory (Buzzard et al. 202I), forcing (Han van Doom 2019). and the ongoing project for Fermat's 's Last Theorem (Buzzard 2024).
tactics. Its open-source nature, coupled with an extensive library
defining feature Lean is its tactic-based framework, which enables the construction of proofs through high-level, human-readable commands that automate common reasoning patterns. Tactics allow users to decompose complex goals into simpler subgoals and guide the proof process inter- actively. Moreover, Lean's extensibility supports the creation of custom tactics tailored to specific domains, offering significant optimizations and abstractions. This tactic-based approach bridges the gap between the machine's 's precision and human intuition, making Lean exceptionally effective for large-scale formalizations and interactive theorem proving.
Below is an example that demonstrates the application of tactics in Lean 4 and their corresponding tactic states. First, we declare a theorem statement to prove:
import Mathlib
theorem Add_Asso (a Nat) :
(a
b)
C
= by sorry
19

---

Published as a conference paper at ICLR 2025
Here, sorry serves placeholder for the actual proof. Lean provides the initial tactic state as feedback:
(b
To complete the proof, we can replace it with tacties like r ring or rw [Nat add assoc] to resolve the goal. After applying of these tactics, Lean responds with No goa 1 s, indicating that all objectives have been satisfied.
In this work, the transitions between tactic states are traced using the REPL (Leanprover Commu- nity 2023), and these transitions are used as inputs for training language models. Notably, the tran- sitions between tactic states employed in our proof search are shared across all tactic-based proof assistants, including Isabelle (Paulson 1994) and Cog (Coq Development Team 2024). Conse-
quently, there are no theoretical barriers to adapting our methods for use with other proof assistants.
Benchmarks. We evaluate theorem-proving performance on the following benchmarks to com- pare model capabilities after each training stage:
MiniF2F (Zheng et al. 2022) focuses 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 the un- dergraduate 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 con- verted to Lean 4.9.0.
Prompting Configurations. For each proof attempt of DeepSeek- Prover- V V.SSeB indepen- dently sample three proof demonstrations from the validation set to construct the few-shot prompts. For the miniF2F benchmark, use numan-writted proofs from Yang (023), while for the ProofNet benchmark, we use correct proofs generated by SeepSeek-Prover V1.5-RL as few-shot demonstra- tions. For DeepSeek PeepSee--Prove-- Prover- VI.5-SFT and DeepSeek- Proeee-roovvrvvie 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 G
Evaluation Settings. We evaluate theorem-prone proving performance using the pass @ K accuracy met- ric, which measures the model's success in generating correct proof within attempts. Each model is deployed single A100-40G GPU, utilizing the vLLM framework (Kwon et al.) (023) for sample generation. The sampling parameters are set with a temperature of I, a top-p value of 0.95, and maximum token limit of 2,048. The generated proofs are then verified using the Lean theorem prover. For this verification, we import Mathlib4 (Mathlib Community, 2020) and Ae- sop (Limperg & From 2023) access predefined premises and tactics. The verification process is subject to a time limit of 300 seconds. The largest-scale experiment presented in this paper, RMMx 32 6400 sample size and CoT generation mode on the miniF2F-test dataset, quires 48 A100 GPUs and approximately 2000 CPUs to complete within 48 hours.
Baselines. We present a comparative analysis of DeepSeck PrepSeck-Prover--- Prover- V1.5 against previous state-of- the-art language models, highlighting its performance and advancements.
General-purpase Models: GPT-3.5 and GPT-4 (OpenAI 2023) are advanced generative AI models developed by OpenAl, known for their effectiveness across diverse tasks, in- cluding 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 al., 2023), ), in-context learning agent that leverages these large language models to propose tactic applications. Additionally, we examine Llemma (Azerbayev et al. 2024), series of language models
20

---

Published as a conference paper at ICLR 2025
trained extensive general mathematical corpora, commonly used as the base model for formal theorem proving.
Specialized Models for Formal Mathematics: GPT-f (Polu & Sutskever) 2020 Polu
et al. 2022) represents an initial effort to apply Transformers (Vaswani et al. 2017 7) to proot-step generation for theorem proving tasks, utilizing a best-first search module to con- struct complete proofs. Subsequent advancements include ReProver (Yang et al., 2023
LLMStep (Welleck & Saha 2023), and Lean-STaR (Lin et al. 2024). Hypertree Proof Search (Lample al. 2022) explores the of Monte Carlo tree search in formal the- orem proving using Lean. Concurrent works, InternL.M2-Math (Ying et al. 2022bb and
InternLMM2-StpPProoer eWu al. 2024), also demonstrate outstanding performance.
Metric. We compare the performance of DeepSeck-Prowet Prooeer---Poe---Ii with state-of-the-arr models us- ing the pass@ K accuracy metric, which evaluates the model's ability to generate 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-eerst-seeteee first-search methods, following the notation of Azerbayee et al. (2024), present K N x S x 7 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. 2022), we present K = N x I where N denotes the number of tree search attempts, and T denotes the number of model generations invoked in tree expansions.
Confidence Interval. We report pass@ K accuracy as μ a where f indicates the average ac- curacy and a denotes the standard deviation. The average score and the standard deviation are computed by running several independent trials (using different random seeds) replicate the sam- pling and evaluation process. Let (a, 1=1 denote the evaluation results of n independent runs. The average accuracy is calculated by μ = 1 E The standard deviation is calculated by
14)2. For the miniF2F dataset, experiments with a sample budget below x 6400 are based on 16 independent runs, while those with a budget of exactly x 6400 are estimated from 4 independent runs. For the ProofNet dataset, the threshold set 3200. The results of ProofNet with sample budget below 3200 are derived from 16 independent runs, while those with sample budget of exactly 3200 are estimated from 4 independent runs.
Dataset
Sample budget
#uns
Dataset
Sample budget
#Runs
< 4 x 6400
16
< 3200
16
miniF2F
= 4 x 6400
4
ProofNet
= 3200
4 x 6400
>> 3200
Checkpoint Selection. The final models are selected from three training runs using different ran- dom seeds. During each training run, the model is evaluated every 100 training steps, with the @ass@ 128 score calculated for the miniF2F-test. Due computational resource constraints, the training-time evaluation is conducted using a single trial of 128 samples. We select the checkpoint that achieves peak performance over several consecutive steps as the candidate for specific training run. Upon completing three training runs, obtain three checkpoint candidates. We then perform evaluation using 16 independent trials to compute the mean and standard deviation. The RL training phase is performed on the selected SFT model. The results demonstrate that the effects of random seeds are marginal compared to the overall improvement achieved during the SET and RL phases.
21

---

Published as a conference paper at ICLR 2025
SFT phase (Pass 128)
minF2F-test
selected
secd-2
sced-3
COT non-CoT
50.6% 0.5%
50.3% 0.3%
49.9% + 0.4%
49.8% 0.4%
48.8% = 0.4%
49.6% = 0.3%
RL phase (Pass@ 128)
minF2F-test
selected
seed-2
seed-3
CoT
51.4% 0.5%
51.2% 0.4% 50.7% + 0.5%
51.2% + 0.5%
non-CoT
50.5% + 0.4%
50.2% + 0.4%
To mitigate the risk of overestimating our evaluation results, we perform cross-validation en- sure the reported scores are robust and reliable. Specifically, we first conduct (modes) x (train seeds) x (eval seeds) x 128 samples to compare the Pass 128 scores of three seed can- perform additional 2 (modes) x 16 (eval seeds) x 128
didate. Upon selecting the final model, samples to recalculate the μ = a scores for the chosen model. The recomputed scores are then reported in the main text. Note that the recomputed scores provide unbiased evaluation of the chosen model, as the evaluation conducted independently from the selection process. This ad- ditional evaluation round is crucial to ensure the reported results rigorous, maximizing random variables inherently leads to an overestimation of expected values.
22

---

Published as a conference paper at ICLR 2025
B.2
SUPPLEMENTARY EXPERIMENT RESULTS
Method
Model
Sample budget
miniF2F-test
Single-pass Whole-Proof Generation Methods
TlaoremLlama (64
8B
33.6%
46.1% 0.5%
DeepSeck-Prover-VV 68
7B
16 x 4096
50.0%
29.7% 0.5%
DeepSeck-PPover-VV V1.5-Bae
7B
3200
39.2%
6400
42.2%
32
48.2% + 0.6%
64
49.6% + 0.7%
128
50.4% = 0.4%
DeepSeck-Prover- V1..5S
7B
3200
53.3% 0.5%
x 6400
55.8% + 0.7% 57.4%
16 x 6400
32
50.0% 1 0.5%
64
50.7% 1 0.4%
128
51.6% 0.5%
PrepSeck-Prover-1..55
7B
3200
54.9% 0.7%
x 6400
58.4% = 0.6%
16 x 6400
60.2%
Tree Search Methods
COPRA (Code Llama)
60
1 x 500
5.7%
COPRA (GPT-3.5)
60
1 x 60
9.0%
COPRA (GPT-4)
x 60
26.6%
Llemma-7B
7B
1 x 32 x 100
26.2%
Llemma 1ammma-34BBBm
34B
1 x 32 X 100
25.8%
ReProver 70
229M
26.5%
LLMStep 666
2.8B
1 32 100
27.9%
GPT-f [48]
770M
64 X 512
36.6%
Hypertree Proof Search 35
600M
64 x 5000
41.0%
Lean-STaR 33
7B
64 x 50
46.3%
IntemLM2-Ne 1-2--Mat-7755 7B
73
7B
1 32 100
30.3%
IntemLM2-Math-
7B
32
43.4%
1 x 32 x 100
48.8%
I P2-StepProver 67
7B
64 x 32 x 100
54.5%
x 3200
53.5% 1 0.4%
4 x 6400
56.3% + 0.3%
DeepSeek-Prover...SSTT RMaxTS
7B
16 x 6400
59.0%
32 x 6400*
60.2%
3200
55.0% 0.7%
x 6400
59.6% 1 0.6%
DeepSeck-Prover Prover-VV..5RL. +1.5-RL+ RMaxTS
7B
16 x 6400
62.7%
32 6400
63.5%
Table 3: Comparison with state-of-the-art methods on the miniF2F-test dataset. The notation jr denotes the average accuracy yı and the standard deviation a. Unless otherwise specified, DeepSeek- Prover-VI Vi.5--II.-BBa.. 1-5ee results are based on 3-shot prompting, while TaatScck--Prverr-.. V1.5-SFT and RL employ CoT mode prompting. The symbol i indicates performance using a mixture strategy with two guiding prompts.
23

---

Published as a conference paper at ICLR 2025
DeepSeck-Prose Proieed---ovv-V..
Prompt mode
Sample budget
SFT
RL
4 x 6400
54.7% + 0.4%
56.5% 1 0.5%
non-CoT
16 x 6400
56. 1%
57.4%
4 6400
55.8% 1 0.7%
58.4% 0.5%
Single-Pass Generation
CoT
16 6400
57.4%
60.2%
(2 + 2) x 6400
56.1 16.1% = 0.8%
58.3% = 0.6%
non-CoT & CoT
(8 + 8) x 6400
58 58.2%
60.7%
(16 + 16) x 6400
58.6%
61.1%
4 6400
55.7% = 0.6%
58.4% + 0.6%
non-CoT
16 6400
57.8%
59.4%
4 6400
56.3% + 0.3%
59.6% 0.6%
CoT
RMaXTS
16 6400
59.0%
62.7%
(2 + 2) x 6400
56.1% + 0.8%
60.0% + 01.8%
non-CoT & CoT
(8 + 8) x 6400
59.0%
63. 1
(16 + 16) 6400
60.2%
63.5 %
Table 4: A large-scale ablation study to investigate the effectiveness of several algorithmic designs on model training. The results are evaluated on the miniF2F-tesl dataset. The notation μ μ a denotes the average accuracy μ and the standard deviation
C PROBLEM CATEGORIES ON MINIF2F BENCHMARK
miniF2F-test
DeepSeek-Provers
DeepSeek-Prover-
V1.5-SF
DeepSeek-Prover- VI.5-RL
single-pass generation
16 1096
1 x 64100
16 6400
4 x 6400
16 6400
IMO
1/20
2/20
2/20
2/20
2/20
Olympiad
AIME
4/15
5/15
6/15
5/15
6/15
AMC
12/45
13/45
14/45
15/45
16/45
Algebra
53/70
55/70
56/70
55/70
56/70
MATH
Number Theory
45/60
47/60
49/60
49/60
51/60
Algebra
4/18
8/18
8/18
9/18
9/18
Custom
Number Theory
1/8
2/8
2/8
4/8
4/8
Induction
2/8
3/8
3/8
3/8
3/8
Table 5: Problems solved by DeepSeek-Proverr V1.55 on miniF2F-rest, grouped by miniF2F cat- egories. The experiments are conducted in CoT mode and incorporate single-pass whole-proof generation.
tini RMaxTS
DeepSeck-Prover
VL.
SeepSeck-Prover V1.5-RL RL
4 6400
16 x 6400
4 x 6400
16 x 6400
IMO
2/20
2/20
2/20
2/20
Olympiad
AIME
5/15
6/15
5/15
6/15
AMC
13/45
14/45
14/45
16/45
Algebra
55/70
58/70
57/70
59/70
MATH
Number Theory
48/60
49/60
52/60
53/60
Algebra
8/18
9/18
9/18
10/18
Custom
Number Theory
3/8
3/8
3/8
4/8
Induction
3/8
3/8
3/8
3/8
Table 6: Problems solved by SeepSeek-Prover-V/7 V1.5 miniF2F-test, grouped by miniF2F cate- gories. The experiments are conducted CoT mode and incorporate RMaxTS.
24

---

Published as a conference paper at ICLR 2025
miniF2F-valid
miniF2F-test
IMO
3/20
3/20
Olympiad
AIME
4/15
6/15
AMC
25/45
16/45
Algebra Number Theory
64/70
59/70
MATH
51/60
53/60
Algebra
17/18
10/18
Custom
Number Theory
5/8
4/8
Induction
7/8
4/8
Table 7: The results of miniF2F-vvlid is collected through the expert iteration. The results of FiniF2F-test refer to experiment of DeepSeek SrepSeck-Prove--I..55 Prover-VI.5-RL. ple size that incorporates both CoT and non-CoT generation modes.
+ RMaxTS with 32 6400 sam-
D EXPERIMENTS SLIDING WINDOW UCB
We conduct experiments on RMaxTS with sliding-window UCB (SWUCB; Garivier & Moulines 2011 another variant of upper confidence bound to tackle non- non-stationary rewards.
Qswucn(s, a) = (8, + (s)
2 Ene (s,(s
(10)
Ex Nw(
M,,a,) W (s, Ex N(xa)-w+1) R((T),
(11)
(s) = min (IT(s,
(12)
where w denotes the window size. The SWUCB described above a slight modification of Garivier & Moulines (201T), leveraging the fact that non-stationarity is independent across different state- action pairs. The results indicate that, with proper window size w = 64, the SWUCB outperforms the standard UCBI but performs slightly worse than DUCB. To explain this performance gap, note that, in the implementation, most tree nodes do not trigger the sliding window mechanism due the sample budget constraints. In contrast, DUCB enables smoother value discounting than SWUCB, which helps to achieve better performance.
DeepSeck-Proveet x 6400
Prover- (CoT)
minF2F-test
6400
UCBI
58.6% + 0.3%
61.1%
SWUCB 32)
58.2% + 0.5%
61.1%
SWUCB 64)
59.1% = 0.4%
61.9%
SWUCB (w 128)
58.4% = 0.4%
61.5%
DUCB (default)
59.6% + 0.6%
62.7%
Table The experiments of RMaxTS with sliding- UCB on miniF2F-test. The notation dt denotes the average accuracy and the standard deviation a.
25

---

Published as a conference paper at ICLR 2025
E EXTENDING CONTEXT LENGTH FOR SFT
During the SFT phase, we use a context window of 4K tokens, which sufficient to cover all our training prompts for formal languages. The longest data sequences sourced from the mathlib dataset, the standard library used for constructing proofs in Lean. As we extract the theorem depen- dencies, the lengthy files in mathlib can also fit within 4K-token context length.
We conduct an ablation study using a 16K-token context length and raw mathlib files for training. The SFT performance shows slight drop, or least no significant benefits observed from extending the context length for training formal languages. One possible explanation for this result is that the raw mathlib files may not align with the distribution of the Olympiad problems in testset.
Pass 128
miniF2F-test
4K (default)
50.4% + 0.4%
16K (with raw mathlib)
49.6% + 0.6%
Table 9: The experiments on extending the context length for SFT. The notation fr + a denotes the average accuracy y and the standard deviation σ.
F STATISTICS OF AVERAGE OUTPUT TOKENS
We compare the average output tokens generated by RL model across four settings: (1) with and without R.MaTT;; (2) with and without thain-of-thoughe The results show that the CoT mode consumes significantly more tokens compared to the non-CoT mode. However, nearly half of the output tokens can be saved through tree search, as the generation leverages existing nodes with partial code.
avg. #tokens / sample
CoT
non-CoT
single-pass generation
495.7
109.6
RMaxTS
244.6
76.1
Table 10: The sampling procedure are conducted on miniF2F-test with a sample budget of 3200. The statistics are averaged across all 244 problems in the minil22F-test dataset.
G 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 aime_1983 1181_p9ppppp.. a problem from the miniF2F benchmark ęZheng et al. (2022). These examples refer to the data format used in the SFT phase. For clarity, inline LaTeX expressions are utilized. Firstly, here is example of whole-proot generation in non-CoT prompting mode:
Input:
Complete the following Zean 4 code:
.*'lean4 import Mathlib
import Aesop
set set_option maxHeartbeats
open Bigoperators Real Nat Topolegy Rat
/-- Show that 92 sin" xt1 > 12 for 0 < O<I<R.-/
theorem aime_1983___
198__p9 (x R) (ho xxxA2 Real.pi)
geing
26

---

Published as a conference paper at ICLR 2025
12 19
(x
RRal.ssn
4) / Reallsin := by
Output:
[le_diviiff (mul_pos ho. 1 (Real ssi__scnn_s....... _aa___f_________________________ ho. ho. 2) nlinarith [mul_self_net (3 Real sin 2)
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-resumee mechanism (see Section A details). The model receives a prompt including 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:
Complete the following Lean 4 code with explanatory conments preceding each line of code:
'1ean
import Mathlib
import Acscp
set_option maxHeartbeats
open Bigoperators Real Nat Topolegy Rat
/-- Show that 92 sin? x+4 12 for < <<I5 sing
theorem aime _im__1983_p (x : R) (ha 0 x 12 $ (9 (x
scal.pi) :
sial.sin x 2) + 4) / (x Real.sin x) := by
/-
To find the minimum value of 9= snn
zeinx for 0 x <T, we need to show that it is at least 12. We start by noting that the expression can rewritten using
division property of inequalities. use the fact that sin and are positive establish the necessary inequalities. Finally, we apply these results to conclude that the minimum value is indeed 12.
then the given range to
We start by ensuring that the product a sin is positive in the given range.
have h1 0 < Real.sin x :- by apply mul_pes is positive in the range (0,
exact ho.1
sinr is positive in the range 10, exact Real.sin pfs_oof_____ooooooooeooeeeeeeooo _t__ooo______________________o__ pos_oo of__ffl_l______ pi_pi bo . he.2
Using the division property of inequalities, rewrite the expression.
Iw (le_div_iff hi]
/- tactic state:
x R
ho :
hi : x x.sin
12 + (x x.sin) $ 9 (x x.sin 2) +
Output:
This is equivalent to showing that 9x " x 12rsin + 0, and the
left haan side can be rewritten as perfect square (3rsinæ - 2)
We use the fact that (3rsin 2) is non-negative to establish this.
nlinarith [sq_nonneg (3 x Real.sin 2)
27

---

Published as a conference paper at ICLR 2025
In this case, the proof completion model first extracts the goal expression from the tactic state, i.e., the inequality 12(z r) S 9(x2 sin r) +4 at the last line of the comment block, and then arranges it into the form 9x² sin" æ 12x sin x + 2 as part of the chain-of-thougee process. Finally, the left-hand side is rewritten square term to establish non-negativity, closing the proof.
H 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.
H.1 PROBLEMS THAT NON- COT OUTPERFORMS COT
theorem induct Inductian_pordiln htt.eooooooooopppoooooooooooooo lo2pookk1tsnn2222 (n N) (ho : 0 < n)
(IT k in Pinsst. Ice 1 n, + (1 R) / 2 k) 5 2 :- by
[Finset.. Icc]
simp all [Nat. suce le iff, Nat. one iff _e__e__e_____ zero] := by apply pow_pos <;> norm num
have h1 norm_num
have he (2 : R) * 0 = by nurm_num field_simp
Iw [div_lt_div iff)
ring_nf
norm_cast
nlinarith
all goals cast
all goals linarith
theorem imo 1960 (x R) (bo : S
(hr (1 Real sqrt (1
x)) 2 * 0) (h2 :
(1 sqrt (1 2 x))
< 2 + x 9) - $
A x
45 / := by
norm_num at hg h1 h2
have ha 0 < 2 x by linarith have ha nlinarith [Real.sqrt _ott__nonnegggggtttttett (1 x) :- by
Real.sqrt (1
x]]
have hs 4 by linarith
2 (1 Real.sgrt (1 * x) 2 x
have he 1 Real.sqrt (1 2 intro apply h nlinarith
by
have hy 4
2 (1 Real.sgrt (1 + x)) 2 2 (1 Real. sqrt
(1 + 2 x)) 2 by fiela simp [bal
nlinarith
(show S : 2 x by linarith)
[h7] at hs constructor <;> nlinarith [sq sqr_sqrt (show 0 $
by linarith)
H.2 PROBLEMS COT OUTPERFORMS NON-COT
theorem mathd_algebra__1 b = C d) (ha : 2 + c - a + b d) (hs : * a
: Q) (ho :
d)
(h1 :
+
10
b 6
c 24) fd.den + d.num = 28 := by
/-
Given the system of equations invelving the times that Anna (a), Bertram (b), Carli (c), and David (d) can hold their breaths:
1. 3a b+++d
2. 4b = a c
3. 2c = +++b+ bbt
Sa 10b 24
28

---

Published as a conference paper at ICLR 2025
We need find the of the numerator and the denominator of the fraction representing David's time minutes, simplified its lowest terms, and show that it is 28.
First, we solve the system of equations step by step: From the first equation, d= 3a --
can express d in terms of a,b, and et
Substitute into the second equatien: 46 - a c+ (3a - -)
simplitying,
get:
46 = 4a -
5b 4a
b= da
Substitute b into the third equation:
=0=a+ 48
(3a ----b-o b-c)
simplifying we get:
2c = 5
da 3a 3
4a
2c 4a Ja
3c
3
Substitute b and into the fourth equation:
8a 10 3/4 + (*x) =4
Simplifying we get:
8a + Sa + Sa ===22
24
Now, wc find b and c:
b b=
da
c= 3
Finally, we find d:
d= 3a b- 3 1.1-- -
13
15
The fraction TE
13 is already its simplest form, and the sum the
numerator and the denoninator is:
13+ 28
-/
have ha a
:= by
have hs : 8 a 10 6 24 := ha
have he 24 a 24 1= by
Solve the system of equations find the value of linarith exact mul_right_cancelo (show (24 : Q) * 0 by norm_num)
(by linarith)
have hs bbbb4 1 5 := by
Solve for b using the value of linarith
have ho : - 4
:= by
-- Solve for è using the value of linarith
have hy
/ 15 :- by Solve for d using the values of a, b, and c
linarith
Sum the numerator and the denominator of num [hr]
<;> rfl
thoorem numberthoory_K5neqp222 (x Σ) : #
2
:= by
/-
To show that for any two integers æ and y, x + we can use
modular arithmetic to demonstrate that the equation x'= +4 (mod 11) will consider the possible values & and y medulo and show that none of these combinations satisfy the equation.
has solutions. Specifically
Use modular arithmetic to show that the eguation has solutions modulo 1J.
29

---

Published as a conference paper at ICLR 2025
have -xx 8
+ $ 11) by
Consider all possible values of modulo 11.
have : x 8 11 v =1 =1 -1-vV 11 22VX 11 V x 8 11
4 V
= -
8 11 = 66x8 - - - V - 9 8 11 10
by omega
Consider all possible values of y modulo 11.
have : $ 11 ovy 11 = v 8 11 2 V 11 = 33V 11
y 11 y 6Vy 7 8 8 V 8 10
by
omega
For each combination of and modulo 11, check if the equation
holds.
reases this with (h reases this with (h' h h h' h h h I ht M b))
h h h <p>
simp [h, h', pow_suce, Int.mu w-m_mmllod,,, Int mattadddee cmod]
Use the result from modular arithmetic to conclude the theorem. omega
theorem amc12_2000 p12 (ame: N) (he - 12)
a 112 by
/-
Given nonnegative integers M,M, and C such that A+ + C' 12, we need to find the maximum value of A.M the fact that the expression
A.M M-C+A
To solve this,
A A.M- MM-C+A A. A- is polynomial in terms of A, M, and C. We can try different values of M,M, and C that sum to 12 and compute the value of the polynonial for each combination. The maximum value of the polynomial will then be the solution.
We use a lemma that states if the sum of three numbers less than or equal to a cortain value, then the product of these numbors is also less than or equal to a certain value. have h constructer
12 A S 12 A 12 by
Since + m m 12, cannot be greater than 12. omega constructor omega
Similarly, cannot be greater than 12.
And с cannot be greater than 12.
omega
Using the lemma, compute the value of the polynomial for different values a, m, and a that sum to 12.
cases' h with he_left h right cases' hi_right with by_middle bı bi_right
We use interval_case to try different values of a, m, and c. interval_cases <;> interval_cases For each combination, we compute the value of the polynomial and check is less than or equal to 112. simp_al1 (config :- (decide :- true))
<;> interval cases <;>
30


Reviews:
[{"review_id": "V1sng1mZjx", "reviewer": "Reviewer_ePCd", "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.", "questions": "Some additional suggestions/questions\n\n-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?\n\n-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?\n\n-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?\n\n-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.\n\n-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?", "limitations": "", "rating": 5, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "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.", "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.\n\nThat 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.\n\nAll 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.\n\nAll 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "csAThvBSGL", "reviewer": "Reviewer_ydok", "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. \n\nThe 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).\n\nThe 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.", "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?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 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.\n* The approach applies several MCTS innovations and uses the Lean prover as a verifier. \n* The paper claims that DS-Prover-V1.5-RL performs the best in single-pass and tree search categories.", "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. \n* The paper provides no pseudo-code or loss function formulas, making understanding the approach's details difficult. \n* GRPO is not described (even in the Appendix).\n* Experiments:\n\t* For some categories, the baselines are other versions of the same model.\n\t* Tables 1-4 do not include confidence bounds for the best-performing methods.\n\t* Some important information is missing:\n\t\t* Not all model details are disclosed for use in the MCTS algorithm.\n\t\t* No comparison is provided between the number of parameters or FLOPS used by the evaluated models.\n\t\t* No wall clock time is given.\n\t* 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?\n\t* The potential data leaks are not discussed.\n\t* No number of seeds is reported.\n\t* What are the $\\mu$'s and $\\sigma$'s (present in tables and figures and defined in the caption of Figure 3) computed over?\n\t* 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.\n\t* The results in Figure 4 suggest that many differences are not statistically significant.\n\nEdit 29 Nov 24: I increased the rating 5->6.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "J79M8j5T9S", "reviewer": "Reviewer_rpvG", "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.", "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?\n2. 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.", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 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.", "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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "IpnlDvUBoo", "reviewer": "Reviewer_dd1U", "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.", "questions": "1.\tCould 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 .\n2.\tThe gains achieved with RL over Supervised Fine-Tuning (SFT) in Tables 1 and 2 are modest. What factors contribute to these limited improvements?\n3.\tSimilar to the RL results, improvements with RMaxTS appear modest in Tables 1 and 2. Could you provide more context?\n4.\tWhat 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?\n      - It would also be interesting to see token-budget-aligned results.\n5.\tThe improvements in Figure 3 also appear modest. Any insights?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The paper tackles a critical problem, merging theorem-proving and reinforcement learning with proof assistant feedback.\n2. Strong empirical results demonstrate improvements in state-of-the-art theorem proving on established benchmarks.", "weaknesses": "1. I have various doubts listed in the question section.\n2. 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?\n3. 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)