Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically

## Abstract

Abstract Mathematical theorem proving is an important testbed for large language models’ deep and abstract reasoning capability. This paper focuses on improving LLMs’ ability to write proofs in formal languages that permit automated proof verification/evaluation. Most previous results provide human-written lemmas to the theorem prover, which is an arguably oversimplified setting that does not sufficiently test the provers’ planning and decomposition capabilities. Instead, we work in a more natural setup where the lemmas that are directly relevant to the theorem are not given to the theorem prover at test time. We design an RL-based training algorithm that encourages the model to decompose a theorem into lemmas, prove the lemmas, and then prove the theorem by using the lemmas. Our reward mechanism is inspired by how mathematicians train themselves: even if a theorem is too challenging to be proved by the current model, a positive reward is still given to the model for any correct and novel lemmas that are proposed and proved in this process.
During training, our model proposes and proves lemmas that are not in the training dataset. In fact, these newly-proposed correct lemmas consist of 37.7% of the training replay buffer when we train on the dataset extracted from Archive of Formal Proofs (AFP). The model trained by our RL algorithm outperforms that trained by supervised finetuning, improving the pass rate from 40.8% to 45.5% on AFP test set, and from 36.5% to 39.5% on an out-of-distribution test set.

## 1 Introduction

The reasoning abilities of large language models (LLMs) are a significant marker of artificial intelligence and critical for complex and safety-sensitive applications, e.g., medical diagnosis (Singhal et al., ; Fleming et al., ), legal document review (Guha et al., ),online tutoring (Wang and Demszky, ; Ruan et al., ). Yet recent studies highlight the limited performance of LLMs on reasoning tasks (e.g., Mündler et al. (); Valmeekam et al. () and references therein).

Figure: Figure 1: Left: in the dashed callout block, we show an example of an Isabelle proof and its explanation in natural language. Right: an example of a proof tree. The two child nodes correspond to the two new lemmas proposed in the proof of the root node.
Refer to caption: extracted/5975509/figures/figure0.png

Automated theorem proving by LLMs is an excellent reasoning task that abstracts away the need for numerical manipulation or tool use (e.g., using a calculator) and allows for precise evaluation of correctness with an automatic verifier (such as Isabelle (Nipkow et al., ) and Lean (De Moura et al., )) even without ground truth.
Thanks to tools such as Sledgehammer (Paulsson and Blanchette, ) that can automatically complete low-level details, the granularity of formal proofs is similar to natural language proofs (see Fig. 1 (Left) for an illustrative example).
Note that verifying a proof is fundamentally much easier than generating the proof.(^1^11The former is in P whereas the latter is undecidable in the worst case Turing et al. (); Church ().) Thus, learning to prove theorems from verifiers’ supervision is reminiscent of weak-to-strong generalization (Burns et al., ).

Previous results in this area largely focus on the setting where the theorem prover can use all the lemmas in the formal proof library, including those particularly written to decompose a specific theorem’s proof (Jiang et al., ; Polu and Sutskever, ).
This setting arguably oversimplifies the problem and doesn’t sufficiently test the models’ planning and decomposition capabilities, and it is unclear whether the resulting models can be used to prove new theorems from scratch when such lemmas are not available at test time. Instead, we work in a more natural setup where the theorem prover needs to propose and prove lemmas to decompose the proof hierarchically itself (see Section 2 for more details). In Section 4.2, we demonstrate that this task is much more challenging.

In addition, most existing proof-generation algorithms leverage the formal verifier by (a) providing the verifier’s current proof state to the LLMs step-by-step, and (b) using best-first search algorithms such as MCTS to build a multi-step proof from many LLM-generated steps (Jiang et al., ; Han et al., ). The major challenge of these methods is the high computation cost incurred because (a) requires re-running LLMs on a different context that consists of a verifier’s (long) proof state at every step, and (b) requires generating many proof steps first and then select the best ones. As a concrete example, the search-based algorithm in Lample et al. () requires more than 1K GPU days with A100s to train a model with 600M parameters, whereas our method only takes less than 36 GPU days to train a 7B parameter model.

Figure: Figure 2: Illustration of our algorithm Proof Decomposer, *ProD-RL*. In step 2b, the statement is locally correct if it is proved correctly using the proposed lemmas, and it is globally correct if all the proposed lemmas are also proved correctly. As an important feature of our algorithm, even if a theorem (Theorem 1) is not proved by the model because some lemmas (Lemmas 1) are not proved, we still train on the correct lemma (Lemma 2) by setting its reward $r=1$.
Refer to caption: extracted/5975509/figures/figure3.png

To address these issues, we design a method, Proof Decomposer (ProD), which uses LLMs to hierarchically propose and prove new lemmas and generate complete proofs directly without searching. We augment the formal proofs syntax so that the model can propose new lemmas by including their statements during the proof, and prove these lemmas separately. Hence, a complete proof of a theorem forms a tree structure where the child nodes are the lemmas proposed in the proof of the parent node (Fig. 1 (Right)), and the theorem is considered proven only if all the proofs in the tree are correct.

We train our models with reinforcement learning (RL) in a way that somewhat imitates a mathematician’s process: we reward correct partial proofs (i.e., proof sub-trees) even if the original theorem (i.e., the root node) is not proved entirely.
Since our model can generate and prove novel lemmas during training, it can still make progress even if the theorem is too challenging. This is reminiscent of how mathematicians prove standalone lemmas which make progress towards solving an open problem. Our training method can also be viewed as an instantiation of hindsight experience replay (Andrychowicz et al., ), where the hindsight trajectories are correct proof sub-trees. We illustrate our algorithm in Fig. 2, and defer the details to Section 3.2.

We test our model, ProD-RL, by generating proof trees on holdout theorems that the model has not been trained on, and show that ProD-RL improves upon existing baselines.
Compared with the supervised fine-tuned (SFT) model, our model improves the pass rate from 40.8% to 45.5% on the holdout test set, and from 36.5% to 39.5% on out-of-distribution test set, whereas vanilla reinforcement learning without lemma proposals during training does not improve the corresponding SFT model (see Section 4.3).
This is partly because our method encourages the model to propose and prove additional lemmas — in fact, 37.7% of the lemmas proved during training are not in the dataset. As a result, the model still improves even if it is already fine-tuned on the same dataset with human-written ground-truth proofs. However, we also observe that our method, ProD-RL, is less robust to distribution shifts, and we leave further investigation of this issue as future work.

