CARTS: Advancing Neural Theorem Proving with Diversified Tactic Calibration and Bias-Resistant Tree Search
Authors: Xiao-Wen Yang
Zhi Zhou
Haiming Wang
Aoxue Li
Wen-Da Wei
Hui Jin
Zhenguo Li
Yu-Feng Li
Venue: ICLR 2025 Poster (2025)
Keywords: Neural Theorem Proving
Diversified Tactic Calibration
Bias-Resistant Tree Search
Monte Carlo Tree Search
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: Recent advancements in neural theorem proving integrate large language models with tree search algorithms like Monte Carlo Tree Search (MCTS), where the language model suggests tactics and the tree search finds the complete proof path. However, many tactics proposed by the language model converge to semantically or strategically similar, reducing diversity and increasing search costs by expanding redundant proof paths. This issue exacerbates as computation scales and more tactics are explored per state. Furthermore, the trained value function suffers from false negatives, label imbalance, and domain gaps due to biased data construction.  To address these challenges, we propose CARTS (diversified tactic CAlibration and bias-Resistant Tree Search), which balances tactic diversity and importance while calibrating model confidence. CARTS also introduce preference modeling and an adjustment term related to the ratio of valid tactics to improve the bias-resistance of the value function. Experimental results demonstrate that CARTS consistently outperforms previous methods achieving a pass@l rate of 49.6\% on the miniF2F-test benchmark. Further analysis confirms that CARTS improves tactic diversity and leads to a more balanced tree search.

Published as a conference paper at ICLR 2025
CARTS: ADVANCING NEURAL THEOREM PROVING WITH DIVERSIFIED TaCtiC CALIBRATION AND BIAS- RESISTANT TREE SEARCH
Xiao-Wen Yang".,, Zhi Zhou', Haiming Wang"., 3.5 Aoxue Li
Wen-Da Weit.2, Hui Jin", Zhenguo Li", Yu-Feng Li
Nattioal Key Laboratory for Novel Software Technology, Nanjing University School of Artificial Intelligence, Nanjing University
3 "Sun Yat-sen University "Noah's Ark Lab, Huawei MMoonshot Al
ABSTRACT
Recent advancements in neural theorem proving integrate large language models with tree search algorithms like Monte Carlo Tree Search (MCTS). where the lan- guage model suggests tactics and the tree search finds the complete proof path. However, many tactics proposed by the language model converge to semantically or strategically similar, reducing diversity and increasing search costs by expand- ing redundant proof paths. This issue exacerbates computation scales and more tactics are explored per state. Furthermore, the trained value function suffers from false negatives, label imbalance, and domain gaps due to biased data construction. To address these challenges, we propose CARTS (diversified tactic CAlibration and Res-stessttnnt Tree Search), which balances tactic diversity and importance while calibrating model confidence. CARTS also introduce preference modeling and an adjustment term related to the ratio of valid tactics improve the bias- resistance of the value funnttion. Experimental results demonstrate that CARTS consistently outperforms previous methods achieving a pass@) @ rate of 49.6% on the miniF2F-test benchmark. Further analysis confirms that CARTS improves tactic diversity and leads to a more balanced tree search. The code for our imple- mentation is available at https::// com
CARTS
INTRODUCTION
Automated theorem proving (ATP) (Harrison et al. 2014) an essential task of artificial intelligence (AI) with significant challenge. Recently, the development of large language models has brought new vitality and advancements to this field (Han al. 2022 Jiang al. 2023 Xin et al. 2024a). For example. AlphaProof (Deepmind] 2024] Trinh et al. 2024) solved four out of six problems from International Mathematical Olympiad (IMO), achieving the same level as silver medalist in the competition. These advancements stem from the integration of language models and formal theorem proving systems (such as Lean (Moura & Ullrich| 202I] or Isabella (Paulson 1994h). which model the theorem proving task as a Markov Decision Process (MDP) (Polu & Sutskever 2020)) The language model functions as policy network that provides heuristic proof tactics, while tree search methods are utilized to explore correct sequence of steps that maximize the reward.
Although the improvements language models (Xin et al. (024a) can significantly improve the performance of theorem proving, efficient tree search methods remains crucial for theorems with long and complex proof steps. Existing search techniques (Polu Sutskever] 2020; Wang et al.) 2023 Xin et al. 2024a) primarily rely on Best First Search (BFS) or Monte Carlo Tree Search (MCTS) (Kocsis Szepesvári 2006). While these method can achieve impressive performance, they have two significant drawbacks. Firstly, the output sampling of auto-regressive language mod- els frequently exhibits significant redundancy, often producing similar tactics. Although the lan- guage model generates substantial number of tacties that differ at the character level, they share the same underlying semantics. For instance, both 'intro h' and ro H' can be generated
"Corresoonding author: Yu-Feng Li (1 ( amda. edu.en)

---

Published as a conference paper at ICLR 2025
n:38
Search Tree
n:N 111 100n-(11)nn
+ 111 n-
Policy Model
Expand
rol podd__o__ddd__ppepe
induction'
no [sub_en__a bat______ddd__ee
0.9
0.9
m:N
case ze1o
-11 n+
11 (--11100
[é-sub sq addd
Q.7
induction' with nih
n:
:::11 110 n-
Induction with
0.6
MMR
nwi (f-zu__qg_ aduaddd neal
101100 (p- 111 (n-3)
agaas doimp
Induction n with hn
0.5
Induction' in with hn
0.1
casa zero
Candidate Tactics
Predicted Score
Calibrated Tactics
V-42
V=lt2
V=01
case SucC n:H
Score
Ph 1:0 (-1)
Diversified Tactic Calibration
11-11) (p-1)
V-09
Training
Debiasing
Inference
Finished
CARTS
Bias-resistant Value Function
Figure 1: Overall Framework. Diversified tactic calibration can calibrate the model confidence and enhance the diversity of candidate tactics, thus mitigating ineffective exploration. The bias- resistant value function can adapt to the test data, provide more accurate scores for evaluating tactics, thus improving the efficiency of utilization.
by the language model; however, they convey the same meaning in Lean4, as they both introduce a hypothesis into the proving context. This redundancy can also lead to imbalance in the number of high-level proof strategies. For example, most of the tactics generated by the language model may focus on the strategy of proof by contradiction, while there are relatively few tactics involv- ing mathematical induction. These will result in huge amount of ineffective exploration during the tree search process, thus increasing search costs. This issue worsens as computation scales and more tactics are explored per state. Secondly, the construction of value function training data often relies on existing policy models generate negative samples and thus introducing bias. On one hand, this construction may produce a substantial number of negative samples, potentially far exceeding the positive ones. This could result label imbalance, causing the cross-entropy loss used in training the value function to easily converge to local optima. On the other hand, the samples generated by the policy model may contain false negatives, introducing noise into the dataset. Additionally, the domain gap between the training dataset (e.g., Mathlib) and the test dataset (e.g.. IMO prob- lems) exacerbates the bias of the value function during the inference stage. This leads to inaccurate evaluations of the current proof state's value, hindering effective exploitation during the tree search process. Overall, these two issues prevent existing tree search techniques from efficient exploration and effective exploitation, resulting in sub-optimal search performance.
In order to solve these challenge, we propose diversified tactic CAlibration and Ressstesttt Tree Search (CARTS). Diversified tactic calibration involves reordering and rescoring multiple candidate tactics generated by a language model's 's sampling output. This approach balances importance and di- versity, thereby enhancing exploration efficiency. We use the Maximal Marginal Relevance (MMR) algorithm (Peng et al.] (005) to achieve this, which is a classical method in the field of information retrieval. Meanwhile, we propose a bias-resistant value function. During the training stage, prefer- ence modeling is employed to construct the training dataset, and the Bradley-Terry model (Bradley) & Terry 1952) is utilized to train the value network. This approach addresses the issue data imbalance and false negatives. During the inference stage, introduce adjustment term related to the ratio of valid tactics into the value function to mitigate the domain gap between the training and test dataset. This stems from insight that if the number of valid tacties is limited, concerns
2

---

Published as a conference paper at ICLR 2025
may arise regarding the effectiveness of the current policy model, necessitating reduced value for the current action. Bias-resias Biastresistant value function can enhance the effectiveness of exploitation during the search process. The complete framework of CARTS is shown in Figure [T] We conducted suffi- cient experiments on the widely recognized theorem-prone
benchmarks, namely miniF2F (Zheng et al.] 2022) and ProofNet (Azerbayev et al.] (023) in Lean. Our proposed CARTS demonstrates superior performances compared to all other search methods when the policy network remains un- changed. We achieved a pass@1 @ success rate of 49.6% on the miniF2F-test dataset, which is the state-of-the--rt performance among all one-step tree search methods.
To summarize, this paper (i). proposes diversified tactic calibration assisted monte carlo tree search to improve the exploration efficiency. (ii) proposes bias-resistant value function to improve the exploitation effectiveness. (iii). demonstrates the effectiveness of the proposed method across different models and benchmarks in experiments.
2 RELATED WORK
Neural theorem proving. In recent years, the advancement of large language models has brought new progress to theorem proving (Li et al. 2024). GPT-f (Polu & Sutskever 2020) is the first to utilize language models trained on proof data to predict candidate proot steps and employ search al- gorithms to discover the complete proof path. A series of subsequent studies have employed diverse language model techmiques from various perspectives to enhance theorem proving performance. In terms of model training, PACT (Han al. 2022) employs set of self-superviss auxiliary tasks to train the model. Curriculum Learning (Polu et al. 2023) introduces curriculum expert iterations to update the network. Llemma (Azerbayev et al. (2224) continues pre-training the CodeLlama models (Roziere et al.) (023) on a math-focused corpus. AlphaGeometry (Trinh et al.] (024)) integrates a transtormer model trained on synthetic geometry data with a symbolic deduction engine to solve olympiad geometry problems. InterL.M2-Math (Ying et al. (024b) compiles a substantial collec- tion of both formal and informal leeve math problems (Ying et al., [024al] Wu et al., 2024). First et al. (2023) incorporates repair feedback mechanism in proof generation. This feedback is facilitated by an LLM fine-tuned on tuples consisting of incorrect proof, error message and correct proof. In terms of algorithmic design, Reprover (Yang et al. (023) employs serreval--ugmenterr generation for proof generation. DSP (Jiang et al. (023) initially uses informal hints to guide proofs by translating informal proofs into formal sketches, which are then completed with Isabelle's au- tomated reasoning tactics. LEGOProver (Xin et al., 2024c) enhances DSP with a skill library that expands throughout the proof search. Lyra (Zheng et al. (024) iterates on DSP by using error feed- back to modify the formal sketch, employing automated reasoning tools to correct incorrect proof's of intermediate hypotheses. COPRA (Thakur al. 2024) utilizes in-context learning agents aug- ment theorem proving. These methods employ different formal systems. In our paper, we focus on Lean, which has been verified to perform well on IMO-level tasks (Deepmind) 2024).
Search methods for theorem proving. Neural theorem proving primarily consists of two cate- gories: whole proof generation methods Xin et al.] (2024a); Wang et al. (2024b) and tree search methods. Tree search methods are increasingly becoming the mainstream approach in recent years. A typical approach involves using Best First Search (BFS), as seen in methods like GPT-f (Polu & Sutskever, 2020). Reprover (Yang et al. 2023) and others (Lin et al. 2024 Welleck & Sahal 2023). In contrast, Thakur et al. (2024) employs depth-first search (DFS). Inspired by AlphaZero (Silver et al., 2018), many methods utilize MCTS, such as HyperTree Proof Search (Lample al.) 2022). There are also several improvements to the MCTS algorithm for theorem proving tasks. For instance, DT-Solver (Wang et al. 2023) uses virtual nodes and a proof-level value function to dy- namically guide the MCTS search. Wang et all (202a)) introduces a novel method that allows for the emergence of unproven lemmas during the search, which are subsequently proven recursively. The aforementioned methods are all one-step tree search techniques, which generates a single tactic at each step. Recently, multi-step tree search methods have been developed. For instance, DeepSeek- Prover-V1.5 (Xin et al., 2024b) employs MCTS to enhance the whole proof generation process, utilizing intrinsic rewards and discounted upper confidence bounds to guide exploration. Despite the success of these methods, challenges remain, namely the lack of diversity for searched proof paths and bias in the trained value function. This paper focuses on addressing these challenges by employing our diversified tactic calibration and bias-resistant tree search.
3

---

Published as a conference paper at ICLR 2025
Algorithm 1 Maximal Marginal Relevance for Diversified Tactic Calibration
Require: current state 8, tactics set {a1, 02,, de). next state set { 8/21 ... sch. number of se-
lected tactics kt parameter À
S {s} A
(
while |A| < min(k; e) do
a" < arg maxa, (a Upaticy (8, ai) - (1 X) maxx3es Sena(s() Tena(()))
Add a" to A Add the corresponding next state s" to 5
end while
return the expanded action set
METHOD
In this section, we present the details our proposed method CARTS, which consists of two com- ponents. We begin by introducing the diversified tactic calibration [3.I. followed by giving details of our bias-resistant value function (3.2). Together, these two approaches enhance the effectiveness of exploration and exploitation during the search process.
3.1 DIVERSIFIED TACTIC CALIBRATION
In practice, the multiple candidate tactics generated by language models often exhibit redundancy. Diversified tactic calibration addresses this by calibrating candidate tactics' model confidence based on their intrinsic similarity. We implement the calibration using the Maximal Marginal Relevance (MMR) algorithm (Peng et al. (2005) and structure our method's framework through Monte Carlo Tree Search (Koesis Szepesváni 2006).
The standard MCTS method used in theorem proving (Wang et al. 2023 Xin et al. 2024b) involves
three steps: Selection, Expansion and Backpropagation. We incorporate diversified tactic calibration into the Expansion phase, resulting in our CARTS method, which comprises three steps: Selection, Calibration Expansion, and Backpropagation. Details each step are provided as follows.
Selection. In the selection phase, the algorithm starts from the root node and traverses the tree down to a leaf node. It uses a tree policy to choose child nodes that balance exploration and ex- ploitation. The tree policy at a tree node selects an action that maximizes the weighted upper confidence bound (WUCB) score, the WUCB score for each tree node is formulated as follows:
W(s, a) N(s,a)
(s..)) + w(s,a) N(s,a)
WUCB(s, a)
(I)
Here, N Nss,) denotes the count of how many times action a has been taken in state s and N(s, .) the total number of times any action has been taken state during the whole search. W
denotes the total value accumulated. Unlike the PUCT score used in DT-Solver (Wang et al. 2023) which incorporates probabilities estimated by the language model, we introduce weight (ss a) that represents both importance (model confidence) and diversity for the tactic at the current state. We will detail the weights in the calibration phase.
Calibration & Expansion. At this stage, multiple candidate tacties are generated from the lan- guage model, followed by verification through the Lean prover. Verified tactics that pass in Lean are calibrated and expanded into the search tree. Concretely, the proof generation model is designed to generate one-step proof tactic from given proof state along with conditional probability p(a]s). Typically, we use beam search to sample large collection of tactics (the quantity E) from the language model, which may result in much low probabilities for each tactic. This will lead to reduced exploration during the search process. To fix this, we apply a length penalty, defined as Upolicy (s, a) = pt (s}a), where is the token length of tactic a. This value reflects the model's confidence the importance of the current action.
4

