Proving Theorems Recursively

Authors: haiming  wang
huajian  xin
zhengying  liu
wenda  li
yinya  huang
jianqiao  lu
zhicheng  yang
jing  tang
jian  yin
zhenguo  li
xiaodan  liang
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-14 17:38:53

Abstract: Recent advances in automated theorem proving leverages language models to explore expanded search spaces by step-by-step proof generation. However, such approaches are usually based on short-sighted heuristics (e.g., log probability or value function scores) that potentially lead to suboptimal or even distracting subgoals, preventing us from finding longer proofs. To address this challenge, we propose POETRY (PrOvE Theorems RecursivelY), which proves theorems in a recursive, level-by-level manner in the Isabelle theorem prover. Unlike previous step-by-step methods, POETRY searches for a verifiable sketch of the proof at each level and focuses on solving the current level's theorem or conjecture. Detailed proofs of intermediate conjectures within the sketch are temporarily replaced by a placeholder tactic called sorry, deferring their proofs to subsequent levels. This approach allows the theorem to be tackled incrementally by outlining the overall theorem at the first level and then solving the intermediate conjectures at deeper levels. Experiments are conducted on the miniF2F and PISA datasets and significant performance gains are observed in our POETRY approach over state-of-the-art methods. POETRY on miniF2F achieves an average proving success rate improvement of 5.1%. Moreover, we observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.

Main paper: 
 introduction: 
 Neural theorem proving has made significant strides in recent years [Polu and Sutskever, 2020 , Han et al., 2022 , Polu et al., 2022 , Wang et al., 2023c , Jiang et al., 2022a , 2021 , 2022b , Wang et al., 2023b , Huang et al., 2024 , Thakur et al., 2024 , Liu et al., 2023 , Xiong et al., 2023] , particularly with the integration of language models and search algorithms [Polu and Sutskever, 2020 , Han et al., 2022 , Jiang et al., 2022a , Yang et al., 2023 , Lample et al., 2022] . The combination of language models, which excel at understanding and generating human-like text, and search algorithms, which systematically explore potential solutions, has proven to be a powerful approach to discovering proofs for intricate theorems [Polu and Sutskever, 2020 , Lample et al., 2022 , Jiang et al., 2022a] .As shown in Figure 1 (a), search-based neural theorem proving methods begin with a theorem statement to prove. A formal mathematic environment like Isabelle will first process the theorem statement and provide the initial proof state. Starting with the initial proof state, the proving process alternates between sampling new proof steps from the language model and obtaining new states assume n_ge: "n ≥ 0" thus ?thesis proof (cases) assume m_ge: "m ≥ 0" thus ?thesis sorry next assume m_lt: "¬ m ≥ 0" with n_ge show ?thesis sorry qed assume n_lt: "¬ n ≥ 0" thus ?thesis proof (cases) assume m_ge: "m ≥ 0" have "inv x [^] (nat m * nat (-n)) = inv x [^] nat (-(m * n))" sorry show ?thesis sorry ... assume m_ge: "m ≥ 0" thus ?thesis using n_ge nat_pow_pow int_pow_def2 assume m_lt: "¬ m ≥ 0" with n_ge show ?thesis apply (simp add: in-t_pow_def2)by (metis assms mult_mi-nus_right n_ge nat_pow_pow)have "inv approach ignores the hierarchical structure inherent in the proof, treating it merely as a sequence of proof steps.The proof cannot be verified as valid until it is fully complete. (b) The recursive proving method decomposes the structured proof into different levels of verifiable proof sketches. Each proof sketch attempts to prove the target theorem or conjecture by outlining the primary steps at the current level and postponing the proof of intermediate conjectures to the next level.by executing the generated proof steps within the formal mathematic enviroment. Additionally, a search algorithm, such as best-first search or Monte Carlo Tree Search (MCTS), is employed to find a complete path of proof steps. The search algorithm selects the next state to explore based on heuristics such as the log-probability of the proof step [Polu and Sutskever, 2020 , Jiang et al., 2022a , Yang et al., 2023] , value function scores of the proof state [Han et al., 2022 , Polu et al., 2022] (in best-first search), or a PUCT score that combines both [Wang et al., 2023c , Lample et al., 2022] (in MCTS). These heuristics assess the plausibility or potential value of a given step, helping to prioritize the most promising actions. However, these scores are approximate, do not ensure the correctness of the proof direction, and can lead to exploring sub-optimal or distracting subgoals.Even if the language model is capable enough to produce correct proof steps, the search algorithm, guided by short-sighted heuristics, often gets trapped exploring a detailed proof of a meaningless intermediate conjecture. This wastes time and may even cause the algorithm to fail in finding the correct proof path due to a search timeout. Moreover, as the length of the proof increases in more challenging problems, the search space expands exponentially. Consequently, the need for an accurate heuristic to guide the search becomes critical, as a myopic step-by-step approach can easily get lost in the vast expanse of the intermediate proving steps.To address the aforementioned drawbacks, we propose POETRY, a novel approach that proves the theorem recursively, level by level. As shown in Figure 1 (b), POETRY first searches for a proof sketch, which is defined to be a verifiable proof outline with the detailed proof of the middle conjecture replaced by a placeholder tactic, sorry. The sorry tactic signals the formal environment to temporarily ignore the proof of the middle conjecture, assuming it as resolved. Once a validated proof sketch is established, POETRY then endeavors to prove the intermediate conjectures that remain unresolved, also in a recursive, level-by-level manner. This procedure persists until every sorry keyword is substituted with a valid proof. Notably, the verified sketch at each level may still contain errors. Since POETRY uses the sorry tactic to skip the proof of intermediate conjectures, these conjectures might represent false statements and be unprovable. However, they still serve as correct conjectures to prove the target theorem or conjecture at the current level, resulting in an incorrect proof sketch. For example, to prove the theorem of the commutative property of addition, a + b = b + a, a false conjecture such as a = b might be used. However, when actually attempting to prove a = b, we would never be able to find a valid proof at the next level. If a false proof sketch is generated and POETRY fails to find the proof for the middle conjecture, it will continue its search to identify a new proof sketch. Nevertheless, Empirical evidence indicates that verifying and ensuring the correctness of the proof sketch at each level before delving into deeper proofs significantly enhances performance. Additionally, we observe a substantial increase in the length of the proofs being able to be generated by POETRY compared with step-by-step approaches. This recursive methodology is inspired by human problem-solving techniques, where complex problems are decomposed into manageable sub-problems, each addressed using a similar recursive strategy.By adopting this approach, POETRY not only improves the efficiency of its search process but also increases the overall success rate in discovering valid proofs.We conduct extensive experiments on the theorem proving datasets miniF2F [Zheng et al., 2021] and PISA [Jiang et al., 2021] to validate the effectiveness of our proposed approach. POETRY significantly outperforms previous approaches, achieving a pass rate of 42.2% on both the miniF2F valid and test datasets, respectively. With a 5.1% absolute improvement on average over the previous state-of-the-art. Additionally, our ablation study shows that with recursive theorem proving, we obtain a 3.9% absolute improvement on average compared with step-by-step baselines. Our case study also reveals that POETRY can find proofs substantially longer compared with sequential stepby-step proving methods, the maximum proof length increases from 10 to 26 compared to the stepby-step baseline in the PISA dataset. 
