DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

Question #4: What is the exact sample budget? Are wall-time comparisons available? Is it comparable between RMaxTS and other baselines?

The sample budget is defined in terms of the number of whole-proof generations, which also corresponds to the number of invocations of the Lean compiler. This setting matches the convention of reinforcement learning, where sample efficiency serves as a key metric to assess the agent's performance within a limited budget of environment interactions. In the context of the Lean prover, the compilation time of Lean code is non-negligible and can sometimes become an additional efficiency bottleneck alongside LLM inference. In extreme cases, a single tactic such as aesop may take over 60 seconds to compile due to its intensive back-end proof search.

Since the majority of prior work on formal theorem proving is closed-source and lacks reporting on token statistics and wall time, direct comparisons with existing methods are not feasible. To compare within the algorithmic framework of our approach, we compare the average output tokens generated by our RL model across four settings: (1) with and without RMaxTS; (2) with and without chain-of-thought. 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.

Weakness: Regarding technical details

In this paper, we train a series of 7B models, aligned with state-of-the-art baselines such as InternLM2-StepProver and Lean-STaR. The model was trained on approximately 20B tokens during the SFT phase and 1.5B tokens during the RL phase. In the paper revision, we incorporate these technical details into the main text and enrich the discussion in the Appendix, along with the ablation studies suggested by all reviewers.

Thanks for the comments. We provide clarification to your questions and concerns as below. If our response does not fully address your concerns, please post additional questions and we will be happy to have further discussions.

Question #1: Clarifications on the standard deviation formulas

The average accuracy $\mu$ and the corresponding standard deviation $\sigma$ are computed by running several independent trials (using different random seeds) to replicate the sampling and evaluation process. For all experiments with manageable sample sizes, we perform 16 independent replications of sampling and evaluation to estimate the confidence interval. Let $\\{a_i\\}\_{i=1}^{16}$ denote the pass@K accuracy values of 16 independent experiment runs. The standard deviation is computed by $\sigma=\sqrt{\text{Variance}(\\{a_i\\}\_{i=1}^{16})}=\sqrt{\frac{1}{16}\sum_{i=1}^{16}(a_i-\mu)^2}$ where $\mu=\frac{1}{16}\sum_{i=1}^{16}a_i$ denotes the empirical average. Please refer to the document of numpy.std for more details.

Question #2&3&5: The gains achieved with RL and RMaxTS are modest. What factors contribute to these limited improvements?

Our experimental results definitely demonstrate significant improvements. The seemingly modest numerical gains in accuracy are attributed to the exceptionally steep difficulty level of the benchmark dataset.

1. MiniF2F and ProofNet are challenging benchmarks

   Both of these gold-standard benchmarks comprise high-quality, human-written Lean problems. The benchmark dataset includes only the formalized problem statements, without the accompanying Lean proofs. Meanwhile, the difficulty levels of the benchmark problems cover an exceptionally wide range, from basic numerical equations to IMO-level competition challenges. A large portion of Lean problems in these benchmarks remains unsolved by any machine learning models. Therefore, any advancements that lead to the resolution of new problems represent a substantial enhancement in the model's capabilities. The record of problem-solving on MiniF2F-test was held at 41% by HTPS (Lample et al., 2022) for nearly two years. It was subsequently advanced to 50% by DeepSeek-Prover-V1 (Xin et al., 2024), further improved to 54.5% by InternLM2-StepProver (Wu et al., 2024), and ultimately reached 63.5% in this paper, marking a breakthrough in the domain of automated theorem proving.

2. RL significantly enhances the sample efficiency of proof completion

   Given the steep difficulty levels of the benchmark problems, another meaningful metric for assessing model capability is the number of samples required to achieve a certain accuracy threshold. Referring back to Figure 3 in this paper, a key insight is highlighting the remarkable sample efficiency of the RL model. To achieve $50\\%$ accuracy on the miniF2F benchmark, the RL model requires approximately $32$ samples, demonstrating a 4-fold improvement compared to the $128$ samples needed by the SFT model. This conclusion also applies to large-scale experiments incorporating MCTS-based approaches. As demonstrated in Table 3, the SFT model requires over $16 \times 6400$ samples to achieve $60\\%$ accuracy on the miniF2F-test benchmark, whereas the RL model achieves the same level of accuracy with just approximately $4 \times 6400$ samples, attaining a 4-fold improvement in sample efficiency.

