3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes

## Abstract

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-valid and miniF2F-test benchmarks by augmenting the ReProver LLM.
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.

## 1 Introduction

Interactive Theorem Proving, as the name suggests,
has traditionally involved a human guiding a proving system
to verify a formal proposition.
It has found applications in a wide range of fields, from secure software (Tan et al., ) to the verification of mathematical results (Hales et al., ).
There has been significant interest in automating this process, with formalization
efforts requiring a high level of human expertise (Klein et al., ).
Beyond this, it is considered a ‘grand challenge’ for AI, requiring a high level of reasoning and planning
to be successful (Reddy, ).
Even the largest current models struggle with the complexity of the task,
with for example GPT-4 only able to solve 13.5% (Thakur et al., ) of the high school level miniF2F-test (Zheng et al., ) benchmark.
This has motivated the development of specialized models and search algorithms to address the unique challenges of the domain (Wang et al., ; Polu et al., ; Jiang et al., ; Han et al., ; First et al., ; Zhao et al., ; Wang et al., ; Whalen, ; Wu et al., ; Wang et al., ; Wang & Deng, ; Rabe et al., ; Polu & Sutskever, ; Mikuła et al., ; Loos et al., ; Li et al., ; Lewkowycz et al., ; Jiang et al., ; ; Gauthier et al., ).

With most non-trivial proofs requiring long chains of correct reasoning,
it is a challenge to generate them in one pass without mistakes.
The addition of a search algorithm is common for addressing this, as is done
by the current state-of-the-art DeepSeek-Prover-V1.5 (Xin et al., ).
Under this paradigm, candidate tactics are generated and executed in the proving system, which
(if successful) results in new subgoals to prove.
This generates a tree of possible proof paths,
where a search algorithm selects the most promising nodes to expand.
The primary challenge faced by these approaches is the exponential growth in the number of proof paths, limiting the complexity of the problems that can be solved efficiently.

Many of the generated tactics are equivalent, modulo variable renaming and other semantics-preserving transformations.
See Figure 1 for a sample search tree from the ReProver (Yang et al., ) system,
where several semantically similar paths are explored, wasting valuable resources.
Simple lexical similarity scores fail to cover the semantics (meaning) of a tactic,
as captured by the effect of the tactic on the environment.
For example, an expression and its negation vary by only a 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, we find approximately 75% of tactics result in an execution error (Section 2.2).
With the execution of tactics in the environment being expensive, this further restricts
the space of proofs which can be explored efficiently.

Figure: Figure 1: An example node expansion for a failed ReProver attempt, which our DPP model was able to prove. Tactics on the left result in the same proof state, tactics on the right result in an error, and tactics in the centre result in a unique proof state. The high error rate and tactic similarity motivates our filtering approach, which prunes the search space to give a diverse set of subgoals.
Refer to caption: x1.png

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 on top of the existing tactic generation and search components.
3D-Prover uses Determinantal Point Processes (Kulesza, ) to prune the proof search space by filtering tactic candidates to a diverse and high quality subset.
The large amount of synthetic data generated from proof attempts enables us to
learn the effect tactics have on the environment, including the likelihood of an error and
the 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 a 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 open source ReProver LLM to obtain a
significant improvement in the success rate, execution time and diversity of tactics,
and the overall proof success rate.

We summarize our contributions as follows:

- •
We study the feasibility of learning the environment dynamics of proving systems.
We demonstrate tactic representations
which capture the likely effect on the environment, using them to predict the likelihood of success and execution time of a tactic,
as well as the resulting proof state or error message.
- •
We propose a novel edge filtering approach using Determinantal Point Processes (Kulesza & Taskar, ),
which leverage these representations to
select semantically diverse subsets of quality tactics.
Our method is modular and can be used with any underlying tactic model.
- •
We evaluate our approach by augmenting ReProver (Yang et al., ) on the miniF2F (Zheng et al., ) benchmark, where
we demonstrate a significant improvement in the tactic success rate, diversity and overall proof success rate.

### 1.1 Related work

There is little prior work on learning the effect of a tactic on the proving environment.
Xin et al. () recently included successful environment responses as an auxiliary learning objective,
however do not investigate the task in detail.
We extend this by modeling the error likelihood,
error messages and execution time, which we use to generate useful tactic representations.
Several approaches have used previous proof attempts to improve performance,
using the sparse binary signal from the proof status of a goal (Bansal et al., ; Wu et al., ).
This has been used to improve search algorithms, as done in (Lample et al., ; Polu et al., ; Wang et al., ).
These approaches do not consider the diversity of the nodes expanded,
with nothing preventing the search from exploring semantically similar paths.
Xin et al. () uses intrinsic reward for exploration by rewarding new nodes in the search tree.
The addition of any node is rewarded equally, even if they are similar (but not identical) to existing nodes.
We instead select tactics based on their diversity with respect to the resulting nodes.
First & Brun () use a diverse ensemble of models to improve
proof performance, whereas we focus on diversity with respect to the environment response, given an arbitrary underlying model (or models).

### 1.2 Preliminaries

We first define the space of goals $\mathcal{S}$, tactics $\mathcal{T}$ and failures $\mathcal{F}$.
For our purposes, these all contain arbitrary strings,
with the goal being a formal proposition, the tactic a command and the failure an error message.
A proof tree is a DAG $G=(V,E)$ where $V\subset\mathcal{S}$ is the set of goals and $E$ the edges between them.
A proof attempt for a goal $g_{0}$ first initialises the proof tree with $V=\{g_{0}\},E=\emptyset$.
The search policy $\pi_{S}:G\times V\rightarrow\mathbb{R}^{+}$ is a distribution over goals given a proof tree,
being used to select a goal $g$ to expand.
The tactic policy $\pi_{T}:\mathcal{S}\times\mathcal{T}\to\mathbb{R}^{+}$ is a distribution over tactics given a goal,
where $N\in\mathbb{N}$ tactics are sampled to give tactics $\{t_{i}\}_{i=1}^{N}\subset\mathcal{T}$.
The goal, tactic pairs $(g,t_{i})$ are then passed to the environment $\mathcal{E}:\mathcal{S}\times\mathcal{T}\to\mathcal{O}$.
For each pair, after $\tau_{i}\in\mathbb{R}$ seconds, it returns either a new set of goals $g_{i}^{\prime}\subset\mathcal{S}$ or an error, $e_{i}\in\mathcal{F}$.
We define this response as the output $o_{i}\in\mathcal{O}$ where ${\mathcal{O}}:=\mathcal{P}(\mathcal{S})\cup\mathcal{F}$.
We further define the status $s_{i}\in\{0,1\}$ as 0 0 if $o_{i}\in\mathcal{F}$, $1$ if $o_{i}\in\mathcal{P}(\mathcal{S})$
and the transition as the tuple $(g,t_{i},s_{i},\tau_{i},o_{i})$.
The proof tree is then updated with $G=G\cup g_{i}^{\prime}$ for all $g_{i}^{\prime}$, and the associated transitions are added as edges to $E$.
This is repeated until a proof is found, or a budget is exhausted.
A proof of $g$ is found when $\mathcal{E}(g,t_{i})=\emptyset$ for any $t_{i}$,
or if all $\{g_{i}^{\prime}\}$ are proven
for $\mathcal{E}(g,t_{i})=\{g_{i}^{\prime}\}\subset\mathcal{S}$.
The result of a proof attempt is the set of transitions $\{(g_{k},t_{ki},s_{ki},\tau_{ki},o_{ki})\}$ for
all selected goals $g_{k}$ and their expanded tactics $t_{i}$.

## 2 Transition Aware Representation Learning

Figure: Figure 2: Our architecture for learning transition aware tactic embeddings. The tokenized tactic $\bf{t}$ and goal $\bf{g}$ are concatenated and passed through the Encoder $E$. A single representation vector $\bf{e}$ is generated by mean-pooling over the tactic token embeddings $\bf{t^{\prime}}$. The Predictor $P$ 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 an error message or new goals to prove. The result is a compact representation of the tactic which captures its effect on the proving environment, enabling our proposed filtering model.
Refer to caption: x2.png

One proof attempt can generate a rather large amount of data.
A single pass of 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.
This section explores the feasibility of using this transition data to learn how tactics affect the environment.
We operationalise 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 further
embed this information into a compact tactic representation.
The upshot, as we show in Section 3, is
that these representations can be utilised to improve the performance of subsequent proof attempts.

### 2.1 Transition Models

We assume a dataset $\mathcal{D}$ of transition tuples $\{(g_{k},t_{ki},s_{ki},\tau_{ki},o_{ki})\}$, as defined in 1.2.
We learn a transition model
$\xi:\mathcal{S}\times\mathcal{T}\to\{0,1\}\times\mathbb{R}\times\mathcal{O}$ which
maps a goal $g_{k}$ and tactic $t_{ki}$ to an estimate of the status $s_{ki}$, time $\tau_{ki}$ and output $o_{ki}$.
We construct our transition model $\xi$ with three components.
For $d\in\mathbb{N}$, the Encoder $E:{\mathcal{S}}\times{\mathcal{T}}\to{\mathbb{R}}^{d}$ takes the goal $g_{k}$ and tactic $t_{ki}$ as input, and outputs a single embedding vector with unit norm,
$E(g_{k},t_{ki})={\bm{e}}_{ki}$, $||{\bm{e}}_{ki}||=1$.
The Predictor $P:{\mathbb{R}}^{d}\to[0,1]\times{\mathbb{R}}$ maps this embedding to
a score for the time prediction and an error probability for the status,
with $P({\bm{e}}_{ki})=(\hat{s}_{ki},\hat{\tau}_{ki})$.
The Decoder $D:{\mathbb{R}}^{d}\times{\mathcal{S}}\to{\mathcal{O}}$ maps the embedding and goal
to the output prediction,
such that $D({\bm{e}}_{ki},g_{k})=\hat{o}_{ki}$.
The transition model is then

$$ $\xi(g_{k},t_{ki})=(P(E(g_{k},t_{ki})),D(E(g_{k},t_{ki}),g_{k}))=(P({\bm{e}}_{ ki}),D({\bm{e}}_{ki},g_{k}))=(\hat{s}_{ki},\hat{\tau}_{ki},\hat{o}_{ki}).$ (1) $$

### 2.2 Experiments

For our experiments, we use an Encoder-Decoder Transformer for the Decoder $D$,
and an Encoder-Only Transformer for the Encoder $E$.
We take the pretrained ReProver (Yang et al., ) 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 $\hat{\tau}_{ki}$ is the output of the first node, and the status prediction $\hat{s}_{ki}$
is taken as the sigmoid of the second.

We investigate four instances of the transition model $\xi$.
For the Combined model (Figure  2), the tactic is concatenated with the goal, and the embeddings from the Encoder are computed for all tokens.
We then generate a single tactic embedding by mean-pooling over the tactic tokens.
We compare this with the Separate model which encodes the tactic without attending to 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, we implement a No Tactic model which does not use the tactic at all, and instead
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 a particular goal which has a high error rate.
This allows us to ground our results in the performance of this baseline, so we can observe the direct effect of the tactic
in predictive performance.
We also compare with an All Tokens model which uses all tactic tokens for the Decoder without reducing to a single embedding.
We maintain the pooling operation over the tactic tokens for the status and time prediction tasks,
but allow the Decoder to attend to all tokens for the output prediction.
We implement this comparison to see the degree of information loss induced by
reducing tactics to a single vector.

Given $\alpha_{s},\alpha_{\tau},\alpha_{o}\in\mathbb{R}^{+}$, with estimates $\hat{s}_{ki},\hat{\tau}_{ki},\hat{o}_{ki}$
and for a minibatch ${\mathcal{B}}\subseteq{\mathcal{D}}$, we optimise the transition loss

$$ $\mathcal{L_{T}}({\mathcal{D}},\xi)=\sum_{(g_{k},t_{ki},s_{ki},\tau_{ki},o_{ki} )\in{\mathcal{B}}}\alpha_{s}\mathcal{L}_{s}(s_{ki},\hat{s}_{ki})+\alpha_{\tau} \mathcal{L}_{\tau}(\tau_{ki},\hat{\tau}_{ki})+\alpha_{o}\mathcal{L}_{o}(o_{ki} ,\hat{o}_{ki}).$ (2) $$

The hyperparameters $\alpha_{s},\alpha_{\tau},\alpha_{o}$ control the weighting of the status, time and output losses.
For simplicity, we set these to 1, however they could be tuned to reflect the relative importance of each task.
We use the binary cross-entropy loss $\mathcal{L}_{s}$ for the status prediction, the mean squared error (MSE) $\mathcal{L}_{\tau}$ for the time prediction,
and the cross-entropy loss $\mathcal{L}_{o}$ for the output prediction.

We obtain the dataset ${\mathcal{D}}$ from a vanilla ReProver attempt on miniF2F-valid,
which results in 498,236 transitions, which we split randomly into 95% training, 5% testing.
There is the possibility of dependence between the splits, as the test set
includes goals seen in training with different tactics.
The No Tactic baseline should capture any of this,
with our results in Section 3.3.1
showing our representations generalise from miniF2F-valid to miniF2F-test.
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 a learning rate of $10^{-5}$ and a batch size of 1.
We train each model for 2 epochs on a single RTX4090, and report the results on the test set.

#### 2.2.1 Results

**Table 1: Results for predicting unseen environment responses given a 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 constraining 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 Section 3. Comparing the Combined and Separate models, allowing the representation to attend to the goal leads to a 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 |
| 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 |

To assess the Output prediction, we use beam search to generate 4 candidate outputs for each transition.
We use the BLEU (Papineni et al., ) and ROUGE-L (Lin, ) scores to assess the quality of the highest scoring beam
in comparison to the ground truth, which is either an error message or a new set of subgoals.
We also report the Top-4 accuracy, which is the proportion of samples which have
one beam identical to the ground truth.
For the Status prediction task, we take the prediction as $1$ if $\hat{s}_{ki}>0.5$ and 0 0 otherwise,
reporting the F1 score, true positive rate (TPR) and true negative rate (TNR).
The Time MSE is the mean squared error of the time prediction over the test set.

Table 1 summarises the performance of our transition models on the test set.
Our results suggest tactic representations 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 higher scores across all metrics of the Combined versus the Separate model support our hypothesis that we can better predict transitions when the tactic embedding attends to the goal.
The All Tokens model, where we allow the Decoder to attend to the full tactic, does not increase performance in comparison to the Combined model.
This shows that we can effectively represent the tactic as a single embedding without any loss of information.
Our results demonstrate the feasibility of learning the environment dynamics of proving systems, which is a difficult task.
To illustrate this, we include all prediction examples for the Combined model, along with their ground truth, in the supplementary material.

## 3 Filtering Model

Figure: (a)
Refer to caption: x3.png

In the previous section we used synthetic proof data to generate semantically aware tactic representations,
allowing us to predict the likelihood of success, execution time and environment response.
We now take this a step further by using these representations to augment proof search.
We first present the necessary background on Determinantal Point Processes, enabling us to introduce our
filtering model 3D-Prover, which prunes tactic candidates based on their quality and the semantic diversity of their representations.
We show that 3D-Prover is able to improve the performance of the ReProver LLM on the miniF2F-valid and miniF2F-test benchmarks,
particularly when a deeper search configuration is used.
We conclude with a multifaceted ablation study showing the effect of our filtering model on the success rate, number of unique responses and execution time.

### 3.1 Determinantal Point Processes

Determinantal Point Processes (DPPs) are a class of probabilistic models for sampling
subsets from a ground set $\mathcal{Y}$.
In line with Kulesza (),
for $|\mathcal{Y}|=n$ we define the kernel $L\in\mathbb{R}^{n\times n}$
of a DPP as the Gram matrix $L=B^{T}B$ for $B\in\mathbb{R}^{n\times d}$,
where column ${\bm{b}}_{i}\in\mathbb{R}^{d}$ of $B$ is a vector representing element $i\in\{1,\dots,n\}$ of $\mathcal{Y}$.
These vectors ${\bm{b}}_{i}$ are commonly decomposed into a set of unit norm diversity features $\bm{\phi}_{i}\in\mathbb{R}^{d}$ and quality scores $q_{i}\in\mathbb{R}^{+}$,
so that ${\bm{b}}_{i}=q_{i}\bm{\phi}_{i}$, $||\bm{\phi}_{i}||=1$ for all $i\in\{1,\dots,n\}$.
The similarity matrix $S$ is then defined as $S_{ij}=\bm{\phi}_{i}^{T}\bm{\phi}_{j}$.

The probability of sampling a subset $A\subseteq\mathcal{Y}$ from a DPP is then proportional to the determinant of the submatrix of $L$ indexed by $A$,
$\mathbb{P}(A)\propto\text{det}(L_{A})=(\prod_{i\in A}q_{i}^{2})\text{det}(S_{A})$.
Geometrically, this determinant is the volume of the parallelepiped spanned by the submatrix $L_{A}$, which
as we see in Figure 3, is maximised based on a 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 () introduce $k$-DPPs which
restricts the size of the subset to a fixed $k\in\mathbb{N}$, and where the probability
of sampling $A$ is normalised over subsets of size $k$.
That is, for a $k$-DPP, $\mathbb{P}(A)\propto\text{det}(L_{A})/\sum_{|A^{\prime}|=k}\text{det}(L_{A^{
\prime}})$.

### 3.2 Filtering Model

Figure: Algorithm 1 3D-Prover

Algorithm 1 defines our filtering model, 3D-Prover,
which maps a list of tactics $T$ from the underlying tactic policy $\pi_{0}$ to a subset $T^{\prime}$ of size $K$.
We use the Encoder $E$ and Predictor $P$ defined in Section 1.2 to generate unit norm tactic embeddings $\bm{\phi}_{i}$ and predict the time and error likelihood.
The embeddings $\bm{\phi}_{i}$ encode the predicted environment response through their direction only, as they are unit norm (Figure 3).
The quality scores $q_{i}$ then scale these tactics based on the underlying model logits $m_{i}$, as well as the predicted error likelihood $s_{i}$ and execution time $\tau_{i}$.
We have hyperparameters for the normalisation temperature $\theta$, as well as the error and time weights $\lambda_{s},\lambda_{\tau}$.
The parameter $\theta$ controls the scaling temperature of the model logits, with a higher temperature flattening out the distribution.
It therefore adjusts the diversity bias of the filtering model by
reducing the impact of the quality scores when sampling.
We then compute the kernel $L$ from $q_{i}$ and $\bm{\phi}_{i}$, and sample a subset of tactics $T^{\prime}$ using the $k$-DPP algorithm (Kulesza & Taskar, ).

### 3.3 Experiments

To test the performance of 3D-Prover, we use ReProver (Yang et al., ) as the underlying tactic policy $\pi_{0}$, with the Encoder $E$ and Predictor $P$ components as defined in Section 1.2.
We chose ReProver as it is a small ($\sim$ 300M parameters), popular and performant open source model, allowing us to run our experiments in a reasonable timeframe.
We run our experiments in Lean 3 (De Moura et al., ) using the BAIT (Lamont et al., ) platform with a modified LeanDojo (Yang et al., )
environment, where we set an environment timeout of 600 seconds per proof attempt.
We train a combined transition model on the miniF2F-valid benchmark,
and use the Encoder and Predictor components to generate tactic embeddings and quality scores as per Algorithm 1.
We first examine the performance of 3D-Prover
without any hyperparameter tuning, setting
$\lambda_{s}=\lambda_{\tau}=0$, $\theta=1$.
We then perform ablation studies using 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 four attempts per proof to increase confidence in the results,
while for miniF2F-valid we allow one attempt per configuration to facilitate a wider set of ablations.

We set the search policy for all experiments to be Best First Search (BestFS), where nodes are expanded in order of their cumulative log probability.
For each node selected for expansion, we generate $N=64$ candidate tactics from the underlying ReProver model using beam search with default settings, as done in the original ReProver implementation.
This forms the ground set for the node, to be sub-sampled by the filtering algorithm.
We use beam search decoding because it is deterministic and so ensures that the ground set for a given node remains fixed across runs, allowing us to isolate and compare
the effect of the filtering algorithm.
The filtering algorithm returns $K$ tactics, which are then executed in the environment
and used to update the proof tree, as outlined in 1.2.
We test three different levels of filtering, with $K\in\{8,16,32\}$.
Lower values of $K$ correspond to more filtering, for which the choice of filtering algorithm will have a greater impact.
We compare the filtering approach of 3D-Prover, as outlined in Algorithm 1, with two baselines.
The Top-$\mathbf{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-focused comparison.

#### 3.3.1 Proof Performance

**Table 2: Percentage of proofs found after one attempt (Pass@1) on miniF2F, with $K$ tactics selected per node, using tactics generated from ReProver. 3D-Prover uses a transition model trained from miniF2F-valid transitions. For miniF2F-test, we report the mean $\pm$ standard error over four runs, with Top-$K$ being deterministic. The Gain column reports the relative improvement over the Top-$K$ baseline. 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.**
|  | miniF2F-test | miniF2F-valid |  |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- |
| $K$ | Top-$K$ | Random | 3D-Prover | Gain | Top-$K$ | Random | 3D-Prover | Gain |
| 8 | 22.4 | 19.0 $\pm$ 0.98 | 24.4 $\pm$ 0.22 | +8.9% | 21.7 | 19.3 | 25.0 | +15.2% |
| 16 | 26.5 | 25.4 $\pm$ 0.39 | 27.3 $\pm$ 0.21 | +3.0% | 26.6 | 24.2 | 29.1 | +9.4% |
| 32 | 27.8 | 27.4 $\pm$ 0.26 | 28.2 $\pm$ 0.25 | +1.4% | 27.9 | 27.5 | 28.7 | +2.9% |

Table  2 shows the Pass@1 results of our experiments on miniF2F,
which is the number of proofs successfully found after a single attempt.
We observe that 3D-Prover significantly outperforms
both baseline approaches.
We also note that Top-$K$ selection performs better than the Random approach, which is unsurprising.
The influence of the filtering algorithm becomes more apparent as $K$ is decreased,
as there are more tactics filtered out.
Our results are consistent with this, with the magnitude of improvement given by 3D-Prover increasing for lower values of $K$.
3D-Prover is able to outperform both baselines by providing a tradeoff between
the quality, as represented by Top-$K$, and the diversity 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), the Pass@1 performance for lower values of $K$ is generally lower, however over multiple attempts it can be beneficial to use deeper searches (see Appendix A.1).
Finding deep proofs has to date been a significant challenge ( e.g. Polu et al. ()),
with the search tree growing exponentially with the proof depth.
The improvement given by 3D-Prover, particularly for deeper search configurations,
is a step towards addressing this.

Tree search should be considered as an augmentation of the base model, with the degree of any improvement much smaller than what can be 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 advancement of new and better generators.
For example, the state-of-the-art DeepSeek-Prover-V1.5 (Xin et al., ) obtains around 2–4% relative improvements
in proof success over miniF2F-test with its novel tree search algorithm, compared to no search (Figure 5).
In comparison, improving their base model yields a $\sim$36% relative improvement (Table 1).
Similarly, Han et al. () obtain $\sim$6–9% relative improvements (Table 7) for search, with $\sim$40,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.

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 with each full attempt taking at least 12h on our hardware.
Despite this, we were able to obtain our improvements without any tuning,
demonstrating the effectiveness of our approach. We also highlight that the
miniF2F-test results were obtained by training with transitions from miniF2F-valid,
showing that 3D-Prover remains effective
for proofs out of distribution.

#### 3.3.2 Ablation Study

##### Effect of the Transition Model

**Table 3: Percentage of proofs found after one attempt (Pass@1) on miniF2F-valid, 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$ | Autoencoder | Transition Model | Gain |
| --- | --- | --- | --- |
| 8 | 23.0 | 25.0 | +8.7% |
| 16 | 27.9 | 29.1 | +4.3% |
| 32 | 27.0 | 28.7 | +6.3% |

To demonstrate the utility of our transition model 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.
In this way, we can test our hypothesis that semantically aware tactic representations
are useful for proofs, justifying the inclusion of the transition model.
As we observe in Table 3, 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 a direct improvement in proof performance.

**Table 4: Tactic success percentage per node for miniF2F-valid (Mean $\pm$ Standard Error), where $\lambda_{s}$ controls the error weight of quality score in 3D-Prover. These results demonstrate that 3D-Prover leads to fewer errors on average, which can be controlled by increasing $\lambda_{s}$.**
|  |  |  | 3D-Prover |  |
| --- | --- | --- | --- | --- |
| $K$ | Top-$K$ | Random | $\lambda_{s}=0.1$ | $\lambda_{s}=0.5$ |
| 8 | 39.0 $\pm$ 0.1 | 33.4 $\pm$ 0.1 | 43.3 $\pm$ 0.1 | 56.5 $\pm$ 0.1 |
| 16 | 39.0 $\pm$ 0.1 | 30.9 $\pm$ 0.1 | 40.0 $\pm$ 0.1 | 51.7 $\pm$ 0.1 |
| 32 | 35.0 $\pm$ 0.2 | 29.7 $\pm$ 0.1 | 35.7 $\pm$ 0.1 | 41.7 $\pm$ 0.1 |

##### Success Rate

We observe from Table 4 that the success rate of tactics chosen by 3D-Prover is significantly improved compared to both baselines.
We also note that 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 weight $\lambda_{s}$,
which scales the quality scores of tactics by their predicted probability of success.
This suggests the error weight term is directly influencing the tactic success rate,
showing that it is working as intended.

**Table 5: Percentage of unique environment responses per node in miniF2F-valid (Mean $\pm$ Standard Error). Unique defines either syntactically distinct error messages or responses including at least one previously unseen subgoal. $\theta$ controls the temperature of the model scores when calculating quality. We see that 3D-Prover gives a higher diversity of environment responses, increasing with $\theta$.**
|  |  |  | 3D-Prover |  |
| --- | --- | --- | --- | --- |
| $K$ | Top-$K$ | Random | $\theta=1$ | $\theta=4$ |
| 8 | 83.9 $\pm$ 0.1 | 88.6 $\pm$ 0.1 | 90.8 $\pm$ 0.0 | 91.7 $\pm$ 0.0 |
| 16 | 77.5 $\pm$ 0.1 | 81.4 $\pm$ 0.1 | 85.9 $\pm$ 0.1 | 86.6 $\pm$ 0.1 |
| 32 | 71.1 $\pm$ 0.1 | 72.7 $\pm$ 0.1 | 77.6 $\pm$ 0.1 | 78.1 $\pm$ 0.1 |

**Table 6: Percentage of successful tactics per node resulting in unique subgoal(s) over miniF2F-valid (Mean $\pm$ Standard Error). $\theta$ controls the temperature of the model scores in 3D-Prover when calculating quality. We observe 3D-Prover gives a higher number of unique subgoals per tactic, leading to a more diverse set of proof paths, with larger $\theta$ controlling this.**
|  |  |  | 3D-Prover |  |
| --- | --- | --- | --- | --- |
| $K$ | Top-$K$ | Random | $\theta=1$ | $\theta=4$ |
| 8 | 85.3 $\pm$ 0.1 | 89.9 $\pm$ 0.1 | 90.1 $\pm$ 0.1 | 91.1 $\pm$ 0.1 |
| 16 | 77.5 $\pm$ 0.1 | 84.1 $\pm$ 0.1 | 84.9 $\pm$ 0.1 | 85.5 $\pm$ 0.1 |
| 32 | 72.3 $\pm$ 0.2 | 76.3 $\pm$ 0.2 | 76.9 $\pm$ 0.2 | 77.5 $\pm$ 0.2 |

##### Diversity

To examine the diversity of a proof attempt, we consider two metrics. For the first, as in Table 5, we look at the percentage of unique environment responses to tactics executed per node, including responses with unique errors.
As it is difficult to select tactics guaranteed to be successful (see Table 4), an exploratory policy should generate tactics
which result in more varied outputs, so as to better explore the space.
Table 6 quantifies the likelihood of a successful tactic resulting in a new proof path, where we restrict only to successful tactics to account for the discrepancy in success rate between approaches.
This gives a direct metric measuring the effectiveness of tactics in providing distinct proof paths to explore.
We first observe that the Random baseline leads to higher diversity, as expected.
3D-Prover outperforms both baselines, giving more diverse responses for both valid and invalid tactics.
As intended, increasing the parameter $\theta$ results in further improvements to diversity under these metrics.

**Table 7: Tactic execution time in milliseconds over miniF2F-valid proof attempts (Mean $\pm$ Standard Error). $\lambda_{\tau}$ controls the time weighting of the quality score in 3D-Prover. 3D-Prover selects faster tactics on average, with larger $\lambda_{\tau}$ magnifying this.**
|  |  |  | 3D-Prover |  |
| --- | --- | --- | --- | --- |
| $K$ | Top-$K$ | Random | $\lambda_{\tau}=0.1$ | $\lambda_{\tau}=1.0$ |
| 8 | 206 $\pm$ 0.8 | 198 $\pm$ 0.9 | 155 $\pm$ 0.5 | 136 $\pm$ 0.5 |
| 16 | 220 $\pm$ 0.8 | 218 $\pm$ 0.9 | 176 $\pm$ 0.6 | 152 $\pm$ 0.5 |
| 32 | 224 $\pm$ 0.8 | 215 $\pm$ 0.8 | 191 $\pm$ 0.7 | 181 $\pm$ 0.6 |

##### Execution Time

Table 7 shows the execution time for tactics over miniF2F-valid transitions.
Again we see that 3D-Prover outperforms both baselines,
with the improvement increasing with more filtering.
Increasing the time weight $\lambda_{\tau}$ 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.

## 4 Conclusion

##### Future work

One might consider structured DPPs (Kulesza, ), which operate at the tree level to select diverse paths, rather than the node level, which selects diverse edges.
Continual learning of the transition model is another avenue, where training on new data as it is generated could lead to more accurate assessments of diversity and quality.
Our approach could also be combined with a separate search algorithm such as HTPS (Lample et al., ), rather than BestFS.
Testing larger models would be a natural extension, for both the transition model and
the underlying tactic generator.
Our methodology may also be useful to enhance search in domains beyond formal proving, such as code generation or game playing.

##### Summary

We introduce 3D-Prover, a method to augment
proof search by filtering candidate tactics to generate diverse and high quality subsets.
By generating tactic representations which
reflect the response of the proving environment,
3D-Prover is able to filter tactics based on their likely outcome.
We evaluate 3D-Prover by augmenting the ReProver LLM on the standard miniF2F benchmark,
where we find an improvement in the overall proof success rate (Table 2), particularly for deeper searches.
Our ablation studies confirm the utility
of our tactic representations, which allow the selection of tactics with improved success rates,
diversity, and/or execution time.
By effectively pruning the search space, 3D-Prover
is a step towards enabling deeper automated proofs.

## Appendix A Appendix

### A.1 Pass@k

**Table 8: Percentage of proofs found after four attempts (Pass@4) on miniF2F-test, with $K$ 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 8 shows the Pass@4 results for miniF2F-test, which is the number of proofs found at least once over four attempts.
We compare 3D-Prover to the Random baseline, taking the same four runs from
Table 2, where $\lambda_{s}=\lambda_{\tau}=0$, $\theta=1$.
With Top-$K$ being deterministic, the Pass@$k$ rate is the same as the Pass@1 rate.
Given several attempts, $K=16$ appears to provide a good tradeoff between breadth and depth, performing the best overall.
3D-Prover maintains a large improvement for
$K=8$, with a modest improvement for $K=16$.

As discussed by Chen et al. (), the Pass@$k$ metric favours exploratory
approaches as $k$ increases, at the cost of lower performance for smaller $k$.
This is because, over many attempts, a highly exploratory approach is more likely to find at least one proof of a given goal, even though it may find fewer proofs in a single attempt than a more exploitative approach.
Further discussion in Lample et al. () finds that
randomly sampling search parameters also improves Pass@$k$.
With Pass@$k$ being expensive to estimate, we fix our parameters over the four runs to give a more accurate estimate of Pass@1.
Given this, a large scale experiment sampling these hyperparameters could
lead to improved Pass@k results, as Lample et al. () show for their HTPS approach.

### A.2 Proof success rate over hyperparameters

**Table 9: Pass@1 results on miniF2F-valid, over different hyperparameter configurations for 3D-Prover.**
|  | ($\lambda_{s}$, $\lambda_{\tau}$, $\theta$) |  |  |  |  |
| --- | --- | --- | --- | --- | --- |
| $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) |
| 8 | 25.0 | 25.0 | 25.8 | 22.5 | 23.8 |
| 16 | 29.1 | 28.7 | 27.9 | 27.0 | 26.6 |
| 32 | 28.7 | 28.3 | 28.7 | 27.9 | 27.0 |

Table 9 shows the Pass@1 results on miniF2F-valid for 3D-Prover for our limited hyperparameter sweep.
These results suggest that a lower time weight $\lambda_{\tau}$ leads to better proving results.
The diversity parameter $\theta$ hinders performance for the larger value,
consistent with what was observed by Chen et al. (), where they observe a tradeoff between exploration and Pass@1.
Although these parameters may not improve Pass@1, different proofs may favour different configurations, with some requiring e.g. more depth or exploration than others. As discussed above, a higher Pass@$k$ can usually be obtained by sampling a wide set of these parameters.
For the set of hyperparameters we tested here,
we found a cumulative proof rate (or Pass@15) of 32.8% on miniF2F-valid.

### A.3 Embedding Discussion

Figure: Figure 4: Cosine similarity between tactic embeddings resulting in unique subgoals, for a 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.
Refer to caption: x5.png

Figure: Figure 5: 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.
Refer to caption: x6.png

##### Embedding Comparison

We now investigate whether the transition model (Figure 2) captures tactic semantics rather than syntax in
its tactic embeddings.
To test this, we examine the cosine similarity of tactic embeddings which lead to unique subgoals.
Figure 4 takes an example node, examining all tactics which lead to a 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.3.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 a 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 in minF2F-valid.
Figure 5 shows 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 embeddings better separate unique tactics than Autoencoder embeddings which are based on syntax alone.
The result of this is a higher likelihood of 3D-Prover selecting tactics which give unique subgoals,
which as we show in Section 3.3.2,
results in the transition model outperforming the Autoencoder for proof discovery.

##### Embedding Objective

As outlined in Section 2, we 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 to tactics
predicted to have errors, where the errors are diverse in terms of their predicted message.
The hyperparameter $\lambda_{s}$ can alleviate this by weighting the scores based on their likelihood of success.
From our experiments (Table 9), there is not necessarily a benefit to Pass@1 by filtering out strongly based on the predicted error likelihood. To speculate,
the error prediction, although quite good, is imperfect with
many false negatives (Table 1).
This can lead to potentially useful tactics being ignored if the error prediction is overly trusted, even though there is a higher tactic success rate overall as in Table 4.
Given these prediction errors, it may be the case that selecting goals which are predicted to lead to (diverse)
errors may be preferable, given the possibility they result in successful new subgoals.
These subgoals may be be quite different from those previously selected, as they are mispredicted, so are clearly outside
the space of tactics 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 error rate of tactics, this would
ignore a large proportion of the transition data.

### A.4 Computational Overhead

On our hardware, we found 3D-Prover adds a constant overhead, taking approximately 2x as long for tactic generation.
The majority of this is in generating embeddings for the 64 tactics, which we were unable to batch on our hardware due to memory constraints.
The DPP algorithm itself added almost no overhead once the embeddings were generated.
This could be sped up by batching (if memory permits), or through a different architecture.
For example, the Separate model in Section 2.2 could be used, where tactics can be batched with much less memory.
An augmented architecture which embeds the goal in isolation, which is then given to the tactic encoder as a single vector, could be used. This would provide a speed up while allowing some attention between the tactic and the goal, although not to the degree allowed for by our Combined model.
As a proof of concept, we used the Combined model as it provides the most goal-aware embeddings to test our filtering algorithm.

## Peer Reviews

confidence: 3
contribution: 3
initial_rating: 6
presentation: 3
questions: For representing the transitions, the paper adopts a specific architecture - encode the goal and tactics followed by a decoder to get the outcome (next goals or error) and a predictor to determine whether the transition led to an error and the time taken. There is no intuition provided to why this is a better architecture. Why note just have a decoder predict the entire tuple? What other architectures were considered and why is the current one most promising? Even if there is no experimental evaluation of other baseline, it would be good to include discussion based on whatever experimentation was done to select this architecture. 

When splitting the 500K transitions into train and test, how did the authors ensure that it is not the case that the same goal, tactics, next-goal triplet in the test set does not show up in another proof and has been included in the training set. Since the transitions are being collected across several proofs, how is the train/test partitioning ensured to be non-overlapping? 

Could you include not just top-4 but also top-k (k= 1 to 4 or 5) in the Table 1?
soundness: 3
strengths: Many generated proof paths are equivalent modulo variable renaming and other semantics-preserving transformations (such as variable renaming). Authors have found that 75% of the proof paths lead to execution error and thus, it is critical to factor them into exploration. Past work has considered sparse binary signal from the proof status of a goal, intrinsic reward for exploration for new nodes, etc but these do not factor in error likelihood, error messages and execution time. Further, addition of new nodes does not factor in node similarity. 

3D-Prover can augment proof search by filtering candidate tactics to generate diverse and high quality subsets. It is able to filter tactics based on their likely outcome. 

The utility of the transition model representations is demonstrated using ablation study where the transition model Encoder is replaced by an Autoencoder of the same size. Augmenting the ReProver LLM on the standard miniF2F benchmark, the paper reports an improvement in the overall proof success rate.
summary: The search space of proofs grows exponentially with the depth of the proof but a number of branches in this space capture sequences that could be semantically similar or lead to errors. Pruning this search space is, thus, critical. The paper looks at using synthetic data from proof attempts to accomplish this pruning. Semantically-aware tactic representations are generated to capture the effect on proving environment and likelihood of success. DPPs are used to select semantically diverse and high quality tactics using these representations.  The developed approach is called Diversity Driven Determinantal Point Process Prover (3D-Prover). The approach is evaluated on miniF2F-valid and miniF2f-test benchmarks by augmenting reProver LLM.
weaknesses: Please see questions for some of the concerns of the reviewer. The reviewer is happy to raise the score if the concerns are addressed.

---

confidence: 4
contribution: 2
initial_rating: 5
presentation: 3
questions: Please address the issues raised in the Weaknesses section.
soundness: 3
strengths: - The paper introduces a novel approach to tactic filtering that emphasizes both diversity and quality. The concepts of transition-aware tactic embeddings and the use of Determinantal Point Processes (DPPs) are innovative in the context of theorem proving, although DPPs themselves are a well-established probabilistic method and not a new contribution of this paper.

- With diversity-driven tactic filtering, the Best-First Search can explore deeper proofs, leading to a faster proof search overall. This is impressive. However, I did not find a comparison of execution times with and without filtering. Table 7 compares execution times with other baselines, but the paper does not clarify the improvement in proof search time specifically due to filtering.

- The tactic filtering method discards a significant portion (87.5%) of sampled tactics from the ReProver LLM for each tactic state, with the proposed 3D-Prover filtering approach outperforming baseline methods like Top-K and Random filtering. By effectively reducing the tactic space, this filtering approach enables more efficient proof searches with fewer resources. While this is a strong result, it would be even more compelling if the paper included a comparison against a no-filtering setup (i.e., considering all 64 tactics).
summary: The paper presents a method to address a key issue in automated theorem proving: the vast search space that grows exponentially with proof depth due to numerous potential tactics. To manage this complexity, the authors introduce 3D-Prover, a filtering mechanism for proof tactics that prioritizes diversity and quality using Determinantal Point Processes (DPPs). The method involves two parts:
  - Tactic Representation Learning: The authors generate semantic representations of tactics to predict their impact on the proving environment, likelihood of success, and execution time. This prediction model uses past proof attempts (synthetic data) to form representations of tactics based on their effect rather than mere syntactic similarity.
  - Filtering Mechanism: Using DPPs, 3D-Prover filters the tactic pool, selecting those that are both high quality and semantically diverse. This selection optimizes proof success while minimizing redundant tactic exploration.

This paper augments the ReProver LLM (proposed in an earlier paper) by introducing a tactic filtering mechanism (3D-Prover) at each step of the proof search, whereby the tactic space is reduced. The authors use Best-first Search for proof search where nodes are expanded in order of their cumulative log probability. Specifically, for each tactic state, the ReProver LLM is used to sample 64 candidate tactics. From the 64 tactics, the proposed tactic-filtering mechanism is used to select a subset of K (set at 8, 16 or 32) tactics. A lower value of K indicates a strong filtering and is aimed to cut down the proof search even more. The authors compared their filtering (from 64 tactics to K = 8, 16 or 32 tactics) with two baselines viz., Top-K (selects top K tactics from 64 candidate tactics, based on their log probabilities) and Random (selects K tactics at random from the 64 candidate tactics). 

3D-Prover is tested on the miniF2F-test and miniF2F-valid benchmark, where the basic prover framework is the same as the ReProver LLM, and 3D-Prover is used as a tactic filtering step at each state. The authors claim that filtering tactics results in an increased proof success rates due to reduced execution time, and more diverse tactic sets. The approach demonstrates scalability and effectiveness for deeper, complex proofs, addressing challenges faced by other models like DeepSeek-Prover-V1.5 and contributing to proof success beyond the generator's baseline. The experiments indicate that 3D-Prover outperforms traditional Top-K or Random tactic selection, when 3D-Prover filtering is applied. 

Notably, from Table 2, it is evident that for the Top-K baseline, the pass@1 metric i.e., the number of proofs found by ReProver after one attempt is 22.4%. And by incorporating filtering by 3D-Prover with K=8 (i.e., a stricter tactic filtering), pass@1 increases to 24.4%. However for K=32, the pass@1 metric increases minutely from 27.8% to 28.2% because of tactic filtering. A Random filtering, as expected, performs worse than Top-K baseline or the proposed 3D-Prover filtering. The authors also perform ablation study to demonstrate that the filtered tactics are indeed diverse. 

The authors claim that 3D-Prover's design, which layers a diversity-driven tactic filter atop conventional LLMs, points to a promising direction for automated theorem proving, enabling faster, deeper proofs while controlling for computational resources.
weaknesses: - The preliminaries and transition models presented in Section 1.2 and 2.1 could have been written in a simplified manner. Some notations are hard to follow and expressed in a circuitous way.

- Why is the decoder taking as input a concatenation of e and g, when e is already an encoded and pooled version of t and g? What is the motive of having g twice?
Also, e is an encoded version. How is concatenating an encoded string to a non-encoded string g, meaningful?

- The authors use metrics like BLEU, ROUGE-L-F1 and top-4 accuracy (proportion of samples which have one beam identical to the ground truth) to evaluate the "Output" in Figure 2. BLEU and ROUGE are similarity metrics. How is checking similarity with the ground-truth "Output" relevant? Because even if the generated "Output" and the ground-truth "Output" are very close according to these similarity scores, they may not be a syntactically and semantically correct next tactic state.

- In lines 408-418, I do not see the quoted values in the referred tables: "∼36% relative improvement (Table 1)" and "∼6–9% relative improvements (Table 7)". It is not clear if these refer to the tables in the respective papers.