formal mathematic enviroments: 
 We choose Isabelle [Paulson, 1994] as our formal environment. It is widely used for formal verification purposes in academia and industry [Gesellensetter et al., 2008 , Klein et al., 2009 , Zhang et al., 2024] . It employs a structured proof language called Isar [Wenzel et al., 2004] , which facilitates the creation of human-readable proofs and bridges the gap between formal verification and human understanding. As illustrated in Figure 1 (a), Isabelle processes each proof step (or tactic) and provides feedback. If the proof step fails to apply, an error message is returned. Otherwise, Isabelle returns a proof state along with a special variable, proof level, indicating the current level after applying the step. In the Isabelle theorem prover, the proof level indicates the depth within a structured proof. This level increases with commands like have, obtain, and show, which introduce new subgoals or conjectures in the proof. Conversely, it decreases with commands like by, qed and done, which conclude a proof block or subgoal.Isabelle is well-suited for POETRY to accomplish recursive theorem proving. The Isar language is elegantly structured in a level-by-level format, and it contains proof level that can be easily used to identify each level. However, the recursive proving technique proposed by POETRY is not specific to Isabelle; the same framework can be extended to other formal mathematical environments like Lean [de Moura et al., 2015] , Coq [Barras et al., 1997] , and HOL [Harrison, 2009] , with additional engineering effort to accommodate the proving strategies. These environments also provide mechanisms to temporarily skip parts of proofs, similar to Isabelle's sorry tactic, such as Lean's sorry, and Coq's Admitted. We will leave the extension of POETRY to other formal environments for future work.Search-based neural theorem proving mostly employs the approach introduced by GPT-f [Polu and Sutskever, 2020] . In this method, a pre-trained causal language model predicts the next proof step based on the current proof state and optional context. The language model is trained using data formatted as follows:EQUATIONwhere $(•) represents the substitution operation, and context denotes the preceding proof steps leading to the current proof state. At test time, GPT-f employs a best-first search strategy to identify a sequence of proof steps that solve the problem. Specifically, The proof search algorithm constructs a tree-like search structure, where each node represents a proof state and each edge represents a proof step. Starting from the root node, the proof search continuously selects the unexplored node with the highest score and performs an expansion. The score for each node is the cumulative log probability of the proof steps that led to the node. During expansion, the language model receives the node's proof state and preceding context, then samples e new proof steps. Isabelle subsequently processes these proof steps, generating new proof states or error messages. The search continues until a proof is found or the computational budget is exhausted. 1 (b), to prepare recursive proving data, we need to split theorems into blocks of proof sketches. Each proof sketch focuses solely on the target theorem, conjectures, or subgoals, with the detailed proof of intermediate conjectures or subgoals replaced by the sorry tactic. Algorithm 1 presents the pseudocode for the sketch data extraction process. POETRY initially inputs the complete theorem text into Isabelle, which parses it into a sequence of proof lines, containing proof steps and corresponding proof levels. Subsequently, the list of proof lines is passed to the ExtractProofSketch function with the index set to 0, initiating the extraction of all proof sketches. The sketch proof extraction process starts by identifying the current proof level, which is determined by the level of the proof step at the initial index (Line 5). Proof steps that are on the same level as the target theorem, conjectures, or subgoals are those that directly focus on proving the target. Our goal is to retain proof steps with a proof level equal to the current proof level (Lines 10-12) and replace higher-level proof steps with the sorry tactic (Lines 13-16). We defer the extraction of higher-level proofs to the recursive call of ExtractProofSketch in Line 15. Finally, the function will return a list of extracted proof sketches, each containing only the current level of proof, as illustrated in Figure 1(b) .Training data construction. Following the extraction of proof sketches, POETRY follows Jiang et al. [2022a] and uses PISA, an interactive environment built on top of Isabelle, to extract proof states for each proof step. Subsequently, the proof states and proof steps are reformatted into lines in Equation 1 and used as training examples to fine-tune the language model. Notably, although sorry is an independent tactic in Isabelle, POETRY integrates the sorry tactic into the preceding proof step (Line 14 in Algorithm 1). This enables the language model to predict the intermediate conjectures and the sorry tactic simultaneously. For example, a proof step with the sorry keyword would appear as have "x + 2 = 2x" sorry. Merging the sorry tactic is crucial to ensure that the language model generates proof steps at the current level and postpones higher-level proofs using the sorry tactic. Without this merge, the model must determine the use of sorry solely based on the context and proof state, which offers no guarantee that the model will generate the necessary sorry after stating a conjecture or subgoal. This approach ensures that deep-level proofs are deferred correctly.  
recursive best-first search: 
 To prove theorems recursively, POETRY introduces a novel recursive best-first search (recursive BFS) algorithm to conduct a level-by-level proof search. Figure 2 illustrates a complete walkthrough.In general, recursive BFS employs the best-first search technique to search for proof sketches at each level. When a proof sketch is found at a certain level, the algorithm pauses the search at this current level and then proceeds to the next level to solve the skipped middle conjectures by this current level. Once all sketches are found and middle conjectures or subgoals are resolved, a complete proof is achieved. Recursive BFS enhances the generic best-first search to handle multi-level proofs and ensures that the search can pause and continue across different proof levels, adapting BFS to dynamically shift between current and subsequent proof layers based on the progress and outcomes of proof sketches. Below, we will introduce the core elements in the recursive BFS: the sorry edge and the node status. For the complete updating rules of nodes status and proof search terminate conditions, please refer to Appendix A.1.Sorry edge and node status. As shown in Figure 2 (a), each node in the proof tree is a proof state, and each edge is a proof step. In a proof state, once a tactic contains a "sorry" keyword (usually after a conjecture or subgoal), we use a special sorry edge to connect the parent node and the child node. Then the sorry edge attaches the root node of the next proof level with an unproved conjecture or subgoal. Such root nodes have a score of 0 and will not be selected in the currentlevel proof search. Moreover, we attach each node in the search tree with one of the status labels: OPEN (the node is open, and no proof has been found so far), FAILED (the node is failed when all potential subproofs or child nodes stemming from it are unable to establish a valid proo), PROVED (the node is proven and part of the successful proof), and HALF-PROVED. A HALF-PROVED node means it belongs to the trajectory that has successfully found a complete proof sketch but contains special sorry edges with unsolved next-level subgoal or mid-conjecture. Only after all the midconjectures or subgoals in the sorry edges from the HALF-PROVED node to the PROVED node are proved will the node be switched to a PROVED node, as illustrated in Figure 2 (f).Using recursive best-first search, POETRY can generate a verifiable proof sketch at each proving level before proceeding to prove the middle conjectures or subgoals at the next level. In essence, POETRY breaks down a lengthy proof into manageable, shorter proof sketches, preventing the search space from expanding exponentially as the proof length increases. This approach allows search-based methods to find more challenging and longer proofs without necessitating a highly performant value function model to guide the proof search procedure. 
experimental setup: 
 This section presents our experimental setup, detailing the baselines and evaluation metrics. The implementation details are covered in Appendix A.2.Baseline methods. To fairly compare POETRY with classic step-by-step baselines like GPT-f [Polu and Sutskever, 2020, Jiang et al., 2022a] , we implement an Isabelle version of GPT-f, denoted as GPT-f Baseline. This baseline model is trained on the same dataset as POETRY, with the only modification being the removal of all sorry keywords in the proof steps. All hyperparameters and setups for training and the BFS search are identical to POETRY to ensure a fair comparison.Notably, the GPT-f Baseline is similar to Thor [Jiang et al., 2022a] , except for three main differences. Firstly, GPT-f Baseline does not use Sledgehammer [Paulson, 2010] , nor replace the smt, metis tactic with <hammer> in the proof step for training. Secondly, GPT-f Baseline fine-tunes a 1.3B parameter proofGPT [Azerbayev et al., 2023] , whereas Thor uses a 700M model pre-trained on The Pile [Gao et al., 2020] . GPT-f Baseline also uses a newer version of Isabelle which contains more state action pairs for training (detailed in Section A.3). Thirdly, during the proof search, the GPT-f Baseline utilizes the beam-search decoding method instead of sampling to generate proof steps for each proof state.Aside from the GPT-f Baseline, we also include state-of-the-art search-based neural theoremproving methods. PACT [Han et al., 2022] , FMSCL [Polu et al., 2022] , Leandojo [Yang et al., 2023] , and COPRA [Thakur et al., 2024] are works focusing on the Lean formal environment. 3 Contrastively, Thor [Jiang et al., 2022a] , Thor with expert iteration on auto-formalized data [Wu et al., 2022] and Thor + Magnushammer [Mikuła et al., 2023] are works done in Isabelle. Moreover, for methods with LLMs, COPRA is an in-context learning agent that uses GPT-4 [OpenAI, 2023] to generate proof steps and prove the theorem step by step.We do NOT compare our methods with LLM-based proving approaches like DSP [Jiang et al., 2022b] , Lyra [Zheng et al., 2023] , or LEGO-Prover [Wang et al., 2023b] . These approaches employ general-purpose large language models (LLMs), such as ChatGPT or GPT-4, which feature several orders of magnitude more parameters than the models considered in our study. Moreover, these methods typically utilize proofs in natural language to guide the generation of formal code without searching and attempting to solve each problem 100 times. In contrast, POETRY provides a performance evaluation at pass@1, attempting to prove the theorem once for each problem.Evaluation datasets and metrics. For evaluation, we use two datasets, the miniF2F dataset [Zheng et al., 2021] , and the PISA [Jiang et al., 2021] . The miniF2F dataset comprises 488 problems with varying levels of difficulty, ranging from basic algebra and number theory, originating from the MATH dataset [Hendrycks et al., 2021] , to more challenging problems found in the AIME 4 and IMO [Daniel Selsam, 2019] . The problems are divided into valid and test sets, with 244 problems each. The miniF2F dataset only contains problem statements and we only evaluate our method on this dataset, without any training. The other dataset we adopt is the PISA test set, which comprises theorems from the Archive of Formal Proofs [MacKenzie et al., 2021] and the Isabelle standard library [Nipkow et al., 2002] . To better understand how POETRY performs in complex problems with multiple levels, we subdivided the test set into two subsets: single-level and multi-level. The PISA single-level subset contains problems with only one level in the ground truth human-written proofs, whereas the PISA multi-level subset includes problems with multiple proof levels. A more comprehensive analysis of the PISA dataset is shown in Appendix A.3. For evaluation metrics, we follow Jiang et al. [2022a] , Yang et al. [2023] and use pass@1 as the evaluation metric, where each theorem in the dataset is proved once by POETRY. Then we calculate the proportion of the theorems being successfully proven.Comparison with language model-only baselines. As shown in Table 5 , we compare POETRY with baselines that only utilize language models to search for proofs. Thor w/o sledgehammer is the language model-only version of Thor [Jiang et al., 2022a] . It does not call the sledgehammer during the proof search. Our reproduced GPT-f Baselines outperform Thor w/o sledgehammer by 13.7% in miniF2F and 10.6% in the PISA test set. This performance boost is mostly due to using the beam-search decoding strategy during the proof search, as we observe the performance of the GPT-f Baseline with sampling drops by 6.8% compared with the beam-search version. This is because the beam-search decoding method is guaranteed to produce e different proof steps for each proof state, whereas the sampling will produce duplicate proof steps, making the actual number of proof steps generated per expansion smaller than e. The remaining performance improvements are mostly contributed by larger model sizes and better pertaining.Compared with the GPT-f Baseline, we can observe the benefit of the recursive theorem proving. POETRY outperforms GPT-f Baselines by 3.9% in the miniF2F dataset on average, and 0.7% in the PISA test set. The modest performance gain observed in the PISA test set is primarily attributed to the skewed distribution of problem complexity, with the majority of problems containing only a single proof level (see Table 3 ). POETRY executes nearly identically to the GPT-f Baseline when encountering proofs with only one level, resulting in similar performance within the single-level subset. In contrast, POETRY achieves a 2.5% improvement on the multi-level subset. Furthermore, POETRY solves a very distinct set of theorems compared with GPT-f Baseline in PISA, with 99 out of 1109 theorem solved by POETRY can not be proved by GPT-f Baseline, taking up 4.4% in total. This outcome well supports the effectiveness of our proposed recursive proving method. Moreover, the gap between step-by-step approaches and POETRY does not end here. The effectiveness of POETRY will become even more pronounced as the language models are continuously improved and solve more complex proofs, where the bottleneck caused by searching comes to the fore yet POETRY is demonstrated effective for searching. The distribution in the single-level subset. In this subset, POETRY and GPT-f Baseline should behave nearly identically; therefore, there are not many differences as expected. (c) The distribution in the multi-level subset. POETRY has a distinctive advantage over GPT-f Baseline. This is the subset where all the complex theorems exist.Comparison with state-of-the-art methods. In Table 2 , we illustrate the proportion of successful proofs found on the miniF2F dataset. Due to the larger amount of formal data, as well as the help of hands in ATP like the sledgehammer, the approaches using Isabelle tend to achieve a higher pass rate compared with approaches using Lean environments. Our proposed POETRY significantly outperforms all such approaches. POETRY outperforms Thor+Magnushammer by 5.1% on average, the highest performance on the miniF2F dataset with the search-based method at pass@1.Notably, the recursive proving method is orthogonal to these baseline approaches. It can be further improved with the use of Sledgehammer or Magnushammer [Jiang et al., 2022a , Mikuła et al., 2023] , running expert iteration on the training set [Polu et al., 2022 , Wu et al., 2022] , using retrieval augmented proof step generation techniques [Yang et al., 2023] , or even better search algorithm in each level [Wang et al., 2023c , Lample et al., 2022] . As these are not the focus of the current paper, we leave the integration for future work.Can POETRY find longer proof? Figure 3 (a) and (b) compares the proof length of proofs discovered by the GPT-f Baseline and POETRY in both the miniF2F dataset and the PISA test set. It can be observed that the proof lengths found by POETRY are longer than those found by the GPT-f Baseline. The average proof length increases from 1.47 to 2.13 in the miniF2F dataset and 1.62 to 2.09 in the PISA test set. Prominently, the maximum proof length increases from 3 to 18 compared with the GPT-f Baselines in the miniF2F dataset, and from 10 to 26 in the PISA test set. This proof length is unattainable without a recursive proving method. By comparison, the maximum proof length found by Leandojo in the miniF2F test set is 4, with an average proof length of 1.35. Therefore, it's evident that POETRY expands the possibility of discovering longer proofs and addressing more challenging problems.Can POETRY find harder proof? The ability to find longer proofs does not necessarily imply the ability to find harder proofs. We analyze this issue from two perspectives. First, POETRY does not generally produce longer proofs than the GPT-f Baseline for problems both approaches successfully solve. Algorithmically, POETRY operates almost identically to the GPT-f Baseline, only progressing to deeper levels when it identifies a complete proof sketch. Therefore, we expect similar proof lengths for problems solved by both methods. Statistically, 82.3% of the problems solved by both methods have identical proof lengths, and 96.0% have proof length differences of less than 3 steps, attributable to algorithmic randomness. Occasionally, POETRY generates longer proofs with redundant steps, as shown in Figure 6 in the Appendix. This is due to POETRYs greedy exploration mechanism, which sometimes explores dummy sketches. These cases are rare (2.4% of solved problems where POETRYs proof is 3 steps longer than GPT-f Baselines). We believe this issue can be addressed by implementing a value function to prioritize informative sketches over redundant ones in future work.Secondly, we included histograms displaying the number of problems categorized by the lengths of the ground truth proofs (Figure 3 (c), (d), and (e)). From these figures, it is evident that POETRY shows a marked tendency to solve harder problems (i.e., those with longer ground truth proofs) and consistently outperforms the GPT-f Baseline across various levels of problem difficulty within the multi-level subset. Therefore, we conclude that POETRY demonstrates a distinct advantage over the GPT-f Baseline, showcasing its ability to solve more complex problems.Case study. As illustrated in Figure 4 , we compare the proof found by the POETRY with the failed attempts by the GPT-f Baseline. The theorem n_mult_closed states that if a polynomial f belongs to the carrier set of polynomials P , then the operation n_mult applied to f results in a polynomial that also belongs to P . As shown in Figure 4 (a), the proof found by the POETRY contains two levels, marked with different shades of blue. The first level is completed by first showing two main properties: (i) Zero polynomial condition (the first show statement in Line 2): For any integer n greater than the degree of f , n_mult f n must be zero. (ii) Closure under carrier (the second show statement in Line 7): For any integer n, the result n_mult f n must be within the carrier set R.When proving the first level, the detailed proof of these two properties will be skipped with the sorry tactic. After the first level of the proof has been found, POETRY searches for the proof of these properties one by one in the next level. In contrast, the GPT-f Baseline failed to find valid proof for this problem, resulting in a search timeout after reaching 600 seconds of time limit. Two failure search trajectories are selected and shown in Figure 4 (b). For proof path 1, the proof searches astray and tries to utilize a more complex way to prove the first property, resulting in a timeout. The GPT-f Baseline also identified the first two steps in POETRY's proof. However, this proof path never had the chance to be further explored before the timeout occurred. From this case, we can see that by recursively proving the theorem, the proof with 11 steps is broken down into 3 proof sketches with a maximum length of 4. Therefore, POETRY effectively prevents the proof search from wasting too much time on searching for useless mid-step conjectures. These are typical successful cases for POETRY; additional failure cases can be found in Section A.4 of the Appendix.Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?Answer: [Yes] Justification: The paper provides detailed steps of the methodology, including the data extraction process, the training details in Section 3 and evaluation settings, results and corresponding explanations in Section 4. Guidelines:• The answer NA means that the paper does not include experiments.• If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not. • If the contribution is a dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable. • Depending on the contribution, reproducibility can be accomplished in various ways.For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed. • While NeurIPS does not require releasing code, the conference does require all submissions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. (d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome to describe the particular way they provide for reproducibility.In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results. 
related works: 
 Search-based neural theorem proving. Our work is closely related to prior work on step-bystep search-based nerual theorem proving. GPT-f [Polu and Sutskever, 2020] is the first to apply transformer-based language models to generate single-step action for theorem proving in Metamath.With the ability to generate arbitrary proof text, modern ATPs advance drastically and are capable of proving theorems in complex ITPs like Lean [de Moura et al., 2015] or Isabelle [Paulson, 1994] . The follow-up work PACT [Han et al., 2022] proposes auxiliary pre-training tasks for actiongenerating language models. Polu et al. [2022] uses expert iteration and syntactic data to bootstrap the language model's performance. Most recently, HTPS [Lample et al., 2022] plugs in Monte-Carlo Tree Search [Silver et al., 2016] in this framework and applies an online version of expert iteration. DT-Solver [Wang et al., 2023c] improves HTPS by enabling backtracking during proof search, increasing the robustness. LeanDojo [Yang et al., 2023] retrieve possible premise to assist the generation of a single proof step. Lisa and Thor [Jiang et al., 2021 [Jiang et al., , 2022a] ] tackle theorem proving in Isabelle, which combines traditional ATPs and language models to suggest proof steps, in a neuro-symbolic way. All theorem-proving method introduced above proves theorems step-by-step, with short-sighted heuristics guiding the search to find a correct proof path.Nerual theorem proving with a large language model. Another popular paradigm for automated theorem proving resorts to large pre-trained language models for proof context generation in an in-context-learning manner, without finetuning on formal mathematic datasets. DSP [Jiang et al., 2022b] uses OpenAI Codex LLM [Chen et al., 2021] to generate the entire proofs guided by informal proof. It suffers from hallucination problems with LLM and requires multiple attempts for each problem to ensure correctness. Lyra [Zheng et al., 2023] improves on DSP and uses GPT-4's auto-correction ability to correct previous error attempts. Baldur [First et al., 2023 ] also uses Minerva [Lewkowycz et al., 2022] for whole proof generation using the initial theorem statement.To prevent hallucination, Baldur finetunes a small model that uses error messages to correct the generated faulty proof. MUSTARD [Huang et al., 2024] generates the problem and the solution simultaneously with ChatGPT and uses Lean as a verifier to check the correctness of the generated content.Subgoal-based AI agents. Another domain that is closely related to our paper is subgoal-based AI agents [Wang et al., 2023b ,a, Wei et al., 2023] . These agents decompose the major tasks into small sub-objectives and tackle them one by one. However, most AI agents do not focus on formal mathematic problems, which require compiling the rules of formal environments. LEGO-Prover [Wang et al., 2023b] approaches the theorem-proving problem by decomposing the target into subgoal lemmas and building the proof block by block. However, not all the subgoals can be easily decomposed into lemmas. Many mid-conjectures or subgoals are specific to the current problem and involve shared variables defined in the previous proving process, making them unsuitable for extraction as lemmas, or sometimes impossible to extract as lemmas. kSubS [Czechowski et al., 2024] utilizes a subgoal generation model to produce mid-step proof states and employs a policy model to generate paths in between. However, the generated proof must adhere to the generated proof states, thus the method cannot be applied to more complex real-world datasets like miniF2F. Moreover, the proposed subgoal generator constrains the ability of the policy model to explore freely and find solutions beyond predefined subgoals.Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material?Answer: [Yes] Justification: The research adheres to ethical guidelines by providing transparency in data generation and model training and by making datasets and models available for further research.Guidelines:• The answer NA means that paper does not include experiments requiring code. • Providing as much information as possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted. 
limitations: 
 The proposed method proves theorems recursively by producing a verifiable proof sketch at each level. Although this leads to consistent performance improvements, there is no theoretical guarantee that it will avoid the problem of infinite action space for each proof step generation and the problem of exponential search space with respect to the depth of the search tree. Furthermore, applying the framework of POETRY to other formal languages such as Lean or Coq is straightforward but would require a non-neglectable amount of engineering efforts on some language-specific aspects.Question: Does the paper specify all the training and test details (e.g., data splits, hyperparameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?Answer: [Yes] Justification: The paper specifies the experimental details, including data splits, hyperparameters, model configurations, and evaluation metrics necessary to understand the results in Section 4 and Appendix A.Guidelines:• The answer NA means that the paper does not include experiments.• The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them. • The full details can be provided either with the code, in appendix, or as supplemental material. 
conclusion: 
 In this work, we introduce a novel theorem-proving method, POETRY, which recursively proves the theorem in a level-by-level manner. POETRY searches for a verifiable proof sketch in each level, focusing on proving the target theorem, conjecture, or subgoals in the current level, and utilizes a special sorry tactic to defer detailed proofs of mid-conjectures or subgoals. POETRY introduces a fundamentally different theorem-proving paradigm to the community, preventing short-sighted proof searches that easily go astray. The recursive dataset decomposes long proofs into short proof sketches within a tractable search space. Extensive experiments show that POETRY can indeed improve the pass rates on the miniF2F dataset and PISA test set, and can find longer proofs compared to step-by-step approaches.Status update rules. The status update happens whenever a node finishes its expansion, which adds all the newly created nodes as children. The update will propagate from the expanded node all the way to the root node. A node's status will be marked as FAILED if all the children are FAILED, and a node will be marked as PROVED or HALF-PROVED if any of its children is PROVED or HALF-PROVED. Additionally, when POETRY encounters a sorry edge there exists special update rules. If a node is connected to a PROVED node with a sorry edge, and the next level root node is OPEN, this means the mid-conjectures/subgoals represented by the sorry edge have not been proved, the node will be marked as HALF-PROVED (Figure 2 (a)). As illustrated in Figure 2 (c), if the sub-root node has failed, the original HALFPROVE status of the node will be updated to OPEN. And if the sub-root node is PROVED, the original HALFPROVE status of the node will be marked as PROVED (Figure 2 (f)).Pause and continue of recursive BFS. Terminate conditions. The proof search of the current level will terminate and return to the upperlevel proof search under these scenarios: 1) A complete proof for this level is found, which means all the middle conjectures or subgoals have been proven by the deeper levels of proof searches, recursively. The root node status of the current level proof search is marked as PROVED. 2) For proof search in a level higher than 1, a timeout of 120s has been reached. The root node status will be marked as FAILED. 3) All the nodes in the proof tree have been explored and no proof has been found, the root node status will also be marked as FAILED. Additionally, a global timeout of 600s is added to the entire recursive BFS, ensuring each theorem will not be searched longer than 5 minutes. We can finally obtain complete proof for the target theorem after the first level best-first search return as proved, as shown in Figure 2 (f).Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?Answer: [Yes] Justification: As our beam search generation of GPT is deterministic, no error bars are provided for some results. However, we do confirm on the reproducibility of our method by providing all relevant materials.Guidelines:• The answer NA means that the paper does not include experiments.• The authors should answer "Yes" if the results are accompanied by error bars, confidence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper. • The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions). • The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.) • The assumptions made should be given (e.g., Normally distributed errors).• It should be clear whether the error bar is the standard deviation or the standard error of the mean. Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)? Answer: [NA] Justification: This paper poses no such risks. Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort. 12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected? Answer: [Yes] Justification: All licenses of open source code (LeanDojo) and datasets (AFP) are included in our code. Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper. • We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution. • For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review. 
 
 Appendix: In this work, we use a decoder-only transformer [Devlin et al., 2019] architecture pre-trained with proof-pile v1.1 dataset [Azerbayev et al., 2023] , with 1.3b parameters, 24 layers, 16 attention heads, a hidden dimension of 2048, and a GPT-2 tokenizer with 50400 vocabulary size. We use the alpaca7 codebase for finetuning the model on our recursive dataset. During fine-tuning, we use a global batch size of 256 with 3500 steps of warmup using the AdamW optimizer. We use the cosine scheduling strategy with a maximum learning rate of 3e -4 and a minimum learning rate of 3e -5. Our model is finetuned with 100, 000 steps training budgets and inferences using the lowest validation loss checkpoints with early stopping.For the configuration of recursive best-first search. We use a global timeout of 600 seconds; each proof step has a timeout limit of 10 seconds. The number of samples per expansion e is set to 32, and we use beamsearch decoding strategies to sample proof steps from the language model. The maximum number of steps for expansion is set to 128, and the maximum recursive depth for searching deeper level proof is set to 10. For proof searches other than the first level, a local timeout of 120 seconds is also applied.Machine configuration. We use Nvidia A800 GPU with 80GB of GPU memory for fine-tuning.The training server has 104 CPU cores and 1024GB of CPU memory. The finetuning takes around 100 GPU hours and requires an additional 50 GPU hours to run a single evaluation on the miniF2F test set.In this section, we further discuss the details of our newly extracted PISA dataset, including the dataset statistics and other interesting aspects of the dataset.Dataset Statistics. We follow Jiang et al. [2021 Jiang et al. [ , 2022a] ] and extract data from Isabelle 2022, as well as the corresponding version of the Archive of Formal Proof library. 8 We provide detailed statistics for our fine-tuning dataset. As shown in Table 3 , the newly constructed PISA dataset contains 3.02 million proof steps in the training data. In contrast, the old PISA dataset extracted by LISA [Jiang et al., 2021] only contains 2.49 million proof steps. Another interesting factor of the dataset statistics is the two subsets of the PISA test. The single-level test set contains 2/3 of the problems in the test set, but only 14% of the proof step. In contrast, the multi-level subset contains the remaining 86% proof steps.How recursive the dataset is? As illustrated in Figure 5 (a), the figure shows the histogram of the number of proof levels in a single theorem against the number of theorems. As expected most of the theorem in the training dataset only contains one proof level, which does not require recursive proving at all. This result matches the Pareto principle [Dunford et al., 2021] where the majority of the problems are simple and could be tackled without the recursive proving technique. However, it's the challenging problems that are of most interest to us, where they can test the boundary of our method's actual proving ability.How much does the search space shrink by proving the theorem recursively? As the verified proof sketches might not always be correct due to mid-conjectures/subgoals' proof being skipped by sorry, we can not accurately calculate the search space is shrunk to which extent. However, we can have a lower bound search space calculated using ground truth proof. Figure 5 (b) shows the histogram of the number of proof steps that need to be completed until a proof/proof sketch can pass the verification of Isabelle against the number of these proofs. For conventional step-by-step approaches, the proof is the original one, and for POETRY, the proof is a proof sketch. We can observe that the proof length of POETRY is substantially shifted towards a shorter proof length per proof. On average, there are 3.3 proof steps for POETRY and 12.7 proof steps for step-by-step baseline per proof. And that would be 32 9.4 times smaller the search space per proof on average with e = 32.Comparison with LLM-based approaches. For a more comprehensive view of the relationship between POETRY and other state-of-the-art methods, we include Table 4 to illustrate the performance in miniF2F using the large language model like ChatGPT [OpenAI, 2023] . 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.Input and output comparison for GPT-f Baseline and POETRY. We also provide a table illustrating the detailed input and output pair constructed for language model training. This is the same theorem example shown in Figure 2 . 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 comes from the data curation process, the novel recursive BFS, and the recursive proving methodology itself. We will include this table in our paper for better illustration.Failure cases of POETRY We provide additional failure cases of POETRY to better understand the limitations of current recursive proving approaches. Compared to the GPT-f Baseline, a notable issue with the recursive framework in POETRY stems from its greedy exploration strategy. POETRY aggressively explores deeper-level proofs as soon as it finds a valid proof sketch, yet sometimes fixes n :: nat assumes h0: "9 \<le> n" shows "\<exists>x::nat. (real_of_nat x)^2 = (fact (n + 2) -fact (n + 1)) / fact n" prooffrom assms show?thesis unfolding power2_eq_square by (intro exI[of _ "n + 1"]) (auto simp: field_simps) qed theorem mathd_algebra_422: fixes x :: real and \<sigma>::"real \<Rightarrow> real" assumes "bij \<sigma>" and \<sigma>:"\<forall> x. \<sigma> x = 5 * x -12" and "\<sigma> (x + 1) = (Hilbert_Choice.inv \<sigma>) x" shows "x = 47 / 24" prooffrom assms have "bij \<sigma>" by (auto intro!: bijI simp: bij_def) show?thesis proof (rule ccontr) assume "x \<noteq> 47/24" thus False using assms by (subst (asm) bij_inv_eq_iff) auto qed qed theorem mathd_algebra_441: show "rev_map g (u \<cdot> v) = rev_map g u \<cdot> rev_map g v" for u v proof (simp add: rev_map_def) show "rev (g (rev v \<cdot> rev u)) = rev (g (rev u)) \<cdot> rev (g (rev v))" using swap by (simp add: g.morph) qed show "rev_map h (u \<cdot> v) = rev_map h u \<cdot> rev_map h v" for u v proof (simp add: rev_map_def)show "rev (h (rev v \<cdot> rev u)) = rev (h (rev u)) \<cdot> rev (h (rev v))" using swap by ( indRelRSTPO_impl_SRel_and_TRel_weakly_reflect_barbs: fixes SRel :: "('procS \<times> 'procS) set" and TRel :: "('procT \<times> 'procT) set" assumes reflection: "rel_weakly_reflects_barbs (indRelRSTPO SRel TRel) ( STCalWB SWB TWB)" shows "rel_weakly_reflects_barbs SRel SWB" and "rel_weakly_reflects_barbs TRel TWB" proofhave "rel_weakly_reflects_barbs SRel SWB \<and> rel_weakly_reflects_barbs TRel TWB" proof (rule conjI)show "rel_weakly_reflects_barbs SRel SWB" using reflection rel_with_source_impl_SRel_weakly_reflects_barbs[where Rel="indRelRSTPO SRel TRel" and SRel="SRel"] by (simp add: indRelRSTPO.source[where SRel="SRel" and TRel="TRel"]) show "rel_weakly_reflects_barbs TRel TWB" using reflection rel_with_target_impl_TRel_weakly_reflects_barbs[where Rel="indRelRSTPO SRel TRel" and TRel="TRel"] by (simp add: indRelRSTPO.target[where SRel="SRel" and TRel="TRel"]) qed thus "rel_weakly_reflects_barbs SRel SWB" and "rel_weakly_reflects_barbs TRel TWB" by simp_all+ qed Answer: [NA] Justification: The paper does not include theoretical results or formal proofs; it focuses on novel nerual theorem proving methods that tries to prove theorem recursivly. Guidelines:• The answer NA means that the paper does not include theoretical results.• All the theorems, formulas, and proofs in the paper should be numbered and crossreferenced. • All assumptions should be clearly stated or referenced in the statement of any theorems. • The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition. • Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material. • Theorems and Lemmas that the proof relies upon should be properly referenced.HTPS[Lample et al., 2022] achieve 57% and41% on miniF2F valid and test set for pass@64, but they didn't provide the pass@1 results. Additionally, the model is fine-tuned on the miniF2F-valid with online training, which is not a fair comparison with POETRY.4 https://artofproblemsolving.com/wiki/index.php?title=AIME_Problems_and_SolutionsThe performance of methods in Lean and Isabelle cannot be directly compared, as the training data differ fundamentally in coding language or data volume. However, despite these differences, the high-level concepts behind these approaches share significant similarities.https://github.com/tatsu-lab/stanford_alpacaThe original dataset is extracted with Isabelle 2021, resulting in x fewer theorems and x fewer lines of state action pair. 


Decision: This paper introduces POETRY, a new method to prove theorems recursively in a 
a top-down fashion similar to humans, proving a conjecture only if it is actually relevant 
to the best overall proof being explored. The best-first search on proof sketches is guided 
by a language model fine-tuned on proof sketches. The ideas, although not revolutionary, appear to
be novel in this domain, the paper is very well written and the experiments show a significant
improvement on the state of the art.

One reviewer inscreased their score from borderline reject to borderline accept after the author-reviewer discussion.

Reviews: review: paper_summary: paper_summary: This paper introduces POETRY, a new method to prove theorems recursively. The key ideas are to use a modified best first search algorithm for the search part, and a *sorry* tactic for assumptions at the current level (to be proven later). The authors provide the intuition that this recursive structure allows POETRY to prove theorems in a top-down fashion similar to humans, getting into the details of proving a conjecture only if it is actually relevant to the best overall proof being explored. The authors conduct experiments with two standard benchmarks, showing notable improvements over baselines and SOTA search-based methods (but not LEGO-Prover etc. which rely on substantially larger general purpose LLMs).
strength_weakness: strength_weakness: Not being very familiar with the area, I am surprised none of the existing SOTA methods use a similar recursive, top-down search of in theorem proving. I will have to defer to other, more knowledgeable reviewers for assessing novelty of the present work.

I did not fully follow why a *novel* recursive best-first search strategy is needed here. The description of this section (3.2) can probably use some clarification. E.g., why could one not account for the conjecture's level in the utility of the conjecture, and thus implicity enforce level-by-level proof search? On the same note, could the authors comment on the relationship between their proposed recursive best-first search and a combination of standard breadth-first search (i.e., staying within a level) and best-first search (i.e., preferring to explore the most promising node first)?

Just for completeness, it would have been good to know how well very large LLM based methods, such as LEGO-Prover, do on the considered benchmarks.
questions: questions: Please see weaknesses section above.
limitations: limitations: Yes
paper_summary: paper_summary: The authors introduce a method called POETRY (proving theorems recursively) for constructing formal proofs in Isabelle/HOL. POETRY performs best-first search on proof sketches guided by a language model fine-tuned on proof sketches. POETRY outperforms other algorithms guided by language models that prove theorems step-by-step. POETRY also outperforms other methods that integrate automated theorem provers and language models.
strength_weakness: strength_weakness: 1. It seems to me that the real reason for the success of POETRY is not the algorithm per say, but the data curation to construct proof sketches. In this vein, it would be instructive to have a before sorry and after having sorry to illustrate how the dataset is constructed. 
2. There should be more context explaining how to compare the Lean results against Isabelle/HOL. These are two different formal systems, with different proof methodologies.
3. More details on success cases and failure cases would help understanding the pros and cons of the approach taken in POETRY. For instance, are there certain kinds of problems that POETRY performs well on, e.g., geometry problems? How does POETRY perform when existentials need to be instantiated? Is it the case that POETRY can prove the same theorems as previous step-by-step approaches and can additionally prove more theorems that are longer, or do the approaches prove different short theorems?
questions: questions: 1. The distinction between a proof sketch and the decomposition of a theorem into a tree of conjectures needs to be addressed. Is there any difference?
2. In your training procedure, do you fine-tune on any theorems in the miniF2F dataset?
limitations: limitations: Yes.
paper_summary: paper_summary: This paper proposes POETRY, a method for formal theorem proving using language models by training the model to iteratively decompose the problem into sketches, recursively. The authors focus on Isabelle. At each step, POETRY takes a proof state and goal and predicts either a formal sketch (a proof using sorry at each step), or a ground proof step (e.g. 'by ...') that requires no recursion. These intermediate states are visited within best-first search, where the score of a node is given by the log-probability of all predictions made so far to get to that node. Intuitively, POETRY works by recursively generating lower level steps / sketches, until finding a complete proof, getting feedback from the formal environment at each step. To train the LM, the authors introduce a simple method to decompose existing Isabelle proofs from the AFP as if they had been generated by this recursive proof generation process. Experiments on minif2f show improvements on top of GPT-f and a version of Thor without Sledgehammer.
strength_weakness: strength_weakness: The choice of baselines (for Table 1) seems a bit convoluted. In particular, I don't really understand why use Thor without sledgehammer. The main point of Thor is to learn when to use hammers in proofs. Removing this makes the model much more similar to the GPT-f baseline.

As for the choice of pass@1, even though POETRY only makes a single prediction at the end, it gets feedback from Isabelle at each node in its tree. So that doesn't seem like a fair comparison either, if POETRY makes many intermediate predictions and calls Isabelle during its search, whereas GPT-f and Thor w/o sledgehammer seem to only produce and test a single prediction. It might be more fair to match the methods based on some other metric, like number of tokens generated, or number of calls to Isabelle (whichever seems to be the most significant bottleneck).

The question of "Can POETRY find longer proof?" is a bit ill posed as is. It would be possible for a method to find very long proofs that do not *need* to be long, and do better on this analysis without really being able to prove more complex theorems. What I think the authors are trying to show here is that POETRY can solve harder problems, estimating hardness by looking at proof length. For this, you might want to compare success rate based on the length of the ground truth proof: perhaps the baselines perform very poorly on theorems where the human proof is longer, whereas POETRY might have a better success rate. Another option is to show that either POETRY generates proofs of similar length to the ground truth proof (so, when POETRY generates long proofs, you'd estimate that the ground truth proof would also be long), or that it generates proofs of similar length to the baselines in cases where they all manage to prove a theorem. Any of these would help show that this result is not trivial.
questions: questions: * Is an intermediate sketch valid (accepted by Isabelle) as long as it's syntactically correct and the last step shows the thesis? Or do you manage to get richer feedback besides that the last step declares to show the thesis?
* For problems that both POETRY and the GPT-f baseline solve, does POETRY tend to generate longer proofs?
* As for the relationship with LEGO-Prover, you mention that in some cases it is impossible to decompose a proof into lemmas, but still possible to decompose it into sketches recursively. Do you have an example?
* What exactly is the search algorithm used in the Thor w/o sledgehammer and GPT-f baselines? It is a one-shot prediction? Or do you use the (also best-first) search method described in the original GPT-f paper?
* What is Thor without sledgehammer? It sounds like a different thing other than Thor.
* I'm confused by what Figure 5 is trying to show. Fundamentally, reorganizing a proof into sketches shouldn't change its inherent complexity (e.g., the atomic proof steps). Is this just comparing the full proof length against the number of steps in the top-level sketch (without considering the deeper sketches recursively)? If you were to consider the steps in the deeper sketches recursively, I'm assuming you would not expect to see a reduction (if you do, where would that come from? do you have an example?)
limitations: limitations: Yes, adequately addressed.
paper_summary: paper_summary: This paper designs a novel hierarchical search algorithm (POETRY) for generating formal proofs with large language models step-by-step. In particular, POETRY will first search for proof steps with proof level 0 (these steps typically correspond to subgoals in the proof), and check the correctness of the level 0 proofs by assuming that all the subgoals can be proved. If and only if the level 0 proofs are correct, POETRY will recursively search for proofs to each of the proposed subgoals. Compared with the baseline best-first search methods with the same compute, POETRY significantly improves the pass@1 succ rate on both miniF2F valid and test set, as well as the PISA test set.
strength_weakness: strength_weakness: -	From Table 1, it seems to me that the improvement from the search algorithm is less significant than the beam search. A drawback of the beam search method is that the algorithm becomes deterministic, meaning that generating more samples per theorem does not improve its performance. Since this paper only shows pass@1 results, it is unclear how the POETRY algorithm scales with more computing resources.
questions: questions: -	In the example shown in Figure 4, it seems to me that Path 1 is quite similar to the first part of the proof found by POETRY. Can the authors elaborate on why is the GPT-f baseline tries to utilize a more complex way to prove the first property?
limitations: limitations: The authors adequately addressed the limitations and potential negative societal impact.

Comments: title: Response to Reviewer BhWC
More explanation on `show ?thesis`
Thank you for your response
Waiting for further discussion
Waiting for further discussion
comment: 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.

| Category | GPT-f Baseline | POETRY |
| -------- | -------- | -------- |
| **Graph Theory**     | 38.7%     | **41.9%**  |
| **Cryptography**     | 65.2%     | **69.5%** |
| **Logic**                    | 48.1%        | **53.2%**    |
| **Linear Algebra**           | 39.3%        | 39.3%        |
| **Set Theory**               | 54.5%        | **59.1%**    |
| **Computation Theory**       | 51.7%        | 51.7%        |
| **Probability and Statistics**| 52.2%       | **65.2%**    |
| **Differential Equations**   | 52.3%        | 52.3%        |
| **Combinatorics**            | 55.0%        | **62.5%**    |
| **Geometry**                 | 46.7%        | **50.0%**    |
| **Abstract Algebra**         | 41.5%        | **50.9%**    |
| **Algebraic Geometry**       | 53.1%        | **61.2%**    |
| **Algorithms and Data Structures** | 59.1%   | **63.6%**    |
| **Functional Analysis**      | **46.7%**    | 40.0%        |
| **Number Theory**            | 35.0%        | **45.0%**    |
| **Miscellaneous**            | **50.5%**        | 50.0%    |


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

Thank you for your prompt reply and for recognizing the value of our work. We will include all the new results in our paper.

Regarding the example you mentioned, POETRY does validate the sketch, and the usefulness of the skipped conjectures was not tested. We are unable to extract additional semantic information from the environment to assist in this situation.

We acknowledge this problem during the development of POETRY, and to address it, POETRY employs the “last unsolved sorry” strategy during proof search (as detailed in Appendix A.1). This strategy focuses on the final sorry in the proof sketch (i.e., the sorry in `show ?thesis sorry`), allowing for quicker validation of the proposed conjectures by first concentrating on the final incomplete part of the proof.

Another potential approach could involve explicitly disallowing the use of sorry after `show ?thesis` and requiring the model to find a complete proof within the `show ?thesis` block. However, this is acceptable for proofs that can be accomplished with a single level of `show ?thesis` (i.e., `show ?thesis by ...`). For proofs requiring more complex structural reasoning within the `show ?thesis` part, this method would reduce POETRY to a step-by-step approach and fail to leverage the structural reasoning capabilities that POETRY is designed to utilize.

Given the current constraints in extracting semantic information from the environment, beyond the “last sorry” strategy, a promising direction might involve using neural-based value functions as assistants to help distinguish between useful and less useful sketches. We are excited to explore this aspect in our future work.

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 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.
I thank the authors for the clarifications on the method, as well as the new analyses. I do think these clarify the results, and have alleviated most of my concerns. I have raised my score assuming the new results will make it to the paper: I think the method contributes a simple but neat idea for the problem.

About q1. (condition of a sketch being valid), I think your answer confirms my understanding, but I'd still like to clarify just because I'm interested (and this would also be helpful to clarify in the paper). Since sorry can prove any goal, my question was whether the semantic validation that Isabelle is capable of doing is essentially just that the sketch ends by concluding the thesis. For instance, this would be a toy example based on the LEGO-Prover example above:

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 -
have c0: "x = 0" by sorry
then show ?thesis by sorry
qed

I'm understanding this would be marked by Isabelle as a valid sketch, or is there something else I'm missing?

What I wanted to understand is exactly how much semantic feedback you can get at the sketch level, since sorry can prove anything. Your results show that structuring the proof search process in this way is helpful overall, but I'm just trying to understand whether it's more of a helpful bias to the LLM vs how much extra feedback it actually enables you to extract from the environment.
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
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