---

Published as a conference paper at ICLR 2025
After verification by Lean, only tactics remain, denoted as {a1, 02, .... ae). Here, do not directly expand these tactics into the search tree because they often exhibit significant redundancy. Therefore, we need to capture the similarity between these tactics and then reorder them for both diversity and importance. We can compare the similarities between two actions using a pre-trained and fixed sentence encoder. However, directly using action similarity poses challenge: similar actions may lead to different next states, or dissimilar actions may result in the same next state. This undermines our goal of enhancing search diversity. Therefore, we assess next states similarities after executing these tactics. Formally, we denote the set of the next states as {s $2...., se),, where s represents the next state of following the execution of action ag We use a sentence encoder [ene(-), which has been already pre-trained on a large-scale corpus, to accept the textualized state and outputs high-dimensional embeddings. Then we utilize the MMR algorithm to reorder the tactics and calibrate the model confidence. The algorithm iteratively selects items (e.g., tactics in our context) from a candidate set to maximize the following objective function:
MMR(s, a.) = X Upolscy (8,a;) - - A) max Se) (een(())))) sJE8
(2)
Where, A is a parameter that controls the trade-off between importance and diversity. It typically ranges from 0 to 1. The calculation of the MMR score serves a calibration, effectively penalizing tactics with low diversity, as represented by the second term in the formula. The algorithm begins with an initial state set S = { and an empty action set A. While the size of A is less than the predefined value k which is smaller than E, the action with the highest MMR score is selected and added to A, along with its next state being added to S. Once k actions have been chosen, the set A returned. < e, we select all the tactics and reorder them. The value k serves as a constraint on the maximum number of expansion nodes. It is worth noting that we add the current state into the initial state set to mitigate the recurrence of identical states. The reason this way is effective is that our algorithm assigns lower MMR score to the actions when the next state closely resembles the current state. Algorithm]] I illustrates the complete process of diversified tactic calibration.
After diversified tactic calibration, obtain small set of actions A that contains both importance and diversity. Then, these actions are treated as edges, with their corresponding next state as nodes, which are expanded into the current search tree. For each edge a,, assign weight w(s, a,) max (0, MMR(s, a.)). utilized during the selection phase to assess the need for exploration. Unlike traditional MCTS (Koesis & Szepesvári (006) DT-Solver (Wang et al., (202)), our weights places greater emphasis on encouraging the exploration of tactics with high diversity.
Backpropagation. At this stage, we update the statistics of the nodes and edges along the search trajectory. We have bias-resistant value function V(s, a) which will be detailed in the next section, estimating the value of taking action a from the source node s. For a given trajectory, we use the value function to evaluate the value of the leaf node and accumulate this value along all edges in the path. Specifically, we update the weight of the edge recursively as follows: W(s,, (x) += V(s, a). where 8t and 0t represent the node and edge the trajectory. Additionally, increment the visit count for the edge: [st, az) += 1. This process ensures that the statistics reflect the outcomes of the simulations, allowing for improved selection in future iterations.
3.2 TESSSTATN VALUE FUNCTION
In HdMMCC-bbaad based methods, training value function is crucial (Polu & Sutskever 2020 Lample et al, 2022]. typically involving the creation of positive and negative samples using the policy network on training data. Positive samples consist of correct actions (or trajectories (Wang et al. (023)) ) from the dataset, while negative samples are those generated by the policy network that lead to undesirable states. Binary cross-entropy loss is then used to train the value network. Due to the hardness of verifying the correctness of actions not on the proof path, previous work (Polu & Sutskever 2020) often treats these actions as negative samples, resulting in an excessive number of negative samples, some of which are even inaccurate. This makes binary loss unsuitable and biases the value function. Furthermore, the domain gap between the training and test datasets also contributes to biases. In this paper, we conduct debiasing during both training and inference stages, as detailed below.
Training. To mitigate bias introduced by data collection, we first structure the dataset into pref- erence pairs of positive and negative samples. We utilize embedding model Sene effectively
5

---

Published as a conference paper at ICLR 2025
filter out noisy samples. Specifically, if fsn the next state from sampled negative action at the current state Spes is the correct next state and T is a threshold. This filtering ensures that the selected negative actions are more likely to be undesirable, thus reducing data noise. Moreover, train our bias-resistant value function. We employ the Bradley-Terry (BT) (Bradley & Terry 1952) model, a widely used technique for preference modeling. The BT model posits that the probability of action Opos being preferred over action aneg given state 8 is expressed as:
fenc((pos) (ennsss)TT(((ffpi
> T, discard the action s' is
adopt the preference modeling framework to
( (pos))
PP(pppe > aneg |)
(3)
exp( (V apos)) )) + exp (Vo(s, Aneg))
{(s!)) function (8, a) and estimate the parameters 0 by minimizing the negative log-likelihood.
Assuming access to the filtered dataset
a(t) )
1 we can parametrize the value
Preference modeling offers several advantages. Firstly, by only providing the relative superiority among samples, false negative samples do not require further processing. This is because we can reasonably assume that the correct proof steps provided the dataset are always optimal and align with human theorem proving's preferences. Additionally, since the dataset is presented in the form of preference pairs, this effectively oversamples (Shi et al.] 2023) the positive pairs, alleviating the issue of class imbalance between positive and negative samples, demonstrated in some studies (hhag et al. 2024 Pattnaik et al. 2024).
Inference. To mitigate the domain gap between the training and test datasets, we introduce an adjustment term into the value function during the inference stage. As previously mentioned, before calibration in CARTS, all E tactics should be processed through the Lean system to filter valid tactics. Intuitively, if the number of valid tactics is small, people will raise concerns about the capability of the current policy model, needing for reduced reward for the current action. We e/ E, representing the ratio between the number of valid define this reward adjustment as: generated by the language model at the current state. This tactics and the total number of tactics adjustment term serves as test-time adaptation to the test dataset. The final bias-resistant value function integrates both the trained value network and this adjustment term as:
0, - 1, (a Vo a)), otherwise.
s' has no child nodes, else if s' is the proved state,
V(s,a)
(4)
Where s' is the next state. Unlike the intrinsic reward introduced by DeepSeck-Prover- V1.5 Xin et al. 2024b), which only considers whether the search expands nodes, we consider both the ex- pansion capability of the policy network and the generalizability of the value network, forming final bias-resistant value function. The adjustment term can be interpreted as a form of test-time adaptation to the distribution of test data, thus mitigate the domain gap.
EXPERIMENTS
In this section, evaluate the theorem prroving performance of CARTS in Lean. We first de- scribe the experimental setup, then present the main results, followed by an analysis of our method. Currently, theorem-proving methods generation methods and tree search methods. Our approach is applicable exclusively to one-step tree search methods; therefore, we focus our comparison solely on this category.
primarily categorized into two main types: whole-proof
4.1 EXPERIMENTAL SETUP
Datasets. We follow Internlm-math YYing et al.) 2024b Wu et al. 2024) and DeepSeek-Prover V1.5 (Xin et al. 2024b), utilizing miniF2F benchmark (Zheng et al. 2022) and ProofNet benchmark Azerbayev al. 2023) for our evaluation. We specifically use the test split of miniF2F same as Xin et al. 2024b). which includes 244 problems ranging from basic algebra and number theory and also contains AIME and IMO challenging problems. ProofNet is benchmark for undergraduate- level mathematics, comprising 371 formal problems derived from widely-used undergraduate pure mathematics textbooks. It covers topics such real and complex analysis, abstract algebra, and

---

Published as a conference paper at ICLR 2025
Table 1: Results the miniF2F-test for various models and search methods. The highest perfor-
mance for each search method is highlighted in bold.
Model
Sample Budget
Search Method
miniF2F-tess
Tree Search Methods
COPRA(Code Llama) (Thakur et al.
2024
500
DFS
5.7%
COPRA(GPT-2) ) (Taakrr et al. 2024
60
DFS
9.0%
COPRA Thakur 2024
2024
60
DFS
26.6%
Llemma-78 (Azerbayev el al.
x 100
BFS
26.2%
Llemma-344B (Azerbayev et 2024
32 x 100
BFS
25.8%
LLMStep (Welleck & Saha 2023
32 x 100
BFS
27.9%
Curriculum Learning (Polu al..
2023
512
BFS
29.6%
MMermLLM-MMthh Ying ci al.
2024b
32 x 100
BFS
30.3%
Ying al.
2024a
32 x 100
BFS
43.4%
Xin
2024b
3200
RMaxTS
53.5%
DhepSeek-Prover-V1.55
Xin al.
2024b
3200
RMaxTS
55.0%
BFS 35.7%
MCTS
36.5%
Reprover-Leeade (229M)
Yang al. 2023
64 100
DTSolver
36.0%
CARTS
37.7%
BFS 38.9%
MCTS
39.3%
InternLM2--Mathhlus-- (Yng et al. 2024b
64 x 100
DTSolver 38.5%
CARTS
41.0%
BFS 48.8%
MCTS
46.7%
StepProver (7B) Wu ct al. 2024
32 x 300
DTSolver 46.3%
CARTS
49.6%
topology. This benchmark presents greater challenge than miniF2F, posing significant difficulties for theorem provers. Although the original versions both benchmarks are Lean3, we have modi- fied them Lean4 for CARTS's 's evaluation, aligning with the development of the Lean community.
Baselines models. We include baselines representing classical and state-of-the-art neural theorem proving in Lean. COPRA (Thakur et al. 2024) is in-context learning agent that utilizes general language models to generate tactics for finding the final proof. Llemma (Azerbayev et al. 2024) trained on extensive mathematical corpora. Additionally, we incorporate advanced models such as LLMStep (Welleck & Saha 2023). Reprover (Yang et al. (023). Curriculum Learning (Polu al., 2023). M22trnLM2-Math (Ying al. 2024b). and StepProver (Wu et al. 2024). All these models are based one-step tree search methods. We also include DeepSeek-Pron Prover-V V1.5 (Xin ctt al., 2024b), which integrates whole proof generation and tree search. However, not suitable for our CARTS, and thus, we mark it in gray.
Baseline models employ various search methods, such as depth-first search (DFS) (Thakur et al. 2024), best first search (BFS) Yangg et al. 2023), and monte carlo tree search (MCTS). Additionally, DT-Soller extends MCTS using virtual nodes, We compared the perfor- mance of BFS. MCTS, DT-Solver and CARTS Reprover (Yang et 2023), InternLMM-Math (Wu et al.) 2024). For MCTS and DT-Solver, we note- worthy that multiple tree search attempts with different seeds can be applied and ensemble (Polu & Sutskever 22200) Lin et al.) 2024 Xin et al.) 2024a); however, due to computational cost limitation, only compared the results for one single tree search attempt.
Search methods.
Ying et al. 2024b). and InternLM22SStpPrrovv
replace the value network with the intrinsic reward (Xin et al.) 2024b) for simplication.
Metrics. We evaluate the performance various search methods using the pass @ metric with budget B. Similar to (Xin et al. 2024b), if B is single value, it indicates the number of model

---

