3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
Authors: Sean Lamont
Christian Walder
Amir Dezfouli
Paul Montague
Michael Norrish
Venue: NeurIPS 2025 poster ()
Keywords: theorem proving
proof search
diversity
representation learning
Primary area: deep_learning
TL;DR: Learning proof system dynamics, pruning proof search based on diversity and expected outcome

Abstract: A key challenge in automated formal reasoning is the intractable search space, which grows exponentially with the depth of the proof. This branching is caused by the large number of candidate proof tactics which can be applied to a given goal. Nonetheless, many of these tactics are semantically similar or lead to an execution error, wasting valuable resources in both cases. We address the problem of effectively pruning this search, using only synthetic data generated from previous proof attempts. We first demonstrate that it is possible to generate semantically aware tactic representations which capture the effect on the proving environment, likelihood of success, and execution time. We then propose a novel filtering mechanism which leverages these representations to select semantically diverse and high quality tactics, using Determinantal Point Processes. Our approach, 3D-Prover, is designed to be general, and to augment any underlying tactic generator. We demonstrate the effectiveness of 3D-Prover on the miniF2F and LeanDojo benchmarks by augmenting popular open source proving LLMs. We show that our approach leads to an increase in the overall proof rate, as well as a significant improvement in the tactic success
 rate, execution time and diversity. We make our code available at https://github.com/sean-lamont/3D-Prover.

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
Sean Lamont 12, Christian Walder Amir Dezfouli', Paul Montague", Michael Norrish'
Australian National University
Defence Science and Technology Group
GGogge DeepMind
*BIMLOGIQ sean. lamont@annu edu. au
Abstract
A key challenge in automated formal reasoning is the intractable search space, which grows exponentially with the depth of the proof. This branching is caused by the large number of candidate proof tacties which can be applied to given goal. Nonetheless, many of these tactics are semantically similar or lead to an execution error, wasting valuable resources in both cases. We address the problem effectively pruning this search, using only synthetic data generated from previous proof attempts. We first demonstrate that it is possible to generate semantically aware tactic representations which capture the effect on the proving environment, likelihood of success, and execution time. We then propose novel filtering mechanism which leverages these representations to select semantically diverse and high quality tactics, using Determinantal Point Processes. Our approach, 3D- Prover, is designed to be general, and to augment any underlying tactic generator. We demonstrate the effectiveness of 3D-Prover on the miniF2F and LeanDojo benchmarks by augmenting popular open source proving LLMs. We show that our approach leads an increase in the overall proof rate, as well as sigmificant improvement in the tactic success rate, execution time and diversity. We make our code available at
com/sean
Prover
Introduction
Interactive Theorem Proving (ITP) traditionally involves human guiding an ITP system verify formal proposition. The applications range from secure software (Tan et al. 2019) to the verification of mathematical results (Hales al. 2017). There has been significant interest in automating this
process, with formalization efforts requiring high level of human expertise (Klein et al. 2009). It also considered 'grand challenge' for AI, requiring a high level of reasoning and planning to
be successful (Reddy 1988). Even large general purpose models struggle with the complexity of the task, with for example GPT-4 only able to solve 13.5% (Thakur et al. (023) of the high school level minis2F-test (Zheng et al. 202T) benchmark. This has motivated specialized models and search algorithms to address the unique challenges of the domain (see e.g. (Li et al. 2024) for a review).
With most non non-trivial proofs requiring long chains of correct reasoning, it is challenge to generate them in one pass without mistakes. The addition of a search algorithm common for addressing this (Xin et al.) 2024 Wu et al.] 2024). Under this paradigm, candidate tactics are generated and executed the proving system, which (if successful) results new subgoals to prove. This generates a tree of possible proof paths, where search algorithm selects the most promising nodes to expand. The primary challenge faced by these approaches the exponential growth in the number of proof paths, limiting the complexity of the problems that can be solved efficiently. Many of the generated
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

a,0,0:
be
simp
[__1]
Db_1]
xw h_1
subat
syumetry
simp Di_1, 2_
Ew [b_1, h_2]
a abcc::C
a, a,b,c:
a, b,b.c:C.
No 10
bg a b
ho 1h:4t 6- 20
Enror: Unknown identifier lgg
h1 :i:==1
F ai + bi -2
hy h1:c= i
+i
} --2 = ac + Dc
An example node expansion for a failed ReProver attempt, which 3D-Prover was able to prove. Tactics the left result in the same proof state, tactics the right result in error, and tactics in the centre result a unique proof state. The high error rate and tactic similarity motivates filtering approach, which prunes the search space to give a diverse of subgoals.
Figure 1:
tactics are equivalent, modulo variable renaming and other comaantics-preserviinn transformations. See Figure for sample search tree from ReProver Yang et al. 2023), where several semantically similar paths are explored, wasting valuable resources. Simple lexical similarity scores fail to cover the semantics (meaning) of tactic, captured by the effect of the tactic the environment. For example, an expression and its negation vary by only single character, but have a large semantic difference. It is therefore desirable to filter tactics by their semantic rather than syntactic diversity, In addition, many tactics lead to an execution error from the prover. From our experiments with miniF2F, find approximately 75-85% of tactics result in execution error (Section 2.2) As tactic execution can be expensive, this further restricts the space proofss which can be explored efficiently.
These challenges motivate our proposed approach, Diversity Driven Determinantal Point Process Prover (3D-Prover). 3D-Prover adds an extra 'dimension' to existing proving systems by including a filtering mechanism top of the existing tactic generation and search components. 3D-Prover uses Determinantal Point Processes (Kulesza 2012) to prune the search space by filtering tactics to diverse and high quality subsets. The rich synthetic data generated from proof attempts enables to learn the effect tactics have on the environment, including the error likelihood and execution time. We leverage this to generate tactic representations which reflect their semantics, which 3D-Prover uses to filter tactics based on a combination of their diversity and quality. 3D-Prover allows for direct tradeoff between search objectives, with hyperparameters controlling the weighting of error, time and diversity in the filtering process. 3D-Prover is a general approach which can be used to augment any underlying tactic generator. We demonstrate this by augmenting the popular ReProver and InternI m2...M2.55. M2. M2.5-Step--Prove LLMS to obtain significant improvement in the success rate, execution time and diversity of tactics, and the overall proof success rate. To summarise our contributions:
We study the fcasibility of learning the environment dynamics of proving systems. We demonstrate tactic representations which capture the likely effect the environment, using them to predict the likelihood success and execution time of a tactic, as well as the resulting proof state error message.
We propose novel edge filtering approach using Determinantal Point Processes (uleezza & Taskar 201T). which leverage these representations to select semantically diverse subsets of quality tactics. Our method is modular and can be used with any tactic generator.
We evaluate our approach by augmenting ReProver (Yang et al., 2023) on the miniF2F (Zheng et al. (202T) benchmarks, where demonstrate significant improvement in the tactic success rate, diversity and overall proof rate.
1.1 Related work
There is little prior work on learning the effect of tactic on the proving environment, with only Xin et al.](222.))) (2024) using successful environment responses as an auxiliary objective. We investigate the task in detail, well learning the error likelihood, error messages and execution time, which

---

we use to generate useful tactic representations. Several approaches use previous proof attempts to improve performance, using the sparse binary signal from the proof result (Li al. (024). This has been used to improve search (Lample et al. 2022 Wang et al. 2023), however these approaches do not consider node diversity, with nothing preventing the exploration of semantically similar paths. First & Brun (2022) examine diverse ensemble of tactic models, whereas we focus on diversity with respect to the search, given an arbitrary underlying tactic model (or models). Recently, Yang et al.) (2025) select subgoals based on their diversity, with simple embedding model over the subgoal text. Our approach does not need to execute the tactics, as we learn embeddings reflecting the environment dynamics and use these to select tactics before execution, thereby saving resources.
1.2 Background: Determinantal Point Processes
Determinantal Point Processes (DPPs) are a class of probabilistic models for sampling subsets from a ground set y. They provide an inherent trade-off between the diversity and quality of the sampled subsets, successfully being applied to this end across a variety of domains (Kulesza 2012, Hsiao & Grauman 2018 Zhang et al. 2016). This motivates their use in our filtering approach (Section 3
In line with Kulesza 2012). for [>] = n we define the kernel I. E R of DPP as the Gram matrix L = B B for B E Raxdd where row b, E IRd of B represents element é E {1....,n.) n3 of y. The b, are commonly decomposed into a set of unit norm diversity features Φ; E I2 and quality scores q: E +R so that b; = y: || = 1 for all E (1..... ..). The similarity matrix S is then defined as S.j = of Φ,. The probability of sampling C y is then proportional to the determinant of the submatrix of T. indexed by A, (PA) xx det( = (ITaa of de)()(())) Geometrically, this determinant is the volume of the parallelepiped spanned by the submatrix LA, which as we see in Figure 3 is maximised based on combination of the similarity and length (quality) of the chosen elements. In this way, DPPs elegantly trade off between the quality and diversity of elements. Normally the size of the sampled subset |A| is variable, however Kulesza & Taskar (201 I) introduce k-DPPs which restricts the size of the subset to fixed k E N. and where the probability of sampling A is normalised over subsets of size k. That is, for a k-DPP, P(A) = det(La)) Σ |A| det(Lar)..
||
2 Transition Aware Representation Learning
One proof attempt can generate large amounts of data. We found a single pass of ReProver on the miniF2F-valid benchmark of 244 proofs results in approximately 500,000 transitions, capturing rich information about the error likelihood, execution time and resulting proof state or error message. We now explore the feasibility of using this data to learn how tactics affect the environment, operational- ising this as a supervised learning task: given a goal and tactic, we predict the error status, execution time and environment output. We effectively learn these targets from only this synthetic data, and embed this information into compact tactic representation. The upshot, as we show in Section B is that this can be used improve the performance of subsequent proof attempts.
2.1 Transition Models
The result of proof attempt (formalised in is the dataset DD of transitions { I, 8, 8, o)}, which captures the results of applying tactics / E 7 to goals g E S. The status E {0, 1}. indicates a success (1) or failure (0), r E IR gives the execution time and the output o e O is the environment response, which is an eтror message, new subgoals, or a proof success. We propose a method to learn tactic representations
Rdd which capture the result (s, T, o) of applying to g. By using these as features for DPP, we can filter tactics based on their expected outcome, before they are executed.
We define our transition model {: S x T - [0, 1] x R O as mapping from a goal g and tactic t to an estimate of the status s, time 7 and output o. To ensure & admits effective representations in e, we construct it follows. The Encoder E S T + Rd takes the goal g and tactic t as input, and outputs our representation E(g, () = e. As e will be used as the diversity feature for DPP, it is constrained to unit norm |/e| = L. The Predictor P: R + 00 1] x RR maps e to an error probability for the status and score for the time prediction, with P(e) (s, f). The Decoder D Rdd x - O
maps e and g to the output prediction, such that D(e, g) = ô. The transition model is then
E(g.t) (P(E(g, t)), D(E t), .)) (5.
(I)
3

---

Takenizo and combine goal tactic
Create goal lactic embedcing
Train embedding encodo transition data
Stat-u (+)
Encoder
Predictor
rv
E
2v [b_1]
Time
Oatput (6)
concel
Decoder
a, a,b,c: C
u.d.0 ho:a+b=2 hiiems
Ap: Ap:at.0 2c hy:0=s
ai
F Fcc do -2
Figure 2: Our COMBINED architecture for learning transition aware tactic embeddings. The tactic t and goal g are concatenated and passed through the Encoder E. A representation vector e is generated by mean-pooling over the tactic token embeddings t'. The Predictor /' takes this embedding and predicts whether the tactic results in an error (Status), and the execution time (Time). The Decoder D takes the embedding and goal to predict the environment response (Output), which is either error message or new goals to prove. This setup yields a compact representation of the tactic which captures its effect the proving environment, enabling our proposed filtering model.
We note that the Decoder and Predictor only access information of through Hence architecture requires the Encoder to learn an effective representation for e, so that the Decoder and Predictor this to determine the subsequent effect of the tactic the environment.
Experiments
For our experiments, we use an Encoder- Decoodrr-Decderr Transformer for the Decoder D, and an Encoder- Only Transformer for the Encoder E. We take the pretrained ReProver (Yang et al. 2023) LLM to initialise both components. We implement the Predictor P as a single hidden layer MLP, with hidden dimension d/2 (where d 1472) and two real valued output nodes. The time prediction O is the output of the first node, and the status prediction is taken as the sigmoid of the second. We use this simple Predictor architecture to speed up our filtering algorithm presented in Section
investigate several variations of transition model Ç. For the COMBINED model (Figure 2 the tactic is concatenated with the goal, and the embeddings from the Encoder are computed for all tokens. then generate a single tactic embedding by mean-pooling over the tactie tokens. We examine the COMBINED model both with the full goal text, and variation COMBINED (SMALL. GoAL) which embeds the goal first, and concatenates as single token vector to the tactic. This variation allows for more efficient batching when used for filtering in Section [ as the goal need only be embedded once for multiple tactics, however gives less information to the model. The SEPARATE model encodes the tactic without attending the goal. We hypothesise that allowing the tactic tokens to attend to the goal will allow the Encoder to better represent the semantics of the tactic. To form a naive baseline, uses only the goal tokens. We do this to account for any inherent patterns in the goal which may be predictive of the outcome, for example particular goal which has high error rate. This allows us to ground our results the performance of this baseline, so we can observe the direct effect of the tactic in predictive performance. We also compare with ALL. TOKENS model which uses all tactic tokens for the Decoder without reducing to a single embedding. We implement this comparison to see the degree of information loss induced by reducing tactics single vector. Given Qa, Qry Og +. with estimates 3, f, Ô and for minibatch B C D, we optimise the following:
implement& No TACTIC model which does not the tactic at all, and instead
Σ (8)
(g, + L., (T, (c. ())
(2)

---

Table 1: Results for predicting unseen environment responses given goal and tactic, for transitions from miniF2F-valid. The No TACTIC result forms a baseline to assess the impact of the tactic representation. We observe that any tactic representation enables far better predictions, and con- straining these to a single vector (COMBINED and SEPARATE) does not hurt the performance gain. This demonstrates tactic representations which capture their effect on the environment, enabling our filtering model in 3 Comparing the COMBINED and SEPARATE ATE models, allowing the representation to attend to the goal leads large improvement.
Output
Status
Time
Embedding
BLEU
ROUGE-L F1
Top-4
F1
TPR
TNR
MSE
ALL TOKENS
0.31
0.38
0.31
0.85
0.82
0.96
0.17
COMBINED
0.33
0.39
0.32
0.88
0.85
0.97
0.16
COMBINED (SMALL GOAL)
0.30
0.36
0.29
0.85
0.81
0.96
0.20
SEPARATE
0.27
0.34
0.27
0.76
0.71
0.94
0.28
No TACTIC
0.17
0.22
0.13
0.22
0.14
0.96
0.37
The hyperparameters Oss, Qr, Ot control the weighting of the status, time and output losses. For simplicity, we set these to 1, however they could be tuned reflect the relative importance of each task. We use the binary cross-entropy loss L, for the status prediction, the mean squared error (MSH) C, for the time prediction, and the cross-entropy loss L. for the output prediction.
We obtain D from a single ReProver attempt on miniF2F-valid, yielding 498,236 transitions split randomly into 95% training. 5% testing. For the error prediction task, we reweight classes to account for imbalance, which is approximately 75% error, 25% success. We use the AdamW optimizer, with learning rate of 10 and a batch size of 1, train for 2 epochs, and report the results on the test set. To assess the Output prediction, we generate 4 outputs with beam search for each transition. We use BLEU (Papineni et al. 2002) and ROUGE-L (Lin 2004) assess the quality of the highest scoring beam in comparison to the ground truth, which is either an error message or new subgoals. The Top-4 accuracy is the proportion of samples with one beam identical to the ground truth. For Status, take the prediction as if Sys >> 0.5 and 0 otherwise, reporting the Fl score, true positive rate (TPR) and true negative rate (TNR). For time, we take the Mean Squared Error (MSE) of the prediction.
Table summarises the performance of our transition models. Our results suggest tactic represen- tations which capture useful information about their effect on the environment which we can see by the clear improvement across all approaches compared to the No TACTIC baseline. The improvement of COMBINED over SEPARATE supports our hypothesis that we better predict transitions when the tactic embedding attends to the goal. As expected, COMBINED outperforms COMBINED (SMALL. GOAL), with COMBINED (SMALL. GOAL.) significantly outperforming the SEPARATE model. COMBINED (SMALL GOAL) therefore gives an effective compromise between the accurate but expensive COMBINED model, and the goal-unaware SEPARATE model. We note the ALL TOKENS model, with the Decoder attending to the full tactic, does not improve upon the full COMBINED model. This shows our architecture effectively represents the tactic a single embedding without losing any relevant information. These results are the first to demonstrate the feasibility of learning the environment dynamics of proof systems. To illustrate the difficulty of this task, all predictions for the COMBINED model and their ground truth are provided with our code.
3 3D-Prover
Algorithm deefines 3D-Prover, which maps tactics T from the underlying tactic policy no a subset T" of size K. We use the Encoder E and Predictor P from Section 2 to generate tactic embeddings Φi and predict the time and error likelihood. As they are unit norm, the embeddings Φi encode the predicted environment response through their direction. The quality score qa then scales Φ; based on the tactic model logits m,, as well as the predicted error likelihood 8; and execution time T,. We have hyperparameters for normalisation temperature 0, as well as error and time weights
'See Appendix E for further analysis of these embeddings.
5

---

subst
subst
s simp
4
simp [h_1]
5 symmetry
Symmetry
rw b_1
rw h_1
(a) Initial tactic embeddings di. representing predicted outcome.
(b) Quality scaled embeddings. q: to be filtered by k-DPP
Figure 3: Visualisation of DPP for tactic filtering. The tactic embeddings from the transition model are scaled by quality scores, before a subset of tactics are selected using k-DPP. Subsets are chosen proportionally to the area spanned by their elements, giving combination of quality and diversity, For this simplified example, we take the 2D PCA projection of embeddings for tactics in Figure [ setting the quality to the scaled generator logits. Comparing the shaded areas in (b) and assuming subst a and rw h1 have been selected, we see that symmetry is favoured over simp [h,]. Although simp [h,] is scored higher by the generator, it is less diverse with respect to subst and rw h1
Algorithm 1:
3D-Prover
Input Goal g. candidate tactics T = { filter size K, Encoder E, Predictor P, error weight Xy, time weight \,, temperature 6 tactic policy To
Output: Output:Filtered: Filtered tacties 7" T
// Compute embeddings and scores for each tactic
for in [1...., N} do
N.....,. Φ; Egg ti)
(8s, T2) - ((Φ))
T.
[r T (TI,., exp(mo(t.lg)))
Jz
m; + Σ (o))/0))0)
4: < m, + A.8; + ATT:
1/ Compute kernel matrix
L + BTB, where B = . @N
Compute eigenvalues A; and eigenvectors v, of L
Sample J C (1...., .)....,)...... N) using Algorithm 2 of Kulesza & Taskar 2011). with {(vs, At)
k
return T = {libie
(s,,Ar Ar). 0 controls the scaling temperature of the model logits, with higher temperature flattening the distribution. therefore adjusts the diversity bias of 3D-Prover by reducing the impact of quality scores when sampling. We then compute the kernel L from qi and á,. and sample subset of tactics using the k-DPP algorithm (Kulesza & Taskar 2011). Figure visualises this process, where tactics subsets are sampled in proportion to their shaded area.
3.1 Experiments
We the performance of 3D-Prover with two setups. We first use ReProver (Yang al. 2023) as the underlying tactic policy as it is a small (~ 300M parameters) and popular open source proving model, allowing us run extensive experiments and ablations in a reasonable time frame. To evaluate our approach over a large (7B) state-of- the-art art model, we also present a smaller scale experiment using M2.55ttp...t Prover (Wu et al. 2024). We run our experiments Lean (De Moura 2015) using the BAIT (Lamont et al. 2024) platform with modified LeanDojo (Yang et al.
et al.
2023) environment, where we set an environment timeout 600 seconds per proof attempt. We
train COMBINED model for Reprover and COMBINED (SMALL GOAL) model for InternLM

---

Table 2: @ass@1 results miniF2F, with K tactics selected per node from ReProver. 3D-Prover uses a transition model trained from miniF2F-valid transitions. For miniF2F-test, we report the mean along with minumum and maximum over four runs, noting that Top- K is deterministic given ReProver uses Beam Search. The Gain column reports the relative improvement over the Top-K baseline. Results for No Filtering were 27.8% for miniF2F-test and 27.9% for miniF2F-valid. We observe a clear improvement using 3D-Prover, which increases as more filtering is applied (lower K). Our results on miniF2F-test show that 3D-Prover can improve search even for proofs out of distribution of the transition model.
K Top-K
Random
3D-Prover
Gain
miniF FFiiFFFFtess (mean, minimum and maximum over four runs)
22.4
19.0 (18.4, 19.6)
24.4 (23.7, 24.9)
+8.9%
16
26.5
25.4 (24.5, 25.7)
27.3 (26.9, 27.8)
+3.0%
32
27.8
27.4 (26.9, 28.2)
28.2 (27.3, 28.6)
+1.4%
miniF22 2F valid (single run)
8
21.7
19.3
25.0
+15.2%
16
26.6
24.2
29.1
+9.4%
32
27.9
27.5
28.7
+2.9%
from Section 2.2 using transitions from their respective base models. The Encoder and Predictor components then generate tactic embeddings and quality scores as per Algorithm We first examine the performance of 3D-Prover without hyperparameter tuning, setting X, X 0, A 1. We then perform ablation studies (3.1.) with ReProver over miniF2F-valid to examine the influence of the hyperparameters on the tactic success rate, execution time and diversity of the environment response. For miniF2F-test we allow the model multiple attempts per proof to increase confidence in the results, while for miniF2FF-vlidd allow one attempt per configuration allow wider set of ablations. We also present an additional experiment over the larger LeanDojo benchmark in Appendix D
The default search policy is set to be Best First Search (BFS), with nodes expanded in order of their cumulative log probability. For each node selected, we generate N = 64 candidate tactics from the underlying model Following the original implementations, we use beam search for ReProver and sampling with T = 0.7 for InternLM. These form the ground set for the node, to be sub-sampled by the filtering algorithm. As beam search decoding is deterministic, the ground set for given node is fixed across runs, allowing us to better isolate and compare approaches. We maintain sampling for InternLM to represent the original deplyoment scenario and test our approach under realistic usage. The filtering algorithm returns K tactics, which are executed in the environment before updating the proof tree. For ReProver, we test three levels of filtering, with K E (8, 16, 32). Lower K corresponds to more filtering, for which the filtering algorithm will have a greater impact. We compare 3D-Prover, as outlined in Algorithm [ with three baselines. The No Filtering baseline represents the original approach with no filtering. The Top-K baseline takes the top K tactics from the ground set as judged by their log probabilities, corresponding to the top K beams. We take K tactics at random from the ground set to form the Random baseline, as an exploration-focusee comparison. For InternLM, we test K with the Top-K and No Filtering baselines. and perform an additional experiment with Critic Guided search from (Wu et al. 2024) in place of BFS.
3.1.1 Proof Performance
Table 2 and 3 shows the results of our ReProver and InternI.M experiments on miniF2F. We observe 3D-Prover outperforming every baseline over both models. The influence of filtering becomes more apparent as K is decreased as there are more tactics filtered out. Reflecting this, the magnitude of improvement given by 3D-Prover increases for lower K. 3D-Prover is able to outperform both baselines by providing a tradeoff between the quality, of the tactics. The choice of K also controls the depth of the proof search, with larger K giving broader search, and smaller K deeper search. As most discovered proofs are short (favouring broad search), we see the Pass performance for lower values of K is generally lower, however over multiple attempts it can be beneficial to use deeper searches (see Appendix B). Our InternLM results As InternLM is sampling, this is up 64. See Appendix H for the distribution of tactic counts per node
represented by Top-K, and the diversity
7

---

Table 3: Results for miniF2F- using tactics selected from InternL.M..5S Steeprrreeee (mean, maximum and minimum for Pass @ 1). We compare results using standard Best First Search model (BFS) and with the M225 Critic Guided model for goal selection. 3D-Prover uses a transition model trained from transitions on miniP2FFtest with the No Filtering model. The Pass@) 1 result for BFS for No Filtering was 44.8. We observe 3D-Prover outperforming both the No Filtering and Top-K baselines, with notable improvement over more attempts for the Critic Guided search model.
Top-K (K = 8)
3D-Prover (K = 8)
Gain
(BFS)
Pass@1 @
44.3 (44.1, 44.5)
45.7 (45.3, 46.1)
+3.2%
Pass
44.9
47.3
+5.3%
No Filtering (K = 64) 3D-Prover (K 8) Gain
InternL.M2.5-StepPPa (Critic Guided)
Pass@1 43.7 (42.4, 44.5)
45.7 (44.5, 47.0)
+4.6%
Pass @6 49.0
53.1
+8.4%
(Table 3) demonstrate this, with the improvements from filtering growing over more attempts. This indicates a better variety of paths being explored, as each different attempt is more likely take a more diverse approach. Finding deep proofs is significant challenge Polu et al. (2022). with the search tree growing exponentially with proof depth. The large improvements from 3D-Prover for deeper search is step towards addressing this.
Tree search should be considered augmentation of the base model, with improvements generally much smaller than those found by improving the generator itself. This is unsurprising, as the generator forms the base set of candidates for the search to explore. Improved search algorithms do, however, have the advantage of being applicable to different base models, which is important given the rapid advance of new and better generators. For example, DeepSeck-Prover-- around 2 2.4% relative improvements in proof success over miniF2F-test with its novel tree search algorithm, compared to no search. In comparison, improving their base model yields 366 relative improvement (Figure 5 and Table in (Xin et al.) 2024)). Similarly, Table from Polu et al. (2022) shows their search approach yielding 0.04-5.7% relative improvements for miniF2F-valid, with 400,000 GPU hours required for their best results. We were able to find our improvements with significantly less resources, training our transition model on only a single attempt per proof.
obtains
We emphasise that these results were obtained without any hyperparameter tuning, only using the representations as diversity features and model logits as quality scores. We present ablation studies looking closer at these hyperparameters, however a comprehensive sweep is prohibitively expensive (Appendix [}.. Despite this, we were able to obtain our improvements without tuning. demonstrating the effectiveness of our approach. For completeness, Appendix C details the Pass @ performance over the hyperparameter configurations we tested for our ablations. We also highlight that the miniF2F-test ReProver results were obtained by training with transitions from miniF2F-valic showing that 3D-Prover remains effective for proofs out of distribution. The results on miniF2F-valid represent the more common online scenario, with previous attempts on the same dataset being used to improve performance (see, for example, [Lample et al. [2022): Polu et al. (2022). We also note that our approach is lightweight with minimal overhead, as we detail in Appendix G
3.1.2 Ablation Study
Efffet of the Transition Model To demonstrate the utility of our tactic representations, we compare to an ablated 3D-Prover where the transition model Encoder is replaced by an Autoencoder of the same size. The Autoencoder is trained to reconstruct the original tactic, and therefore generates representations which reflect only the syntax of the tactic. This tests our hypothesis that semantically aware tactic representations are useful for proofs, justifying the inclusion of the transition model. From Table the performance of 3D-Prover with the transition model embeddings is indeed superior to that of the Autoencoder across all values of K. This shows that selecting for diversity with respect to the predicted semantics, rather than the syntax, leads to direct improvement in proof performance.
8

---

Table Percentage proofs found after one attempt (Pass@) on miniF2F- comparing 3D- Prover with a Transition Model Encoder to an Autoencoder trained to reconstruct the original tactics. We see that 3D-Prover with the Transition Model gives a clear improvement in proof success over the Autoencoder, demonstrating the utility of our representation architecture in Section 2
K
K 16
32
Autoencoder
23.0
27.9
27.0
3D- 3D-Prover
25.0
29.1
28.7
We have demonstrated that 3D-Prover improves proof success rate without any hyperparameter tuning, with fixed A, = X, = 0, = 1. We now examine whether we can use 3D-Prover to direct search optimise secondary objectives, namely the execution time, tactic success rate and the diversity of environment response.
Success Rate We observe from Table 3D-PPover significantly improves the success rate of chosen tacties. As K decreases, this improvement increases in magnitude, reflecting the heightened influence of the filtering model. We see that this improvement increases with the error term X₃, which scales the quality scores of tacties by their predicted probability of success, as was intended.
Table 5: Tactic success rate per node for miniF2F-valid (Mean + Standard Error), where A, controls the error weight of quality score 3D-Prover. No filtering gives 27.7% = 0.2%. We see that 3D-Prover leads to fewer enrors average, which can be controlled by increasing Xg-
Top-K
Random 3D-Prover (²2 = 0.1) 3D-Prover (A, = 0.5)
8
39.0 + 0.1
33.4 + 0.1
43.3 0.1
56.5 0.1
16
39.0
+ 0.1
30.9 + 0.1
40.0 0.1
51.7 + 0.1
32
35.0 = 0.2 29.7 + 0.1 35.7 0.1
41.7 + 0.1
Diversity To measure diversity, we examine the percentage of successful tactics which result in a new proof path. We restrict to successful tactics to account for the discrepancy in success rate between approaches. We observe 3D-Prover gives more unique subgoals per successful tactic, which is noteworthy given the higher rate of successful tactics from 3D-Prover overall (Table As intended, increasing 0 gives further improvements under these metrics. This demonstrates that our approach is effective at avoiding redundant tactics, instead selecting tactics which yield more unique proof paths. Appendix F provides additional analysis, further supporting our claim of improved diversity.
Table 6: Percentage of successful tactics per node resulting in unique subgoal(s) miniF2F-valit
(Mean + Standard Error). No filtering gives 67.8 67.8% 0.3%. We observe 3D-Prover results more unique subgoals per tactie, leading more diverse of proof paths, with larger 0 controlling this.
K
Top-K
Random 3D-Prover (f = 1) 3D-Prover (0 4)
8
85.3 0.1
89.9 0.1
90.1 0.1
91.1 0.1
16
77.5
0.1
84.1 0.1
84.9 0.1
85.5 + 0.1
32
72.3 0.2
76.3 0.2 76,9 0.2
77.5 + 0.2
Execution Time Table shows the execution time for tactics over miniF2F-valid transitions. Again we see that 3D-Prover outperforms the baselines, with the improvement increasing with more filtering. Increasing the time weight X results in further reductions to the average execution time, demonstrating the accuracy of the predictions, and that they can directly result in faster tactics when filtering. has been noted that preferring faster tactics can prevent the excessive application of powerful automation tactics such as simp (Lample et al. 2022 Appendix E). As these generally take longer to run, using faster tactics can help models learn underlying proof arguments which are often hidden by the automation. It can also greatly reduce the number of timcout errors.

---

Table 7: Tactic execution time in milliseconds over miniF2F-valid proof attempts (Mean = Standard Error). No filtering resulted in 232 0.9 milliseconds. x controls the time weighting of the quality score in PD-Pro 3D-Prover selects faster tacties on average, with larger A magnifying this.
K
Top-K K
Random 3ID-Prover (A, 0.1) 3D-Prover (A, = 1.0)
206 = 0.8
198 + 0.9
155 = 0.5
136 + 0.5
16
220 +: 0.8
218 +: 0.9
176 +: 0.6
152 + 0.5
32
224 + 0.8 215 + 0.8
191 + 0.7
181 + 0.6
4
Conclusion
Limitations Our main limitation was the scale of experiments we were able to run, with other results often requiring thousands of hours of train time using hundreds of provers and larger models (Lample et al.] [2022] Polu et al. 2022] Xin et al., 2024). Given the large computational cost of evaluations (as we outline in Appendix I. we were only able to test M225 up to Pass @2 for BFS and Pass@6 for Critic Guided, and ReProver up to Pass @4 4 on miniF2F-test, with hyperparameter analysis of 15 runs on FiniF2F-valid (Table We could only evaluate over the large LeanDojo benchmark (Appendix D) for single run with each approach.
Summary We demonstrate the feasibility of learning proof system dynamics, where we generate tactic representations reflecting the response of the proof environment. We then leverage these with 3D-Prover, which filters candidate tactics to diverse and high quality subsets based on their likely outcome. We evaluate 3D-Prover by augmenting popular proving LLMs the standard miniF2F and LeanDojo benchmarks, where we find an improvement in the overall proof success rate, particularly for deeper searches. Our ablation studies confirm the utility of our tactic representations. enabling the selection of tactics with improved success rates, diversity, and/or execution time. By effectively pruning the search space, 3D-Prover is step towards enabling deeper automated proofs.
Acknowledgements
We acknowledge Defence Science and Technology Group (DSTG) for their support in this project.
References
Chen, M., Tworek, J., Jun, H., Yuan, Q., Pinto, H. P. d. O.,, Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., Ray, A., Puri, R., Krueger, G., Petrov, M., Khlaaf, H., Sastry, G., Mishkin, P. Chan, B., Gray, S., Ryder, N., Pavlov, M., Power, A., Kaiser, L., Bavarian, M., Winter, C., Tillet, Such, F. P., Cummings, D., Plappert, M., Chantzis, F., Barnes, E., Herbert- Voss, A., Guss, W. H., Nichol, A., Paino, A., Tezak, N.. Tang, J., Babuschkin, I., Balaji. S., Jain, S., Saunders, W., Hesse, C., Carr, A. N., Leike, J., Achiam, J., Misra, V., Morikawa, E., Radford, A., Knight, M., Brundage, M., Murati, M., Mayer, K., Welinder, P., McGrew, B., Amodei, D., McCandlish, S., Sutskever, I., and Zaremba, W. Evaluating Large Language Models Trained on Code, 2021. URL Version Number: 2.
https://arxiv org. abs/ 03374
De Moura, L., Kong. S., Avigad. J.. Van Doomn, F., and Von Raumer, J. The Lean Theorem Prover (System Description). volume 9195, pp. 378-388, Cham, 2015. Springer International Publishing. ISBN 978-3-319-21400- 978-3-319-214011 http://link.. springer...... com 10. 3717//9778-3-9-1100000
2000-111--66222 26. URL doi: 10. 10.11007/97--3311991
Book Title: Automated Deduction CADE-25 Series Title: Lecture Notes in Computer Science.
First, E. and Brun, Y. Diversity-driven automated formal verification. In Proceedings of the 44th International Conference on Software Engineering, ICSE '22, pp. 749-761, New York, NY. USA, July 2022. Association for Computing Machinery. ISBN 978-1-4503-9221-1 10.1 145/35 101133100000.311110 URL https: : //dl.
doi: acm. www.aaa......................... org/doi/10. 1145 3510010331011181
Hales, T., Adams, M., Bauer, G., Dang, D., Harrison, J., Hoang, I.. T. Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T. T., Nguyen, Q. T., Nipkow, T., Obua, S., Pleso,
10

---

J., Rute, J., Solovyev, A., Ta, T. H. A., Tran, N. T. Trieu, T. D., Urban, J., Vu, K., and Zumkeller, R. FORMAL PROOF OF THE KEPLER CONJECTURE. Forum of Mathematics, Pi, 5:e2, January 2017. ISSN 2050-5086. https://www. cambridgggsse formal-proof- of-
doi: 10.1017//mpp2017.11 URL ottp://all/oooo.ooooaaaaaaaaaaaa
Publisher: Cambridge University Press.
Hsiao, W.-L. and Grauman, K. Creating capsule wardrobes from fashion images. In CVPR, pp. 7161-7170, 06 2018. doi: 10. P0.100//V
Klein, G., Elphinstone, K., Heiser, G., Andronick, J.. Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M.. Sewell, T.. Tuch, H., and Winwood, S. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp. 207-220, New York, NY, USA, October 2009. Association for Computing Machinery. ISBN 978- 1-5555---5522
doi: 10. 10.1145/629555.1129999
URL https://doi
org/10. 1ww.11111111191 1629596
Kulesza, A. Determinantal Point Processes for Machine Learning. Foundations and Trends@ in
Machine Learning, 5(2-3):123-286, 2012. ISSN 1935-8245. doi: 10. 10.1561/22000000444, URL http://dxx doi wtt..r/...............0.. 1561/20000004
10. 1561
Publisher: Now Publishers.
Kulesza, A. and Taskar, B. k-DPPs: fixed-size determinantal point processes. In Proceedings of the 28th International Conference on International Conference on Machine Learning, ICML''1, pp. 1193-1200, Madison, WI, USA, June 2011. Omnipress. ISBN 978-1 118-1-5503-061-55
Lamont, S., Norrish, M., Dezfouli, A., Walder, C., and Montague. P. BAIT: Benchmarking (Em- bedding) Architectures for Interactive Mheorem-Provinge Proceedings of the AAAI Conference on Artificial Intelligence, 38: 18607-1066,,, March 2024. doi: 10.1609/aaai 338.9.289)
Lample, G., Lacroix, T. Lachaux, M.-a., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. HyperTree Proof Search for Neural Theorem Proving. In Advances in Neural Information Processing Systems, October 2022. URL URRLhtttp://opperevviee net/forum?id J4pX808cxHH
Li, Z., Sun, J., Murphy, L., Su, Q., Li, Z., Zhang, X., Yang, K., and Si, X. A survey on deep learning for theorem proving, 2024. Utttttss://aaxii org/ abs 2404. 2240 09939.
Lin, C.-Y. ROUGE: A Package for Automatic Evaluation of Summaries. In Text Summarization Branches Out, pp. 74-81, Barcelona, Spain, July 2004. Association for Computational Linguistics.
URL https: htt////ccaaatttotooyoooo owg.oogg///o......o...o W00-/W04-1033
Papineni, K., Roukos, S., Ward, T., and Zhu, W.-J. Bleu: a Method for Automatic Evaluation of Machine Translation. In Isabelle, P., Charniak, E., and Lin, D. (eds.), Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics, pp. 311-318, Philadelphia, Pennsylvania, USA, July 2002. Association for Computational Linguistics. doi: 10.31 1073135. URL
wwwpggg..rrr/PPo wwwp///---P.... 1040
Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. Formal mathe- matics statement curriculum learning. In The Eleventh International Conference on Learning Representations, 2022. UtLp hwtp:/iwww..eeeeeememm forett/formmmddd-PPo0 P7G-BBddhh
Reddy, R. Foundations and Grand Challenges of Artificial Intelligence: AAAI Presidential Address. |tttssss:///o3 aaai Section: Articles.
Al Magazine, 94):9, December 1988. doi: 10. 19..1//99aaaaa.vv...... org/ hes/aimasne wwwaaaaaieeeiiiiee hntp/xiixxx//mm/// whw.ppppppaaaa http://aimgaaaieeaarrieee///eeee
Tan, Y. K. Myreen, M. O., Kumar, R., Fox, A., Owens, S., and Norrish, M. The veri- fied CakeML compiler backend. Journal of Functional Programming. 29:e2, January 2019. ISSN 0956-7968, 1469-7653. doi: 10. 00.10177/50956796811000000 7/www. htt.a//www...a....oo/oo//o//aa/a
URL https
article/verified cakeml- ott.aaac......aaaaaaaaaaaaaaoooa
Publisher: Cambridge University Press.

---

Thakur, A., Tsoukalas, G,, Wen, Y. Xin, J., and Chaudhuri, S. An In Context Learning Agent for Formal Theorem-Proving, 2023. URL
04353 04353
Version
Number: 5.
Wang. H., Yuan, Y., Liu, Z.., Shen, J., Yin, Y., Xiong, J., Xie, E., Shi, H., Li, Y., Li, L., Yin, Li. Z.,, and Liang, X. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. In Rogers, A., Boyd-Graber, J., and Okazaki, N. (eds.), Proceedings of the st Anmual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 22632-12646, Toronto. Canada, July 2023, Association for Computational Linguistics. doi: 10.18653/v htw/2/222..llloogg700000000 UR/pttpss:///cclatttoooooo
org/ 2tgg/222..cl-1ong..17 706
ac1
Wu, Z., Huang, S., Zhou, Z., Ying. H., Wang, J., Lin, D., and Chen, K. (0teeLLMM2.-SStpPPrro Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems, October 2024. Uttptttp:/// /ww.vv.vvvvvvv/////i///axa/..av. org/ abs abs/ab/s/////// 2410. 15700 arXiv:2410.15700 [cs].
Xin, H., Ren, 7.. Z.,, Song, J., Shao, Z., Zhao, W., Wang. H., Liu, B., Zhang. L.,, Lu, X., Du, Q., Gao, W., Zhu, Q., Yang, D., Gou, Z.,, Wu, Z. F., Luo, F., and Ruan, C. DeepSeek-Provers V1.55 Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search, 2024. /0t/0///LL///////aaa/o/////////0 08152
Version Number: 1.
Yang, K., Swope, A., Gu, A., Chalamala, R., Song. P., Yu, S., Godil, S., Prenger, R., and Anandkumar, A. LeanDojo: Theorem proving with -ummented language models. In Neural Information Processing Systems (NeurIPS), 2023.
Yang, X.-W., Zhou, Z., Wang. H., Li, A., Wei, W.-D., Jin, H., Li, Z., and Li, Y-F. Carts: Advancing neural theorem proving with diversified tactic calibration and bias-resistant tree search. ICLR, 2025.
Zhang, K., Chao, W.-L., Sha, F., and Grauman, K. Video summarization with long short-term memory. In Leibe, B., Matas, J., Sebe, N., and Welling, M. (eds.), Computer Vision ECCV 2016, pp. 766-782, Cham, 2016. Springer International Publishing. ISBN 978-3-319-46478-7.
Zheng, K. Han. J. M., and Polu, miniF2F: cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2021. URL https (ogeeneerees.ett/oooruaaaa/aa22e
A Proof Search Setup
We first define the space of goals S, tactics T and failures F. For our purposes, these all contain arbitrary strings, with the goal being a formal proposition, the tactic command and the failure an error message. We then define the output space as O = P(S) F. A proof tree is DAG G = (V, E) where V S is the set of goals and E the edges between them. A proof attempt for goal 9n first initialises the proof tree with V = } E = 0. The search policy TT G x V + R+ is a distribution over goals given proof tree, being used to select goal g to expand. The tuctic policy Wr S x T + IR+ is distribution over tactics given goal, where N E N tacties are sampled to give tacties [N C The goal, tactic pairs (g, 44) are then passed to the environment For each pair, after T, E seconds, it returns either new set of goals of C S or eιror, e, F. We define this response as the output o E O. We further define the status 5; E {0, 1] as 0f E F. I of E P(S) and the transition as the tuple (g, f,, 8i, Ti, o;) The proof tree is then updated with G G=GU J of for all g'. and the associated transitions are added as edges to E. This is repeated until a proof is found, or budget is exhausted. A proof of g is found when E(g. t,) 0 for any t,, if all {g/} are proven for E(g.t) = {g[} C S. The result of a proof attempt is then the set of transitions ((g,, tki, Ski This 9k.) } for all selected goals 9h and their expanded tacties t. For simplicity, drop the indices to denote the set of transitions as {(g, 1, 8, T)).
x - O.
B Pass@1
Table summarises the Pass@4 results for ReProver over miniF2F-test, which the number proofs found at least once over four attempts, with Table 9 showing the Pass@A k up to k 4. We compare
12

---

Table 8: Percentage of proofs found after four attempts (Pass @4) with ReProver miniF2F-test, with tactics selected per node.
K
Random
3D-Prover
Gain
8
25.7
28.6
+11.3%
16
30.2
31.0
+2.6%
32
29.8
29.8
+0.0%
Table 9: Pass k rates for proof attempts on miniF2F-test
3D-Prover
Random
Pass@k k
=
8
= 16
32
K
K
32
1
24.9
27.8
28.6
18.0
21.2
28.1
2
26.1
29.4
29.0
22.9
28.6
29.0
3
26.5
29.8
29.8
24.9
29.4
29.8
4
28.6
31.0
29.8
25.7
30.2
29.8
3D-Prover to Random baseline, taking the same four runs from Table where A, = 0 = 1. With Top- K being deterministic, the Pass @ k rate is the same the Pass @ rate. Given several attempts, K appears to provide good tradeoff between breadth and depth, performing the best overall. 3D-Prover maintains large improvement for K 8, with modest improvement for = 16.
As discussed by Chen et al. (2021). the Pass@ k metric favours exploratory approaches as t: increases, the cost of lower performance for smaller k. This is because, over many attempts, highly exploratory approach is more likely to find at least one proof of a given goal, even though it may find fewer proofs a single attempt than a more exploitative approach. Further discussion Lample et al.) (2022) finds that randomly sampling search parameters also improves Pass @ k. With Pass @ being expensive to estimate, we fix our parameters over the four runs to give more accurate estimate of Pass 1. Given this, large scale experiment sampling these hyperparameters could lead to improved Pass k results, as Lample et al. (2022) show for their HTPS approach.
C Proof success rate over hyperparameters
Table 10: Pass@1 results on miniF2F-valid, over different hyperparameter configurations for 3D- Prover with ReProver.
(A., Ar,
K
(0.0, 0.0, 1.0)
(0.1, 0.1, 1.0)
(0.5, 0.1, 1.0)
(0.1, 1.0,
1.0)
(0.1, 0.1, 4.0)
25.0
25.0
25.8
22.5
23.8
29.1
28.7
27.9
27.0
26.6
32
28.7
28.3
28.7
27.9
27.0
Table 10 shows the Pass@1 I results on miniF2F-valid for 3D-Prover for our limited hyperparameter sweep. These results suggest that lower time weight x leads to better proving results. The diversity parameter hinders performance
the larger value, consistent with what was observed by Chen et al.) (202I), where they observe a tradeoff between exploration and Pass 1. Although these parameters may not improve Pass@ I, different proofs may favour different configurations, with some requiring e.g. more depth or exploration than others. As discussed above, a higher @ can usually be obtained by sampling wide set of these parameters. For the set of hyperparameters we tested here, found cumulative proof rate (or Pass @ 15) of 32.8% miniF2F-valid
13

---

D Evaluation on LeanDojo Benchmark
We ran an additional experiment on the LeanDojo Novel Premises Yang et (2023) benchmark testing 3D-Prover on a larger dataset. This dataset has 2000 evaluation proofs in comparison to the 244 from miniF2F-valle and miniF2F-test, allowing us evaluate the performance of 3D-Prover on a larger scale.
We trained transition model from a single ReProver attempt on LeanDojo Novel Premises, before evaluating 3D-Prover using ReProver with the methodology in Section We set K=32 for 3D-Prover, and compare the model with No Filtering (i.e. K=64), and Top-K=32. We further examine the distribution of proof lengths found from this experiment. To account for different proof's of the same goal, we adjust proof lengths be the shortest found from any attempt c.g. if 3D-Prover finds proof of length 10, which was found in 3 steps by No Filtering, we count it as length 3). Hence, all proof lengths reported are the shortest found by any method. We report the number of proofs found by each approach, organised by the proof length in Table
Table 11: Number of Proofs found on LeanDojo Novel Premises, sorted by proof length.
Proof Length
3D-Prover (K = 32)
Top-K (K = 32)
No Filtering (K 64)
236
233
237
167
162
174
3
134
126
131
60
60
54
40
39
24
7
6
2
2
0
0
Total
646
626
622
Pass
32.3%
31.3%
31.1%
3D-Proved obtains a relative improvement of 3.2% over Top-K, and 3.9% relative improvement over No Filtering in terms of the number of proofs found, comparable to the same performance gain for 32 found in miniF2F-valid (Table [ We see that 3D-Prover finds deeper proofs, while maintaining a high proof success rate for shallower proofs, unlike Top- K. The No Filtering approach, as expected, finds the most shallow proofs, however quickly drops off in performance for deeper proofs. We also note that 3D-Prover found the longest proofs of length 7, with neither baseline finding any.
E
Embedding Discussion
Embedding Comparison We now investigate whether the transition model (Figure captures tactic semantics rather than syntax in its tactic embeddings. To test this, we examine the cosine similarity of tactic embeddings which lead unique subgoals. Figure 4 takes an example node, examining all tactics which lead to unique subgoal. The upper value displays the cosine similarity given by the transition model, while the lower value displays that given by the Autoencoder in Section 3.1.2 We observe that in most cases, the similarity given by the transition model is much lower than that given by the Autoencoder, which is only considering the syntax of the tactic. For example, the similarity between tactic 3 and 4 is very high for the Autoencoder, given the similar syntax between the two as they use the same lemma. Despite this similar syntax, the transition model embeddings show high degree of dissimilarity. reflecting the different outcome they have on the environment. We present additional examples in the supplementary code. To generalise beyond these examples, we ran this comparison over the tactic embeddings which lead to unique subgoals for all 244 root nodes valid. Fisors the distribution of the average cosine similarity for each node, for both the transition model and the Autoencoder. The average cosine similarity for the transition model embeddings was 0.44 while the Autoencoder gave 0.57. While this comparison does not account for similarity between the unique subgoals, it is still clear that the transition model
14

---

(simpl icatinot proper divisorskiia,, <ao-not.sum, proper, divisers, _en _en_one_______eeo_ iet prime 0)
011
I'convert <a sapnat.sum, proper, diviserdsssssecccmmo eq, Iff prpppeeeese
2.35
0.5
02
5.0
0.31
(transitivity,
0.55
0.00
065
0.74
I'hw
047
822
0.45
5.00
9/4
3.3
0.31
3
0.55
002
315
84
335
542
0.00
l'classical,,
2.48
0.74
05
6.00
0.2
2.64
5.17
3.30
(symmetry, 5)
3.53
0.0
Figure 4: Cosine similarity between tactic embeddings resulting in unique subgoals, for sample root node in miniF2F-valid. The top value gives the similarity for embeddings from 3D-Prover, while the bottom gives the similarity for embeddings from an Autoencoder. We see that 3D-Prover better separates these semantically distinct tactics, in comparison to the Autoencoder, which only separates based on their syntax.
60
Transition Model
Autoencoder
50
Frequency
20
10
0.1
0.2
0.3
0.4
0.5 Similarity
0.6
0.7
0.8
Figure Distribution of cosine similarity for tactic embeddings resulting in unique subgoals, averaged over root nodes in miniF2F-valid. We see that 3D-Prover gives embeddings which better separate these semantically distinct tactics, in comparison the the syntax focused embeddings of the Autoencoder.
embeddings better separate unique tactics than Autoencoder embeddings which are based syntax alone. The result of this is a higher likelihood of 3D-Prover selecting tactics which give unique subgoals, which Autoencoder for proof discovery.
show in Section 3.1.2 results in the transition model outperforming the
Embedding Objective As outlined in Section 2 train our embeddings to be reflective of the tactic semantics across all three components of Status, Time and Output. Hence 3D-Prover, which selects diverse embeddings. may lead tactics predicted have errors, where the errors are diverse in terms of their predicted message. The byperparameter A can alleviate this by weighting the scores based their likelihood of success. From our experiments (Table TO), there is necessarily benefit to Pass by filtering out strongly based on the predicted error likelihood. To speculate, the error prediction, although quite good, imperfect with false negatives (Table This can lead to potentially useful tactics being ignored if the eтror prediction is overly trusted, even though there higher tactic success rate overall as Table 5 Given these prediction errors, may be the case that selecting goals which are predicted to lead to (diverse) errors may be preferable, given the possibility they result successful new subgoals. These subgoals may be be quite different from those previously selected, they are mispredicted, are clearly outside the space of tactics
15

---

where the transition model is confident about the outcome. Further analysis could be worthwhile to investigate this. An embedding architecture trained only on successful tactics could be used, however given the high enror rate of tactics, this would ignore large proportion of the transition data.
F
Additional Diversity Analysis
To further examine diversity, first look at the percentage of unique environment responses to tactics executed per node, including responses with unique errors (Table 12), using the same ReProver setup in As it is difficult to select tactics guaranteed to be successful (see Table [5). we would expect a good exploratory policy to select tactics which result in more varied outputs (both errors and successes alike), across unique subgoals (Table 13). using a simple text embedding model This more precisely quantifies the diversity in the contents of the subgoals. We do this to account for simple changes (such as variable renaming). which would not be differentiated under a simple check for uniqueness, and so allows
to better explore the space. We also examine the degree of cosine similarity
examine how varied the contents of the resulting subgoals are.
In both cases, we see that 3D-Prover results in more diverse responses. As intended, increasing results in further improvements to diversity under both metrics. The increased diversity in subgoal content (Table 13 strengthened by the fact that 3D-Prover also gives more unique subgoals on average (Table 6p. suggesting that our approach yields more unique subgoals, and that these subgoals are more varied in their contents.
Table 12: Percentage of unique environment responses per node in miniF2F-valid (Mean + Standard Error). Unique defines either syntactically distinct error messages or responses including at least one previously unseen subgoal. No filtering results 63.3% = 0.2%. We see that 3D-Prover gives a higher diversity of environment responses, increasing with the diversity parameter 0. 3D-Prover
K
Top-K
Random
0 =
0 0=4
8
83.9 + 0.1
88.6 0.1 90.8 0.0
91.7 0.0
16
77.5 + 0.1
81.4 + 0.1
85.9 + 0.1
86.6 0.1
32
71.1 + 0.1
72.7 + 0.1 77.6 +
0.1 78.1 0.1
Table 13: Average cosine similarity between subgoal embeddings for ReProver over miniF2R-valid
(Mean Standard Error). We observe consistently lower similarity among subgoals generated from 3D-Prover, increasing with the diversity parameter 0.
3D-Prover
K
Top-K
Random
0 1
0 4
8
0.939 + 0.000 0.945 + 0.000 0.931 +: 0.000
0.930 + 0.000
16
0.916 + 0.000
0.926 + 0.000
0.910 + 0.000
0.905 + 0.000
32
0.904 0.000
0.909 + 0.001 0.900 + 0.001
0.896 + 0.001
G
Computational Overhead
3D-Prover adds a constant but minimal time and memory overhead, the majority of which is in generating embeddings for the candidate tactics. Taking our first run for 3D-Prover with InternLM, we found the filtering time over nodes to be 0.07s with a standard deviation of 0.02s. In comparison, the average tactic generation time was 7.5s with standard deviation of 4s. This gives a time overhead of approximately 0.9%. The memory overhead was approximately 3GB of VRAM, while the tactic model took 44GB of VRAM, giving approximately 7% memory overhead.
We also note that the average time to execute a tactic from the No Filtering model was approximately 0.13s (with 0.12 standard deviation). With up 64 candidate tactics per node, the filtering time
16

---

of 0.07 seconds is around half the average time to execute single tactic. Given the improvements in success rate (Table 5). our filtering model therefore gives an effective way reduce the total computational resources by preventing the wasteful execution of erronoous tactics. To further support this, we observed the average total time for proof search attempt with 3I>-Prover with InternI (K 8) to be 993.8 seconds (1761.5 Standard Deviation), while the total time for Top- K = 8 was 1116.8 seconds (2126.0 Standard Deviation).
H Number of tactic candidates for InternLM
As noted in 3 experiments with InternL -M2..-Step--PP..- Prover sampling rather than beam search for tactic generation, as done in Wu et al. (2024). As a result, there is no guarantee there will be 64 unique tacties, with many samples being identical. As result, sample 128 initial tactics, and take the total unique candidates as our ground set (up to 64 total). We plot the distribution of unique tactic candidates per node in Figure This informed our choice of K 8 for experiments, as higher K would give minimal filtering in comparison to a beam search approach.
Frequency
2
Tactic candidates per node
Figure Distribution of unique tactic candidates per node for InternL 10..2.5-ttee-Prver over miniF2F-test (μ 35.4, 11.5).
Computational Resources and Usage
For traning our transition models, we used a singe RTX4090 GPU with Intel 19 13900k processor. For evaluating, we used two internal machines each with two RTXA6000 GPUs, and a Intel Xeon W-2223. For each evaluation experiment 31 assigned a single RTX A6000 GPU which contained both the tactic generator and transition model, which served 2 CPU provers which request tactics and evaluate in the Lean environment.
For each transition model, training for 2 epochs took approximately 2 days for each run, giving a total of 10 days of 4090 training for our results in 2.2. Each evaluation run for ReProver took around 12h, while each evaluation run for MnternL.M2.5-95 12.5-Sttep-Proer around 2 days. Counting the number of runs for all baselines and 3D-Prover, 22 for miniF2F-valid and 17 runs for InternL.M. The additional result over the large LeanDojo dataset in took around days per run, with 7 total. We therefore estimate the total evaluation time (for a single machine with RTX6000s and a Xeon W-223) to be 94 days, which was around 47 days with our machines. The full research project included additional compute and experiments, different architectures and approaches were prototyped, however we do not have an estimate for the amount.
miniF2F
have 28 runs for ReProver with miniF2F-test.
17

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: Section demonstrates our first claim of proof outcome learning, with Section demonstrating our second and third claims, showing improvements over two base models with our approach.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: Please see the limitations section and the section on computational cost G Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (c.g.. independence assumptions, noiseless settings, model sell-speciiiitiinn asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex, system might not be used reliably to provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and faimesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
18

---

Answer:
[NA]
Justification:
No new theoretical results are presented.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proof's can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided not)?
Question:
Answer: [Yes]
Justification: Our transition model and 3D- 3D-Prover architectures are fully described in section 2 and with code provided in the supplementary material.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, descríbing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make clear how reproduce that algorithm. (b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is new model (e-g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing verifying the results.
5. Open access to data and code
19

---

reproducible, they Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
Justification: code is provided the supplementary material, with instructions for reproducing the main results.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips.c cc/
for more details.
While we encourage the release of code and data, we understand that this might be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
/
Cotee//bdeeeSbmmmcia ssi onPolicy) for more details.
The authors should provide instructions data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: We specify all training and test details for our results, outlined in each relevant section.
Guidelines:
The answer NA means that the paper does include experiments.
The experimental setting should be presented in the core the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: We clearly state the standard error for the relevant results.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
20

---

The method for calculating the error bars should be explained (closed form formula, call a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that out of range (e.g. negative error rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification:
Computational resources are detailed in
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary failed experiments that didn't make it into the paper).
9. Code ethics
Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics http::////eeappp...cc//////cataa
Question:
Answer: [Yes]
Justification: Yes, all research conforms the NeurlPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g.. if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: Positive societal impacts are discussed in the introduction (i.e. furthering research in the area of Neural Theorem Proving). As Neural Theorem Proving models are used only for the benign task of proving theorems, find clear negative societal impacts.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
21

---

Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), faireess considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied partieular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there negative societal impacts, the authors could also discuss possible mitigation strategies (c.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of MI).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: There is no clear risk of misuse of our data or models, they are used only for theorem proving, which is a benign application.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: All code, data and models used in the paper properly cited, with their usage properly respected.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
22

---

If assets are released, the license, copyright information, and terms of use in the thcode. has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
package should be provided. For popular datasets, batasets.papersstt paperswi
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. If this information is available online, the authors encouraged to reach out the asset's s creators.
13. New assets
Question: Are assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: The code for the paper is the primary asset introduced, which is documented and provided in the supplementary material.
Guidelines:
The answer NA means that the paper does not release assets.
Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsoureing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
crowdsourcing or human subjects were involved this research.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
No crowdsourcing or human subjects were involved in this research.
Guidelines:
The answer NA means that the paper does involve crowdsourcing nor research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
23

---

We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Question:
Answer: [Yes]
Justification: The usage LLMs fully described for our approaches, with LLMs being component of our transition model (forming the base architecture to fine-tune in 2 and our
3D-Prover model (being used as tactic generators
Guidelines:
The answer NA means that the method development in this research does not involve LLMs as any important, original, or non nta-standard components.
Please refer to our LLM policy for what should or should be described.
24


Reviews:
[{"review_id": "GPWQRkj1BI", "reviewer": "Reviewer_Bo1h", "summary": "The paper introduces 3D-Prover, a novel approach to enhance automated theorem proving by addressing the challenge of intractable search spaces in proof trees. It proposes a filtering mechanism using Determinantal Point Processes (DPPs) to select semantically diverse and high-quality tactics, leveraging tactic representations that capture their effect on the proving environment, likelihood of success, and execution time. These representations are learned from synthetic data generated from previous proof attempts. The method is designed to augment existing tactic generators and is evaluated on the miniF2F and LeanDojo benchmarks, demonstrating improvements in proof success rate, tactic success rate, execution time, and tactic diversity when applied to models like ReProver and InternLM2.5-Step-Prover. The paper also explores learning environment dynamics to predict tactic outcomes, contributing to more efficient proof search.", "questions": "1. The hyperparameter sweep is limited (Table 10, Page 13), and the authors note computational constraints. Could you provide additional results or analysis (e.g., in supplementary material) showing the sensitivity of 3D-Prover to key hyperparameters (e.g., \\(\\lambda_s\\), \\(\\lambda_t\\), \\(\\theta\\))? This could strengthen the quality score by demonstrating robustness or optimal configurations. A response showing improved performance with tuned parameters could increase the quality rating to 4.\n\n2. The DPP-based filtering mechanism is mathematically dense (Page 3). Could you include a more intuitive explanation or a concrete example (beyond Figure 3) to clarify how DPPs balance quality and diversity in tactic selection? This could improve the clarity score to 4 by making the method more accessible to a broader audience.\n\n3. The evaluation focuses on ReProver and InternLM2.5-Step-Prover. Have you tested 3D-Prover with other theorem-proving models or environments beyond Lean? Providing evidence of generalizability could elevate the significance score to 4 by showing broader applicability.\n\n4. The paper highlights improved performance for deeper proofs (Table 11, Page 13). Could you quantify the improvement in proof depth (e.g., average proof length) across benchmarks and compare it to baselines? This could strengthen the significance score by emphasizing 3D-Prover’s contribution to a known challenge in theorem proving.", "limitations": "Yes. The authors addressed limitations and potential negative societal impact of their work.", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "#### Strengths:\n\n1. The paper presents a novel application of Determinantal Point Processes (DPPs) to theorem proving, a domain where such probabilistic models for diversity-driven filtering are underexplored. The idea of learning tactic representations that capture semantic effects on the proving environment (rather than syntactic similarity) is innovative and addresses a critical gap in automated theorem proving (Section 1.1, Page 2).\n2. The experimental evaluation is robust, with clear results on standard benchmarks (miniF2F and LeanDojo) using two different models (ReProver and InternLM2.5-Step-Prover). The paper provides detailed metrics, including Pass@1, tactic success rate, execution time, and diversity (Tables 2, 3, 5, 6, 7, 11), supported by statistical significance measures (standard error). The use of a transition model to predict tactic outcomes (status, time, output) is well-executed and validated (Table 1, Page 5).\n3. The paper is well-structured, with clear explanations of the problem, methodology (Sections 2 and 3), and evaluation. Figures (e.g., Figure 2, Page 4; Figure 3, Page 6) and Algorithm 1 (Page 6) effectively illustrate the architecture and filtering process. The use of standard metrics like BLEU, ROUGE-L, and cosine similarity enhances interpretability.\n\n#### Weaknesses:\n\n1. The evaluation is somewhat limited by the scale of experiments, as acknowledged in the limitations section (Page 9). The hyperparameter sweep is minimal (Table 10, Page 13), and the authors note that comprehensive tuning was computationally prohibitive. This raises questions about the generalizability of the results across different hyperparameter settings or larger models.\n2. While the paper is generally clear, the explanation of the DPP-based filtering mechanism could be more accessible to readers unfamiliar with DPPs. The mathematical formulation (Page 3) is dense, and a more intuitive explanation or example could improve understanding. Additionally, the truncation of text in several sections (e.g., Pages 1, 2, 3) makes it harder to fully assess some details.\n3. The improvements, while notable (e.g., 3.2–3.6% relative improvement on LeanDojo, Page 13), are modest compared to advancements in base model improvements (e.g., 36% improvement cited in Xin et al., 2024, Page 8). This suggests that 3D-Prover’s impact may be incremental rather than transformative, particularly for shallow proofs where broader search is favored (Page 7).", "was_revised": false, "final_justification": "", "rebuttal": "We thank the Reviewer Bo1h for their valuable feedback and for recognizing the novelty of applying Determinantal Point Processes (DPPs) to theorem proving, the innovation in our semantic tactic representations, and the robustness of our experimental evaluation.\n\n## W1 / Q1\n- *The evaluation is somewhat limited by the scale of experiments, as acknowledged in the limitations section (Page 9). The hyperparameter sweep is minimal (Table 10, Page 13), and the authors note that comprehensive tuning was computationally prohibitive. This raises questions about the generalizability of the results across different hyperparameter settings or larger models.*\n- *The hyperparameter sweep is limited (Table 10, Page 13), and the authors note computational constraints. Could you provide additional results or analysis (e.g., in supplementary material) showing the sensitivity of 3D-Prover to key hyperparameters (e.g., (\\lambda_s), (\\lambda_t), (\\theta))? This could strengthen the quality score by demonstrating robustness or optimal configurations. A response showing improved performance with tuned parameters could increase the quality rating to 4.*\n\nThank you for this insightful question. While a large-scale hyperparameter sweep was computationally infeasible during the rebuttal period, we believe our results already demonstrate significant robustness. **Crucially, 3D-Prover delivers consistent performance gains *without any specific tuning*, across two different base models (the small ReProver and the large 7B-parameter InternLM2.5) and three benchmarks (miniF2F-test, miniF2F-valid, LeanDojo Novel Premises).** This effectiveness suggests our method is not overly sensitive to its configuration and provides immediate value.\n\nOur hyperparameter studies were intended to systematically validate their impact on the auxiliary proof objectives of tactic success, execution time and diversity, where we show they can be tuned to bias specific objectives (Section 3.1.2). We therefore test high and low values of each parameter respectively, with all others held fixed, in contrast to a full grid search to find an optimal configuration for proof success. We agree that a larger sweep could identify an optimal configuration for Pass@1 and see this as a valuable avenue to further improve our results. \n\n## W3\n- *The improvements, while notable (e.g., 3.2–3.6\\% relative improvement on LeanDojo, Page 13), are modest compared to advancements in base model improvements (e.g., 36\\% improvement cited in Xin et al., 2024, Page 8). This suggests that 3D-Prover’s impact may be incremental rather than transformative, particularly for shallow proofs where broader search is favored (Page 7).*\n\n As we discuss (line 229), and as Reviewer SA37 astutely observed, our work is **complementary to advances in base models.** While improving the generator model will always be the primary driver of performance, our method addresses a different, fundamental challenge which is the search procedure itself. An advantage of this approach is its longevity and generality. Base models may become outdated, but an improved search algorithm can enhance both current and future state-of-the-art generators. We demonstrated this by applying our method to InternLM2.5-Step-Prover (which was SoTA during our experiments). Beyond improving the proof rate, our method is lightweight and **reduces overall proof search time** (Appendix G), making it a valuable and efficient addition to any proving pipeline. Please also see our response to Q3, where we present additional results showing a larger improvement over an additional baseline. \n\n## W2/Q2\n- *While the paper is generally clear, the explanation of the DPP-based filtering mechanism could be more accessible to readers unfamiliar with DPPs. The mathematical formulation (Page 3) is dense, and a more intuitive explanation or example could improve understanding. Additionally, the truncation of text in several sections (e.g., Pages 1, 2, 3) makes it harder to fully assess some details.*\n- *The DPP-based filtering mechanism is mathematically dense (Page 3). Could you include a more intuitive explanation or a concrete example (beyond Figure 3) to clarify how DPPs balance quality and diversity in tactic selection? This could improve the clarity score to 4 by making the method more accessible to a broader audience.*\n\nFor brevity, we chose to keep the background for DPP to the minimum required, which was noted as a strength by reviewer SA37. We can see how additional exposition and intuitive explanations might make our approach more accessible, and we are happy to include additional background on this as an Appendix in the revision. \n\nFor some more intuition on how DPP balances quality and diversity, keeping the example from Figure 3:\n\nRecall that sets are chosen in proportion to the area of the parallelepiped (Figure 3, see [1] for a proof), which is based on both the angle and magnitude (quality) of the component vectors $\\phi_i$\n\nFavoring Quality: If a tactic A, for example, `simp [h1]` is of very high quality, its feature vector $\\phi_A$ will be high in magnitude. When $\\phi_A$ is included in a subset, it therefore highly contributes to the volume spanned by the feature vectors of that subset, thereby increasing the volume and, consequently, the subset's probability (unless the other elements are overly similar, as below).\n\nEnforcing Diversity: Consider two highly similar tactics, A (`simp [h1]`) and B (`rw h1`). Their feature vectors $\\phi_A$ and $\\phi_B$ will be nearly linearly dependent (i.e., they point in almost the same direction, forming a very small angle). If a subset includes both A and B the volume spanned by their feature vectors will be extremely small, leading to a very small (near zero) volume for that subset, even if they are both high quality. As a result, the DPP will assign a very low probability to such a redundant set. Instead, the DPP will favor a set that includes one of A or B and a very different item, such as C (`subst c`). Taking A as an example, the feature vectors $\\phi_A$ and $\\phi_C$\nwill be far apart (large angle), spanning a much larger volume, and a greater probability for that diverse subset.\n\n[1]: Kulesza et al. (2013). Determinantal point processes for machine learning. https://arxiv.org/abs/1207.6083\n\n## Q3\n- *The evaluation focuses on ReProver and InternLM2.5-Step-Prover. Have you tested 3D-Prover with other theorem-proving models or environments beyond Lean? Providing evidence of generalizability could elevate the significance score to 4 by showing broader applicability.*\n\nWe chose Lean as it is currently the primary focus of research in the field, with well established benchmarks and baselines. It would be a useful extension to test over systems such as Coq, HOL4 or Isabelle, but would require significantly more engineering effort as there are far fewer pre-trained models and codebases to work with.\n\nIn addition to ReProver and InternLM2.5 with Best First Search, in the period since submission we have tested an additional search setup. We test our approach with InternLM2.5-Critic [1] guided search instead of Best First Search, using the the same setup as our other InternLM experiments. We were able to test 6 runs of InternLM Critic with No Filtering, and 6 runs with our approach. We only compare to No Filtering to enable a higher Pass@k. The results are given below, where we present mean, (min, max) values for Pass@1 and the observed Pass@6 result:\n\n|   | InternLM2.5-StepProver-CG | 3D-Prover |\n|--|--|--|\n| Pass@1 | 43.7 (104, 109) | **45.7 (109, 115)** |\n| Pass@6 | 49.0 | **53.1**| \n\n\nThese results show for a larger scale (Pass@6), our approach was able to outperform the original baseline approach, and that this extends to another, more performant search algorithm than Best First Search. Furthermore, the total number of proofs found is greatly increased over more iterations, supporting the scaling of our approach to higher Pass@k. \n\n\n[1]: Wu et al. (2024). InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems. https://arxiv.org/abs/2410.15700. \n\n## Q4\n- *The paper highlights improved performance for deeper proofs (Table 11, Page 13). Could you quantify the improvement in proof depth (e.g., average proof length) across benchmarks and compare it to baselines? This could strengthen the significance score by emphasizing 3D-Prover’s contribution to a known challenge in theorem proving.*\n\nHere are additional results for proof depth, with the results for ReProver over LeanDojo presented in Table 11. As we discuss for Table 11, these depth results normalize by the shortest proof found by any method (I.e. if a proof is depth $k$, there is no proof of depth $<k$ by any other approach). This accounts for proofs which appear deep, but are in fact more efficiently solved by a simpler approach, making the adjusted proof depth a better measure of difficulty. \n\nFor ReProver, over miniF2F, we present the (average proof depth, maximum proof depth found) tuples below (corresponding to Table 2): \n\n| K | Random | 3D-Prover | Top-K |\n|:---|:---|:---|:---|\n| 8 | (1.33, 4) | **(1.83, 6)** | (1.60, 5) |\n| 16 | (1.84, 4) | **(2.08, 6)** | (2.02, 5) |\n| 32 | (2.02, 4) | **(2.12, 5)** | (2.04, 3) |\n\nFor our InternLM2.5 experiment in Table 3 we have:\n\n| Approach | Average Depth | Max Depth |\n|:---|:---|:---|\n| 3D-Prover | **1.52** | 8 |\n| No Filtering | 1.45 | 4 |\n| Top-K | 1.46 | 8 |\n\nFinally, for our additional experiment testing with InternLM2.5 critic (detailed in Q3 above), we have: \n\n| Approach | Average Depth | Max Depth |\n|:---|:---|:---|\n| 3D-Prover | **1.72** | 9 |\n| No Filtering | 1.48 | 5 |\n\nWe see that in all cases we observe higher average proof depths, as well as higher maximum depths obtained by 3D-Prover. We were unable to show these as statistically significant due to the small sample sizes, a limitation we expand on in our response to reviewer SA37."}, {"review_id": "ADkLsEbk6P", "reviewer": "Reviewer_yzrR", "summary": "The paper introduces 3D-Prover, a novel approach to automated theorem proving that leverages Determinantal Point Processes (DPPs) to filter semantically diverse and high-quality tactics. Evaluated on miniF2F and LeanDojo, 3D-Prover enhances models like ReProver and InternLM2.5-Step-Prover, boosting proof success rates, tactic quality, speed, and diversity.", "questions": "1. Could you provide an analysis of the computational cost associated with the proposed method?\n\n2. Table 11 shows that 3D-Prover tends to generate longer proofs. Does this raise concerns about potential redundant proofs?\n\n3. The ablation study appears insufficiently evaluated. Tables 5, 6, and 7 only conduct experiments on two specified hyperparameter settings. Are more hyperparameter ablation studies needed?\n\n4. Can neural network embeddings effectively characterize proof states? To my knowledge, they are primarily used for shallow semantics.", "limitations": "yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n1. The use of DPPs for filtering tactics in theorem proving is innovative and addresses the challenge of exponential search space growth.\n2. The paper provides extensive empirical results, including ablations and comparisons with baselines, demonstrating consistent improvements across multiple benchmarks.\n3. The method has a solid mathematical foundation.\n\nWeaknesses:\n1. The experimental results are not sufficiently pronounced, and the latest SOTA models (e.g., BFS-Prover) were not employed in the experiments.\n2. There are certain computational cost considerations that the authors need to further address.", "was_revised": true, "final_justification": "The author's response has solved my questions, and I will keep the score.", "rebuttal": "We thank Reviewer yzrR for their insightful comments and for acknowledging the innovation of our DPP-based filtering method and the extensive empirical results.\n\n## W1\n- *The experimental results are not sufficiently pronounced, and the latest SOTA models (e.g., BFS-Prover) were not employed in the experiments.*\n\nRegarding the magnitude of improvements, we believe they are meaningful as they represent fundamental gains in search efficiency, a point we elaborate on in our response to Reviewer Bo1h (W3). Regarding SoTA models, BFS-Prover was released concurrently with our experiments. The base model we used, InternLM2.5, was SoTA at the time of our work. Importantly, our method is complementary to tactic generators like the one in BFS-Prover; in fact, the Best First Search (BFS) algorithm they use is precisely the baseline we demonstrate improvements upon. Please also see our response to Q3 of Bo1h for an additional result demonstrating larger improvements over InterLM2.5-Step-Prover-CG, which is the critic-augmented search model from InternLM. \n\n## W2 / Q1\n- *There are certain computational cost considerations that the authors need to further address.*\n- *Could you provide an analysis of the computational cost associated with the proposed method?*\n\nAn analysis of the computational cost of our approach is presented in Appendix G, which was noted as a strength in our evaluation by Reviewer SA37. Overall, our approach has minimal overhead, where we observed 7\\% memory overhead and 0.9\\% time overhead in terms of tactic generation. Despite this, we found resulting improvements in tactic execution time which reduced the overall proof search time, even including the tactic generation component.\n\n## Q2\n- *Table 11 shows that 3D-Prover tends to generate longer proofs. Does this raise concerns about potential redundant proofs?*\n\nThis is an excellent question. We interpret the concern about \"redundant proofs\" as the risk of finding a longer proof path for a theorem when a shorter one exists in comparison to another baseline. We agree this would be an undesirable outcome and took specific steps to control for it.\n\nIn our analysis for Table 11, **a proof is only reported at depth $k$ if no shorter proof (of length $<k$) was found for the same theorem by *any* method, including all baselines.** This filtering addresses the above concern, so that that our results on deeper proofs represent genuinely solving problems that were previously intractable at shallower depths, rather than simply finding less efficient solutions.\n\n## Q3\n- *The ablation study appears insufficiently evaluated. Tables 5, 6, and 7 only conduct experiments on two specified hyperparameter settings. Are more hyperparameter ablation studies needed?*\n\nThank you for this suggestion. The primary goal of our ablation studies (Tables 5, 6, 7) was to validate that our hyperparameters ($\\lambda_s, \\lambda_\\tau, \\theta$) function as effective and direct controls for their corresponding search metrics. **Our experiments confirm this, showing statistically significant improvements in success rate, execution time, and diversity when their respective parameters are adjusted.**\n\nWe believe this analysis is sufficient to demonstrate the claimed functionality and utility of these controls. While we agree that a more exhaustive hyperparameter study would be valuable for mapping the precise trade-offs—a point we note as a limitation due to computational cost (line 242)—our current results successfully validate the core mechanism of our approach.\n\n## Q4\n- *Can neural network embeddings effectively characterize proof states? To my knowledge, they are primarily used for shallow semantics.*\n\nTo answer the question of whether embeddings can effectively characterize proof states, our results in Section 2.2 can provide some insight. In particular, the difference in performance between the SEPARATE and COMBINED (SMALL GOAL) models. The SEPARATE model encodes the tactic without access to the proof state information, whereas the COMBINED (SMALL GOAL) model generates a tactic embedding given access to a single embedding of the original proof state. For our tasks of predicting the environment output, status and time, we observe that this additional goal information is beneficial, indicating a proof state embedding which effectively captures some relevant information for these tasks.\n\nMore generally, there have been works which use only a single embedding of the proof state as input to a proof model (e.g. [1]). In some cases, the embeddings are based on structuring the proof state as an AST which can help improve performance for smaller models. The results from these works also provide a positive answer to the question of whether NN based embeddings can effectively characterize a proof state.\n\n[1]: \nWu et al. (2023). TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning. https://arxiv.org/abs/2102.09756."}, {"review_id": "2aHmUmscLq", "reviewer": "Reviewer_YkZF", "summary": "The paper addresses a critical issue in the intersection of LLMs and Lean: the semantic redundancy among multiple strategies generated by LLMs, which significantly increases unnecessary computational overhead. To tackle this, the authors propose 3D-Prover, a strategy selection algorithm for automated theorem proving. Its objective is to select a subset of candidate strategies that are both high-quality and diverse, thereby improving proof efficiency and success rates.", "questions": "1.If the predictor ( P ) does not predict the execution time, how much would it affect the performance of the algorithm?\n2.Did the encoder, predictor, and decoder in the paper reuse the internal architecture of the LLM, or were they additional components introduced by the authors?\n3.My understanding is that this method has two advantages: on the one hand, it ensures the diversity of the subsets and reduces redundancy; on the other hand, it allows for the selection of higher-quality tactics.\nI am not sure if my understanding is correct.", "limitations": "As mentioned by the authors in the paper.", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths：\nThe content of the paper is comprehensive and the presentation is relatively clear. It addresses an important problem in the field.\n\nWeaknesses：\nThe proposed method relies heavily on black-box models, such as the encoder and predictor, whose internal mechanisms are not transparent to us. Therefore, I have some doubts about the generalizability of this approach. Methods that are effective on the small miniF2F dataset may not necessarily perform well on other tasks.", "was_revised": true, "final_justification": "N/A", "rebuttal": "We thank Reviewer YkZF for their thoughtful review and for recognizing that our paper addresses an important problem in the field with comprehensive content and a clear presentation.\n\n## W1 / Q2\n- *The proposed method relies heavily on black-box models, such as the encoder and predictor, whose internal mechanisms are not transparent to us. Therefore, I have some doubts about the generalizability of this approach. Methods that are effective on the small miniF2F dataset may not necessarily perform well on other tasks.*\n\nThe reviewer raises an important point. We intentionally designed our transition model (Section 2.1) to be an **abstract framework, making it agnostic to the specific architecture of the Encoder and Predictor.** This modularity is in fact a key strength for generalizability.\n\nOur empirical results present a concrete validatation of this design. The *same* framework was successfully applied to two different base models (ReProver and the much larger InternLM2.5) and demonstrated effectiveness on both the miniF2F benchmark and the significantly larger LeanDojo Novel Premises dataset.\nFinally, our response to Q3 of Reviewer Bo1h presents an additional experiment where we found improvements to critic guided search in addition to Best First Search. This performance across different model scales, benchmarks and search approaches provides strong evidence for the generalizability of our approach.\n\n\n## Q1\n- *1.If the predictor ( P ) does not predict the execution time, how much would it affect the performance of the algorithm?*\n\nCan we clarify whether you are referring to the performance of the transition model (Table 1) or the performance of 3D-Prover (Algorithm 1, Table 2/3), as they both utilise the Predictor?\n\nIgnoring the value of the execution time from P in 3D-Prover is equivalent to setting $\\lambda_\\tau=0$, which is the default setting for the results in Table 2 and 3.\n\n## Q2\n- *2.Did the encoder, predictor, and decoder in the paper reuse the internal architecture of the LLM, or were they additional components introduced by the authors?*\n\nAs we discuss from line 123, we initialise the Encoder and Decoder using the pre-trained components from the ReProver LLM, and the Predictor is an additional component which is a single layer MLP. We then fine-tune this architecture over our transition dataset.\n\n## Q3\n- *3.My understanding is that this method has two advantages: on the one hand, it ensures the diversity of the subsets and reduces redundancy; on the other hand, it allows for the selection of higher-quality tactics. I am not sure if my understanding is correct.*\n\nYou are correct in noting two advantages of our approach are ensuring the diversity of subsets, reducing redundancy, as well as selecting high quality tactic subsets. An additional advantage is that it provides a trade-off between the two, through the mechanics of DPP and with the parameter $\\theta$ (Apppendix F, Table 6). Our approach also reduces the computational cost of tactic execution, and leads to faster proof searches (Appendix G)."}, {"review_id": "6dijXe2Wrt", "reviewer": "Reviewer_SA37", "summary": "This paper introduces a novel search algorithm for guiding LLM-based automated (interactive) theorem proving. The core idea is to train a small model to predict the \"dynamics\" of the theorem proving environment, and to then use this model as a signal from which to select a set of diverse and high-quality tactics at each timestep. In order to turn the signal into a distribution over the tactics which incorporates both notions, the authors leverage Deterministic Point Processes (DPP). The experiments are somewhat limited in scope, but suggest this method can lead to small (but meaningful, if statistically significant) improvements over existing methods. As the authors point out, while improving search is unlikely to ever yield as large of an improvement as improving the policy model, progress in this area is still meaningful as it is complementary to works seeking to improve the base model.", "questions": "Suggestions:\n- In the introduction there is a typo: \"It applications\"\n- On page, \"columns b_i\" should likely be \"rows b_i\" (or you have accidentally transposed your matrix dimensions)\n\nQuestions:\n- In table 3, you state that you report the mean += one std dev over 2 runs for pass@1. Am I understanding correctly that you literally computed the arithmetic mean and sample std dev over 2 samples? That is not a meaningful metric, if so. If your sample size is small it would be much better to report (min, max) ranges, or a confidence interval which does not rely on asymptotic normality (eg based on Hoeffding's inequality).\n- In general, do you have any supporting (statistical) evidence that suggests your findings are even statistically significant? I am sympathetic to the difficulties of doing research in this field without access to large computational resources, but as it stands I am not entirely convinced that the single-digit improvements reported downstream are significant.", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 4, "significance": 3, "originality": 4, "strengths_and_weaknesses": "Strengths:\n- The idea is, as far as I know, novel. Leveraging DPPs in particular is a fun and interesting approach to balanced diversity and quality.\n- The paper is well-written, with clear figures and methodology and no unnecessary formalizations (that is: the math that is in the paper serves its purpose).\n- The limitations of the study, including limited (but non-zero) impact on downstream performance and the limited scope of the experiments, are both acknowledged and discussed extensively in the paper.\n- I appreciate that the authors quantitatively evaluated the overhead that this search procedure introduces. In particular, a priori I expected that running the pipeline on each generated tactic would exceed the time it takes to simply execute that tactic, however this appears not to be the case as per Appendix G. This makes me much more optimistic about the method's practical relevance.\n- Work in this area is complementary to a lot of the other stuff that is happening in NLP right now, which from the point of view of interactive theorem proving largely boils down to improving the base (policy) model.\n\nWeaknesses:\n- While it is good that the authors acknowledge that a lack of computational resources casts some doubt on the signifance and generalizability of their findings, it is hard to quantify how big this effect is. As a result, future work would need to confirm that this methodology indeed works as well as these initial findings would suggest.", "was_revised": true, "final_justification": "This paper is not without its flaws. The experiments could really use some fleshing out in order to give a more confident account of when and how this method is applicable; in particular, I agree with Bo1h that the sensitivity of the method to the additional hyperparameters is understudied, which I not believe was resolved completely during the rebuttal. Other reviewers have also rightly questioned the impact of this method, given the marginal gains.\n\nHowever, the paper does a good job of explicitly calling out and addressing these limitations, which I believe to be commendable, and with the changes made to the presentation of the results I am confident that the overall methodology is both novel and valid. I do not think the fact that the gains are not very large is sufficient grounds to reject the paper, since (as pointed out by the authors) improvements in the search method complement other developments in the literature, such as having a stronger base model.\n\nIn conclusion, I find this paper well scoped and written. I believe the community will find the methodology interesting, and that it may prove valuable in practice. I therefore recommend the paper for acceptance.", "rebuttal": "We are grateful to Reviewer SA37 for their thorough and encouraging review, and we appreciate their recognition of our work's novelty and clarity, particularly our \"fun and interesting\" use of DPPs and the quantitative analysis of computational overhead. We are also grateful for their typo suggestions, which we will incorporate into the revision. \n\n## W1 / Q1 / Q2\n- *While it is good that the authors acknowledge that a lack of computational resources casts some doubt on the signifance and generalizability of their findings, it is hard to quantify how big this effect is. As a result, future work would need to confirm that this methodology indeed works as well as these initial findings would suggest.*\n-*In table 3, you state that you report the mean += one std dev over 2 runs for pass@1. Am I understanding correctly that you literally computed the arithmetic mean and sample std dev over 2 samples? That is not a meaningful metric, if so. If your sample size is small it would be much better to report (min, max) ranges, or a confidence interval which does not rely on asymptotic normality (eg based on Hoeffding's inequality).*\n-*In general, do you have any supporting (statistical) evidence that suggests your findings are even statistically significant? I am sympathetic to the difficulties of doing research in this field without access to large computational resources, but as it stands I am not entirely convinced that the single-digit improvements reported downstream are significant.*\n\nWe very much appreciate your thoughtful comments and your recognition of the inherent difficulties in conducting research in Neural Theorem Proving (NTP) without access to extensive computational resources. \n\nAs we discuss in our response to Q3 from Reviewer Bo1h, we have been running additional experiments since submission to obtain larger Pass@k values (and thereby better estimates for Pass@1). **Our results here also represent a larger improvement**. We are actively working to expand our experimental runs to enable more robust statistical analysis in future work.\n\nRegarding your specific comment on Table 3 and the reporting of mean ± one std dev over 2 runs for pass@1: We fully agree that computing the arithmetic mean and sample standard deviation over only two samples is not a statistically meaningful metric. Given the small sample sizes, we acknowledge that this reporting could be improved. For greater transparency, we will revise Table 2 and 3 to report the mean pass@1 value, as well as the maximum and minimum values. The results are as below:\n\n## Pass@1 adjusted (average, max, min) for Table 2\n\n| K | Random (Avg, Max, Min) | 3D-Prover (Avg, Max, Min) |\n|---|------------------------|---------------------------|\n| 8 | (19.0, 19.6, 18.4) | **(24.4, 24.9, 23.7)** |\n| 16 | (25.4, 25.7, 24.5) | **(27.3, 27.8, 26.9)** |\n| 32 | (27.4, 28.2, 26.9) | **(28.2, 28.6, 27.3)** |\n\n## Pass@1 adjusted (average, max, min) for Table 3\n\n| Approach | Average | Max | Min |\n|:---|---:|---:|---:|\n| 3D-Prover (K=8) | **45.7** | **46.1** | **45.3**|\n| No Filtering | 44.8 | 45.7 | 43.7 |\n| Top-8 | 44.3 | 44.5 | 44.1 |\n\nThe broader point about the lack of statistical significance for Pass@k values is highly relevant and reflects a common practice within the NTP community. Pass@k values in the current literature are often reported as point estimates from a single value, often without explicit statistical significance measures such as confidence intervals or p-values.   \n\nFor example, the highly influential [1] report pass@k values without associated statistical significance. Similarly, the recent ICLR25 CARTS [2] reports pass@l rates over the miniF2F-test benchmark explicitly noting that their paper \"does not explicitly report on statistical significance for the experimental results\". \n\nThis practice is largely a direct consequence of the prohibitive computational cost associated with NTP experiments. The process of generating and verifying formal proofs demands considerable resources, given the integration of large LLMs, costly search algorithms and CPU intensive verification. For instance, [2] explicitly states that \"due to computational cost limitation, we only compared the results for one single tree search attempt\". This inhibits the multiple repetitions necessary for robust confidence intervals or p-values.\n\nWe want to assure you that we are committed to statistical rigor where feasible. To address your concern about statistical significance, we highlight that our hyperparameter ablations (Tables 5, 6, and 7) do show statistically significant improvements. Furthermore, the reduction in average proof time presented in Appendix G was significant (p < 0.05), which provides statistical evidence for speeding up proof attempts.\n\n\n[1]: \nLample et al. (2022). HyperTree Proof Search for Neural Theorem Proving. https://proceedings.neurips.cc/paper_files/paper/2022/file/a8901c5e85fb8e1823bbf0f755053672-Paper-Conference.pdf\n\n[2]: \nYang et al. (2025). CARTS: Advancing Neural Theorem Proving with Diversified Tactic Calibration and Bias-Resistant Tree Search. https://openreview.net/pdf?id=VQwI055flA"}]

Author rebuttal:

Meta-review: The paper introduces 3D-Prover, a novel approach to enhancing automated theorem proving by addressing the challenge of intractable search spaces in proof trees.  This method ensures the diversity of selected subsets and reduces redundancy, while also enabling the selection of higher-quality tactics.  During the discussion, it was agreed that the proposed approach is effective, practically applicable, and clearly presented. The authors conducted extensive experiments during the rebuttal period and successfully addressed some of the reviewers’ concerns, I recommend accepting this paper.
Decision: Accept (poster)