CARTS: Advancing Neural Theorem Proving with Diversified Tactic Calibration and Bias-Resistant Tree Search

6. Clarify algorithms in Table 3

We would like to clarify that in Table 3, the algorithm labeled “Bias-resistant Value Function” refers exclusively to our proposed bias-resistant value function integrated within the MCTS framework. In contrast, the label “Diversified Tactic Calibration” denotes the MCTS framework incorporating only the diversified tactic calibration. In this case, the value function does not require training and instead directly utilizes the intrinsic reward, as described in Line 367.

7. Effectiveness of BT model

Thank you for your suggestion. We have included a comparative experiment between the BT model and the binary cross entropy loss (CE) in Appendix B.1. Using Qwen2.5-0.5B [3] as an example, the results are summarized as follows:

We find that the BT model consistently outperforms CE in our experiments. While the use of oversampling improves the performance of CE, it still does not surpass the BT model. Additional experiments on other models and further experimental details can be found in Appendix B.1 of the revised version.

8. Can $w(s,a)$ be negative?

The value of $w(s,a)$ cannot be negative. Therefore, in the actual implementation, we set $w(s,a) =\max (0,\text{MMR}(s,a))$ to ensure that all $w$ are non-negative (clarified in Line 241). Additionally, this issue can be avoided by setting a large value for $\lambda$.

9. Ablation study on $k$

We supplement the ablation study results for $k = 1, 2, 4$, as shown in the table below. Additionally, the corresponding results are incorporated into Figure 3 (only the $k = 4$ is included for aesthetic purposes).

The experimental results demonstrate that as $k$ increases, the pass@1 initially improves, reaching a peak, and then gradually declines. Therefore, we recommend choosing a moderate $k$, such as $k=8$, in practice.

10. Analysis for the ranking of the right tactics

Thank you for your advice. The MMR in diversified tactic calibration influences the ranking of the $w$ values for the correct tactics. Using Reprover-Lean4 on miniF2F (for k = 8, E = 64), we statistically analyze the improvement in the ranking of correct tactics on the first state of proved theorems. We find that diversified tactic calibration can lead to an average ranking improvement of 14.8 for the right tactics. The bias-resistant value function has no effect on the ranks because it does not modify $w$.

Reference:

[1] Xin, Huajian, et al. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data.

[2] Wang, Haiming, et al. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function.

[3] Qwen Team. Qwen2.5: A party of foundation models.

Thank you for taking the time to review our paper and provide feedback! Below we address your questions and concerns.

1. About statistical significance

We would like to clarify that the improvement achieved by our method occurs without requiring additional data to train the tactic generator. Notably, Deepseek-Prover [1] achieved an 11.4% improvement only after leveraging an additional dataset 13 times the size of Mathlib (3.108B vs. 0.238B) (see [1], Table 2), highlighting the inherent difficulty of the theorem proving task. We argue that the consistent improvement of our method (about 2%) across different pre-trained tactic generators can demonstrate the effectiveness of our approach.

2. About Label imbalance

The term "local optima" refers to that CE loss training tends to prioritize predicting the majority class when faced with label imbalance, resulting in suboptimal performance. About empirical evidence, we provide additional experiments comparing the performance of CE and BT in Appendix B.1. The results demonstrate that BT consistently outperforms CE in situations involving class imbalance. Further details of the experiments can be found in our revised version.

3. About domain gap

The reward adjustment term can be interpreted as a form of test-time adaptation to the distribution of test data. If the number of valid tactics is low, the value of should be decreased, as the current state is more likely to correspond to a wrong state. Conversely, if the number of valid tactics is high, the value should be increased to encourage exploration. As a result, the adjustment term can mitigate the domain gap. We make corresponding revisions to the content in the main text (Line 303). About empirical evidence, we conduct additional experiments in Appendix B.1 to demonstrate the severity of the domain gap. Furthermore, the ablation study presented in Table 3 has shown the effectiveness of the adjustment term.

4. Example of $f_{enc}$ The sentence embedding model demonstrates a relatively strong capability for recognizing similarities. Below is an example to illustrate this point (MiniF2F, amc12_2000_p6), where two tactics, ‘intro h’ and ‘intro H’, yield the following next states:

p q : ℕ
h₀ : Nat.Prime p ∧ Nat.Prime q
h₁ : 4 ≤ p ∧ p ≤ 18
h₂ : 4 ≤ q ∧ q ≤ 18
h:  ¬p * q - (p + q) = 194
⊢ false

p q : ℕ
h₀ : Nat.Prime p ∧ Nat.Prime q
h₁ : 4 ≤ p ∧ p ≤ 18
h₂ : 4 ≤ q ∧ q ≤ 18
H:  ¬p * q - (p + q) = 194
⊢ false