Published as a conference paper at ICLR 2025
Table 2: Results the ProofNet for various models and search methods.
Model
Sample Budget
Search Method
ProofNet
BFS
11.1%
MCTS
11.7%
Reprover-Lean4
Yang et 2023
64 x 100
CARTS
11.9%
BFS
18.1%
MCTS CARTS
18.3%
StepProver Wu et al. 2024
32 x 300
18.8%
Reprover-Lean4
StepProver
38
$0.0
36
47.5
45.0
Passi8 (9)
34
Pass@0 (%)
32
BF'S
BFS
30
MCTS
37.5
MCTS
28
DT-Sollver
35.0
DT-Solver
CARTS
CARTS
26
20
200
250
Expansion Budget T
Expansion Budget Y
Figure 2: Improvement curve in pass@1 for the miniF2F test the expansion budget varies. Left illustrates Reprover-Leand (Yang et al. 2023) and right illustrates StepProver (Xin et al., 20246).
generations used in tree expansions. If B = x T, E represents the number tacties generated per expansion, and I denotes the number of expansion iterations.
Experimental details. In terms of parameter settings, for Reprover-Leand Yang et al. 2023 ) we set À 0.8, and for MnterLL-M-MMahhPPhe Pluu--Puus-.8B (Ying al. 2024b) and StepProver (Wu et al. 2024). we set = 0.9. Additionally, we set k for models. We use the text embedding model selfffltt//ssaallll collection and training for the bias-resistant value function are presented in Appendix
(Wang et al. 2022 as the encoder fenc- Details regarding data
4.2
MAIN RESULTS
In Ta illustrate the pass@1 successful rate the miniF2F-test benchmark of various mod- els and search methods. Our proposed CARTS surpasses all compared search methods when the policy model is fixed. The results encompass different architectures and parameter sizes of lan- guage models, demonstrating that our method is more effective at search stage regardless of the policy model. Notably, we achieve 49.6% success rate the minil-2F-test, representing state-of- the-art performance among one-step tree search methods. Table 2 demonstrates the results on the ProofNet benchmark. Due to the dataset's complexity, current policy models exhibit low accuracy, which constrain the search performances. However, our proposed CARTS also achieves the highest performance compared to other search methods when the budget fixed.
Additionally, to demonstrate that CARTS has the superior search efficiency, we present a comparison of the pass performance among four search methods on miniF2F-test when varying the expansion budget, as illustrated in Figure It is evident that while the performance of different search methods comparable under a low budget, our method exhibits a significant improvement as the expansion budget increases. Furthermore, to other search methods. These findings demonstrate that our approach enhances the efficiency and effectiveness of tree search.
observed that the CARTS curve increases rapidly relative
8

---

Published as a conference paper at ICLR 2025
Table 3: Ablation study of various components of CARTS the miniF2F-test. We compare the pass @ performance across three models, with the highest performance highlighted in bold.
Model
Search Method
Reprover-Leand
Internl M2-MnMMM-M-hh-
StepProver
> Baselines:
BFS MCTS
35.7%
38.9%
48.8%
36.5%
39.3%
46.7%
> Ablations:
Diversified tactic calibration Bias-resistant value function
36.1% %
41.0%
49.2%
36.9%
40.6%
46.3%
CARTS (without adjustment term)
37.3%
41.3% %
49.2%
CARTS (Ours)
37.7%
41.0%
49.6% %
4.3 ANALYSIS
In this section, conduct detailed analysis of CARTS' effectiveness through experiments. We include ablation studies and specifically investigate the length distribution of results produced by CARTS, supplemented by several case studies.
Ablation for different components of CARTS. CARTS consists of two components: diversified tactic calibration and a bias-resistant value function. We isolated these components for analysis. Additionally, we compared the performance of CARTS without the adjustment term in the value function. The experimental results are shown in Table The results indicate that both components enhance performance, and their combination further increases the pass rate, suggesting that CARTS can significantly improve the efficiency of tree search exploration. Our findings reveal that for InterLL -atLLMh--Mah-PPP 111---Mat-PP------ Plus-1.8B, CARTS without the adjustment term achieves superior results, whereas CARTS with the adjustment does not perform optimally. We believe this is because the adjustment term merely a heuristic calibration; the policy model generates more unacceptable tacties, the less likely it is generate accurate tacties. This is not always valid due to differences between the properties of the proof state. Nonetheless, experiments across multiple models suggest that is generally effective for debiasing the value function.
Ablation study for k. The parameter & limits the maximum expansion number of nodes after di- versified tactic calibration. A smaller & significantly restricts the search space, potentially leading to performance degradation. Conversely, a larger expands the search space, increasing the likelihood of identifying the correct tactic. However, this comes at the cost of substantially increased search time, thereby reducing overall efficiency. To assess its impact on CARTS, we test multiple values of & using Reprover-Lean4 of Figure 3 As k increases, the pass rate initially improves, reaching a peak, and then gradually declines. This indicates that there is optimal range for that balances performance and search efficiency. Therefore, we recommend choosing a moderate k; such as = 8, in practice.
the miniF2F-test. The experimental results
shown in the left side
Analysis of the length distribution of discovered proofs. To comprehensively demonstrate the effectiveness of CARTS, we analyze the proof step lengths obtained by the Reprover- Leand model on the miniF2F-test. The results are presented on the right side of Figure 3 As illustrated, BFS yields a higher proportion of theorems with step lengths of one and two, but with none exceeding three steps. In contrast, CARTS achieves more theorems with lengths of three or greater, signifi- cantly outperforming both BFS and MCTS. This indicates that CARTS enhances search efficiency, enabling the exploration of longer proof chains within the same budget. Additionally, we find that CARTS discover two proofs with the length of five. We examine this case in detail in next paragraph.
Case study. We conduct a comprehensive case study to closely examine the results the CARTS search. Figure demonstrates theorem which is proved by CARTS Reprover-Leand model.

---

Published as a conference paper at ICLR 2025
38.5
38.0
31.7
37.7
37.5
31.3
100
36,9
36.9
37.0
36.5
80
36.5
Percentage
BES
Pass
MCTS
35.5
CARTS
35.0
34.5
34.0
34.0
37.6
BFS
DT-SSlvvrr CARTS
20
33.5
MCTS
33.0
8
16
24
48
56
64
Proof Length
Figure 3: The left figure shows the ablation study for k while the right figure illustrates the length distribution of proofs searched by CARTS, Both analyses are conducted the miniF2F-test using the Reprover-Leand (Yang et al. 2023 model.
Case: induction 12dvd
theorem inauction 12tp:iien__22dddddeepppp22222 (n N) 12 4 +1) +20
by
norm_num [Nat pow_suec induction' with n n_ih
case zero => simpa using n in rw [pow_succ) omega
Figure 4: Case study. Proved theorem induct ietptttionnn1vvvdi. 1dvvvveeep by CARTS in mini-
F2F-test of ReProver-Lean (Yang et al. 2023). This theorem is proved 77 expansions.
This case has proof path of five length. This theorem divisibility and its initial step involves simplification using norm num [Nat poo sucel. However, the tactic generated by Repover-Lean to other incorrect tacties. If the BFS approach is be applied, would necessitate the exploration of numerous redundant tactics before arriving at this specific action. Our experiments reveal that the CARTS improves the score of this tactic and increases its rank to six. Furthermore, we find that score of the second tactic, namely induction' of sixth to fourth. While the increase the ranking of the correct tactic score is only by two, the exponential growth in the complexity of tree search highlights the significance of early exploration of the correct action at the root node. Therefore, these improvements in rankings play a crucial role in successfully proving this theorem within limited number of expansion.
pertains to
exhibits a low confidence level, only ranking eight compared
with r.ih, improves from initial rank
CONCLUSION AND LIMITATION
In this paper, we presented CARTS, a novel approach that combines diversified tactic calibration with a bias-resistant value function for enhancing the performance of neural theorem proving. Our diversified tactic calibration effectively mitigates the redundancy in language model generations, promoting more diverse and balanced exploration of candidate tactics. The bias-resistant value function addresses the prevalent biases during both the training and inference stage, thereby refining the exploitation capabilities of the tree search by providing tactics. Experimental results on FiniF2F and ProoiNet have demonstrated that CARTS significantly outperforms existing one-step tree search methods, achieving state-of-ie of-the-an results.
accurate and reliable evaluations of
While CARTS has proven effective, it also has limitations. Our method currently only supports one- step tree search, whereas multi-step tree search, such as PeappSeek--reeee V1.5 (Xin et al. 2024b), has shown promise but is not supported by our approach. In the future, we will explore variants of CARTS that can be integrated into multi-step tree search methods.
10

---

Published as a conference paper at ICLR 2025
ACKNOWLEDGMENT
This research was supported by the Key Program of Jiangsu Science Foundation (BK20243012) Leading-edge Technology Program of Jiangsu Science Foundation (BK20232003), the Jiangsu Sci- ence Foundation (BG2024036) and the Fundamental Research Funds for the Central Universities (0221 14380023).. We would like thank the reviewers for their constructive suggestions.
REFERENCES
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. ProofNet: Autoformalizing and Formally Proving Undergraduate-LLvel Mathe- matics. arXiv preprint arXiv:2302.12433 2023.
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Al- bert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An Open Language Model for Mathematics. In Proceedings of the International Conference on Learning Representations, 2024.
Ralph Allan Bradley and Milton E Terry. Rank analysis of incomplete block designs: I. the method of paired comparisons. Biometrika, 1952.
Deepmind. AI Achieves Silver-medal Standard Solving International Mathematical Olympiad Prob- lems. 2024.
Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang. Angela Fan, al. The llama 3 herd of models. arXiv preprint arXiv:2407.2178. 2024.
Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-Proof Generation and Repair with Large Language Models. In Proceedings of the ACM Joint European Software Engi- neering Conference and Symposiun on the Foundations of Software Engineering, 2023.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof Artifact
Co- Co-Training for Theorem Proving with Language Models. Proceedings of the International Conference on Learning Representations, 2022.
John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Compu- tational Logic, volume 9, pp. 135-214. 2014.
Edward J Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. Lora: Low-rank adaptation of large language models. arXiv preprint arXiv: NVv:2/06.09685 2021.
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, Sketch, and Prove: Guiding Formal Theo- rem Provers with Informal Proofs. In Proceedings of the International Conference on Learning Representations, 2023.
Levente Kocsis and Csaba Szepesvári. Bandit based monte-carlo planning. In Johannes Fürnkranz, Tobias Scheffer, and Myra Spiliopoulou (eds.), European Conference on Machine Learning, vol- ume 4212, pp.
2006.
Guillaume Lample. Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree Proof Search for Neural Theo- rem Proving. In Proceedings of the International Conference Neural Information Processing Systems, 2022.
Yuanzhi Li, Sébastien Bubeck, Ronen Eldan, Allie Del Giomo, Suriya Gunasekar, and Yin Tat Lec. Textbooks all you need ii: 1.5- technical report. arXiv preprint arXiv:2309.05460 2023.
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. In First Conference on Language Modeling, 2024.
11

---

Published as a conference paper at ICLR 2025
Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-STaR: Learning to Interleave Thinking and Proving. arXiv preprint arXiv:2407.10040, 2024.
Leonardo de Moura and Sebastian Ullrich. The Lean Theorem Prover and Programming Lan-
guage. In Proceedings of the International Conference on Automated Deduction, 2021.
Pulkit Pattnaik, Rishabh Maheshwary, Kelechi Ogueji, Vikas Yadav, and Sathwik Tejaswi Mad- husudhan. Curry-dpo: Enhancing alignment using curriculum learning & ranked preferences. arXiv preprint arXiv:2403.0722 2024.
Lawrence C Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994.
Hanchwan Peng, Fuhui Long, and Chris Ding. Feature selection based on mutual information criteria of max- nux--epenndecy, max-relevance, and min-redundancy. IEEE Transactions on pattern analysis and machine intelligence, 27, 2005.
Stanislas Polu and Ilya Sutskever. Generative Language Modeling for Automated Theorem Proving. arXiv preprint (tX.iv:2009.0339990 2020.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal Mathematics Statement Curriculum Learning. In Proceedings of the Inter- national Conference on Learning Representations, 2023.
Qwen Team. Qwen2.5: A party of foundation models, September 2024.
Baptiste Roziere, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoging Ellen Tan, Yossi Adi, Jingyu Liu, Romain Sauvestre, Tal Remez, et al. Code llama: Open foundation models for code. arXiv preprint arXiv:2308. /2950, 2023.
Jiang-Xin Shi, Tong Wei, Yuke Xiang, and Yu-Feng Li. In Proceedings of the International Confer- ence on Neural Information Processing Systems, 2023.
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Mare Lanetot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et General Reinforcement Learning Algorithm That Masters Chess, Shogi, and Go Through Self-Play. Science, 2018.
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An In- Context Learning Agent for Formal Theorem-Proving. arXiv preprint arXiv:2310.00333,, 2024.
Trieu H Trinh, Yuhuai Wu, Quoe V Le, He He, and Thang Luong. Solving Olympiad Geometry without Human Demonstrations. Nature, 2024.
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-Tres -ree Sampling Guided by Proof-level Value Function. Proceedings of the Annual Meeting of the Association for Computational Linguistics, 2023.
Haiming Wang. Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, et al. Proving Theorems Recursively. arXiv preprint arXiv:2405. 144144 2024a.
Liang Wang, Nan Yang, Xiaolong Huang, Binxing Jiao, Linjun Yang, Daxin Jiang, Rangan Ma- jumder, and Furu Wei. Text embeddings by weakly-supervised contrastive pre-training. arXiv preprint arXiv:22 2022.
Ruida Wang, Jipeng Zhang. Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang Theorem- laam: Transforming general -prrpose 1lms into lean4 experts. arXiv preprint arXiv:2407.03203. 2024b.
Sean Welleck and Rahul Saha. LLMSTEP: LLM Proofstep Suggestions in Lean. In International Conference on Neural Information Processing Systems Workshop on MATH-AI, 2023.
Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. Lean gith-g: Compiling github lean repositories for versatile lean prover. arXiv preprint 240i /7227, 2024.
12

---

Published as a conference paper at ICLR 2025
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeck-Proven Prover: Advancing Theorem Proving in LLMs through Large- Scale Synthetic Data. arXiv preprint 1433133300.. 2024a.
Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Zhao Wanjia, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang. Zhibin Gou, Z.F. Wu, Fuli Luo, and Chong Ruan. DeepSeek-Provee Prover-V1.55 Harnessing Proof Assistant Feedback for Rein- forcement Learning and Monte- Cante-Carlo Tree Search. arXiv preprint arXiv:2408.08/52. 2024b.
Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et LEGO-Prover: Neural Theorem Proving with Growing Libraries. In Proceedings of the International Conference on Learning Representattons, 2024c.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In Proceedings of the International Conference on Neural Information Pro- cessing Systems, 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:2406.03887, 2024a.
Huaiyuan Ying. Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, al. InternL.M-Math: Open Math Large Language Models Toward Verifiable Reasoning. arXiv preprint arXiv:2402.06332. 2024b.
Xuan Zhang, Chao Du, Tianyu Pang, Qian Liu, Wei Gao, and Min Lin. Chain of preference opti- mization: Improving offiin-o--thuugee reasoning in llms. arXiv preprint arXiv:2406. 2tt.:240600911666 2024.
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. Transactions on Machine Learning Research, 2024.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics. In Proceedings of the International Conference on Learning Representations, 2022.
13

---

Published as a conference paper at ICLR 2025
A DETAILS OF BIAS-RESISTANT VALUE FUNCTION
Data Construction To train our bias-resistant value function on Lean4, we utilized two data sources. The first source is the random portion of the beandojo.bencharee (Yang et al. 2023), which derived from mathlib4 (commit: 3ce43cl 8 (16111866666611e11 617
620EE),
The second source is Lean-Github (Wu et al. 2024). recently released dataset compiled from over 100 Lean 4 repositories. We employed
(Ying et al. 2024b) to gen- erate eight candidate tactics for each proof state in the dataset. Tactics that differed from the correct tactic in the generations are used as negative samples, which we then paired with positive samples form preference pairs. However, as discussed in the main text, this dataset contains signifi- cant noise, with positive and negative samples being semantically similar, as illustrated in Figure 5 To address this, filtered the samples based on their similarity, using the embedding model intfloat / 155-mmll-vv2 (Wang al. (2022) and threshold 0.85. After filtering, the dataset consists of 1,797,951 (about 1800K) training preference pairs and 2,000 test preference pairs.
STATE:
STATE:
case 0.h
case a. Type
Type
n Type
n Type
Type
a Type
inst=
DecidableEq
inst-
DecidableEq
inst+3
Fintype
inst= Fintype n
inst#2
DecidableEq
inst+ DecidableEq
inst+3 Fintype
insted Fintype m
inst* CommRing
inste CommRing
A Matrix n
A Matrix n n
nn (x Perm n),
+
V (x Perm n),
x univ
univ
1: (Pi.single j 1) (ix i_1) i_1
t'(tsign x)
updateRow A I
tiCtsign x)
i_1
updateRow A
(Pi.single j 1) C1x i_1) i_
M1ssgg x) L111
updateColurn
MiCtsign x) П L1
updateColumn A
j (Pi.single 1) (tx i_1)
j (Pi.single 1) (tx i.1) i_1
POSITIVE ACTION:
POSITIVE ACTION:
intro
intro NEGATIVE ACTION:
NEGATIVE ACTION:
intros 6
simp only [updateRow_apply updateColumn.opply)
Before Filtering
After Filtering
Figure 5: This illustrates example of our dataset organization: the left side contains unfiltered data with noise, while the right side shows the samples after filtering.
Training Details We utilized the mi crcoooottphi- i-15 model (Li et al. 2023 which contains 1.3 billion parameters. Phi-1.5 has been trained on large-scale code corpus, endowing it with a strong understanding of formal languages. We fine-tuned the model using LoRA (Hu et al. (021) for one training epoch, using the learning rate as x 10-4 After training, the model attained an ccuracy of 94.10% on the test dataset. The training loss curve and validation accuracy curve illustrated Figure 6
B EFFECTIVENESS OF BIAS-RESISTANT VALUE FUNCTION
In this section, we supplement experiments to demonstrate the effectiveness our bias-resistant value function and draw the following conclusions: The Bradley-Tery (BT) model effectively
addresses the issue class imbalance training the value function. 2. Our analysis underscores the critical importance of data filtering and provides way for determining the hyperparameter
14

---

Published as a conference paper at ICLR 2025
Training Loss
Eval Accuracy
onginal smoothed
onginal smoothed
0.90
Wval
0.75
0.3
0.70
0.1
20000
42000
60000
80000
100000
20000
60000
80000
100000
Steps
Steps
Figure The training loss curve and the validation accuracy curve.
B. ANALYSIS BETWEEN BT AND CE
We reconstruct the pairwise dataset and employ various models validate the effectiveness of the BT modeling approach for the value function. Unlike the main text, where both Leandojo..eenchmack (Yang al. 2023 and Lean-Githup (Wu et al. 2024) are utilized as data sources, this analysis exclusively uses Leandojo benchnark for trainin. with its test split serving as the evaluation dataset. Furthermore, data frome Lean-Github are employed for Out- of-Distribution (OOD) evaluation. To enable training of Cross-Entropy (CE) loss, we convert the pair-wise datasets into the binary classification datasets. The training data exhibits an imbalance between positive and negative samples (approximately 5), while we ensured that both test sets remains class- balanced. Detailed statistics of the dataset are presented Table
Table Statistics of our constructed dataset.
Count
Split
For BT
For CE
Train
694,600
861,186
Test
3,465
6,930
Test-00n
3,499
6,998
We conducted training on three models to compare the differences between BT and CE, including Qwen-2.5-0.55 (Qwen Team 2024). Llama3.2-1P (Dubey et al.] (024),, and Llama3.2-3B (Dubey et al. 2024p. We evaluated the accuracy (Acc) on Test and the out-of-distribution accuracy (Acc- OOD) Test-O00 All experiments
full fine-tuning for one epoch with learning rate of le-5. The experimental results are presented in Table 5
The experimental results show that BT significantly outperforms CE in terms in-domain accuracy, highlighting the advantages of using BT for modeling. Furthermore, we observe slight perfor- mance improvement in BT as model size increases; however, the improvements remains relatively small. We attribute this to the limited dataset size, which hinders the emergence of clear scaling properties. addition, we observe that CE shows poor performance in scenarios with a significant domain gap, and its accuracy is almost the same as random guessing, In contrast, the BT model achieves approximately 5% improvement in such cases, although its overall performance remains limited. We believe this is due to the significant domain gap between the and Lean-Githur datasets, making the task inherently challenging. (Note: In our main text, both datasets were included in the training set to mitigate the gap with miniF2F.)
15

---

Published as a conference paper at ICLR 2025
Table 5: Results between BE and CE of different models.
Model
Method
Acc (%)
Ace-OOD (%)
CE
63.2
50.9
Qwen-2.5-0.5B Qwen Team
2024
BT
76.5
55.2
CE
67.4
52.2
Llama3.2-1B (Dubey et al.
2024
BT
76.6
54.6
CE
63.0
50.7
Llama3.2-3B (ubey et al.
2024
BT
77.7
56.0
B.2 ANALYSIS OF DATA FILTERING
In Section 3.2 we introduced filtering step for the data constructed. Here we conduct experiments to analyze the necessity of this step. Specifically, we perform an ablation study on the filtering process using the Qwen-2.5-0.5B model (Qwen Team 2024), comparing the model's performance before and after applying filtering. The results in Table demonstrate that filtering improves the model's ' performance. We have presented examples of noise introduced by the absence of filtering in Figure 5 further highlighting the necessity of this step.
Table 6: Ablation study of data filtering.
Method
Acc
Acc-OOD
Before filtering
76.2
54.9
After filtering
76.5
55.2
The choice of r represents a trade-off: setting it too high introduces excessive noisy data, while setting too low reduces the number of training samples. To provide insight into the selection of r, we analyze the similarity distribution of positive and negative samples before data filtering, as shown Figure 7 The results reveal bimodal distribution. Higher similarity values indicate a greater likelihood of noisy samples, leading to hypothesize that one of the components corresponds to noise. Using Gaussian Mixture Model (GMM) analysis, we identify an approximate threshold of 0.87 distinguish noisy samples. Consequently, the selection of 0.85 for in the main text is considered reasonable.
GMM Component 1
6
GMM Component 2
5
Density
4
3
2
0.70
0.75
0.80
0.85
0.90
0.95
1.00
Similarity
Figure 7: The distribution of similarities between positive and negative samples.
16

---

Published as a conference paper at ICLR 2025
C
EXAMPLE SOLUTIONS
We show several typical theorems proven by CARTS below.
Case 1: mathd algebra 148
theorem mathd_ aar_aalgebb_____ 148 (a R)
(f R-+R)
(ho Vx, f =c *x"3 *x +3)
(h1 f =9) =3 by
reases or_or_n 1 with ho he cases C
all_goals simp_all [ho]
on_goal norm_num linarith only [ho, hi]
Figure 8: Case 1. Proved theorem mathd algebra 148 by CARTS in mini-F2F-test of
ReProver-Lean Yang et 2023). This theorem is proved 68 expansions.
Case 2: mathd wwmbertthoryrree..oo. .234
theorem nathi_numbercheor__244 (a b N) (ho 1 Sa Aa 59 Ab <9)
(hi (10 +b) =912673)
a +b : by
simp only [Nat. one Le_iff__e_eeeeeeeeeeeeeee___eeee ne__oo]__err] at ho obtain (h2, as, n4) interval_casee <;> anterval_casen b <イ> simp_all
Figure 9: Case 2. Proved theorem MMeemLMM-PPlus-I.. (Ying al. 2024b). This theorem is proved in 12 expansions.
by CARTS in mini-F2F-test of
17

---

Published as a conference paper at ICLR 2025
Case 3: mattho...
theorem mathd_ hathh__nubberhheoy__uku
(n A B c N)
(ho n =3-17 +3"10)
(hi 11 (n +1))
(hg
.Pairwise ((-1)
(hs (A, [Finset. Ice 9)
thu Odd & AOdd C)
(hs -3 1
(he Nat.digits 10 -I,, (,
100 *A +10 *B +C -129 ;-
by
[ho] at h
simp [ho]
linarith [h6]
Figure 10: Case 3. Proved theorem mathd www.ddnmmberthhhee -135 113 by CARTS in mini-F2F-test of I (Yang et al. 2023). This theorem is proved 38 expansions.
Case 4: mathd www.hrthorbberrry..oooommmmm 314
theorem mathd_numberrheery__33 (r N)
(he I =1342 & 13)
(hr < n)
(ha 1342 n)
(ha n $ 13 < r)
6710 In :=
by
obtain (k, hk) :-hg
contrapose! h1
[hk] at h1
have he < = linarith interval_case cases <;> simp all
Figure 11: Case 4. Proved theorem mathd numbertheory 314 by CARTS in mini-F2F-test of StepProver (Wu et al. 2024). This theorem is proved in 159 expansions.
Case 5: artin exerci se 13 6 10
theorem svercise_13_5 {K : Type*) [Field [Fintype k*1
(TT x K*, x) --1 :-
by
have h simp only [inv_inv] at haveI DecidableEq K :=Classical, decEq K apply FiniteField. univ units id eq neg
: K", x -IIx K", -11 :-by congr
Figure 12: Case 5, Proved theorem artin in exercise ise 13 10 by CARTS in ProofNet Step- Prover (Wu al. 2024 This theorem is proved in 119 expansions.
18


Reviews:
[{"review_id": "LgUEAMvnN0", "reviewer": "Reviewer_kceZ", "summary": "The paper propose to improve MCTS for Neural Theorem Proving. It adds a measure of diversity in the exploration that takes into account the diversity of the tactics searched.", "questions": "Does your method scale with more budget?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "The paper addresses a hot and interesting topic.\nThe experimental results show better results than alternative search algorithms.\nThe experiments are well illustrated", "weaknesses": "Only one step tree search is supported.\nLack of experiments with more processing power.", "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": "GHdSR3wvpg", "reviewer": "Reviewer_cJwa", "summary": "This paper introduces two major improvement over the MCTS-based theorem proving framework: (1) diversified tactic calibration which re-scores generated tactics, by the [MMR algorithm](https://www.cs.cmu.edu/~jgc/publication/The_Use_MMR_Diversity_Based_LTMIR_1998.pdf) for diversity-based re-ranking; and (2) bias-resistant value function, with embedding-based tactic filtering and preference modeling with the Bradley-Terry model. Take Reprover-Lean4 (a 0.3B model) as an example, the proposed method CARTS reaches 37.7%, while its MCTS counterpart is 36.5%.", "questions": "Please see the weakness part.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "- **Impact**: The paper is well-motivated -- improving the efficiency of tactic search and the accuracy of the value function addresses key challenges that practitioners in this field are eager to solve.\n- **Originality**: Both designs of tactic calibration and bias-resistant value function are new and useful (incremental) contribution to the existing theorem proving framework. \n- **Writing**: The paper is very well-written and easy-to-follow.\n- **Practicality**: The proposed method looks to be easy-to-implement, and authors have provided relevant codes. It would be nice if this could be made as a modular design that can be plugged into different pipelines/repositories.", "weaknesses": "My concerns are mostly on experiments.\n- Both designs are non-trivial, however, it looks like the improvement over the MCTS benchmark is rather marginal. How many independent runs were used? Could the authors report the confidence interval, or provide some discussions on this?\n- CARTS is based on MCTS (is this correct?); i wonder if it could be applied on top of BFS as well. Also, what is the value function used for BFS and MCTS in the tables? Do they use the model likelihood or some other value models?\n- In Line 267, how to determine $\\tau$? Could the authors do some ablations on this?\n- Could the authors evaluate the method on more benchmarks, e.g., LeanDojo (i.e., mathlib theorems)?\n- The paper uses the phi-1.5 model as the base model for the value function. There has been controversy or potential ethical concerns on this model (e.g., Schaeffer, Rylan. \"[Pretraining on the test set is all you need](https://arxiv.org/pdf/2309.08632).\" arXiv 2023), though not directly relevant to theorem proving tasks. Could the authors do some ablations with other models, like llama-3.2-3b? Orthogonally, it might be nice to check if the performance will improve as the value model scales up. By the way, please add the model parameter count to reprover and stepprover in the tables.\n\nOverall, i think the paper is well-written and brings useful information to the community, and I lean towards acceptance. I am happy to raise my score if the authors can further address the above concerns.", "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": "x9Fr7pRtbU", "reviewer": "Reviewer_JC1S", "summary": "This work proposed two ways to enhance neural theorem proving performance. One is to caliberate generated tactic, which can alleviate the problem of tactic redundancy and further helps to diversify the proof path. The second is to use bias-resistant value function by introducing preference modeling and adjustment according to valid tactic ratio. Experimental results show the combination of this two components could achieve remarkable performance gain.", "questions": "1. What's the comparison beween this method and other related method in terms of running efficiency? It would be great to clarify this point.", "limitations": "", "rating": 8, "confidence": 2, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "1. The presentation of this paper is very clear, vitual demonstration is easy to understand as well.\n2. The proposed method is reasonable and well-motivated, the first component is motivated by the redunancy of generated tactic and the second component is motivated by common gap-bias between different dataset. \n3. The reported results is good and stable, it can be applied to many existing methods and achieve a boost in performance.", "weaknesses": "1. The proposed method is not that generalizable for now, as it can be only applied to one-step tree search methods. \n2. The operating logit looks a little bit complex, raising concern about the running effiency, for example, in the tactic calibration process, this method need to run the tactic to get the next state at first and then perform MMR algorithm, which could be time-consuming.", "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": "evWRNwpksS", "reviewer": "Reviewer_YALN", "summary": "This paper designs a new search algorithm for formal theorem proving called CARTS. Compared with the standard MCTS algorithm, CARTS encourages diverse tactics that lead to significantly different next states. This paper also trains a value function using pairwise feedback. When applied to three different models, this paper shows that CARTS outperforms baseline methods such as best-first search and MCTS on miniF2F-test and ProofNet at the test time (in other words, the model that generates the tactic is not trained).", "questions": "-\tHow good is the off-the-shelf sentence embedding model when applied to Lean’s states? Since the standard sentence embedding model is trained on natural language data, it is unclear to me whether they can distinguish the subtle differences in Lean’s states. Can you show some concrete examples to demonstrate the performance of $f_{enc}$?\n-\tIs there a typo in Eq (1)? Currently, the bonus term might be bigger than 1 if the action a is only taken a few times.\n-\tIn Table 3, what is the algorithm for the “Bias-resistant value function” row? Is the value function the only difference to CARTS, and how is the alternative value function trained?\n-\tThe choice of the Bradley-Terry model sounds arbitrary, although the argument that the BT model effectively oversamples the positive pairs makes sense. Is the value function trained with BT model better than the value function trained with binary cross entropy loss with explicit oversampling of positive examples?\n-\tCan w(s,a), or MMR(s,a), be negative? If w(s,a) is negative, the exploration bonus (the second term in Eq. 1) is then increasing when action a is taken more times.\n-\tIn the ablation for k, the conclusion is “as k increases, the pass@1 value generally decreases”. What about even smaller k such as k = 1,2,4? Intuitively the performance when k=1 should be very bad.\n-\tThe case study in Section 4.3 shows that the ranking of the right tactic is improved. This could be a good place for more ablation studies. Which feature of the algorithm contributes to this improvement, length penalty, MMR, the new value function, or the adjustment term?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 4, "contribution": 4, "strengths": "-\tThe algorithm, CARTS, introduces a more aggressive exploration strategy compared with the standard MCTS algorithm, by encouraging the diversity of the next state using the MMR algorithm. While the idea of encouraging the diversity of next states is explored in prior works such as [1], using an embedding model to measure the diversity of the next state is novel.\n-\tThis paper identifies the label imbalance problem when training the value function, and mitigate this issue by training the value function using pairwise feedbacks.\n\n[1] Xin, Huajian, et al. \"DeepSeek-Prover-V1. 5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search.\" arXiv preprint arXiv:2408.08152 (2024).", "weaknesses": "My major concern is the statistical significance of the results. On the one hand, the CARTS algorithm in this paper has many new components compared with the standard MCTS algorithm, and the design of the new components seems arbitrary (or at least heavily relies on vague heuristics). On the other hand, the improvement of CARTS on miniF2F-test is less than 2%. Since the miniF2F test set only has 244 questions, it means that the difference only comes from a few questions, which is not significant enough given the complexity of the algorithm design.\n\nA few claims in the paper are not justified by empirical evidence:\n \n-\tLine 86: “This could result in label imbalance, causing the cross-entropy loss used in training, the value function to easily converge to local optima.” Why does label imbalance with cross-entropy loss lead to local optima?\n-\tLine 287: I don’t see how the adjustment term can mitigate the domain gap between the training and test datasets. The following sentences in this paragraph are irrelevant to the domain gap.", "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)