We release our carefully structured test sets that has a clean separation of the train and test theorems from AFP at [https://huggingface.co/kfdong/ProD/tree/main](https://huggingface.co/kfdong/ProD/tree/main). We hope that our test bed can help the community develop and validate models that generalize effectively to novel theorems without human-written lemmas.

## 2 Setup

#### Conditional proofs.

We use the term *conditional proof* to denote a proof that, in addition to the standard formal proof syntax, can propose new lemmas by enclosing their statements by <invoke> and </invoke> tokens (examples shown in the blue boxes of Fig. 1). In particular, a conditional proof has the following format:

$$ $t_{1}\;\text{<invoke>}\;l_{1}\;\text{</invoke>}\;t_{2}\;\text{<invoke>}\;l_{2} \;\text{</invoke>}\;\cdots\;t_{k}\;\text{<invoke>}\;l_{k}\;\text{</invoke>}\;t _{k+1}$ $$

where $t_{1},\cdots,t_{k+1}$ denote proof segments in the original formal proof syntax (see e.g., Fig. 1, proof texts in black), and $l_{1},\cdots,l_{t}$ denote proposed lemma statements (see e.g. Fig. 1, proof texts in red).(^2^22In this paper, we use the terms ‘lemma’ and ‘theorem’ relatively — theorem refers to the statement that we are currently focusing on, and lemma refers to the statement proposed during the proof. In other words, there is no fundamental difference between a lemma and a theorem.)

#### Proof tree nodes.

With the proposed lemmas, a complete proof forms a tree structure (as shown in Fig. 1).
A node in a proof tree is a tuple of premises, context, a theorem statement, and a conditional proof.
Premises represent the lemmas that are treated as common knowledge, which are typically not directly relevant to the proof. We allow the model to directly use them in the proof so that it does not have to repetitively prove all the fundamental facts, such as properties of continuous functions and natural numbers.
Context represents the necessary contents to prepare the theorem statement, such as the definition of specific objects/functions. We use the context as part of the prompt for the LLMs to generate proofs, and to configure the proof verifier to check the generated proofs.

#### Correctness of conditional proofs and proof trees.

A proof tree node $n$ with conditional proof

$$ $t_{1}\;\text{<invoke>}\;l_{1}\;\text{</invoke>}\;t_{2}\;\text{<invoke>}\;l_{2} \;\text{</invoke>}\;\cdots\;t_{k}\;\text{<invoke>}\;l_{k}\;\text{</invoke>}\;t _{k+1}$ $$

is *locally correct* if, after adding $l_{1},…,l_{k}$ to the set of premises, $t_{1}…t_{k+1}$, is a proof to the statement of $n$ that is accepted by the formal verifier under the context of $n$.

We consider a proof tree valid if, for every node, each of its child nodes corresponds to one proposed lemma and shares the same premises and context with its parent node. A tree node $n$ is *globally correct* with respect to a given set of tree nodes $N$ if we can construct a valid proof tree with root $n$ using the locally correct tree nodes in $N$. We use this more flexible definition of global correctness since if we generate more than one proof tree per theorem, we may mix their locally correct nodes to form a globally correct proof.

Global correctness corresponds to the standard notion of correctness (i.e., whether the theorem is proved), and local correctness is a weaker concept, referring to the correctness of conditional proofs assuming the proposed lemmas. When a tree node is globally correct, we can construct a complete proof to its statement that is acceptable by the formal proof verifier — first, we build a valid proof tree from the locally correct subset of $N$, and then list all the statements and their corresponding conditional proofs in a child-first order and remove all the lemma proposal steps (since the proposed lemmas and their proofs will be already listed in the proof text according to child-first order).

#### Dataset construction.

We construct the datasets by parsing raw proof-library files into tuples of the form (premises, context, statement, conditional proof).

In particular, we first segment each of the files into blocks
$c_{1}\;s_{1}\;p_{1}\;\cdots\;c_{l}\;s_{l}\;p_{l}$
where the $s_{i}$ are theorem statements, the $p_{i}$ are the corresponding proofs, and the $c_{i}$ are the file contents between proofs, such as object definitions and local assumptions.
Next, we build proof trees from each segmented file by iteratively removing ($s_{i}$, $p_{i}$) pairs from the file if the theorem $s_{i}$ is not referred to in the remaining file contents (in other words, in the first iteration we peel off the root nodes of the proof trees from the file, and then the nodes in the next level, etc.). Note that some theorems cannot be peeled off by this process because they are referred to in some file content $c_{j}$ (e.g., lemmas used to instantiate local objects). We use ${\mathcal{T}}_{\text{tree}}$ to denote the subset of theorems peeled off during the process.

For every theorem $s_{i}$, we construct an example where the context is the concatenation of $\{c_{j}:j<i\}$ and $\{s_{j}:j<i,s_{j}\not\in{\mathcal{T}}_{\text{tree}}\}$ in the order they appear in the file. That is, we exclude all the lemmas that are ever peeled off — the remaining lemmas are included in the context.

To construct the conditional proof of theorem $s_{i}$, we add the proposed lemma statements to the original proof $p_{i}$. In particular, we split the proof $p_{i}$ into steps $t_{1},\cdots,t_{k}$ using the formal language parser. Then for every step $t_{j}$ that uses lemmas $l_{j,1},\ldots,l_{j,n_{j}}$ from ${\mathcal{T}}_{\text{tree}}$, we insert the statements of these lemmas enclosed by the <invoke> and </invoke> tokens, denoted by $\zeta_{j}=\text{<invoke>}\;l_{j,1}\;\text{</invoke>}\;\cdots\;\text{<invoke>}
\;l_{j,n_{j}}\;\text{</invoke>}$, into the proof right before $t_{j}$. In other words, the conditional proof is the concatenation $\zeta_{1}\;t_{1}\;\cdots\;\zeta_{k}\;t_{k}$.
Similar to Jiang et al. (), we use Sledgehammer, a premise selection tool that automatically searches for proofs to the current goal, to replace proof steps that are originally generated by it (see Section A.3 for more details) so that the mode can focus less on the tedious low-level details.

The premises are all the theorems from *predecessor* files, which are typically not directly relevant to the theorem (otherwise they will be stated in the same file). Theorems in the premise set can be used directly in the proof, or they can be selected by Sledgehammer to search for proof steps. In our implementation, the premises are implicitly defined by the dependency graphs of the files.

We split the training and test set (AFP test) based on the dependency of the files in the proof library so that the examples in the training set never refer to any files in the test set (see Section 4.2 for details).
We also construct an additional test set, AFP 2023, by parsing AFP files submitted after the knowledge cutoff date of the Llemma model (April 2023) to eliminate potential data leakage issues.
Compared with prior works (Jiang et al., ; First et al., ), the two major differences in our setup are the availability of lemmas from the same file and the training/test split. In Section 4.2, we discuss and test their effects in detail.

Finally, to construct the SFT dataset, for each example in the training set, if its conditional proof proposes at least one lemma, we create an augmented example by moving the proposed lemmas from the conditional proof into the context — this augmented example does not propose new lemmas and is always locally correct.

## 3 Methods

In this section, we first describe how to use LLMs to generate proof trees, and then introduce our reinforcement learning method (ProD-RL) that rewards the model to decompose proofs hierarchically.

### 3.1 Generating proof-trees using LLMs

To generate proof trees using an autoregressive model $\pi_{\theta}$, we need to first fine-tune the model to follow a specific format:

- (a)
the input $x$ to the model $\pi_{\theta}$ is the concatenation of a context and a theorem statement, and
- (b)
the expected output $y$ of the model is a special token $t_{0}$ followed by a conditional proof, where $t_{0}$ is either <use_invoke> or <no_invoke>, denoting whether the following conditional proof should propose new lemmas.

We introduce the special token $t_{0}$ before a conditional proof so that we can increase the probability of the <use_invoke> token during RL to let the model propose more lemmas for better exploration.

We summarize our proof-tree generation algorithm in Alg. 1. Given a theorem statement $s$ and the corresponding context $c$, we first sample from $\pi_{\theta}$ autoregressively starting with the prompt $x=c\;s$, and ideally the model outputs a special token $t_{0}$ followed by a conditional proof $\rho$ (Line  3). Next, we parse the conditional proof $\rho$ and collect the proposed lemmas $l_{1},\cdots,l_{k}$ for the next round of generation (Line  5). We force the model to generate conditional proofs without proposing new lemmas at a certain depth so that the proof tree doesn’t grow indefinitely, which can be implemented easily by replacing the prompt with $x\textquoteright=c\;s\;\text{<no_invoke>}$ (Line  6).

Figure: Algorithm 1 Generate proof trees (test time)

### 3.2 Reinforcement learning with lemma proposal

Our reinforcement learning method is illustrated in Fig. 2. We start with a supervised fine-tuned model so that it can generate conditional proofs in the desired format. Then at every round, we randomly sample a batch of examples $D$ from the training dataset and perform the following steps.

#### Step 1: Generate proofs.

We first generate proof trees for every theorem in $D$.
For better exploration, we use a modified version of Alg. 1 (shown in Alg. 2 of Appendix A.1) with the following differences:

- (a)
for the theorems where the probability $\pi_{\theta}(\text{<use_invoke>}\mid x)$ is among the top 50% in the batch, we will force the model to generate conditional proofs with $t_{0}=\text{<use_invoke>}$. Otherwise, we sample $t_{0}$ according to the probability of $\pi_{\theta}(\cdot\mid x)$, and
- (b)
for every theorem where the model generates a conditional proof with new lemmas, we also let the model generate another conditional proof without proposing lemmas. If any of these two conditional proofs is globally correct, it can be used to construct proof trees for other theorems.

#### Step 2: Determine the reward of an example.

In this step, we first check the local correctness of each conditional proof using the formal verifier (Step 2a in Fig. 2).

In addition to the verifiers’ output, we apply two filters to help train the model: (a) we filter out trivial lemma proposals — if a proposed lemma directly implies the theorem (e.g., if the proposed lemma has exactly the same statement as the theorem), we simply discard this example, and (b) we remove unnecessary lemma proposals — if the conditional proof is still correct after removing all the references to a proposed lemma, we remove this lemma from the conditional proof.

We then determine the global correctness of the generated proofs. Finally, we assign a binary reward $r(c,s,\rho)$ to each tree node with context $c$, statement $s$, and conditional proof $\rho$ based on its global correctness (Step 2b in Fig. 2).

#### Step 3: Update the model by REINFORCE.

In this step, we first construct a training dataset consisting of examples with format (prompt, target, weight) from the conditional proofs collected in Step 1, and then update the model $\pi_{\theta}$ using the weighted cross-entropy loss.

For each generated conditional proof, we add one example to the training dataset where the prompt is the context concatenated with the theorem statement, and the target is the conditional proof prepended by the <use_invoke> or <no_invoke> token.
Note that the reward of a conditional proof depends not only on the correctness of the conditional proof, but also on the correctness of the proposed lemmas.

To reduce the variance of our gradient updates, we train a value function $V_{\phi}$ that predicts the expected reward of the current policy on a given proof tree node (i.e., $V_{\phi}\approx\mathbb{E}_{\rho\sim\pi(\cdot\mid c,s)}[r(c,s,\rho)]$). The weight of an example is the product of the value function’s outputs on invoked lemmas multiplied with a length penalty to incentivize shorter proofs — for a proof tree node with conditional proof length $h$ and proposed lemmas $l_{1},\cdots,l_{k}$, the weight $w$ of this example is
$w=\gamma^{h}\prod\nolimits_{i=1}^{k}V_{\phi}(l_{i})$
with discount factor $\gamma\in(0,1)$, or $w=0$ if the proof tree node is not locally correct.

To simplify the implementation, we train the value function to predict two special tokens, <true> and <false>, conditioned on the context and theorem statement. Let $p_{\text{t}}$ be the probability of the <true> token conditioned on the context and theorem statement, and $p_{\text{f}}$ the probability of the <false> token. The output of the value function is then $p_{\text{t}}/(p_{\text{t}}+p_{\text{f}})$.

As done for the SFT dataset, we add one augmented example by moving the proposed lemma from the conditional proof to the context for any locally correct conditional proof with new lemmas.
We also add examples constructed from the human-written conditional proofs (i.e., the ground-truth proofs) of theorems in the batch $D$. In addition, we use a replay buffer to stabilize the training.

#### Remarks.

Note that we update the model using partial proofs (i.e., proof sub-trees) even if the original theorem from the dataset (i.e, the root of the proof tree) is not proved. Hence, our method can also be viewed as an instantiation of hindsight experience replay (Andrychowicz et al., ), where the hindsight trajectories are correct proof sub-trees.

Our algorithm is also closely related to expert iteration. In our notation, expert iteration is equivalent to using a binary weight $w=\mathbb{I}\left[\text{the proof tree node is \emph{globally} correct}\right].$

## 4 Experiments

This section presents our experimental results. We first list additional experiment details (Section 4.1) and then compare our setup with prior works (Section 4.2). Finally, we show our main results in Section 4.3 and examples of proposed lemmas in Section 4.4.

### 4.1 Experiment details

#### Proof verification software.

We use Isabelle (Nipkow et al., ) as our proof verification software since the proofs are declarative and human-readable without knowing the verifier’s proof state, and we use PISA (Portal to ISAbelle, Jiang et al. ()) to interact with Isabelle. To check whether a proof tree node is locally correct, we import all the theorems from its premises, move each of the proposed lemmas from the conditional proof to the context, and then add a fake proof indicated by the keyword ‘sorry’ to every lemma statement in the context (In Isabelle, ‘sorry’ will register the statement as a fact even without any actual proof.) The remaining proof steps will follow the original Isabelle syntax, and we can check their correctness directly. We set a 10s timeout for each proof step.

#### Datasets.

Our SFT dataset consists of theorems from Archive of Formal Proof(^3^33[https://www.isa-afp.org/](https://www.isa-afp.org/)) (AFP, retrieved on 2022-12-06) and Isabelle built-in files (such as HOL which contains the theorems that define natural numbers, etc.). The resulting dataset contains 312k examples.

For the test datasets AFP test and AFP 2023, we only keep the theorems in ${\mathcal{T}}_{\text{tree}}$. To construct the test set AFP 2023, we parse the AFP files submitted after the knowledge cutoff date of our pretrained model (April 2023) to eliminate possible data leakages.(^4^44Here we use the archive of AFP retrieved on 2023-11-22.) The AFP test set contains 4.3k theorems and the AFP 2023 test set 2k theorems.

#### Testing setup.

To measure the performance of the models, we sample $k$ proof trees per theorem independently on the test set and report the pass@k performance (that is, a theorem is proved if at least one of the conditional proofs is globally correct with respect to all the generated tree nodes). When generating proofs, we use temperature 0.7 and truncate the context to only include the last 1k tokens. The proof trees are truncated at depth 2.

#### Supervised fine-tuning.

We start from the Llemma 7b model (Azerbayev et al., ) and fine-tune the model for 2 epochs with the standard cross entropy loss.(^5^55In our preliminary experiments, we observe that the model overfits after 2 epochs)
On theorems from AFP, we compute the loss only on the special token and the proof, but not on the context and statement. On Isabelle built-in theorems, we compute the loss on the statement to help the model internalize basic facts.
We use the AdamW optimizer (Loshchilov and Hutter, ) with linear warmup followed by a constant learning rate 1e-5, macro batch size 128, and context window 2048.

#### Reinforcement learning.

The dataset we use for the reinforcement learning stage is ${\mathcal{T}}_{\text{tree}}$, the set of theorems that are iteratively peeled off when parsing AFP files — ${\mathcal{T}}_{\text{tree}}$ contains 104k examples. We first train the model with 1 epoch of supervised fine-tuning, and then run RL for 20 rounds with a batch of 5k random examples per round.
We truncate the proof tree at depth 3 and sample with temperature 0.7 during training for better exploration. We use the same hyperparameters as the SFT stage to update the policy $\pi_{\theta}$,
We initialize the value function $V_{\phi}$ with a Llemma 7b model fine-tuned on our SFT dataset.

### 4.2 Comparison of our new setup with prior works

In this section, we concretely compare our new setup with prior works (Jiang et al., ; First et al., ). Recall that there are two main differences in how we process our dataset:

- (a)
we split the train/test set based on file dependencies so that no theorems in the test set are referred to in the training set, whereas PISA splits theorems randomly, and
- (b)
when testing a proof, we remove certain lemmas from the context.

To show that our setup is indeed more challenging, we first construct datasets formatted similarly to those in (First et al., ). Specifically, we parse the AFP files into examples using the method described in Section 2, with the only exception being that all human-written lemmas are kept in the context. Then we select a subset of theorems as the test set $D_{\text{test}}^{\text{w/ l}}$ based on the dependencies of the AFP files so that the examples in the test set are never used by the remaining theorems (see Section A.3 for more details). Then we split the remaining examples randomly into training and validation datasets, denoted by $D_{\text{train}}^{\text{w/ l}}$ and $D_{\text{val}}^{\text{w/ l}}$ respectively. We use $D_{\text{test}}^{\text{w/o l}}$ to denote the test dataset of our setup where the lemmas are removed from the context. The validation dataset $D_{\text{val}}^{\text{w/ l}}$ mimics prior works’ setup (Jiang et al., ; First et al., ), and $D_{\text{test}}^{\text{w/ l}}$ is an interpolation between prior works’ setup and our setup. Table 1 shows the performance of the model with supervised fine-tuning on $D_{\text{train}}^{\text{w/ l}}$ and all Isabelle built-in theorems. The results suggest that both features of our setup, removing the lemmas and splitting the training/test set by file dependencies, increase the difficulty of the task.

**Table 1: Pass rate on different dataset formats and partitions of the SFT model trained on the $D_{\text{train}}^{\text{w/ l}}$. The validation dataset $D_{\text{val}}^{\text{w/ l}}$ mimics the test setup of prior works, and our setup is $D_{\text{test}}^{\text{w/o l}}$ where the same model performs much worse. The results suggest that our setup is indeed more challenging.**
| Test setup | $D_{\text{val}}^{\text{w/ l}}$: w/ lemmas | $D_{\text{test}}^{\text{w/ l}}$: w/ lemmas | $D_{\text{test}}^{\text{w/o l}}$: w/o lemmas |
| --- | --- | --- | --- |
| split randomly | split by dependency | split by dependency |  |
| pass@4 | 45.7 | 39.7 | 35.7 |

### 4.3 Main results

This section reports the models’ pass@k performance on AFP test and AFP 2023 datasets. For a given dataset, pass@k measures the percentage of the theorems proved by at least one of $k$ proofs generated by the model.
Recall that the theorems in the test set are selected based on the dependencies of the AFP files and are not used in any proofs from the training set (see Section 4.2 for more details). In other words, we do not train the model on test datasets using reinforcement learning. Instead, we test whether ProD-RL is a fundamentally better model when tested on new theorems.

**Table 2: Pass@16 of different models on AFP test sets. Our model with reinforcement learning (ProD-RL) improves upon the SFT model and outperforms baseline methods.**
| Test set | SFT w/o<br>lemma proposal | RL w/o<br>lemma proposal | ProD-SFT | ProD-RL |
| --- | --- | --- | --- | --- |
| AFP test | 43.4 | 42.4 | 40.8 | 45.5 |
| AFP 2023 | 39.4 | 37.7 | 36.5 | 39.5 |

As a baseline method, we train a model on a variant of the SFT dataset where all lemmas are kept in the context. It can be seen as a reproduction of First et al. () with a slightly different way to obtain the context — First et al. () includes all the file content before the statement of the theorem, whereas we only keep the statement of previous lemmas. We also run reinforcement learning on the same RL dataset as our method (see Section A.2 for more details).

Figure: Figure 3: The pass rate of different models on AFP test (Left) and AFP 2023 (Right) test sets. Our RL model improves upon the SFT model whereas without proposing new lemmas (RL w/o lemma proposal), we do not observe any improvement.
Refer to caption: extracted/5975509/figures/AFPtest.png

Table 2 shows the performance of our model on the AFP test sets. For a fair comparison, the baseline models are tested in our new setup without human-written lemmas. Note that the SFT model without lemma proposal outperforms the SFT model with lemma proposal. We hypothesize that it is because proposing correct lemmas itself is challenging, which distracts the model from learning to generate direct proofs. However, RL with lemma proposal improves the SFT model and outperforms others because the model proposes and proves additional lemmas that are not in the training dataset, whereas RL without lemma proposal yields no improvement.

In Fig. 3, we plot the pass rates with different numbers of samples per theorem on both AFP test and AFP 2023. Fig. 3 shows that on AFP test, the ProD-RL model significantly improves upon baseline methods as well as the ProD-SFT. However, on AFP 2023, the improvement is minor over SFT w/o lemma proposal, while ProD-RL still outperforms ProD-SFT. The results suggest that the baseline methods are more robust to heavier distribution shifts, while our method has a larger improvement when the test distribution is closer to the training distribution.

Figure: Figure 4: The pass rate of theorems in AFP test grouped by the depth of their ground-truth proof. Grey bars represent the proof generated by the model SFT w/o lemma proposal, and the colored bars represent the proof trees generated by ProD-RL with various depths.
Refer to caption: extracted/5975509/figures/depth_decomposition.png

In Fig. 4, we decompose the proved theorems by the depth of their ground-truth proofs (shown on the $x$-axis) and the depth of generated proof trees (indicated by color). When there are multiple correct proof trees, we plot the one with the maximum depth. As a comparison, we also plot the success rates of the proofs generated by the RL model trained w/o lemma proposal. Fig. 4 shows that the improvement of ProD-RL mostly comes from proving theorems with low-to-medium difficulty where the depth of the ground-truth proof is at most 2. For more complex theorems, both models’ pass rates are low and the improvement of our method is not significant, meaning that they are currently beyond the models’ capability.

### 4.4 Case study of proposed lemmas

In this section, we manually examine the new lemmas proposed during RL and list the typical cases where new lemmas are proposed. Note that many AFP files focus on complex concepts and results in mathematics or computer science, making manual examination challenging. Therefore, examples in this section are biased toward easier theorems.

#### Case 1: Model decomposes theorems into lemmas.

In this case, the model correctly decomposes the proof of a theorem into several lemmas. The following example belongs to the AFP file List-Infinite, which focuses on lists and sets with infinite size. The theorem (Line 1) states that the cardinality of the set $A\cup\{x\}$ equals $|A|$ if $x\in A$, or the successor integer of $|A|$ otherwise (i.e., $|A|+1$ for finite $A$ and $\infty$ otherwise). During the proof (Lines 2-4), our model proposes two lemmas in Lines 2 and 3 to deal with the two possible cases ($x\not\in A$ or $x\in A$) respectively. Finally, Line 4 proves the original theorem using the two proposed lemmas.

#### Case 2: The proposed lemma is a rephrase of an existing lemma.

We also find that some proposed lemmas are rephrases of existing lemmas in the training dataset. Although in this case, the proposed lemma is not fundamentally useful for proving new theorems, they can be viewed as data augmentation to enhance the models’ performance. In the following example, the model produces a lemma equivalent to one in an AFP file. Line 1 shows the original form of the lemma stated in the AFP file, while Lines 2-4 show an equivalent lemma proposed by our model during RL.

#### Case 3: The proposed lemma is novel but not useful to the original proof.

We also observe cases where the proposed lemma is novel, but the conditional proof of the theorem is incorrect. In the following example, the proposed lemma states that the shortest path between vertices $u,v$ is a lower bound for the length of any path that connects $u,v$ (in an unweighted and undirected graph):

This lemma is proposed to prove that the shortest path between the vertex $u$ and itself has length 0 (which is a theorem in the AFP file). However, the conditional proof of the theorem contains a few mistakes while the proposed lemma is proved separately. In this case, we still train on the correct lemma even though it might not be directly useful to the theorem in the training set.

#### Remarks.

We observe that the lemmas proposed by the model typically do not involve complex ideas. We attribute this to two main factors: (a) the limited size of our model and formal proof dataset, and (b) the fact that many human-written lemmas in the AFP file are indeed about basic facts and basic properties (which are often used to prove more complex theorems later). Nevertheless, our model still proposes and proves reasonable lemmas that are not present in the training dataset, and our experiments demonstrate that with these proposed lemmas, ProD-RL outperforms ProD-SFT on holdout test sets. We leave it to future work to scale up our method and force the model to focus on more challenging theorems.

## 5 Related works

To generate formal proofs with language models, most prior methods provide the verifier’s state to the model to sample the proofs step-by-step, and use algorithms like MCTS to search for a correct complete proof (Polu and Sutskever, ; Jiang et al., ; Han et al., ; Polu et al., ; Jiang et al., ; Lample et al., ; Wang et al., ; Yang et al., ). The major drawback of these methods is their high computation cost at test time.
Several recent works (First et al., ; Xin et al., , ) use large language models to generate a whole proof directly without the verifier’s state. Our baseline, the SFT model without lemma proposal, can be viewed as a reproduction of First et al. () with a slightly different way of computing the context.

Prior works also use reinforcement learning or expert iteration to improve the models’ performance on writing formal proofs, where the training datasets contain formal synthetic inequalities (Polu et al., ) or statements translated from natural language mathematical problems (Wu et al., ; Xin et al., , ). In contrast, we aim to improve the models’ performance without any additional (even unlabeled) data. As future works, one can extend our algorithms to more diverse additional datasets.

Another line of research aims to translate natural language proofs into formal proofs (Jiang et al., ; Zheng et al., ). Xin et al. () build a library of useful lemmas by decomposing natural language proofs into lemmas with an LLM and then formalizing the decomposed proofs. In contrast, we propose new lemmas entirely in formal language.

Automated theorem provers (ATPs) have been extensively studied, with various learning- or search-based methods developed to generate tactics for a given proof state (e.g., Gauthier et al. (); Schulz et al. () and references therein). In comparison, our method focuses on generating multi-step proofs with LLMs while using existing ATP tools to complete low-level details. Orthogonally, a recent method (Mikuła et al., ) improves existing provers with a transformer-based retrieval model as the premise-selection tool, and could potentially be combined with our methods.

In general, mathematical question-answering tasks (such as GSM8K (Cobbe et al., ) and MATH (Hendrycks et al., )) and theorem-proving tasks (such as Welleck et al. ()) are well-accepted benchmarks for the reasoning capability of large language models. Prior works show that instruction tuning or RL can significantly improve the models’ performance (Shao et al., ). However, evaluation on these tasks is either performed by another language model (which is prone to errors) (Lightman et al., ), or requires ground-truth answers that are hard to acquire at scale.

## 6 Conclusion

In this paper, we design a reinforcement learning algorithm that encourages LLMs to write formal proofs by decomposing them hierarchically. We also design a more natural testing setup by removing the directly relevant lemmas from the context. We show that, by proposing and proving new lemmas that are not present in the training dataset, the resulting model ProD-RL outperforms or achieves comparable performance to baseline methods trained on the same dataset.

#### Limitation.

We observe that the improvement of ProD-RL over SFT w/o lemma proposal is significant only when the test distribution is close to the training distribution. On miniF2F (Zheng et al., ) where the theorems are very different from theorems in the training dataset, ProD-RL performs worse than SFT w/o lemma proposal, as shown in Table 3. We also observe that when tested on miniF2F theorems, our model failed to propose meaningful lemmas. This may be because proving to miniF2F-level mathematics questions typically does not require hierarchical decomposition. Therefore we leave it as future work to extend our methods to other domains such as miniF2F and PutnamBench (Tsoukalas et al., ).

**Table 3: Pass@64 of different models on miniF2F. ProD-RL performs worse than SFT w/o lemma proposal.**
| Test set | SFT w/o<br>lemma proposal | RL w/o<br>lemma proposal | ProD-SFT | ProD-RL |
| --- | --- | --- | --- | --- |
| miniF2F valid | 46.3 | 40.6 | 44.7 | 41.4 |
| miniF2F test | 40.6 | 38.9 | 39.3 | 39.3 |

### Acknowledgment

The authors would like to thank Neil Band, Zhizhou Ren, and Yuanhao Wang for their helpful discussions. The authors would also like to thank the support from NSF CIF 2212263.

## Appendix A Additional experiments details

### A.1 Generating proof trees for RL

In Alg. 2, we present the algorithm for generating proof trees during RL training. Recall that, compared with Alg. 1, there are two major differences:

- (a)
for the theorems where the probability $\pi_{\theta}(\text{<use_invoke>}\mid x)$ is among the top 50% in the batch, we will force the model to generate conditional proofs with $t_{0}=\text{<use_invoke>}$ (Line 4-6), and
- (b)
for every theorem where the model generates a conditional proof with new lemmas, we also let the model generate another conditional proof without proposing new lemmas (Line 11).

Figure: Algorithm 2 Generate proof trees (train)

### A.2 Training details of baseline models

In this section, we describe the additional details for training the baseline models using reinforcement learning.

Our RL training pipeline for the baseline models is similar to that of ProD-RL, except that the models only generate proofs without lemma proposal. For RL baselines, we use the same dataset and the same hyperparameters as our method. To mix the ground-truth conditional proofs with generated proofs, we convert the conditional proofs to proofs without lemma proposal by moving all the proposed lemma in the conditional proof to the context.

### A.3 Additional experiment details

#### Details of using sledgehammer in the proof.

Sledgehammer is a premise selection tool that can automatically generate proofs to solve the current goal. Although sledgehammer is not always applicable, Jiang et al. [] shows that letting the model to call sledgehammer whenever it is applicable greatly improves the model’s performance.

To let the model use sledgehammer, we replace the actual proof steps in the training dataset by a call to sledgehammer if the proof step either (a) contains the proof tactics ‘meson, metis, and smt’ (these tactics are typically generated by sledgehammer), or (b) belongs to a predefined simple set of proof tactics that can be easily generated. In particular, they are

When testing a generated proof with calls to sledgehammer, we follow the pipeline of [Jiang et al., ] — first, we try to replace the ‘sledgehammer’ command by one of the predefined tactics. If all the attempts fail, we call the actual premises selection tool in Isabelle with a 10s timeout. If the tool does not return a valid proof, we consider this step incorrect.

Note that Jiang et al. [] decide when to replace the actual proof step by a call to sledgehammer more aggressively. They attempt to call sledgehammer at every proof step, and replace the actual proof step with sledgehammer if the attempt is successful. In contrast, our decision is made without interacting with the formal verifier. This is because applying sledgehammer to every proof step requires a lot of compute, which would significantly slow down the reinforcement learning process.

#### Dataset split.

Here we describe how to split the training and test data based on the dependency of the AFP files. We first compute the dependency graph by crawling the AFP website [https://www.isa-afp.org/entries/](https://www.isa-afp.org/entries/), which lists the dependency of the AFP entries. Then we find the set of AFP entries that all other entries do not depend on using the dependency graph, in which we randomly sample 10% of the entries as the holdout test set. The resulting holdout entries are:

#### Additional training detail.

We use the Llemma code base ([https://github.com/EleutherAI/math-lm](https://github.com/EleutherAI/math-lm)) for finetuning and updating the model in reinforcement learning. The discount factor used to compute the weight is $\gamma=\exp(-0.0005).$

### A.4 Compute resources

For supervised finetuning and reinforcement learning, we use a machine with 8 A100-80G GPUs. It takes approximately 8 GPU days in total (i.e., 1 day wall-clock time on a single machine with 8 GPUs) to finetune a 7B model on 300k examples for 2 epochs. It takes approximately 30 GPU hours to run a single RL experiment.

To generate proofs using the trained model, we use a mix of A100-80G and A5000 GPUs. On 8 A5000 GPUs, generating proof trees of depth 2 for 4k test examples takes about 1-2 hours, depending on the length of the proof and the number of proposed lemmas.

### A.5 Licenses for existing assets

In this section, we list the licenses for existing assets used in this paper.

- •
LLemma [Azerbayev et al., ]: Llama 2 Community License Agreement
- •
Archive of Formal Proofs: GNU LGPL
- •
Portal to ISAbelle [Jiang et al., ]: BSD 3-Clause License
- •
Isabelle [Nipkow et al., ]: BSD licenses
- •
miniF2F [Zheng et al., ]: MIT License

## Appendix B Additional results

In this section, we present additional experimental results.

### B.1 The effect of sampling temperatures

In our preliminary experiments, We tune the sampling temperature using the models trained on the AFP training sets $D_{\text{train}}^{\text{w/ l}}$ and $D_{\text{train}}^{\text{w/o l}}$ (that is, training sets constructed with and without helper lemmas, respectively). We test the model on the AFP test set $D_{\text{test}}^{\text{w/o l}}$ with different temperatures to decide the best choice for testing our models. Fig. 5 shows the performance of the SFT model without lemma proposal using different sampling temperatures. We conclude that the temperature 0.7 is best for testing both models.

Figure: Figure 5: Pass rate of the SFT model without lemma proposal tested with different sampling temperature. We observe that lower temperature leads to better performance with 1 sample per theorem, and mildly larger temperature have better performance with more samples.
Refer to caption: extracted/5975509/figures/temp_baseline.png

### B.2 Varying the size of the RL dataset

In this section we report the performance of the ProD-RL models trained with different rounds. Recall that in each round we generate proofs to a batch of 5k examples. Therefore equivalently, Figure 6 shows the performance of ProD-RL with a smaller RL dataset.

Figure: Figure 6: Pass rate of models trained with different rounds of RL training. Recall that in each round we generate proofs to a batch of 5k examples. The model trained with 20 rounds of RL achieves the best performance, and all RL models outperforms the baseline ProD-SFT model.
Refer to caption: extracted/5975509/figures/RL_dataset_size.png

Note that although the performance is not monotone with respect to the RL dataset size (e.g., ProD-RL at round 15 is worse than ProD-RL at round 10), which might due to training instability, all the RL models significantly outperforms the baseline ProD-SFT.

## Peer Reviews

confidence: 4
contribution: 4
initial_rating: 6
presentation: 2
questions: 1. Regarding *Weakness 4*, the advantages of lemma proposal for more challenging proofs are not immediately clear in *Figure 4*, as the data only presents absolute counts, and the relative advantage is not obvious. Could it be that the relative advantage for proofs with at least 5 steps is indeed more significant?

2. It appears that the tree search depth is limited to 2 or 3. Why have deeper experiments not been conducted? Would increasing the depth help tackle more difficult proofs by allowing finer-grained decomposition, thereby making each lemma more manageable for the model?
soundness: 3
strengths: 1. While the concept of splitting test sets based on file dependencies has been explored in the LeanDojo project ([arXiv:2306.15626](https://arxiv.org/abs/2306.15626)), the minimalist lemma approach introduced here is novel, with comparative experiments validating its challenges.

2. The RL training framework designed to enhance lemma-proposing capabilities is both innovative and practical. The global and local reward design can be generalized to other tree search tasks. Notably, the use of special tokens to control lemma exploration is an exceptional feature.
summary: According to my understanding, this paper has the following two main contributions:

1. **A Setting for Theorem Proving without the Help of Human-Written Lemmas**

- **Contribution**: This paper introduces a new, more challenging evaluation setting in theorem proving, focusing on the use of human-written code libraries but with minimal reliance on human-proven lemmas. 

- **Motivation**: This setting arises from the observation that proofs in human-written projects display strong modularity: proofs are often broken down into lemmas, making final theorems relatively easy to prove by combining these intermediate steps. While efficient, this approach may obscure a prover's ability to handle full-scale proofs of original theorems independently, limiting evaluation of the prover's core capabilities.

- **Method**: To address this, lemmas referenced in the proof of each selected theorem are excluded from the evaluation (however, the authors describe this as removing those "not referred to in the remaining file contents," which seems intended to remove only redundancies). Additionally, the test set is split by dependency—ensuring that no theorem in the test set is refered by any theorem in the training set.

- **Soundness**: Experiments show that the pass rate under the "without lemma proposal" setting is lower than in the "with lemmas  proposal" setting, demonstrating the increased difficulty of this approach.

2. **An Interface for Actively Proposing Lemmas during Proof Generation**

- **Contribution**: This work offers a solution for language models to comply with the above lemma minimalism setting (in my words), enabling models to actively propose lemmas during theorem proving while relying minimally on human-written lemmas.

- **Method**: The theorem proving process is structured as a hierarchical tree search. During proof generation for a specific statement, the model actively proposes lemmas and leverages them in subsequent proof steps, with the proofs of these lemmas deferred to a lower hierarchical level. For model training, reinforcement learning is applied to the supervised-fine-tuned model. By distinguishing between global and local rewards, the model is optimized both to propose provable lemmas that help solve the original theorem and to complete the proofs of proposed lemmas. Special tokens are used to guide the model in deciding when to propose lemmas, effectively controlling exploration.

- **Soundness**: Experimental results indicate that the RL-trained model achieves a higher pass rate than the SFT model, with a 4.7% absolute improvement. Additionally, some proposed lemmas are successfully proved. Experiments over multiple rounds of RL further demonstrate the effectiveness of this approach.
weaknesses: 1. Although the test set split is restricted by file dependencies, the risk of lemma proposal leakage has not been fully addressed. It is possible that some theorems in the training and test sets rely on the same lemmas, which may have been learned during the supervised-finetuning phase. Furthermore, splitting the test set based on file dependencies might introduce bias. These isolated AFP files could be separated precisely because they are experimental or less widely used, which may not accurately represent the average difficulty of the AFP. The challenges observed in dependency-splitting experiments might instead arise from unfamiliar or unseen knowledge and proving skills specific to these isolated files. An alternative approach would be to train and test on an out-of-domain benchmark, such as miniF2F, which has fewer dependencies and reduces the risk of lemma proposal leakage.

2. The comparison between the SFT and RL models, though straightforward, might be insufficient. It seems that the RL model’s advantages arise from additional exploration and feedback on successful lemma proposals during the online training. A more fair comparison might involve comparing the RL model with an SFT model trained with additional expert iterations, where the SFT model also attempts lemma proposals while without the hierarchical reward.

3. The comparison between proving with and without lemma proposals might also be unfair. In lemma proposal mode, the difficulty of proving theorems is deferred to lemma proving, which has more computational resources than direct theorem proving.

4. *Figure 4* demonstrates that extra lemma proposals may not benefit proofs of higher difficulty. Instead of highlighting the hierarchical approach’s advantages for difficult problems, this approach may exacerbate concerns that its benefits stem from unequal computational budgets.

---

confidence: 4
contribution: 3
initial_rating: 6
presentation: 3
questions: - Why does the performance of `RL w/o lemma proposal` fare worse than `SFT w/o lemma proposal`? Does the RL loop function as an alternative to expert iteration, serving as an advanced version of it? If so, expert iteration has been shown to be effective for neural theorem proving in previous works such as GPT-f and PACT. Why does the current proposed RL loop fail to improve upon these results?
- Why has the miniF2F result been removed in this submission, despite being presented in the previous NeurIPS submission?
soundness: 4
strengths: - The motivation for this work is strong, addressing a critical problem in the domain of neural theorem proving. The proposed framework is highly useful for this task.
- The experimental results demonstrate its effectiveness in creating lemmas during the theorem-proving process.
- The paper is well-written and easy to follow.
summary: The paper proposes a novel paradigm in neural theorem proving. Previous methods assume pre-provided lemmas during the proving stage. In contrast, this paper encourages the model to decompose the theorem into lemmas, prove the lemmas, and then use these lemmas to prove the theorem. This approach more closely resembles a real-world theorem-proving process. And the effectiveness of the proposed framework is demonstrated by the experiments.
weaknesses: - The primary concern with the proposed method is its performance. While effective, the enhancement offered by the framework is marginal when compared to the baseline scenario, with a modest 2.1% increase in the AFP test and a negligible 0.1% improvement in the AFP 2023 set.
- One drawback of the lemma proposal mechanism is that the model’s performance can be hindered by meaningless proposed lemmas. This issue is evident in the case study section. The key challenge lies in the ability to refine the proposed method to be able to generate lemmas that are genuinely beneficial.

---

confidence: 4
contribution: 2
initial_rating: 3
presentation: 2
questions: 1. Could the authors address the large experimental difference between ProD-RL (45.5%) and MagnusHammer’s 71% on the PISA benchmark [2]? A direct comparison/discussion of scalability/ablation study could strengthen the work. 

2. Why is “MiniF2F” only in the licensing section without experiment inclusion? This benchmark is a robust test for theorem-proving tasks.
it could be better to add the evaluation PutnamBench [1] which assesses the methods on hard competition level problems.



[1] Tsoukalas, George, et al. "PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition." arXiv preprint arXiv:2407.11214 (2024).
[2] Mikuła, Maciej, et al. "Magnushammer: A transformer-based approach to premise selection." arXiv preprint arXiv:2303.04488 (2023).
[3] Wang, Haiming, et al. "Lego-prover: Neural theorem proving with growing libraries." arXiv preprint arXiv:2310.00656 (2023).
[4] Aygün, Eser, et al. "Proving theorems using incremental learning and hindsight experience replay." International Conference on Machine Learning. PMLR, 2022.
soundness: 3
strengths: 1. This work proposes an RL-driven approach to proof decomposition without lemma reliance, an original contribution that aligns with similar ideas in [3], [4]
2. ProD-RL’s methodology yields improvements over SFT, highlighting the model’s capability to generalize beyond pre-existing lemmas, and trains on a more realistic dataset, splitting by dependency rather than at random.
3. The work contributes to LLM for theorem proving, an important direction for mathematical reasoning research.
summary: This paper introduces ProD-RL, an RL method to enhance LLM’s theorem-proving capabilities by encouraging them to decompose proofs into lemmas. It avoids oversimplifying the task by removing direct lemma support from the training setup, requiring the model to independently propose intermediate steps in the proof process. The paper evaluates the model’s performance on the Isabelle AFP dataset and shows 45.5%/39.5% accuracy on AFP-test/AFP-2023, which outperforms SFT baselines.
weaknesses: 1. Clarity and Readability: The paper is a little bit difficult to follow, especially in algorithmic explanations and conditional proof notation. The baseline and proposed methods are not clearly differentiated in the results. Improved organization, clearer definitions, and visuals would make the methodology more accessible.
2.  Generalization and Complexity: There is limited exploration of scalability to higher-complexity proofs. It's better to address whether ProD-RL is viable for deeper proof trees.
3.  Comparative Benchmarks and Dataset Exclusion: The absence of benchmarks like minif2f in experiments raises questions, given its mention in the license section. Also, there could be more comparisons with other theorem-proving techniques in the experiment section.

---

confidence: 4
contribution: 1
initial_rating: 3
presentation: 3
questions: * Could you evaluate the proposed method on the miniF2F benchmark? This dataset is more commonly used and would help assess the generalization of your approach beyond AFP.

* The paragraph starting at Line 270 suggests that the reward in the RL setting is based on the conditional proof, with its weight influenced by the conditional proof as well. However, in practice (as described in Line 277), it appears that the proposed method uses a language model as a value network to predict True/False, and the probability is used as the reward score, without incorporating any information from the conditional proof. Could you clarify why the conditional proof is discarded for the value function? Additionally, in the RL w/o lemma proposal, what rewards or weights are used in the absence of lemmas?

* Why does RL w/o lemma proposal underperform SFT w/o lemma proposal? For ProD-RL, you first apply SFT, followed by RL, which (almost) ensures that ProD-RL always outperforms ProD-SFT. Does RL w/o lemma proposal also involve an initial SFT stage? If so, it seems that RL w/o lemma proposal negatively impacts performance, and I would like more details on why this happens (since there are no details provided). If not, the comparison between RL w/o lemma proposal and ProD-RL may not be entirely fair.
soundness: 2
strengths: * The paper is well-written, clearly structured, and easy to follow.

* The proposed method is well-motivated. Experiments on the AFP dataset effectively demonstrate the advantages of lemma proposal with reinforcement learning.
summary: This paper explores neural theorem proving in a setting where existing lemmas cannot be used and proposes a RL-based approach that encourages the model to decompose proofs into multiple subgoals and propose new lemmas to prove. The authors demonstrate that their approach, which combines supervised fine-tuning with reinforcement learning, achieves superior performance on the AFP dataset compared to baseline methods, including those that do not propose new lemmas or rely solely on supervised fine-tuning.
weaknesses: * The idea of decomposing proofs into subgoals and proposing new lemmas is not entirely novel, as it has been explored in previous work. For instance, LEGO-Prover [1] uses informal proofs to break down proofs into manageable subgoals and leverages language models to either propose new lemmas or retrieve existing ones from a growing library. While the proposed setting of excluding relevant premises is indeed challenging, I believe it does not always reflect practical scenarios. Incorporating both lemma selection and lemma proposal would present a more generalized and realistic approach.

* The experiments are conducted exclusively on the AFP dataset, which may not provide a thorough evaluation of the method's robustness, particularly in out-of-distribution scenarios like the miniF2F dataset, a more commonly used benchmark. As a result, it is unclear how well the proposed approach generalizes beyond the training set. Additionally, in Case 2, there seems to be evidence that the model may be memorizing lemmas from the training data rather than proposing genuinely novel ones, which raises concerns about its ability to generate useful new lemmas in unseen contexts.

* Minor Points: There are some missing references to works that share similar ideas or components with this paper [2,3,4]. For instance, POETRY [4] introduces a recursive approach that decomposes proofs into subgoals and generates lemmas in a hierarchical, level-by-level manner. A broader overview of related work can be found in [5]. Additionally, the statement in Line 80 ("the best method along this line of research requires more than 1k GPU days with A100s to train a model with 600M parameters") may not be entirely accurate. More recent methods, such as InternLM-Step Prover [6], appear to have surpassed HTPS in both efficiency and requiring less computational resources.

[1] LEGO-Prover: Neural Theorem Proving with Growing Libraries

[2] TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning

[3] Proving Theorems Using Incremental Learning and Hindsight Experience Replay

[4] Proving Theorems Recursively

[5] A Survey on Deep Learning for Theorem Proving

[6] LEAN-GitHub: Compiling GitHub LEAN Repositories for a Versatile LEAN Prover

Meta-review: This paper focuses on neural theorem proving in contexts where the relevant premises are unavailable. The authors propose Proof Decomposer (ProD), a RL approach that utilizes hindsight experience replay to reward a LLM in hierarchically decomposing a given theorem into lemmas, and subsequently proving these lemmas to prove the theorem. Experiments on the AFP dataset indicate that the proposed method (ProD-RL) outperforms several baseline approaches, including those relying solely on supervised fine-tuning (SFT), as well as methods without lemma proposal.

Reviewers generally agree that the paper is well-written (Reviewers CLmw, vahD) and find the new task both challenging and interesting (Reviewers kLVh, CLmw). They also note that the method is well-motivated (Reviewers kLVh, CLmw). However, as pointed out by Reviewers CALz and vahD, ProD shares notable similarities with existing methods, albeit in a slightly different setting. A key point raised by multiple reviewers (CLmw, CALz, vahD) is the lack of experiments on the miniF2F dataset, which appeared to be selectively omitted. 

In summary, while the motivation and setup of the proposed method are compelling, the novelty and especially the generalization performance of ProD-RL remain concerns. The authors are encouraged to conduct further experiments to strengthen generalization on miniF2F and to include these extended results in the revised paper.

Decision: Reject