- I have concerns about the training dataset used for the Transition Model. Specifically, in lines 220-222, it is mentioned that "We obtain the dataset D from a vanilla ReProver attempt on miniF2F-valid, which results in 498,236 transitions, which we split randomly into 95% training, 5% testing." i.e., 3D-Prover uses a transition model trained from miniF2F-valid transitions. In that case, doesn't that mean that in Table 2, the proof search results for miniF2F-valid, are trained and evaluated on the same dataset? And for this reason, the results for miniF2F-valid in Table 2 are significantly better than those for miniF2F-test? 
Further, the improvement in pass@1 values on the miniF2F-test is not that significant. For K=8, there is a 22.4% to 24.4% i.e. a 2% increase in the number of proofs found. And this improvement goes down to 0.4% (27.8% to 28.2%) for K=32.
Also, the paper does not provide the results without any kind of filtering.

- One of the most concerning weaknesses of this paper is that it does not compare the ReProver (for tactic prediction) + 3D-Prover (for tactic filtering) framework against any state-of-the-art method like DeepSeek-Prover, InternLM-Math, etc. The filtering method is only compared with two baseline tactic filtering mechanisms i.e., Random filtering and top-k filtering. But the paper does not show whether the effect of this filtering is significant enough, such that it outperforms other state-of-the-arts that do not use filtering or use some kind of state-of-the-art filtering.

Although the 3D-Prover introduces a novel design by layering a diversity-driven tactic filter on top of conventional LLMs, the paper falls short in evaluating and demonstrating its superiority over state-of-the-art theorem provers. Additionally, the results show only minimal improvement compared to baseline tactic filtering methods, such as Top-K and Random filtering.

---

confidence: 4
contribution: 3
initial_rating: 5
presentation: 3
questions: Please refer to the first point in Weaknesses.
soundness: 2
strengths: 1. This paper introduces an additional filtering mechanism within language model-based tactic tree search, providing a fresh perspective for research on tree search in theorem proving.
2. Experimental results demonstrate noticeable performance improvements even with a relatively small number of filtered tactics, suggesting that the diversity-based screening method is effective for scenarios with limited computational resources.
summary: - This paper proposes a method to filter tactics generated by sampling a tree search policy based on diversity in formal theorem proving. To capture tactic diversity, it uses an encoder to embed both the tactic and the goal it is applied to, followed by Determinantal Point Processes (DPP) to select tactics based on these embeddings.
- The encoder used for embedding is trained on two tasks: (a) an auxiliary decoder that applies cross-attention on the embedding to predict the environment’s response after applying the tactic (yielding the next goal if successful, or error messages if unsuccessful); (b) a single-layer MLP that predicts both the success of the tactic and the time required by the Lean prover to verify it. In the final tactic selection step, embeddings are also weighted according to predictions from the MLP regarding tactic success and Lean prover verification time.
- Experimental results show that the tactics selected by 3D-Prover achieve a significantly higher pass rate compared to the baseline.
weaknesses: 1. The paper filters tactics only after they have been sampled by a language model, so the computational cost of model sampling remains unchanged. While the paper tries to reduce Lean prover calls with a specialized filtering algorithm, it does not provide a comparative analysis on this aspect. Does 3D-Prover achieve better results than the case that these computational resources were used to apply the Lean prover to all tactics the language model generated?

2. The paper emphasizes balancing quantity and diversity in tactic selection from the sampled tactics. However, given limitations in the language model’s capability, it may not generate tactics diverse enough to meet the problem’s requirements. This suggests that the proposed method may not fundamentally improve the success rate beyond the language model’s own capacity, limiting 3D-Prover’s primary advantage to efficiency (though this, as noted in *Weakness 1*, requires further estimation).

---

confidence: 4
contribution: 3
initial_rating: 6
presentation: 3
questions: I wonder what the intuition is for preferring shorter execution time for tactic. Tactic execution time can vary based on factors like the goal state; for example, `linarith` may require different durations depending on the complexity of the arithmetic expressions involved. Moreover, while tactics like `linarith` can take longer for more complex arithmetic, they are often the very effective in reducing the theorem down to its underlying logic.
soundness: 4
strengths: - The proposed algorithm, 3D Prover, is well-motivated and practical. The paper presents an approach to augmenting proof search history using an existing LLM to enhance tactic selection, resulting in more efficient navigation within the search space.
- The semantic-aware representation learning of proof states and tactics is well-established and analyzed. The representations learned from proof history are useful for downstream tasks, including proof synthesis. The experimental design and results demonstrate the impact of each component of the proposed learning framework.
- The proposed filtering framework is straightforward and effective, with results outperforming ReProver without modifying the underlying model. This approach is thus beneficial for advancing proof synthesis in large language models.
summary: The paper introduces 3D Prover, a framework that combines a representation learning algorithm to generate semantically aware encodings of proof states and tactics with a filtering algorithm for enhancing semantic diversity in LLM-generated tactics for proof synthesis. The proposed method was tested on top of ReProver, demonstrating its effectiveness. Additionally, ablation studies validate the contribution of each component in the design.
weaknesses: - Section 3.1 could benefit from greater clarity. Specifically, the motivation behind using this method could be expanded upon - why was DPP chosen over other sampling algorithms for balancing quality and exploration in this context?
- In the experiments, both $\lambda_s$ and $\lambda_{\tau}$ are set to zero. Additionally, Section A.2’s hyperparameter sweep further suggests that these terms (or at least $\tau_i$) do not significantly contribute to filtering performance. Although this result is not unexpected, it should be explicitly discussed in the experiments section to enhance the clarity of the findings.

Meta-review: This paper concerns pruning proof search of neural theorem proving and proposes 3D-Prover, which is built on top of the previous work ReProver and consists of a representation learning component capturing the transition semantic of theorem proving, and a filtering mechansim for proof tactics using Determinantal Point Processes (DPPs). DPPs are used to select semantically diverse and high quality tactics. The experimental evaluation shows that 3D-Prover outperforms baselines like Top-K and random filtering. Using DPPs to filter proof tactics in the context of neural theorem proving is novel, however, its effectiveness is not significant. Reviewers and the AC share concerns regarding the evaulation setup (e.g., filtering vs no-filtering) and effectiveness (e.g., marginal improvement compared to simple baselines).

Decision: Reject