The similarity score calculated using the pretrained sentence embedding model is 0.998, indicating that the two states are recognized as similar. Then our diversified tactic calibration can be applied for deduplication.

5. About typo in Eq (1)

We would like to clarify that there is no typo in Eq. (1). The expression for the WUCT score in Eq. (1) is consistent with the formulation of PUCT presented in DT-Solver [2]. The bonus term is divided by the visit count $N(s,a)$, ensuring that its value does not exceed 1.

Thank you for the detailed response. I’ve raised the score accordingly.

Regarding Eq (1), if I understand correctly, if the state s has two actions a_1 and a_2, then N(s,\cdot) = N(s,a_1) + N(s,a_2). Isn’t it possible that N(s,a_1)=100, N(s,a_2)=1 so that the term \sqrt{N(s,\cdot)}/N(s,a_2) is bigger than 1? Could you clarify?

Thank you for your valuable feedback. Below are our responses to your questions:

About generalizability: Our method is specifically designed for one-step tree search approaches, which currently represent the mainstream in ATP. We are also exploring the possibility of extending our method to multi-step tree search approaches in our future work.

About computational efficiency: The additional computational cost of our method compared to baseline methods (BFS and MCTS) primarily comprises two components: obtaining embeddings and executing the MMR algorithm. We utilize a lightweight embedding model, which keeps the computational cost relatively low. Regarding the MMR algorithm, the number of tactics expanded is quite limited (typically 64), rendering the computational time for this component negligible.

Thank you for your valuable feedback. Below we address your concerns.

About experiments: In Appendix B, we add additional experiments to further demonstrate the effectiveness of our bias-resistant value function. The main conclusion of the supplement is elaborated in our overall response.

About the more budget: We have conducted relevant experiments, as shown in Figure 2 in the main text, to illustrate that our method achieves improvements as the budget scales up. Experiments with larger budgets may exceed our current computational resource capacity. However, we believe that the current experiments are sufficient to demonstrate that our method can scale effectively, particularly as the search depth increases.

Thank you for taking the time to review our paper and provide feedback! Below we address your questions and concerns.

1. About independent runs

Due to limitations in computational resources, we did not conduct multiple experimental runs. However, we believe the results remain robust, as our proposed method does not introduce additional randomness. The only source of randomness arises from the LLM’s sampling process, which tends to stabilize with a large sample size. Prior works [1, 2] have similarly opted not to perform repeated experiments. Furthermore, theorem proving is a relatively special task—once a theorem is successfully proved in a single run, it is considered solved.

2. Applicability of CARTS to BFS

CARTS could indeed be adapted to use a BFS framework. However, we think that MCTS is more suitable for ATP tasks. Our work partly focuses on a biased value function, and BFS is generally less robust in the presence of noise. In contrast, MCTS dynamically adjusts value estimates during exploration, enabling it to better handle noises.

3. Details of BFS and MCTS in experiemnets

In our experiments, BFS employs the model likelihood approach commonly used in ATP studies and MCTS utilizes the intrinsic reward, as described in Line 367 in the paper.

4. Determining $\tau$ and the ablation study

We provide additional analysis on our data filtering in Appendix B.2. Observing the bimodal distribution of similarity scores (Figure 7), we find that the value of $\tau$ can be determined using a Gaussian Mixture Model (GMM). Furthermore, through the ablation study (Table 6), we demonstrate that omitting filtering introduces noise, which negatively impacts the value function. Detailed results are available in the revised version.

5. Regarding the LeanDojo Mathlib Benchmark

We did not conduct experiments on the LeanDojo Mathlib benchmark in our study. The primary reason is that some tactic generators (e.g. StepProver) were trained on Mathlib, and our bias-resistant value function was also trained on Mathlib. This overlap introduces a potential risk of data leakage, which could compromise the fairness of comparisons. Instead, we opted for experiments on MiniF2F and ProofNet, adhering to the experimental setups established by prior work [2]. We believe that the ATP field would greatly benefit from the development of more standardized benchmarks to ensure consistent and fair evaluations across studies.

5. Additional experiments of training the value function.

In Appendix B.1, we present additional experiments to demonstrate the effectiveness of training the value function using the BT modeling approach. We conducted training across three models (Qwen2.5-0.5B, Llama3.2-1B, Llama3.2-3B), with the results summarized in Table 5. Here we show the results for Llama3.2-3B and more results please see our revised version.

We find that a slight performance improvement as model size increases; however, the improvements remain relatively modest. We attribute this to the limited dataset size, which constrains the emergence of distinct scaling properties.

[1] Yang, Kaiyu, et al. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models.

[2] Wu, Zijian, et al. LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover.