Proving Theorems Recursively

Thank you for your detailed and constructive comments. And thank you for your acknowledgment in POETRY. We hope our responses and rebuttal materials (RM) address your concerns.

Weaknesses

w1. How POETRY scales with more computing resources.

Indeed, a large portion of the improvement comes from using the beam-search decoding method, resulting in deterministic outcomes. However, we believe the performance improvement brought by POETRY is unrelated to the specific decoding method used. Several alternative methods, such as beam sampling or sampling with a larger number of samples per input, can replace beam-search decoding.

Regarding scaling POETRY with more computing resources, it can be extended with larger models, more training data, and expert iteration processes. Arming POETRY with more capable language models, the advantage of recursive theorem proving will be amplified as we tackle more complex problems that require more structural reasoning.

Moreover, POETRY opens up new avenues for parallel computing. The current version of rBFS is single-threaded, adapted from BFS to showcase the performance of recursive theorem proving. In future work, we could explore parallel recursive Monte Carlo tree search, where each sub-level proof sketch can be explored concurrently. Information from different sub-searches can backpropagate to the main branch, dynamically allocating computing resources to more promising sub-searches.

Therefore, we believe POETRY’s advantage will not diminish as computing resources scale up; instead, it will show more prominent advantages compared to step-by-step approaches. We are excited to explore this aspect in our future work.

Question

Q.1 Cause of complex proof in Figure 5(b).

The GPT-f Baseline example in Figure 4(b) uses a standard best-first search algorithm to find the proof, where the choice of nodes to explore is determined by the cumulative log probability of the tactics. Although the GPT-f Baseline manages to produce the first two steps in Path 2, the log probability for the second line show "⋀n. deg R f < n ⟹ n_mult f n = 0" is too low compared to other generated tactics. Consequently, the search algorithm keeps exploring other states (like steps in Path 1) with higher log probabilities.

While one might use a separate value function model to re-rank the proof states, it is still challenging to ensure the value function will always prefer the better path. POETRY, on the other hand, takes advantage of the Isabelle system, allowing proofs to be validated in advance and thus reducing the dependency on the value function.

Thank you for your detailed and constructive comments. We hope our responses and rebuttal material address your concerns.

Clarifications on the summary

There are a few misunderstandings in summary that we would like to clarify: Within each proof sketch, POETRY operates step-by-step, searching for a complete proof sketch. At each step, POETRY takes a proof state (goal) as input and predicts one proof step, not the entire proof sketch. This step could be a conjecturing step followed by “sorry” (e.g., have c1:"a=1" sorry), or a normal proof step (e.g., by …). The search for the current sketch only stops after the sketch is complete and accepted by Isabelle.

Weaknesses

w1. Clarification on the baseline

Both Thor w/o Sledgehammer and the GPT-f Baseline are reproductions of the GPT-f paper in the Isabelle formal system. Thor w/o Sledgehammer is directly adopted from the original Thor paper as an ablation setting using only LM. Since Thor is not open-sourced, we reproduced it as GPT-f Baseline. The methodology in Thor w/o Sledgehammer is the same as in our GPT-f Baseline, with only implementation differences detailed in Section 4.1. So the use of Thor w/o Sledgehammer in Table 1 is not convoluted, as it illustrates the performance of the previous paper’s implementation result of the GPT-f Baseline.

w2. Pass@1 metric

POETRY, GPT-f Baseline, and Thor w/o Sledgehammer all perform step-by-step searches using the best-first search algorithm. Therefore, the number of interactions with Isabelle and the language model are the same for POETRY and both baselines. So it’s perfectly fair to use the pass@1 score for comparison.

w3. On "Can POETRY find longer proof?"

It is crucial to demonstrate POETRY’s ability to find longer proofs, as it shows its capability to solve complex problems. Previous step-by-step methods often result in significantly shorter proofs than those found by POETRY, diminishing the possibility of solving more complex problems.

We appreciate your insightful suggestions for analyzing POETRY’s results. We further included histograms showing the number of problems solved by GPT-f Baseline and POETRY, categorized by the length of the ground truth proofs (Figure 1 in the RM). From the Figure, it is evident that POETRY has an obvious tendency to solve harder problems (longer ground truth proofs). And outperforms the GPT-f Baseline across various problem difficulties in the multi-level subset. Therefore, we believe POETRY demonstrates a clear advantage over GPT-f Baseline and is capable of solving more complex problems.

Question

q1. The condition of a sketch being valid

When a sketch is accepted by Isabelle (receiving ONE signal no goals), it means the sketch is both syntactically and semantically correct. There is no difference in the signal given back from Isabelle whether a proof sketch is valid or the complete proof is valid. POETRY relies on post-checking to determine if the proof contains sorry.

q2. Proof length differences

According to w3, POETRY can indeed solve harder proofs. For proof lengths, POETRY does not tend to generate longer proofs than the GPT-f Baseline for problems they both solve. Algorithmically, POETRY behaves almost identically to GPT-f Baseline, only proceeding to deeper levels when a complete proof sketch is found, which is challenging. Statistically, 82.3% of the problems solved by both have the same proof length, and 96.0% have proof length differences smaller than 3, caused by algorithmic randomness.

Occasionally, POETRY generates longer proofs with redundant steps, as shown in Figure 2(a) in the RM. This is due to POETRY’s greedy exploration mechanism, which sometimes explores dummy sketches. These cases are rare (2.4% of solved problems where POETRY’s proof is 3 steps longer than GPT-f Baseline’s). We believe this issue can be addressed by implementing a value function to prioritize informative sketches over redundant ones in future work.

Therefore, combining the w3 response, it is evident that POETRY not only handles simple problems but also excels at solving harder problems and conducting complex structural reasoning.

q3. Example in LEGO-Prover

Here is an example from the LEGO-Prover GitHub:

theorem aime_1983_p9:
  fixes x::real
  assumes "0<x" "x<pi"
  shows "12 \<le> ((9 * (x^2 * (sin x)^2)) + 4) / (x * sin x)"
proof -
  define y where "y = x * sin x"
  have "12 \<le> (9 * y^2 + 4) / y"
  proof -
    have c0: "y > 0"
      by (simp add: assms(1) assms(2) sin_gt_zero y_def)
    have "(9 * y^2 + 4) \<ge> 12 * y"
      by sos
    then show ?thesis
      using c0 by (simp add: mult_imp_le_div_pos)
  qed
  then show ?thesis
    by (simp add: power_mult_distrib y_def)
qed

Conjectures like have "12 \<le> (9 * y^2 + 4) / y" or have c0: "y > 0" are relatively local. Making these into independent lemmas requires many local variables, resulting in redundant proof lines and lemma statements. This example is not cherry-picked and this problem is common in many theorems. POETRY addresses this by building proofs level-by-level directly within the proof, avoiding redundant lemma statements.

q4. The search algorithm used in the baselines

Thor w/o sledgehammer and GPT-f Baseline use the best-first search algorithm described in the original GPT-f paper.

q5. Explanation with Thor w/o sledgehammer

Please refer to w1.

q6. Confusion in Figure 5(b)

This figure compares the full proof length (Original) against the number of steps in all sketches (Recursive), including both top-level and deeper sketches. The Original line counts each complete theorem as a single data point (e.g. proof with length 20), whereas the Recursive line treats each decomposed proof sketch as a single data point (e.g., decomposed sketches with length 9 and 11). Therefore, the total number of data points for these two plots is different. We will provide a more detailed explanation in our final paper.

Dear Reviewer 9pow,

We hope our rebuttal sufficiently addressed your concerns. Is there any additional information we can provide that might lead you to increase your rating? We look forward to your feedback.

Many thanks, Author

Thank you for your detailed and constructive comments. We hope our responses and rebuttal material (RM) address your concerns.

Clarification on strengths.

There are a few misunderstandings regarding our strengths that we would like to clarify. While we are not the first to use the term proof sketch, there are significant differences between the proof sketch in POETRY and those in previous works like Draft, Sketch and Prove or LEGO-Prover:

• In previous work, proof sketches do not use the keyword sorry to defer the proof of concrete conjectures but instead use Sledgehammer to directly prove these conjectures.
• The “proof sketch” is not used recursively in previous work, with only one sketch per problem. In the appendix, we present examples of proofs that require multiple layers of recursive expansion, which are challenging to resolve using automated tools like Sledgehammer within a single sketch. Our method allows these subgoals to be addressed incrementally, maintaining a consistent level of difficulty throughout the process.

Weaknesses

w1. Dataset construction.

Please see Figure 1 in the paper for the process of data construction. Figure 1(a) shows the original proof, and Figure 1(b) depicts the decomposed proof sketches with sorry added. Additionally, Table 1 in the RM shows the final training crops for this problem. The final training data for POETRY and GPT-f Baseline have the same input text and the same number of training examples. The only difference is the additional sorry keyword in proof steps that state conjectures or subgoals. Therefore, the model trained with POETRY data does not receive more information compared to the GPT-f Baseline. The success of POETRY not only comes from the data curation process but also from the novel recursive BFS and the recursive proving methodology itself. We will include this table in our paper for better illustration.

w2. Context explaining the comparison with Lean result against Isabelle.

The results for Lean and Isabelle are indeed not directly comparable, and we will add context explaining this matter in the paper. Here is a brief explanation:

• We follow previous work like Li et al. to provide a comprehensive demonstration of the benchmark results in miniF2F.
• Although the results are not directly comparable, the high-level ideas of these approaches share many similarities. The GPT-f Baseline shows much resemblance to PACT, FMSCL, and LeanDojo. By showing these results side by side, we can better understand how different formal systems perform in the benchmark.

w3. Details on Pros and Cons of POETRY

We have followed your advice and conducted a more thorough analysis of POETRY.

• Problem types that POETRY excels at. In the RM, Figure 1 shows the number of problems solved by GPT-f Baseline and POETRY based on the length of the ground truth proofs. POETRY has a clear tendency to solve harder problems with longer ground truth proofs. As a domain-agnostic method, POETRY may not demonstrate a clear advantage in specific mathematical domains. However, Figure 1(c) clearly shows that POETRY has a significant advantage in problems requiring multiple levels of reasoning.

• POETRY performance on existential instantiation. In Isabelle, existential instantiation can be performed using the define, let, or obtain tactics. define and let typically require explicit construction of a term that satisfies the existential condition and does not introduce a new level, making POETRY’s behavior similar to GPT-f Baseline. In contrast, obtain allows extracting a term that satisfies a given property without explicit construction, with POETRY using sorry to skip the verification of satisfiability. This approach offers more flexibility, enabling the proof to focus on variable usage and deferring validation. Although not directly involving existential instantiation, below is an example of a proof by POETRY using obtain:

  lemma terminates_tl_raw: 
    assumes "terminates g"
    shows "terminates (tl_raw g)"
  proof
    fix st :: "bool \<times> 'a"
    obtain n s where "st = (n, s)"
      by (cases st) blast+
    from assms have "s \<in> terminates_on g"
      by (metis terminatesD)
    thus "st \<in> terminates_on (tl_raw g)"
      unfolding \<open>st = (n, s)\<close>
      apply(induction s arbitrary: n)
      by(case_tac [!] n)(auto intro: terminates_on.intros)
  qed
  

  Here, the top-level sketch instantiates n and s and proceeds with proving conjectures, with the actual verification of the condition deferred.

• POETRY indeed proves more theorems that are longer and harder. From Figure 1 in the RM, it is clear that POETRY is capable of proving more difficult problems (with longer ground truth lengths) and excels in multi-level subsets.

Figure 2 in the RM provides more cases to better understand POETRY’s pros and cons. As illustrated, though happening sparsely, POETRY’s greedy exploration mechanism might lead to finding proofs with redundant steps or failing to find shallow proofs. However, we believe this issue can be addressed by implementing a value function to prioritize informative sketches over redundant ones in future works.

Questions

q1. Relations between proof sketches and the tree of conjectures.

Proof sketches strictly include the tree of conjectures and also contain various other elements. For example, the obtain and show statements instantiate variables, and the subgoal tactic focuses on specific goals (shown in Figure 2(c) in the RM). POETRY inserts sorry whenever a proof step increases a proof level, allowing any form of proof sketch as long as it is permitted by the Isabelle language.

q2. Finetuning on miniF2F.

No, we do not finetune any data with the miniF2F dataset. All the training data we use comes from the AFP Library and Isabelle built-ins.

Dear Reviewer BhWC,

We hope our rebuttal sufficiently addressed your concerns. Is there any additional information we can provide that might lead you to increase your rating? We look forward to your feedback.

Many thanks, Author

Thank you for your response and clarifying the strengths. Perhaps I mis-worded the section on the strengths poorly, but I understood that the proof sketches both insert a sorry and are applied recursively. I'm merely pointing out that recursive decomposition and lazy evaluation is in general not novel. On the contrary, I think it is clever to take a formal proof dataset and algorithmically insert sorry/admitted at strategic points and show that this additional signal can be leveraged is novel.

w1. Dataset construction. Thank you for the reference to Figure 1. To clarify my original question concerning having a before and after sorry, which is partially shown in Figure 1, is precisely what information is contained in the arrow from the upper level to a recursive level. In particular, does it contain the minimal proof context for the entire theorem required to make the subgoal well-typed or just the local subgoal plus a reference to a location in the existing proof? It was not clear to me which it was from the Figure or the paper description.

Therefore, the model trained with POETRY data does not receive more information compared to the GPT-f Baseline.

I disagree with this statement. Your approach augments the dataset with sorry which precisely indicates when multi-level proofs are required as per your dataset curation process. Put another way, sorry indicates that a hammer will likely fail. This is additional information that other methods do not see and could benefit from! To test this, you could change the dataset curation process to insert a sorry every n proof levels instead of 1, or at random proof levels, to tease apart the effect of dataset augmentation on your approach.

w2. Context explaining the comparison with Lean result against Isabelle. Thank you for this additional clarification.

w3. Details on Pros and Cons of POETRY Thank you for the additional work in the RM. With regards to the types of problems that Poetry excels at, I buy that it does indeed prove longer theorems. However, I was wondering how it performs on kinds of problems such as algebraic vs. geometric, since algebraic are more compute heavy (longer proofs) and geometric problems require more constructions (i.e., existentials). Thank you for the discussion on existentials as this is a limitation of this work.

I appreciate the work overall and find the approach with dataset augmentation with sorry is valuable. I am inclined to maintain my score since I still have slight concerns about weakness 1.

Dear Reviewer BhWC,

We appreciate your prompt reply and recognition of our work.

w1. Dataset Construction

Regarding your question, the language model perceives only the local subgoal when entering the next level, without knowing the location of the sorry. The rBFS handles all movements, whether going deeper or jumping backward. As the model progresses to the next level (as indicated by the arrow in Figure 1), the rBFS identifies the sorry and extracts the proof state immediately preceding it (i.e., the state of the conjecture). This proof state is then used to prompt the model for the next steps. Therefore, there is no difference between the input in the middle of the sketch and the input that starts a low-level sketch. While adding minimal proof context from the upper level could improve POETRY’s performance (and we believe it would), we did not include this to ensure a fair comparison with the GPT-f baseline. This allows us to clearly assess the impact of recursive proving.

This is additional information that other methods do not see and could benefit from!

We agree that the model receives more information compared to the GPT-f baseline in this aspect, and we acknowledge the value of the suggested ablation experiment. However, due to the limited time remaining during the rebuttal period, we may not be able to complete this experiment. We will include these ablation results in our final paper.

w3. Types of problems that POETRY excels

To provide more clarity on the types of problems where POETRY excels, we’ve included the table below, comparing the performance of POETRY and the GPT-f baseline across different mathematical categories in the PISA dataset. The results are categorized based on the directories of lemmas in the AFP library. From the table, we can see that POETRY outperforms the GPT-f baseline in most categories, including geometry and algebra.

Have our responses above adequately addressed your concerns? Is there any additional information we can provide to persuade you to improve your rating?

Thank you for your detailed and constructive comments. We hope our responses and rebuttal material address your concerns. As you mentioned in the strengths section, we will release all the code, models, and data on the POETRY system to support further research on this topic.

Weaknesses

w1. Novelty on the recursive method.

To the best of our knowledge, we are the first to introduce this type of recursive, top-down search in the domain of neural theorem proving. The challenge of the step-by-step proof search has been long recognized, but no effective method has been proposed until now. Other reviewers (BhWC, 9pow, p8XS) acknowledge the novelty, simplicity, and effectiveness of POETRY’s design, and believe it will be crucial to advancing neural theorem proving.

w2. The necessity of the novel recursive best-first search

There are various options to handle recursive proving approaches, and we chose to use recursive best-first search (rBFS) for the following reasons:

• Alignment. The rBFS algorithm aligns well with the recursive proving paradigm. As proofs are broken into several proof sketches, it's natural to align each sketch with an individual BFS search.
• Equal Treatment for Equivalent Matters. Within a single problem, each sketch we seek to find is fundamentally the same, allowing the same structure to occur in every sketch. Thus, we want equal treatment for every sketch and avoid unnecessary defunctions at certain levels.
• Better extensiveness. Equal treatment also enhances the algorithm’s extensiveness. Currently, we experiment with BFS as the core algorithm, but it will be easy to integrate new search algorithms like MCTS or other improved search methods into rBFS.
• Easy parallelization. Currently, rBFS is executed in a single-threaded manner, but since each sub-search is identical to the others, rBFS can easily run in parallel, leveraging more powerful computation resources.

As you pointed out, one could indeed use vanilla BFS for recursive theorem proving with a dedicated design of node priority scores to enforce implicit level-by-level search. However, while it’s straightforward to prioritize the conjecture’s level at the top level, ensuring the same behavior for the conjecture level inside the proof of the top-level conjecture becomes complex. Adding the uncertainty of log-prob makes the algorithm intricate and uncontrollable. Nonetheless, we acknowledge that such an algorithm is possible and may have advantages over rBFS in certain aspects. However, this design would lose the beneficial properties of rBFS listed above.

Regarding the combination of standard breadth-first search and best-first search, it’s important to note that the current best-first search operates similarly to the breadth-first search in the GPT-f paper. The priority score for the best-first search is cumulative log-prob, where the score for each node is calculated by accumulating all the log-prob from the root node to the current node. Consequently, nodes at deeper levels tend to have lower scores, and the actual behavior of best-first search resembles breadth-first search. Therefore, we could not come up with a way to combine breadth-first search and best-first search to tackle recursive proving approaches.

w3. The performance on miniF2F with large language model.

We have included Table 2 in the RM, listing baseline methods that utilize large language models on the miniF2F benchmark. It is important to note that these methods use a completely different approach to prove theorems. Instead of performing searches using BFS algorithms, these approaches leverage the general-purpose capabilities of LLMs to translate natural language proofs into formal code (often termed autoformalization). Therefore, comparing these methods with POETRY is not only unfair in terms of model size and the amount of training data but also incomparable in core methodology.