Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically

We thank Reviewer vahD for their comments. In the following, we address the reviewer’s question in detail.

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.

We thank the reviewer for the constructive comments. In fact, combining our methods with premise selection tools such as MagnusHammer is straightforward, as we can simply replace Sledgehammer with MagnusHammer. Since we cannot find an open-sourced implementation of MagnusHammer, we leave this direction as future work.

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.

We acknowledge that the model may memorize lemmas in some cases. However, in both Cases 1 and 3, the lemma proposed by our model is indeed useful since the proposed lemmas are not present in the training dataset. Figure 4 also demonstrates that, with lemma proposals, our ProD-RL model outperforms baseline methods by proposing lemmas in the test dataset where the context of theorems is never seen by the model during training.

There are some missing references to works that share similar ideas or components with this paper…

We thank the reviewer for the additional references. We will update our paper accordingly upon revision.

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. … Could you evaluate the proposed method on the miniF2F benchmark?

On miniF2F, we find that our method does not have significant improvement over the baselines. We hypothesize the reasons to be: (a) the theorems are very different from theorems in the training dataset, and (b) 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. In contrast, the AFP datasets work with abstract mathematical objects and theorems, which intrinsically have hierarchical decompositions.

Nonetheless, our results on miniF2F are shown in the following table:

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?

We do not discard the conditional proof when computing the reward. For a theorem with conditional proof p, we only use the value function to compute the probability that the current model can prove the proposed lemmas.

As a concrete example, suppose the conditional proof to the theorem proposes two lemmas l1, l2 and the conditional proof itself is locally correct (meaning that it proves the theorem using lemmas l1 and l2, assuming both lemmas are correct). Then the reward of this conditional proof is V(l1) * V(l2) times the additional discount factor.

In comparison, we can also simply set a binary reward whose value depends on whether the proofs to lemmas l1 and l2 are also correct. If the value function is perfect, the two ways of computing the reward have the same expected value, and using the value function is a common trick to reduce the variance of the reward estimation.

Additionally, in the RL w/o lemma proposal, what rewards or weights are used in the absence of lemmas?

Without lemma proposal, the reward of a conditional proof is simply the correctness of the proof.

Thank you for your detailed response. I have a few follow-up questions and suggestions for clarification and improvements to the paper.

1. Regarding the Use of Sledgehammer

• Has Sledgehammer been used into the proposed approach? Specifically, is it used to fill proof gaps for the proposed lemmas?
• If Sledgehammer is indeed part of the method, I recommend providing additional details about its integration, as the current description includes very limited discussion. Furthermore, rather than independently proposing every lemma, have you considered leveraging existing lemma retrieval techniques like those in [1]? This approach could potentially address a broader range of cases and enhance the method's generality.
• If Sledgehammer is not used, and proof steps are still predicted by LLMs, why not consider modeling each proof step as an individual action in the RL framework? This would better align with existing RL approaches to theorem proving.

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

2. On the RL Formulation

If the action in your RL w/o lemma proposal setup is defined as generating the entire proof, this reduces the RL problem to a bandit-like setting, as there is no exploration during the proving process. This formulation faces significant challenges:

• The action space is almost infinite.
• Correct proofs often involve lengthy token sequences but rewards are extremely sparse.

These challenges likely contribute to the observed underperformance of RL w/o lemma proposal compared to SFT w/o lemma proposal. The lack of intermediate structure or guidance in this setup may also have a negative impact on the learning process. I suggest adding a more detailed settings of the baseline methods and discussing these challenges explicitly to provide further clarity.

3. Performance on miniF2F

• You mention that your method does not show significant improvement (and indeed has a negative impact) over baselines on miniF2F, potentially due to the lack of hierarchical decomposition in these problems. However, I believe miniF2F does exhibit hierarchical decomposition (albeit different from AFP), which is why methods like LEGO-Prover perform well in this domain.
• I posit that the underperformance of your approach may be more related to its generalization ability. Including these results in your paper to clearly illustrate the limitations of your method would be beneficial and add transparency.

4. Insights on Novelty and Contributions

• From my understanding, decomposing theorems into lemmas is intuitive for declarative proof assistants like Isabelle and has been extensively explored in the literature. The main contribution of your work appears to be the use of RL to train a lemma proposal mechanism. Beyond this, can the authors provide additional insights into the novelty or other valuable aspects of the proposed approach?

• One potential reason for your improved performance on AFP could be that RL facilitates the generation of more diverse intermediate lemmas compared to purely SFT approaches. This diversity could better guide the proving process. I suggest analyzing and comparing the diversity of lemmas generated by ProD-RL and SFT without lemma proposal to evaluate this potential advantage.