References

[1] Lample et al. (2022). Hypertree proof search for neural theorem proving.

[2] Xin et al. (2024). DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data.

[3] Wu et al. (2024). Lean-Github: compiling Github Lean repositories for a versatile Lean prover.

Thanks for the comments. We provide clarification to your questions and concerns as below. If our response does not fully address your concerns, please post additional questions and we will be happy to have further discussions.

Weakness #1: General introduction of Lean

Thank you for your insightful suggestion regarding enriching the background of our work. We agree that providing a more comprehensive context will enhance the overall clarity and depth of our study. In particular, formal theorem proving with Lean is a rapidly evolving research area. In ICLR 2025, the number of submitted papers on Lean and formal theorem proving has at least doubled compared to the previous ML conference (e.g., NeurIPS 2024), reflecting its growing prominence in the machine learning community. Additionally, Lean has been adopted by DeepMind's AlphaProof to address challenging problems from mathematics competitions, underscoring its capability in tackling advanced mathematical problems.

In the paper revision, we include a general introduction in Appendix B.1, explaining how the Lean’s tactic mode works, along with an example to illustrate the underlying state transitions. Notably, the tactic-state transition system employed by our proof search algorithm is a common framework shared by all tactic-based proof assistants, including Isabelle and Coq. There are no theoretical barriers to adapting our proposed methods for use with other proof assistants.

Question #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?

During training, we use a context window of 4K tokens, which is sufficient to cover all our training prompts for formal languages. The longest data sequences are sourced from the mathlib dataset, the standard library used for constructing proofs in Lean. As we carefully extract the theorem dependencies, the lengthy files in mathlib can also fit within a 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 a slight drop, or at 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.

Extending the context window is, in fact, highly crucial for addressing real-world applications in formal theorem proving. One of our future goals is to advance beyond proving individual theorems to real-world Lean projects with complex, multi-theorem Lean files. This may require reorganizing the training dataset, shifting from purely problem-solving tasks to complex engineering challenges, which warrants further investigation.

Question #2: Experiments on sliding-window UCB

We evaluate the performance of RMaxTS using the Sliding-Window Upper Confidence Bound (SWUCB) algorithm with window sizes $w \in \\{32, 64, 128\\}$. The SWUCB algorithm is slightly modified to leverage the fact that non-stationarity is independent across different state-action pairs. The results indicate that, with a proper window size $w=64$, the SWUCB outperforms the standard UCB1 but performs slightly worse than DUCB. To explain this performance gap, we note that, in the implementation, most tree nodes do not trigger the sliding window mechanism due to the sample budget constraints. In contrast, DUCB enables smoother value discounting than SWUCB, which helps to achieve better performance.

3. (Cont'd) RL Phase: The workflow of RL for LLM finetuning differs from that of traditional deep RL

   Technically, the RL stage for an LLM agent involves far fewer gradient steps compared to traditional deep RL, usually amounting to just a few hundred steps. In our case, the RL model is fine-tuned over just 800 gradient steps. Meanwhile, the reference policy model remains fixed throughout the entire training process, i.e., do not update $\pi_{ref}$ in PPO’s KL penalty. This design is a common practice when applying policy gradients to LLM fine-tuning, ensuring that the model retains the general world knowledge acquired during the pre-training phase. By keeping the reference policy fixed, the fine-tuning process focuses on aligning behavior without overriding foundational knowledge. Moreover, the action space for language tasks is extraordinarily large (e.g., 100k unique tokens), and the concept of a step is inherently ambiguous (as there are countless possible sentences). As a result, the RL procedure for LLMs is typically driven by trajectory-level reward supervision without discount factors ($\gamma=1$), operating outside the framework of multi-step MDPs. These technical differences result in the workflow of applying RL to LLMs being significantly distinct from traditional deep RL. As a result, intuitions from traditional deep RL on classical control problems cannot be directly transferred or applied to LLM fine-tuning.

4. MCTS Phase: RMax's significance lies in its tailored application to Lean's unique problem structure

   Our exploration strategy for Lean proof search is inspired by RMax (Brafman & Tennenholtz, 2002), a classical method for PAC-learning on MDPs. However, rather than being a straightforward application of RMax to MCTS framework, the intrinsic reward mechanism of RMax plays a crucial role within the unique problem structure of Lean. In the formal verification system, each transition between tactic states represents a meaningful proof step, typically involving a valid simplification of the premises or goals. Any superfluous proof code, though correct in syntax-level, will be rejected by the Lean proof assistant and trigger a compiler error. This tightly constrained environment differs significantly from traditional code completion tasks and other search problems typically encountered in LLM-based reasoning.

   The intrinsic reward mechanism of RMax incentivizes the discovery of previously unseen tactic states. Given the strict constraints of the Lean compiler, the reward for exploring new tactic states extends beyond the standard principle of “optimism in the face of uncertainty”. The discovery of new tactic states in Lean is not a merely exploratory behavior but represents genuine progress in formalizing and advancing proofs. The RMax-style reward is designed to serve as the primary objective for MCTS in constructing complete Lean proofs, rather than functioning as an auxiliary exploration bonus.

References

[1] Brafman & Tennenholtz (2002). R-max-a general polynomial time algorithm for near-optimal reinforcement learning.

Question #2: Why not generate one tactic at a time, as is standard in multi-step RL?

From a theoretical perspective, generating a complete proof in one sequence is equivalent to generating it step-by-step, as both approaches ultimately compose the same final proof. Our approach adopts the whole-proof generation paradigm based on several practical engineering considerations.

1. One major purpose of our truncation mechanism is reducing the communications between LLM generation (GPU jobs) and Lean verification (CPU jobs). Leveraging the underlying infrastructure for LLM inference, generating a complete sequence in a single request is significantly faster than breaking it down into multiple steps. In a multi-step MDP setup, where Lean verification is required at each proof step, each step would involve transferring the generated tokens from the GPUs to CPUs, decoding them into UTF-8 proof codes, transmitting the data to the Lean server, waiting for the verification response, and then re-encoding the proof assistant's feedback into LLM tokens before transferring them back to the GPUs for further processing. This process introduces significant overhead to the proof generation pipeline.
2. Breaking down the proof generation into step-by-step processes does not offer additional extrinsic supervision for reinforcement learning. The only extrinsic reward is a binary signal indicating whether the entire proof is complete or not. Unlike classical control tasks in traditional deep RL, there is no intermediate reward signal to guide the generation of individual proof steps. Given the sparse-reward nature of the task and the equivalence in downstream data processing, we develop our algorithmic pipeline upon the whole-proof generation model.

Question #3: Am I correct that given an equivalent sample budget the difference between MCTS and 1-shot generation methods is simply the way candidate solutions are generated? Does the reduced number of new tokens generated result in meaningful compute savings for the MCTS algorithm?

Yes. Given an equivalent sample budget, the tree search approach and 1-shot generation differ only in their prompt sampling strategies, while the total number of model invocations remains the same. For the second question, the answer is also yes: the use of MCTS can effectively reduce the number of output tokens. We compare the average output tokens generated by our RL model across four settings: (1) with and without RMaxTS; (2) with and without chain-of-thought. The results show that nearly half of the output tokens can be saved through tree search, as the generation leverages existing nodes with partial code.

Major Concern #2: The results as presented seem incremental 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

Our experimental results definitely demonstrate significant improvements. The seemingly modest numerical gains in accuracy are attributed to the exceptionally steep difficulty level of the benchmark dataset.

1. MiniF2F and ProofNet are challenging benchmarks

   Both of these gold-standard benchmarks comprise high-quality, human-written Lean problems. The benchmark dataset includes only the formalized problem statements, without the accompanying Lean proofs. Meanwhile, the difficulty levels of the benchmark problems cover an exceptionally wide range, from basic numerical equations to IMO-level competition challenges. A large portion of Lean problems in these benchmarks remains unsolved by any machine learning models. Therefore, any advancements that lead to the resolution of new problems represent a substantial enhancement in the model's capabilities. The record of problem-solving on MiniF2F-test was held at 41% by HTPS (Lample et al., 2022) for nearly two years. It was subsequently advanced to 50% by DeepSeek-Prover-V1 (Xin et al., 2024), further improved to 54.5% by InternLM2-StepProver (Wu et al., 2024), and ultimately reached 63.5% in this paper, marking a breakthrough in the domain of automated theorem proving.

2. RL significantly enhances the sample efficiency of proof completion

   Given the steep difficulty levels of the benchmark problems, another meaningful metric for assessing model capability is the number of samples required to achieve a certain accuracy threshold. Referring back to Figure 3 in this paper, a key insight is highlighting the remarkable sample efficiency of the RL model. To achieve $50\\%$ accuracy on the miniF2F benchmark, the RL model requires approximately $32$ samples, demonstrating a 4-fold improvement compared to the $128$ samples needed by the SFT model. This conclusion also applies to large-scale experiments incorporating MCTS-based approaches. As demonstrated in Table 3, the SFT model requires over $16 \times 6400$ samples to achieve $60\\%$ accuracy on the miniF2F-test benchmark, whereas the RL model achieves the same level of accuracy with just approximately $4 \times 6400$ samples, attaining a 4-fold improvement in sample efficiency.

Question #1: GRPO vs. PPO

To evaluate the effectiveness of PPO compared to GRPO, we conduct PPO experiments using hyperparameters aligned with those used for GRPO in the paper. The results indicate that PPO does not outperform the GRPO baseline.

GRPO is a simplified implementation of PPO, widely adopted in numerous LLM projects for its computational efficiency. The exclusion of the value network is motivated by the observation that learning a value function is often not simpler than addressing the core policy learning task, particularly for language tasks with trajectory-level sparse rewards. In policy gradient algorithms, the major functionality of the value function is to reduce the variance of gradient estimation. The choice of any arbitrary value function, as long as it depends solely on the state, preserves the unbiased estimation of the policy gradient. Since a learned value function often deviates significantly from the true value function, as noted in prior studies (Ilyas et al., 2020), using group-level average return as a Monte Carlo estimation serves as a satisfactory approximation.

References

[2] Lample et al. (2022). Hypertree proof search for neural theorem proving.

[3] Xin et al. (2024). DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data.

[4] Wu et al. (2024). Lean-Github: compiling Github Lean repositories for a versatile Lean prover.

[5] Ilyas et al. (2020). A closer look at deep policy gradients.

Thank you for your detailed and thoughtful review! We greatly appreciate the opportunity to engage with researchers outside the field of formal theorem proving and are eager to further clarify our contributions. Below, we provide comprehensive responses to your questions and concerns. Should any unresolved points remain, please do not hesitate to raise additional questions—we would be delighted to continue the discussion.

The review highlights two primary concerns:

Major Concern #1: The application of reinforcement learning (RL) and Monte Carlo Tree Search (MCTS) to formal theorem proving with large language models (LLMs) seems straightforward, raising concerns about its novelty.

Below, we restate and expand upon the core contributions of our work, positioning them within the context of relevant literature to enhance clarity.

1. Formal theorem proving with Lean is an important problem domain

   This paper is specifically tailored for formal theorem proving using Lean, deliberately designed to address the intricacies and specialized requirements of this domain. The proposed approach is not intended to be a general-purpose composition that can be seamlessly applied to other decision-making tasks. Instead, it focuses on advancing the capabilities within Lean by incorporating methodologies and optimizations that align with Lean's formal system and proof strategies. The contributions of our work should be evaluated within the literature context of ML-aided formal theorem proving, considering the rapid growth of the Lean community.

   In particular, formal theorem proving with Lean is a rapidly evolving research area. In ICLR 2025, the number of submitted papers on Lean and formal theorem proving has at least doubled compared to the previous ML conference (e.g., NeurIPS 2024), reflecting its growing prominence in the machine learning community. Additionally, Lean has been adopted by DeepMind's AlphaProof to address challenging problems from mathematics competitions, underscoring its capability in tackling advanced mathematical problems.

2. SFT Phase: Integrating chain-of-thought reasoning into symbolic proof synthesis

   A key innovation in our SFT phase lies in augmenting proof code generation with chain-of-thought (CoT) reasoning. Chain-of-thought reasoning allows for a more interpretable, step-by-step formulation of the solution, closely resembling the way humans decompose and tackle complex problems. This stands in contrast to the majority of previous work on formal theorem proving, which primarily relies on purely symbolic methods, lacking the inherent reflection and stepwise reasoning that chain-of-thought provides. In our approach, natural language reasoning is further combined with tree search algorithms, efficiently navigating the solution space to identify the most promising planning paths.

3. RL Phase: The workflow of RL for LLM finetuning differs from that of traditional deep RL

   In traditional deep RL, such as Atari games and MuJoCo control tasks, the RL algorithms typically run for millions of environment steps, enabling the emergence of decision-making capabilities from a randomly initialized policy network. In contrast, when training a LLM, the foundational capabilities are primarily developed during the pre-training and supervised fine-tuning (SFT) phases. During pre-training, the model is exposed to vast amounts of diverse text data, allowing it to learn a wide range of patterns and general world knowledge. In the subsequent SFT phase, the model is further refined and adapted to more specific tasks and desired behaviors through carefully curated datasets. The final RL phase, also known as the alignment phase, acts as an online tuning stage that complements supervised fine-tuning (SFT) to further refine the model's sequential generation. From the perspective of traditional deep RL, this phase can be seen as an on-policy fine-tuning of an imitation-learned policy. While SFT trains the model on static data, the alignment phase uses real-time feedback, such as the proof assistant feedback used in this paper, to adjust the model's behavior based on newly observed trajectories.

Question #4: 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.

The shaded regions in Figure 4 represent the confidence interval, corresponding to one standard deviation around the mean accuracy. The experimental results in Figure 4 contain two parts. The left panel presents the experimental outcomes for a sample budget of fewer than $6400$ samples, where the performance difference between the RMaxTS algorithm and its ablation version is approximately one standard deviation. As the sample size increases, the right panel highlights a more pronounced performance gap. With a larger sample budget, i.e., $4\times 6400$, the difference between RMaxTS and the ablation version widens, reaching up to two standard deviations. This demonstrates a clear improvement in sample efficiency for RMaxTS, as it scales more effectively than the baseline methods.

Question #5: Why do some accuracy numbers have +- intervals and others don't?

In this paper, we have prioritized making the statistical results more rigorous by providing confidence intervals alongside our key findings. For all experiments with manageable sample sizes, the average accuracy $\mu$ and the corresponding standard deviation $\sigma$ are computed by running 16 independent trials (using 16 random seeds) to replicate the sampling and evaluation process. Specifically, for the miniF2F dataset, experiments with a sample budget below $4\times 6400$ are based on 16 independent runs, while those with a budget of exactly $4\times 6400$ are estimated from 4 independent runs. For the ProofNet dataset, the threshold is set at $3200$. The results of ProofNet with a sample budget below $3200$ are derived from 16 independent runs, while those with a sample budget of exactly $3200$ are estimated from 4 independent runs. Due to computational constraints, we do not perform multiple trials for experiments with the largest sample budgets. In the paper revision, we include a detailed description in Appendix B.1 to clarify the computation of confidence intervals.

Additionally, we would like to highlight that the results from smaller sample sizes are sufficient to demonstrate significant improvements over baseline models. For instance, on the miniF2F benchmark, our RL model achieves an accuracy of $54.9\\%\pm0.7\\%$ with a sample size of $3200$, which is comparable to the strongest baseline, InternLM2-StepProver, that requires a substantially larger sample budget of $64 \times 3200$ to reach an accuracy of $54.5\\%$. This underscores the superior sample efficiency of our model.

Question #1: In the MCTS expansion phase, was the rollout a single whole-proof generation?

Yes. In the MCTS expansion phase, each rollout is a single whole-proof generation. A detailed description of our parallelization strategy is included in Appendix A.4. We employ the techniques of Chaslot et al. (2008) to diversify search paths, allowing for the exploration of a wider range of solutions from different tree nodes, i.e., we allocate the sample budget towards exploring different tree nodes simultaneously, rather than performing many expansions on the same node. This approach promotes broader coverage of the search space, increasing the likelihood of discovering diverse proofs, while also improving overall efficiency by avoiding over-exploration of any single tree node.

Question #2: Did the Authors consider bootstrapping in the AlphaZero style?

Yes. This paper aims to make steps towards an RL-driven bootstrapping framework for formal theorem proving, similar to AlphaZero, while leaving certain limitations to be addressed in future work.

1. MCTS for policy learning. In this paper, we take a step towards integrating MCTS into the training process. The SFT dataset definitely includes some synthetic proofs generated by MCTS. Specifically, our SFT dataset is curated using an expert-iteration process, as adopted by many prior work on formal theorem proving, such as GPT-f (Polu & Sutskever, 2020) and InternLM2-StepProver (Wu et al., 2024). This iterative approach alternates between model training and proof data collection, facilitating continuous enhancement in both the quality and complexity of the generated proofs. This iterative training approach is motivated by the fact that most open-source datasets provide only formal problem statements without accompanying Lean proofs.
2. Sparse-reward challenge. The training phase of AlphaZero is designed to be a fully online fashion, as chess games provide dense supervision signals—one of the players always receives a clear win reward. In contrast, the reward signals in Lean proof search are significantly more sparse. In the expert iteration procedure, an unseen problem might require hundreds or even thousands of proof generation attempts before it is successfully solved. This highlights that improving the sample efficiency is a critical challenge in formal theorem proving.
3. Statement auto-formalization for self-improment. Theorem proving is not a closed problem domain, unlike chess or Go. Both SFT and RL training rely on a predefined problem set, restricting the scope for self-improvement. To enable continual improvement in theorem proving capability, a problem generation mechanism is required to expand the difficulty range of the training domain, as demonstrated in AlphaGeometry. In formal theorem proving, a classical approach is to develop an auto-formalization pipeline that translates natural language math problems into formal statements. This module is essential for enabling the scalable bootstrapping of a formal theorem proving agent, which remains as the future work.

References

[1] Chaslot et al. (2008). Parallel Monte-Carlo tree search.

[2] Polu & Sutskever (2020). Generative language modeling for automated theorem proving.

[3] Wu et al. (2024). Lean-Github: compiling Github Lean repositories for a versatile Lean prover.

Weakness #4.5: 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?

In Appendix C, we provide statistics on the distribution of problems solved by our model, based on the categorization defined by the miniF2F dataset. The improvement of our model can be explained in two key aspects. First, compared to DeepSeek-Prover-V1, the model presented in this paper demonstrates comprehensive improvements across all categories of problems, including Olympiad problems, algebra, number theory, and induction. Additionally, the performance gains achieved through RL and RMaxTS are primarily observed in algebra and number theory problems, which represents the most standard problem set aligned with the training distribution. This indicates that the improvements achieved through RL and RMaxTS are attributed to the enhancement of sample efficiency, as no significant gains are observed in the complex Olympiad domain.

Weakness #4.6: The potential data leaks are not discussed.

We thank the reviewer for identifying this critical issue regarding potential data leakage. 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 pretraining 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 ML research and were not gathered from arbitrary sources on the internet. On the other hand, potential leakage of natural language statements from math problems may exist, but it is generally considered acceptable within the research community, as the formalization of natural language proof to Lean codes is one of the core challenges of formal theorem proving.

Weakness #4.7: The confidence intervals are asymptotic and one-$\sigma$, corresponding to $68\\%$, a rather narrow confidence level. The results in Figure 4 suggest that many differences are not statistically significant.

The experimental results in Figure 4 contain two parts. The left panel presents the experimental outcomes for a sample budget of fewer than $6400$ samples, where the performance difference between the RMaxTS algorithm and its ablation version is approximately one standard deviation. As the sample size increases, the right panel highlights a more pronounced performance gap. With a larger sample budget, i.e., $4\times 6400$, the difference between RMaxTS and the ablation version widens, reaching up to two standard deviations ($\approx 95\\%$ of the population within the distribution). This demonstrates a clear improvement in sample efficiency for RMaxTS, as it scales more effectively than the baseline methods.

Thanks for the comments. We provide clarification to your questions and concerns as below. If our response does not fully address your concerns, please post additional questions and we will be happy to have further discussions.

Weakness #1&2&3: Descriptions on base model, pseudo code, loss function formulas, and GRPO

1. We adopt the base model of DeepSeek-Prover-V1 and its synthetic dataset as the basis for our model training. The base model is trained with vast amounts of diverse natural language mathematical content, as well as formal languages like Lean, Isabelle, and Metamath.
2. We include the pseudo code of RMaxTS in Appendix A.5.
3. The loss function is the standard next-token-prediction paradigm for LLM training. The construction of training prompts is illustrated in Figure 1. We include several examples in Appendix G.
4. Group Relative Policy Optimization (GRPO) is a streamlined variant of PPO that eliminates the need for a critic model, instead estimating the baseline using average scores from the training batch.

In the revision, We incorporate explanations of these technical details into the relevant sections of the Appendix.

Weakness #4.1: For some categories, the baselines are other versions of the same model.

Since most baseline models are closed-source, we can only reference the benchmark scores reported in the original papers. In particular, for ProofNet, a recently proposed benchmark, the available baseline results are relatively limited. Confidence interval statistics for the baselines are also unavailable, as none of the previous works in the literature have reported confidence intervals for their sampling results.

Weakness #4.2: Tables 1-4 do not include confidence bounds for the best-performing methods. No number of seeds is reported. What are the $\mu$'s and $\sigma$'s computed over?

In this paper, we have prioritized making the statistical results more rigorous by providing confidence intervals alongside our key findings. For all experiments with manageable sample sizes, the average accuracy $\mu$ and the corresponding standard deviation $\sigma$ are computed by running 16 independent trials (using 16 random seeds) to replicate the sampling and evaluation process. Specifically, for the miniF2F dataset, experiments with a sample budget below $4\times 6400$ are based on 16 independent runs, while those with a budget of exactly $4\times 6400$ are estimated from 4 independent runs. For the ProofNet dataset, the threshold is set at $3200$. The results of ProofNet with a sample budget below $3200$ are derived from 16 independent runs, while those with a sample budget of exactly $3200$ are estimated from 4 independent runs. Due to computational constraints, we do not perform multiple trials for experiments with the largest sample budgets. In the paper revision, we include a detailed description in Appendix B.1 to clarify the computation of confidence intervals.

Additionally, we would like to highlight that the results from smaller sample sizes are sufficient to demonstrate significant improvements over baseline models. For instance, on the miniF2F benchmark, our RL model achieves an accuracy of $54.9\\%\pm0.7\\%$ with a sample size of $3200$, which is comparable to the strongest baseline, InternLM2-StepProver, that requires a substantially larger sample budget of $64 \times 3200$ to reach an accuracy of $54.5\\%$. This underscores the superior sample efficiency of our model.

Weakness #4.3: Not all model details are disclosed for use in the MCTS algorithm.

In this paper, the MCTS approach is developed for proof code completion. The policy model used in MCTS is directly derived from the SFT and RL training phases, without any additional tuning or specialized prompting. Additionally, RMaxTS, our proposed MCTS variant, is a reward-free exploration algorithm that runs without a critic model, eliminating the need to train any additional models to support the tree search procedure.

Weakness #4.4: No comparison is provided between the number of parameters or FLOPS used by the evaluated models. No wall clock time is given.

Since the majority of prior work on formal theorem proving is closed-source and lacks reporting on FLOPs and wall time, direct comparisons with existing methods are not feasible. We include the model size information in Table 3 of the Appendix. The state-of-the-art baseline results are based on a series of 7B models, matching the size of our model, and therefore share comparable deployment and inference costs. The largest-scale experiment presented in this paper, RMaxTS with a $32 \times 6400$ sample size and CoT generation mode on the miniF2F-test dataset, requires 48 A100 GPUs and approximately 2000 CPUs to complete within 48 hours.