Thank you for your response. I appreciate the detailed discussion and insights provided by the authors. However, I believe the paper, in its current form, still requires significant improvement in clarity and a more comprehensive analysis and refinement of the experimental results, to be considered for acceptance. While the proposed method is intuitive and well-motivated, I could hardly find it "novel" as the core ideas (decomposing theorems into lemmas, Hindsight Experience Replay) appear to overlap with existing work. Additionally, the authors emphasize that their approach operates entirely in formal language, in contrast to some related methods that leverage natural language. However, if leveraging natural language can yield better results, as demonstrated in [1], why not explore its use as a means to guide formal proofs to achieve better performance? Another critical concern is the generalization ability of the proposed method. The authors acknowledge that their model struggles to propose meaningful lemmas for problems in the miniF2F dataset and even underperforms basic SFT approaches. This suggests that even simple SFT exhibits better generalization than the proposed method. Without presenting a strategy to address this critical limitation or additional experiments demonstrating potential improvements in generalization, simply labeling it as a limitation feels insufficient for acceptance. In my opinion, achieving the best performance is not always necessary for a method to be considered impactful. However, underperforming compared to basic SFT makes it difficult to view this work as a "significant contribution" to the field in its current state.

[1] Lean-STaR: Learning to Interleave Thinking and Proving

I appreciate the authors' quick response and would like to address my concerns in detail.

• Regarding the novelty

While I understand that assessing novelty can be subjective, I find the core idea of the proposed method overlaps with existing works. As you acknowledge, decomposing theorems into lemmas and using Hindsight Experience Replay are established techniques within theorem proving research, even if applied to different settings (e.g., alternative logics or LLMs). However, combining previously known approaches in a somewhat distinct setup does not, in my view, qualify as entirely ''novel''.

• Regarding the generalization ability

I appreciate the motivation to rely solely on formal verifiers like Isabelle without the assistance of powerful teacher models (i.e., "weak-to-strong generalization"). However, I find it unconvincing to downplay the limitations in generalization by stating that MiniF2F is not a major focus, especially considering this dataset is the most widely used benchmark in this field. Furthermore, the proposed method underperforms even simple SFT on the formal proof of the AFP dataset when testing on the MiniF2F. If the goal is to improve the reasoning abilities of weak LLMs, performance on problems beyond similar training instances is also crucial. This concern is amplified by the fact that problems in MiniF2F, which consist of high-school competition-level math, may be less challenging than those in the AFP dataset, which spans diverse mathematical research topics.

In my view, while proposing entirely novel approaches is very commendable but not always essential, addressing generalization remains a critical factor. If the authors can present strategies to overcome these limitations and provide additional experiments showing potential improvements in generalization (better than simple SFT), I would like to reassess and raise my score.

We thank Reviewer CALz for their comments. In the following, we address the reviewer’s question in detail.

Could the authors address the large experimental difference between ProD-RL (45.5%) and MagnusHammer’s 71% on the PISA benchmark [2]?

First, there are two major differences between ours and PISA’s evaluation setup:

• We split the test set based on the dependency of the files, while PISA splits the test theorems randomly. As a result, for the theorems in the PISA test set, there may exist proofs of similar theorems in the PISA training set.
• When testing on a theorem, we do not allow the proof to directly use lemmas in the same AFP file. Instead, we let the model propose and prove every lemma it needs in the proof. In comparison, MagnusHammer focuses on training a retrieval model that selects useful lemmas from the context, including those in the same AFP file.

As a result, our test setup is fundamentally harder than PISA. As shown in Table 1, the same model has much worse performance on our setup.

Second, we also test the pass@64 performance of our baseline model on $D_{val}^{w/l}$, our reproduction of the PISA test set. The baseline model achieves 63.9% on the test set with Sledgehammer. In comparison, Thor with MagnusHammer archives 71%. We’d also like to emphasize that, according to First et al., (2023), whole-proof generation with 64 examples is 6x faster than search methods like Thor.

Finally, the contribution of MagnusHammer is orthogonal to ours. In fact, combining our methods with MagnusHammer is straightforward, as we can simply replace Sledgehammer with MagnusHammer. We leave this direction as future work.

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.

We use MiniF2F benchmark in the early development of this work. We find that our method does not have significant improvement over the baselines. We hypothesize the reasons to be: (a) the theorems are very different from theorems in the training dataset, and (b) 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. In contrast, the AFP datasets work with abstract mathematical objects and theorems, which intrinsically have hierarchical decompositions.

There is limited exploration of scalability to higher-complexity proofs. It's better to address whether ProD-RL is viable for deeper proof trees.

We thank the reviewer for the suggestion. We observe that in AFP test sets, theorems that require deeper proof trees are too challenging for our current model since the pass@64 performance is below 10%, as shown in Figure 4. It might require scaling up the model or the dataset before we can test the scalability of our methods. Unfortunately, we are currently limited by the compute budget and therefore cannot perform a larger scale experiment.

We hope that our response addressed the reviewer’s concerns, and we are happy to answer any follow-up questions.

We thank Reviewer CLmw for their comments, and for noting “The motivation for this work is strong, addressing a critical problem in the domain of neural theorem proving”. In the following, we address the reviewer’s question in detail.

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?

Yes, the RL method is an alternative to expert iteration. Regarding the performance of RL vs. SFT, we note that an important difference between our experiment setups and prior works, such as GPT-f and PACT, is that we let the model generate a complete proof directly without looking at the verifier’s proof state. In the MDP language, the state in our setup is the theorem’s statement and the action is the whole proof, while in GPT-f and PACT, the state is the verifier’s internal proof state (plus some contexts) and the action is a single proof step. Therefore, running RL in GPT-f’s setup can generate data with new MDP states because different proofs may lead to different verifier’s proof states, whereas RL in our setup without lemma proposal cannot generate data with new MDP states. Therefore, the naive RL algorithm on top of the SFT model in our setup cannot collect fundamentally new data, since the ground-truth action for every MDP state in the dataset is already given, and may simply cause overfitting problems. In contrast, with lemma proposals, we can generate data with new MDP states (i.e., the novel lemma statements) and therefore boost the performance of the SFT model.

Why has the miniF2F result been removed in this submission, despite being presented in the previous NeurIPS submission?

After the NeurIPS deadline, we conducted more extensive parameter tuning and found a better learning rate schedule that significantly improves the performance of both our methods and the baselines (as we pointed out during the NeurIPS rebuttal phase) — we found that models trained with constant learning rates have much better pass@k performance than those trained with cosine learning rate decay because learning rate decay causes more deterministic behavior. As a result, with the new hyperparameters, we do not observe significant improvement on miniF2F compared with the improved performance of the baseline models.

Thank you for your detailed clarifications.

Therefore, the naive RL algorithm on top of the SFT model in our setup cannot collect fundamentally new data, since the ground-truth action for every MDP state in the dataset is already given, and may simply cause overfitting problems.

Apologies for not being an RL expert here. Doesn’t the RL process involve sampling additional actions (proofs) for each MDP state (i.e., each problem in the training set) using the current model, and subsequently utilizing these newly sampled actions for RL updates? While I understand that the MDP state (the problems) remains fixed in this context, wouldn’t increasing the diversity of actions used for training improve model performance? From an expert iteration perspective, providing the model with more varied solutions for each problem could potentially enhance performance, even if the effect is less pronounced than in setups like GPT-f.

Thank you for your further clarification. This is a fascinating and counterintuitive result. Normally, we expect that more diverse proof data would help with the proving process.

I’m now more convinced that this is a really challenging task, and this work demonstrates a solid start in this direction. Current theorem-proving frameworks like AlphaProof have already shown their capability in solving very complex IMO-level problems. Therefore, I believe the direction of attempting the lemma generation task is very important as a future step. I’ve raised my score to 8.

We thank Reviewer kLVh for their comments, and for noting “the minimalist lemma approach introduced here is novel”, and “RL training framework … is both innovative and practical”. In the following, we address the reviewer’s question in detail.

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 … 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.

We test on the miniF2F benchmark and find that our method does not have significant improvement over the baselines. We hypothesize the reasons to be: (a) the theorems are very different from theorems in the training dataset, and (b) 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. In contrast, the AFP datasets work with abstract mathematical objects and theorems, which intrinsically have hierarchical decompositions.

We also agree with the reviewer that, even if we split the training and test set by the file dependencies, or even by the submission date like our AFP 2023 test set, theorems in the training and test set may rely on the same lemma. Such dependency cannot be eliminated easily even if we test on the miniF2F benchmark because the proof still depends on some basic lemmas such as the properties of prime numbers.

Nonetheless, we believe that our train/test split serves as a step toward building rigorous benchmarks for testing the fundamental reasoning capabilities of LLMs.

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?

We are not sure whether we understand the reviewer’s question correctly (please kindly let us know if not). In Figure 4, we show the pass rate of the theorems grouped by the depth of their ground-truth proof trees. Taking the right-most stacked bar as an example, there are 336 theorems with ground-truth depth >= 4 in the test set, and our model proves 14 of them. Therefore the pass rate is 4.17% as shown in Figure 4. Among the 14 proved theorems, 1 of the theorems is proved with a proof tree of depth 2, and 1 of the theorems is proved with a proof tree of depth 3. Similarly, the baseline model proves 10 theorems with direct proofs only, which translates to a pass rate 2.98%. The relative advantage for theorems with ground-truth depth >= 4 is then 40%, subject to a non-negligible statistical error due to the small sample size.

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?

We thank the reviewer for the suggestion. First, at the risk of being redundant, we would like to point out that our current algorithm does not involve tree search. We construct the proof tree merely by sampling the proof for each proposed lemma once. While combining our proof tree structure with search algorithms such as MCTS is an interesting question, we leave it as a future work and mostly focus on the effect of proposing new lemmas during training in this paper.

While allowing finer-grained decomposition may make each lemma easier, proposing more lemmas may not always increase the pass rate of the model due to the definition of global correctness — a theorem is proved only if all the proposed lemmas are also proved. As a concrete example, even if each proposed lemma can be proved with probability 50%, with tree depth 5, the overall pass rate drops to about 3% even if only one lemma is proposed in every conditional proof. This is consistent with our empirical observation in Figure 4, where only a very small amount of theorems can be proved with tree depth > 3. To handle deeper proof trees, we might need a fundamentally better model by scaling up either the model size or the dataset, which are unfortunately out of our compute budget.