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 2024 poster (2024)
Keywords: Nerual Theorem Proving
Language Model
Primary area: machine_learning_for_other_sciences_and_fields

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.

Proving Theorems Recursively
Haiming Wang
Huajian Xin
Zhengying Liu
Wenda Li
Yinya Huang* Jianqiao Lu Zhicheng Yang"
Jing Tang Jian Yin!
Zhenguo Li Xiaodan Liangl
Sun Yat-sen University Huawei Noahs Ark Lab University of Edinburgh CityU *HKU "HKUST (Guangzhou) 'HKUST *Pengcheng Laboratory (wanghm39, xinhj. issjyin| @ 2email2.ssu.ediil
wli ed.ac.uk, jqlu gglu@es.hkuu hkku.k (liuzhengying2, Li.hheguu @ @huawei.com, Siny..huangee liang@har hotmaiil.com jingtang@ust.l ust.hk (yangzhch6, xdliang328) @ gmail.com
Abstract
Recent advances in automated theorem proving leverages language models to ex- plore 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 sub- goals, preventing us from finding longer proofs. To address this challenge, we propose POETRY (PrOvE Theorems RecursivelY), which proves theorems in recursive, level-by-Level manner in the Isabelle theorem prover. Unlike previ- step-by-step methods, POETRY searches for 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 placed by 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 deeper levels. Experiments and significant performance gains are observed in our POETRY approach over Llate-of-the-ae methods. POETRY on miniF2F achieves an average proving suc- cess rate improvement of 5.1%. Moreover, we observe a substantial increase in the maximum proof length found by POETRY, from 10 26.
conducted on the miniF2F and PISA datasets
Introduction
Neural theorem proving has made significant strides in recent years [Polu and Sutskever, 2020, Han al., 2022, Polu al., 2022, Wang et al., 2023c, Jiang al., 2022a, 2021, 2022b, Wang 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 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 al., 2022, Jiang et al., 2022a].
As shown in Figure ((a), search-based neural theorem proving methods begin with a theorem state- ment to prove. A formal mathematic environment like Isabelle will first process the theorem state- ment 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
These authors contributed equally. Corresponding authors
htttps://github.. cote:/hhbb.oooeooooeooeeeeeeeeee http://wii////eeeeeeeeeeeeee
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

Proof Level
Proof Level 2
Proof Level 3
the group) pnt.pox.pow:
LOST Teme
1L00: "n O' Pthosta
assure "In 2 0' Fthesss
aosurmes "x carrtor
theoron( in group) int_pooc_po:
proof (cases)
assumes "x cartier O"
re.ee: thus ?theo Ea darte
usling rugA nst_poo.ppw fnt_ pot_ppo_
shows *(x [+] (n oo intt) [-) (m so
shows *(x [+] (n ot imt) (+) (m
Ent) Wingeee
pooof (cases)
you so assuno ruge: "n 8" thus Pthesis
Snt)"
2: knt) F. [1] (n xin int)"
pooof (cases)
200
jassure 1t:
with go show Pthesia (oorry
ansuum Itlt: 1' i 8*
nige show Pthesis apply (simp add: in- t_pow_daf2)
2/2.2011 essesaa biste
110 aiing the d goid saagud)
aessume r-ge:
by (netis asons milt rá- nus_right ruge nwt rwT__poM_row)
proof (casee)
thus 7theois (bor1y
asssmm ru1:: * n > D' ?thesis
10 gosl 12 subeuaaalo 2. a assume Tuge: 'tr 2 6* thus Ptheese auspat)............
Sacceapa
naxt
113 gosd (1 suppaat L. Ba D4
proof (cases)
using nuge not. pow. paw
dasume le: * n Masii Dan
assure ruge: "n 0'
have "inv [*] (not
r. poo def2
thus 2thei la siatt//
have *inv 1-] [not + not
nat (- n)) iime x [+] not
fu solve gul (wr
(- n)) inv [*] not (- (n
(n nly'
by (metis (ypel))
20o Zhrests sorrye
ruge nult.ninnarrghh))
suggeial
>>>
...
(a) Step-by-step Proof
(b) Recursive Proof
Comparison between the step-by-step proof and the recursive proof. (a) A step-by-step proving approach ignores the hierarchical structure inherent in the proof, treating it merely as sequence of proof steps. The proof cannot be verified 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 altempts 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.
Figure 1:
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-prodee bog-robbbbiitty 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 PUCT score that combines both [Wang et al., 2023c, Lample et al., 2022] (in MCTS). These heuristics assess the plausibility or potential value of 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 accu- rate 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 proof sketch, which is defined to be a verifiable proof outline with the detailed proof of the middle con- jecture 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 prove the intermediate conjectures that re- main unresolved, also in a recursive, level-by-level manner. This procedure persists until every sorry keyword is substituted with 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= 6 + a, false conjecture such as a = 6 might be used. However, when actually attempting to prove a = b. we would never be able find valid proof at the next level. If false proof sketch is generated and POETRY fails to find the proof for the middle conjecture, it will continue its search to identify 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 sig- nificantly 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-arts Additionally, our ablation study shows that with recursive theorem proving, we obtain 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 step- by-step proving methods, the maximum proof length increases from 10 to 26 compared to the step- sy-step baseline in the PISA dataset.
2 Preliminary
2.1 Formal Mathematic Enviroments
We choose Isabelle [Paulson, 1994] as our formal environment, It is widely used for formal verifica- tion purposes in academia and industry [Gesellensetter et al., 2008, Klein et al., 2009, Zhang et al., 2024]. 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 ((a), Isabelle processes each proof step (or tactic) and pro- vides 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 af- ter applying the step. In the Isabelle theorem prover, the proof level indicates the depth within structured proof. This level increases with commands like have, obtain, and show, which introduce new subgoals or conjectures in the proof. Conversely, 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 spe- cific 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 addi- tional engineering effort to accommodate the proving strategies. These environments also provide mechanisms to temporarily skip parts of proofs, similar Isabelle's sorry tactic, such Lean's s sorry, and Coq's Admitted. We will leave the extension of POETRY to other formal environments for future work.
2.2 Search-Based Neural Theorem Proving
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 trained using data formatted as follows:
INPUT: CONTEXT $ (context) GOAL $ (proof state) STEP
OUTPUT: $ (proof step)
where 8(-) represents the substitution operation, and context denotes the preceding proof steps leading to the current proof state. At test time, GPT-f employs best-first search strategy to identify sequence proof steps that solve the problem. Specifically, The proof search algorithm constructs a tree-like search structure, where each node represents 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 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.
3

---

3 Methodology
Algorithm 1 Core data curation process
I: function
inder)
proofLines: a list of pairs of the format "(proofStep, proofLevel)"
3: index: the starting index in proofLines for processing
4:
currentSketch, allSketches + empty list, empty list
5:
-. .currentLeeed &- proofLines (indee)
b Obtain the current proof level being extracted
6: proofLevel curventLevel
while proofLevel 2 currentLevel do b Extraction ends after the proof level drops below the current
proof level
8:
proofStep, proofLevel +- proofLines neatLevel < proofLines (indez +
9:
10:
if neatLevel = currentLevel then (ureatSheettt.appeddmooo//f
11:
12:
indez + inder +
13:
else if nertLevel > currenlLevel then
14:
Replace the next level proof with sorry deeperSketches, index <- DXTTRACTRROFSSEETCHHHH prort index + 1)
* sorr")
15:
16:
allSketches extend deeperSkecches) end
17:
18:
end while
19:
allSketches app.eeddsppppdd(((( curventSketch)
20:
return aliSketches, indez
21:
end function
3.1 Recursive Data Construction
Proof sketch extraction. As illustrated in Figure 1(b), to prepare recursive proving data, need to split theorems into blocks proof sketches. Each proof sketch focuses solely on the target theorem, conjectures, subgoals, with the detailed proof of intermediate conjectures by the sorry tactic. Algorithm presents the pseudocode for the sketch data extraction process. POETRY initially inputs the complete theorem text into Isabelle, which parses it into 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 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 ExtractProofSktth 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 (bb).
subgoals replaced
Training data construction. Following the extraction of proof sketches, POETRY follows Jiang al. [2022a] and uses PISA, interactive environment built top of Isabelle, extract proof states for each proof step. Subsequently, the proof states and proof steps are reformatted into lines in Equation and used training examples 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 have "x language model generates proof steps at the current level and postpones higher-level proofs using 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 conjecture subgoal. This approach ensures that deep-level proofs are deferred correctly.
2x" sorry. Merging the sorry tactic is crucial ensure that the

---

Leve 1 BES
(b) Deeper Invel 2 subooal RPS
(c) Rarkpragacoto stale
(d) Continue search on Lovel
Terna/ theoren
subgon]
Lerma// theoren
Bubgosl
Termar theorer
subgoai
Lonna/ theoxan
HP
HP
theoren LI
conjecturo SERON
subgoal
Lomma thoorem ME
PROVED
HALF-PROVED
FAILED
nornal edge
serry edge
proof level
Desper level coniecture
Backpepugate vuccesfulll proved
Figure 2: A walkthrough example of recursive BFS. Each node in the proof tree is a proof state and each edge is a proof step. (a) The proof search begins by finding the proof sketch the first level using BFS. The search paused upon identifying a successful proof path, marked with and HP nodes. This proof path contains sorry edge, indicating that it includes skipped conjectures or subgoals that must be addressed in the next level. (b) Recursive BFS enters the next level of proof search to attempt to prove the skipped subgoal from the first level. Unfortunately. the proof search for this subgoal fails due to lack of valid nodes to explore, and the search returns the first level. (c) After the failed attempt prove the subgoal, the previously established proaf path at the first level becomes invalid. Consequently, we hackpropagate the failure from the second level's root node up to the first-level root node, updating all the HP nodes to an O node. (d) At the first level, with the status set to open for searching proofs, we continued to explore new proof paths. Fortunately, we discovered another proof path. However. this path also contained sorry edge with a skipped conjecture that needs be proved at the next level. (e) Similar to (b), recursive BFS proceeds to the next level to search for proof for the previously skipped conjecture. It successfully finds a proof path without any "sorry" edges (denoted as P nodes), indicating that the conjecture has been proven successfully without any skipped intermediate conjectures or subgoals in the proof path. (f) After finding the sub-level proof, the recursive BFS returns the first level and backpropagates the PROVED message the root, completing the proof.
3.2 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 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, 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, 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.
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 proof state, once tactic contains "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 score of 0 and will not be selected in the current- level 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
child nodes stemming from it are unable to establish 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 complete proof sketch but contains special sorry edges with unsolved next-level subgoal or mid-conjecture. Only after all the mid- conjectures 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 2f)).
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
5

---

search space from expanding exponentially as the proof length increases. This approach allows search-based methods find more challenging and longer proofs without necessitating highly performant value function model to guide the proof search procedure.
4 Experiments
4.1
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 smnt 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 700M model pre-trained on The Pile [Gao et al., 2020]. GPT-f Baseline also uses 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 theorem- proving methods. PACT [Han al.. 2022]. FMSCL [Polu et al., 2022], Leandojo [Yang, al., 2023], and COPRA [Thakur et al., 2024] are works focusing on the Lean formal environment. Con- trastively, Thor [Jiang et al., 2022a], Thor with expert iteration on formafoodd data [Wu et al., 2022] and Thor Magnushammer [Mikula 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 al., 2022b], Lyra [Zheng et al., 2023], or LEGO-Prover [Wang et al., 2023b]. These approaches em- ploy general-purpose large language models (LLMs), such as ChatGPT 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 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 1, attempting to prove the theorem once for each problem.
Evaluation datasets and metrics. For evaluation, we use two datasets, the miniF2F dataset [Zheng 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 [[endrycks et al., 2021], to more challenging problems found in the AIME 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 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@) I as the evaluation metric, where each
*HTP [Lample al., 2022] achieve 57% and 41% 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 Finii2F-valid with online training, which is not fair comparison with POETRY. ttckps://artofproblleeeo
http:///a//dddo.ppptttttteooo-// wwpptitlee Problems, and mnd_ttonioons www.////.////.eeeeeeeoceeeeeeeee

---

Table 1: Comparing with baseline. The table displays the pass@1 success rates of the baselines and POETRY, The highest success rates for each set are highlighted in hold.
Success rate
miniF2F-valid
minif22-test
PISA
single-level
multi-level
Thor w/o sledgehammer
25.0%
24.2%
39.0%
GPT-f Baseline
39.3%
37.3%
49.0%
65.5%
11.1%
with sampling decoding
30.3%
31.5%
43.2%
57.8%
9.8%
POETRY
42.2%
42.2%
49.7%
65.4%
13.6%
Table 2:
Comparing with state-of-the-art search-based methods the miniF2F dataset. The table displays the pass [ass@] success rates of previous works and POETRY. The highest success rates for each highlighted bold."
Success rate
environment
miniF2F-valid
miniF2F-test
Baselines
PACT [Han et al., 2022]
Lean
23.9%
24.6%
Leandojo (Yang et al., 2023]
Lean
26.5%
FMSCL [Polu et al., 2022]
Lean
33.6%
29.6%
COPRA [Thakur al., 2024]
Lean
30.7%
Thor [Jiang et al., 2022a]
Isabelle
28.3%
29.9%
Thor expert iteration [Wu al., 2022]
Isabelle
37.3%
35.2%
Thor Magnushammer [Mikula et al., 2023]
Isabelle
36.9%
37.3%
Ours
POETRY
Isabelle
42.2%
42.2%
theorem in the dataset is proved once by POETRY, Then we calculate the proportion of the theorems being successfully proven.
4.2
Main Results
Comparison with language model-only baselines. As shown 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, Baseline with sampling drops by 6.8% compared with the beam-search version. This is because the beam-search decoding method guaranteed to produce 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.
observe the performance of the GPT-f
Compared with the GPT-f Baseline, POETRY outperforms GPT-f Basclines by 3.9% the miniF2F dataset on average, and 0.7% 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 the GPT-f Baseline when encountering proofs with only one level, resulting in similar performance within the single-level subset. In contrast, POETRY achieves 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.
observe the benefit of the recursive theorem proving.
'The performance 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.
7

---

Proof length histogram on minif
Proof length histogram on PISA
2214
method cert Baschrre
12
method GPTT sascline
Prodiom counts
Protnem counts
121
33
17
16
Proof length
Proof length
(b)
P5AA
Single-level
Multi-level
method ROCTEY
othhoo od POTTTO
107
method POETRY
Splved counts
Salver Dovee.congg counte
001
101
Ground
Ground
(c)
(d)
(e)
Figure 3: (b)&(b) Proof length comparison between POETRY and GPT-f Baseline. The y-axis is shown in the log scale. (a) Proof length's 's histogram of found proof in miniF2F dataset. most of the proof found is within 3 steps long, especially for GPT-f Baselines, but POETRY managed find longer proof up 18 proof steps in one proof. (h) Proof length's 's histogram of found proof in the PISA dataset. POETRY discovers lot more proofs with longer proof lengths. (c), (d) and (e) Number problems solved by GPT- Baseline and POETRY based on the length of the ground truth proofs.
(a) The distribution in the entire PISA dataset. POETRY has a clear tendency to solve problems with longer ground truth proofs. (b) 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 the multi-level subset. POETRY has 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, well 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+-Manuusaamma 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 orthogonal to these baseline approaches. It can fur- ther improved with the use of Sledgehammer or Magnushammer [Jiang et al., 2022a, Mikula et al., 2023], running expert iteration on the training set [Polu et al., 2022, Wu 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.
4.3 Analysis
Can POETRY find longer proof? Figure (a) and (b) compares the proof length of proofs discov- ered 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 Base- line. The average proof length increases from 1.47 to 2. 13 in the mini 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 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,

---

Lemma (in UP_cring) n_mult_elosed: assunes "f carrier P
lenna UP_oring) n-mult_closed: assumes "f carzier P showe "n_muit cacrier, PM proof UP-car_nent[of "deg ['))
shows "n_mult
carrier P"
(rule UP_car _ "deg (']) show "An, deg R f n n_mult f
fix n
assune A: "deg R. c.n"
unfolding __nulttdaf
using ssems
Path 1
show "n.nult J
unfolding n_nulr_def proof
unfolding P_der
by (einp add: uP_csr__meete _2)_m))((()
X Timmout after 500 seconds
show "An. n_mult n corrier
using asans
[ruef(rule [P_ *deg [n]) show "An. R. nulu f
unfolding n_mult_dee
by (sinp add: cfe_closed)
Proof level
Path 2
X NNever explored
qed
(a)
(b)
Figure 4: Case comparison between POETRY and GPT-f Baseline. (a) Recursive proof found by POETRY in 71.2 seconds, the proof contains two proof levels. (b) Failure-proof paths found by the GPT-f Baseline. GPT-f Baseline failed to find proof due to timcout after 600 seconds. We seleet two different failure proof paths found by GPT-f Baseline.
only progressing to deeper levels when it identifies 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 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 (c)). From these figures, it is evident that POETRY shows a marked tendency 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 s_mult__ cl osed states that if a polynomial I belongs the carrier set of polynomials P. then the operation n_ n_mult applied to ʃ 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 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' must be zero. (ii) Closure under carrier (the second show statement in Line 7): For any integer n, the result n mult fn 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 timcout. 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 timcout occurred. From this case, we can that by recursively proving the theorem, the proof with 11 steps is broken down into 3 proof sketches with 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.
5 Related Works
Search-based neural theorem proving. Our work is closely related to prior work on step-by- step search-based nerual theorem proving. GPT-f [Polu and Sutskever, 2020] 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 capa- ble 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- vre-training tasks for action- generating language models. Polu 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, 2022a] tackle theorem prov- ing in Isabelle, which combines traditional ATPs and language models to suggest proof steps, in a neuro-symbolic way. All theorem prrvving method introduced above proves theorems step-by hep-by-step. with sighte 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-learinng manner, without finetuning on formal mathematic datasets. DSP [Jiang et al., 2022b] uses OpenAl Codex LLM [Chen al., 2021] to generate the entire proofs guided by in- formal 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 small model that uses error messages to correct the generated faulty proof. MUSTARD [Huang et al., 2024] generates the problem and the solution simultancously 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 Al 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 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 sub- goal lemmas and building the proof block by block. However, not all the subgoals can be easily decomposed into lemmas. Many mijeconjestures and involve shared variables defined in the previous proving process, making them unsuitable for ex- traction lemmas, sometimes impossible to extract 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.
subgoals are specific to the current problem
6 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 some language-specific aspects.
7 Conclusion
In this work, we introduce novel theorem-proving method, POETRY, which recursively proves the theorem in level-by-level manner. POETRY searches for 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 sigrt-sighted proof searches that easily go astray. The recursive dataset decomposes long proofs into short proof sketches within 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.
10

---

Acknowledgements
This work is supported in part by the Major Key Project of PCL (No. PCL2024A04), National Natural Science Foundation of China Technology Plan Project of Guangzhou City0023B01J000122222222 W0004, National Science and Technology Major Project (2020AA000)9704)) National Science Foundation of China Grant No. 62476293, Guangdong Outstanding Youth Fund (Grant No. 1151500006)), Shenzhen Science and Technology Program (Grant No. GJH77202209131226600000 Nansha Key RD Program under Grant No.202220014.
Research Foundation of Science and
References
Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad. Proofnet: Autoformalizing and formally proving undergraduate--ever mathematics, 2023. 6, 14
B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin-Mohring. A. Saibi, and B. Werner. The Coq Proof Assistant Reference Manual Version 6.1. report, INRIA, May 1997. URL https: //hal, inrin. fr/ -00ia-0006996.. Pages: 214.
M. Chen, J. Tworek, H. Jun, Q Yuan, H. P. de Oliveira Pinto, Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, A. Ray, R. Puri, G. Krueger, M. Petrov, H. Khlaaf, G. Sastry, P. Mishkin, B. Chan, Gray, N. Ryder. M. Pavlov, A. Power, Kaiser, M. Bavarian, C. Winter, P. Tillet, F. P. Such, D. Cummings, M. Plappert, F. Chantzis, E. Barnes, A. Herbert- Rerbert-Voss. W. H. Guss,
A. Nichol, A. Paino, N. Tezak, J. Tang, Babuschkin, S. Balaji, S. Jain, W. Saunders, C. Hesse, A. N. Carr, J. Leike, J. Achiam, V. Misra, E. Morikawa, A. Radford, M. Knight, M. Brundage, M. Murati, K. Mayer, P. Welinder, B. McGrew, D. Amodei, S. McCandlish, I. Sutskever, and W. Zaremba. Evaluating large language models trained code. CoRR, abs/2107.03374, 2021.
URL https:://///. /tttapp::///xxiiii /arxxiiv../ org/ abs abs/2107 03374. 10
K. Czechowski, Odrzygód, M. Zbysiski, M. Zawalski, K. Olejnik, Y. Wu, ukasz Kuciski, and
P. Mio. Subgoal search for complex reasoning tasks, 2024. 10
R. B. Daniel Selsam, Kevin Buzzard. Imo grand challenge. 2019. URL https:// imo- mmo-grand-challenn waw.aalleengggihbb.......
L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The Lean Theorem Prover (System Description). In A. P. Felty and A. Middeldorp, editors, Automated Deduction CADE- 25. Lecture Notes in Computer Science, pages 378-388, Cham, 2015. Springer International Publishing. ISBN 978-3-319-21401-6 doi: 10. 00010007978-3-31-211000
3,
J. Devlin, M. Chang. K. Lee, and K. Toutanova, BERT: pre-training of deep bidirectional transform- ers for language understanding. In J. Burstein, C. Doran, and T. Solorio, editors, Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Lin- guistics: Human Language Technologies, MAACL-HLT 2019, Minneapolis, MN. USA, June 2-7, 2019, Volume I (Long and Short Papers), pages guistics, 2019. doi: 10. 10.18853/v1/n19.. 1423 1423. URL
Association for Computational Lin- https: / /doii. org/10..///0 /ttp///..11153///1111149499
R. Dunford, Q. Su, and E. Tamang. The pareto principle. The Race, 2021. URL https://api. semanticscholar Trg/CorpusID. 15925174. 15
E. First, M. N. Rabe, T. Ringer, and Y. Brun. Baldur: Whole-proof generation and repair with large language models. CoRR, abs/23033044911 2023. doi: 10448550/arXx..200..00000 URL https://doi. org/10. hetg//..8550//// 48550/arXiv 2303. 04910. 10
L. Gao, S. Biderman, S. Black, L.. Golding, T. Hoppe, C. Foster, J. Phang, H. He, A. Thite, N. Naheshima, S. Presser, and C. Leahy. The pile: An 800gb dataset diverse text for language modeling, 2020. 6
11

---

L. Gesellensetter, S. Glesner, and E. Salecker. Formal verification with isabelle/hol in practice: finding bug in the gee scheduler. In Formal Methods for Industrial Critical Systems: 12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers 12, pages 85-100. Springer, 2008.
M. Han, J. Rute, Y. Wu, E. W. Ayers, and S. Polu. Proof artifact co-training for theorem proving with language models. In The Tenth International Conference Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL net set/forrumid=rpxxee5
2, 6, 10
J. Harrison. HOL light: An overview. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 60-66. Springer, 2009. doi: 10.1007/978--3642-0333333 _4 URL https://doi. 03359-3359--- 9_4.
org/10. 0/5/100.007/97888
D. Hendrycks, C. Burns, S. Kadavath, A. Arora, S. Basart, E. Tang, D. Song, and J. Steinhardt. Measuring mathematical problem solving with the math dataset, 2021.
Y. Huang. X. Lin, Z. Liu, Q. Cao, H. Xin, H. Wang, Z. Li, L. Song, and X. Liang. Mustard: Mastering uniform synthesis of theorem and proof data, 2024. 1, 10
A. Q. Jiang, W. Li, M. Han, and Y. Wu. Lisa: Language models of isabelle proofs. 2021. 1, 1,3, 6, 10, 15
A. Q. Jiang. W. Li, S. Tworkowski, K. Czechowski, T. Odrzygóżdž, P. Mitoš, Y. Wu, and M. Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. arXiv preprint arXiv:2205. 200,:22300.8933 2022a. 1, 2, 4, 6, 7, 8, 10, 15
A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and G. Lam- ple. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. CoRR, abs/2210.1224 2022b, doi: 20.48550/arxiv.2210..2. 12283. URL https::///// //sttps://oi.. argg/0.44550 arXiv arXiv.2210.2 12283. 1, 6, 10
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207-220, 2009.
G. Lample, M.-.. Lachaux, T. Lavril, X. Martinet, A. Hayat, G. Ebner, Rodriguez, and T. Lacroix. HyperTree Tree Proof Search for Neural Theorem Proving. Technical Report arXiv:2205. 1491, arXiv, May 2022. URL http://arx:: /taxxvv org/ abs/ /205 11491. arXiv:2205. 11491 [es] type: article. 6, 10 10
A. Lewkowycz, A. Andreassen, D. Dohan, E. Dyer, H. Michalewski, V. V. Ramasesh, A. Slone, C. Anil, I. Schlag, Gutman-Solo, Y. Wu, B. Neyshabur, G. Gur- Ari, and V. Misra. Solving quantitative reasoning problems with language models. In NeurlPS, 2022. URL http://papers. http:///apprs..iss.... cc/paper cocppappr_filesseeeeeeeeeeeeeeee files/
Abstract- /ttps//pppeee/222////// /ppppr//222//hah// html. 10
C. Liu, J. Shen, H. Xin, 7. Liu, Y. Yuan, H. Wang, W. Ju, C. Zheng, Y. Yin, L. Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint Stt.::20090429955 2023.
C. MacKenzie, J. Fleuriot, and J. Vaughan. An evaluation of the archive of formal proofs, 2021. 6
M. Mikula, S. Antoniak, S. Tworkowski, A. Q. Jiang, J. P. Zhou, C. Szegedy, L. Kucinski, P. Miloš. and Y. Wu. Magnushammer: A transformer-based approach to premise selection. arXiv preprint wrXiv:2303.04488, 2023. 6. 8
T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer-Veriie Verlag, Berlin, Heidelberg, 2002. ISBN 3540433767.
OpenAI. GPT-4 technical report. CORR, abs/2303.08774, 2023. doi: 10.48550\axxx.2223..8777
URL https: / //wii. org/10, 48550/arXiv 2303. 08774. 6, 16
12

---

L. C. Paulson. Isabelle Generic Theorem Prover. Springer Verlag, 1994. 3,
L. C. Paulson. Three years of experience with sledgehammer, practical link between automatic and interactive theorem provers. R. A. Schmidt, S. Schulz, and B. Konev, editors, Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scot- land, UK. July 14, 2010, volume 9 EPiC Series in Computing, pages 1-10. EasyChair, 2010. doi: 10.29007/TNFD. URL https: //::://doooo /dii. org/ 10. 29007/tnti 6
S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03320 00399, 2020. URL https: http///axvvv..////v//////..a org/ 2009 03393. 1, 2, 2, 6,
Polu, J. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever, Formal Mathematics State- ment Curriculum Learning. (arXiv:2202.01344)) Feb. 2022. doi: 10.48550/arXiv.22000 wttp:rrw....222.1144.44
URL atttp://arxiv www.oogggg...oooo.ooo.o.ooo 01344. arXiv:2202.01344 10
[cs] type: article. 1, 2, 6, 7, 8,
D. Silver, A. Huang, C. Maddison, A. Guez, L. Sifre, G. van den Driessche, J. Schrittwieser, I. Antonoglou, V. Pannerrshellam, M. Lanctot, S. Dieleman, D. Grewe, J. Nham, N. Kalchbren- ner, Sutskever, T. Lillicrap. M. Leach, K. Kavukcuoglu, T. Graepel, and D. Hassabis. Mas- tering the game of Go with deep neural networks and tree search. Nature, 529(7587):484
Jan. 2016. ISSN 1476-4687. doi: 10. 10.108//aaur
URL attps://wwa nature com/
articles/natureleee
Number: 7587 Publisher: Nature Publishing Group. 10
A. Thakur, G. Tsoukalas, Y. Wen, J. Xin, and S. Chaudhuri. An in-context learning agent for formal theorem-proving, 2024. 1, 6,
G. Wang, Y. Xie, Y. Jiang, A. Mandlekar, C. Xiao, Y. Zhu, L. Fan, and A. Anandkumar. Voyager: An open-ended embodied agent with large language models. arXiv preprint arXiv: Arxiv-2305.16291, 2023a. 10
H. Wang, H. Xin, C. Zheng, L. Li, Z. Liu, Q. Cao, Y. Huang. J. Xiong, H. Shi, F. Xie, J. Yin, 7. Li, H. Liao, and X. Liang. Lego-prover: Neural theorem proving with growing libraries, 2023b. 1, 10
H. Wang, Y. Yuan, Z. Liu, J. Shen, Y. Yin, J. Xiong, E. Xie, H. Shi, Y. Li, L. Li, et al. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the s Annual Meeting the Association for Computational Linguistics (Volume I: Long Papers), pages 2632-12646, 2023c. 1, 8, 10
J. Wei. X. Wang, D. Schuurmans, M. Bosma, B. Ichter, F. Xia, E. Chi, Q. Le, and D. Zhou. Chain- of of-thought prompting elicits reasoning in large language models, 2023. 10
M. Wenzel al. The isabelle/isar reference manual, 2004.
Y. Wu, A. Q. Jiang, W. Li, M. Rabe, C. Staats, M. Jamnik, and C. Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353-32368 2022. 6,
J. Xiong, J. Shen, Y. Yuan, H. Wang, Y. Yin, Z. Liu, L. Li, Z. Guo, Q. Cao, Y. Huang, C. Zheng, X. Liang, M. Zhang, and Q Liu. Trigo: Benchmarking formal mathematical proof reduction for generative language models, 2023.
K. Yang, A. M. Swope. A. Gu. R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anand- kumar. Leandojo: Theorem proving with retrieval-augmenned language models. arXiv preprint arXiv:2306. 15626, 2023. 1, 2. 6, 7,8, 10
I. Zhang, S. Lu, and N. Duan. Selene: Pioneering automated proof in software verification, 2024. 3
C. Zheng, H. Wang, E. Xie, Z. Liu, J. Sun, H. Xin, J. Shen, Z. Li, and Y. Li. Lyra: Orchestrating dual correction in automated theorem proving, 2023. 6, 10
K. Zheng, J. M. Han, and S. Polu. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics. Sept. 2021. URL httpp://opperrevie..c htt.aa/wwww.........oooooa/a/aaa 3,
13

---

A
More Details on POETRY
The outline of the Appendix A is as follows:
More details on our proposed recursive best-first search.
Implementation details for POETRY, including the hyperparameters for the methods and
machine configuration.
More details on the newly extracted PISA dataset, and additional analysis of the statistics and characteristics of the dataset.
Additional results include a comparison table with LLM-based approaches, input/output comparisons for GPT-f Baseline and POETRY, and an analysis of POETRYs failure cases.
Appendix B discusses the broader impacts of POETRY.
Appendix C includes more examples of found theorems by POETRY.
A.1 Details on Recursive BFS
In this section, we discuss more details on the recursive BFS algorithm. Section 3.2 only introduces the overall process of how recursive BFS runs, and no detailed introduction on status update rules, pause and continue of the recursive BFS and terminate conditions. We discuss each in detail below.
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 node will be marked as PROVED or HALF-PROVED if any of its children is PROVED HALF- PROVED. Additionally, when POETRY encounters sorry edge there exists special update rules. If a node is connected to PROVED node with sorry edge, and the next level root node is OPEN, this means the mid--conjecturesssubggabl 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())).
Pause and continue of recursive BFS. Figure (d) illustrates the pause and continue of recursive BFS. During the proof search, whenever a proof sketch is found (Figure 2(a)), the current level of the best-first search will be paused, and POETRY will find the last unproved sorry edge and recursively call the best-first search algorithm to find the proof for the next-level root node attached in the sorry edge (Figure 2(b)). If the next-level best-first search fails find proof for the sub-root node (The status of the sub-root node is marked as FAILED), POETRY will update the status of the search tree and continue the paused best-first search for the current level and try to find new proof sketches (Figure (dc).
Terminate conditions. The proof search of the current level will terminate and return to the upper- level proof search under these scenarios: 1) A complete proof for this level is found, which means all the middle conjectures recursively. The root node status of the current level proof search is marked as PROVED. 2) For proof search in level higher than 1, 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, 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).
subgoals have been proven by the deeper levels of proof searches,
A.2 Implementation Details
In this work, we use 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, hidden dimension of 2048, and GPT-2 tokenizer with 50400 vocabulary size. We use the alpaca'
Phttps://githhnn
http:p///gg..ta.o.ooo//aaaaaaaaa con/tatsu-lab/stann alpaca
14

---

Table 3:
Dataset statistics. The table displays the dataset statistics for newly extracted PISA dataset
based on Isabelle 2022.
train
valid
test
single-level
multi-level
Number of theorems
236, 978
2.317
2, 236
1, 1,858
681
Number of proof steps
3, 018, 407
27,419
27, 653
3, 982
23, 671
Average proof length
12.7
11.7
11.8
2.4
33.5
Maximum proof length
10, 320
1,236
1,079
204
1079
Average proof level
1.5
1.5
1.5
1.0
2.6
Maximum proof level
26
9
10
1
10
codebase for finetuning the model on our recursive dataset. During fine-tuning, we use global batch size of 256 with 3500 steps of warmup using the AdamW optimizer. We use the cosine scheduling strategy with maximum learning rate of 3e 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 timeout limit of 10 seconds. The number of samples per expansion 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 timcout of 120 seconds 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.
A.3 Dataset Details
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 Statisties. We follow Jiang et al. [2021, 2022a] and extract data from Isabelle 2022, as well as the corresponding version of the Archive of Formal Proof library. 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 the two subsets of the PISA test. The single-level test 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 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 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 anddconjcctures//uugolls proof being skipped by sonry, we not accurately caleulate the search space is shrunk which extent. However, 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 proof sketch. We can
'The original dataset is extracted with Isabelle 2021, resulting in x fewer theorems and x fewer lines of state action pair.
15

---

Proof level histogram on PISA
Proof/sketch length histogram on PISA
10a
Data format Original
10
Recursive
Problem counts
10
Problem counts
101
10a
10a
10*
10
10a
104
7
10
16 Proof level
19
22
20
80
>100
Proof/sketch length
(a)
(b)
Figure 5: Distribution of proof level and proof length in PISA dataset. (a) Histogram of proof level in the PISA training set. The maximum proof level can reach 26 (h) Comparison between the number of steps in the original proof and the extracted proof sketches. By breaking the original proof into proof sketches, the proof length is reduced substantially.
Table 4: Proving Success Rates on the miniF2F Dataset with Isabelle. The table displays the success rates of previous works using large language models. These approaches not directly comparable with POETRY but are listed here only demonstration.
Success rate
LLM
miniF2FFvalid
miniF2F-test
Draft, sketch, and Prove Bobgoal-LLearning
Codex
42.6%
39.3%
ChatGPT
48. 48.0%
45.5%
I.EGO-Prover (model informal proof)
ChatGPT
52.0
45.5%
POETRY
ProofGPT-1.3B
42.2%
42.2%
observe that the proof length of POETRY is substantially shifted towards shorter proof length per proof. On average, there are 3.3 proof steps for POETRY and 12.7 proof steps for step-by step-by-step baseline per proof. And that would be 32 times smaller the search space per proof average with 32.
A.4 Additional results
Comparison with L.M--based approaches. For more comprehensive view of the relationship be- tween POETRY and other state-of-the the-art art methods, we include Table to illustrate the performance in miniF2F using the large language model like ChatGPT [OpenAI, 2023]. It is important to note that these methods use completely different approach to prove theorems. Instead of performing searches using BFS algorithms, these approaches leverage the to translate natural language proofs into formal code (often termed autoformalization) Therefore, comparing these methods with POETRY not only unfair in terms of model size and the amount of training data but also incomparable in core methodology.
capabilities of LLMs
Input and output comparison for GPT-f Baseline and POETRY. We also provide table illus- trating the detailed input and output pair constructed for language model training. This is the same theorem example shown in Figure 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 paper for better illustration.
Failure cases of POETRY We provide additional failure cases POETRY better understand the limitations of current recursive proving approaches. Compared to the GPT-f Baseline, notable issue with the recursive framework POETRY stems from its greedy exploration strategy. POETRY aggressively explores deeper-level proofs as soon as it finds a valid proof sketch, yet sometimes
16

---

Table 5: Input and Output Comparison for GPT-f Baseline and POETRY the Training Data. Both GPT-f Baseline and POETRY have the exact same input state and number of training examples. The only differences are in lines 2, 6, and 21, where a sorry is appended to the end of the tactic.
Iuput States
GPT-f Baseline Ouquut
POETRY Outpet
1. goal mabgoal:: 1. (x n)
[]]
proof (cases)
proof (cases) assumw suge: Ysgu? 0r thea Pthaa aorry
2 goul (2 sobgoala): 1. TP -> (x [*] e) ...
ааauня n_gw: "n Vige> d" thus ?theaia
3 goal (2: snhgnala]: 1.
-> PPI...
uxing n, n_ge nat,,pov pov
uxing nige* nat,pow, pow by (alup add; mult__laa____3 next
4 using this: 0 <- a < a (x [*] nat a...
by (sinp add; ault__eee____111
5 Successful atteept. to nolve goal
6 goal wobgoul): 1. 88a -> 60
axause 1, "..." ahow Pcheali apply (eiop add: int_pou, dox2)
axsumw n. nt: "..." whow ?theaia sorey apply (einp add: sat_pox_dcc2)
using thin:
goal
8 goal (1 subgnal): 1. 0 <- -2. B.D.
by (autis asasa sult wult_iiims i riight)
by (eMtia uonza malt,aiiussright)
21 goal sahgaal): 1.
<....
a*ause m, "..." thux Pcheala
assuEM n_lt: "..." thux ?theaia sorey using a,it
22
proot (grove) using this:
...
using n,1t
23
proof (prove) using this:
x 4 o...
by (suto eimp: int_pou_der2)
by (auto simp: ist_pou_dcf2) qed ged
24 Successful actenpt to solve goal by..
ged
25
goal: this: (x (*) [".... No subgoais!
ged
Chaocen amcl2a 2013
real"
Lecketion, 21
2e122 (re))
AESLMeE Txcelleed (e413 (e-3)*
stess
5200y
pead]
p2eef [seduct +)
ther 2tresis
ads: ax37a(2))
(xsee(1))
rea
Lse
lite m) 1x25
eeiing He 11 x2 nnteerl
scaly Liddat
sungee1 30100 euploretten
(indact 1)
aroms
116
(b)
(c)
Figure 6: Failure cases of POETRY in Proof Search. (a) A case where POETRY finds a longer proof compared to GPT-f Baseline. Due to the greedy exploration of successful proof sketches, POETRY might find proofs with redundant wrapping of proof steps, comprising 5 steps, whereas GPT-f Baseline finds proofs with 2 steps and less redundancy. Note that this happens very rarely (2.4% of both solved problems). (b) and (c) A failure case where POETRY fails to find proof due to greedy exploration of successful sketches. The correct proof is shown in (b), where the correct proof steps remain the same level after the tactic apply (induct n). However, POETRY finds sketch in advance and greedily explores deeper sketches of the last sorry, eventually failing to find the correct proof due to a timcout.
these sketches are dummy sketches, lacking meaningful proving steps (e.g., a general deduction framework as shown in Figure 6 (a)). In other cases, the correct solution exists at a shallow proof level but is bypassed, never returning from deeper exploration (Figure (b) and (c)). Introducing a value function to prioritize informative sketches and selectively deepen or retain the current level of exploration could address these issues.
B
Broader Impact
The research presented in this paper has the potential to advance automated theorem proving, AI for Math and software engineering. The advancement can enhance the capabilities of large language models in formal theorem proving, contributing to more reliable mathematical proof verification and providing valuable educational resources for students and researchers. By directly releasing the code, model and data, we aim ensure the responsible use of our work, fostering further innovation and maintaining high standards of data privacy and intellectual property compliance.
We anticipate no foresecable negative societal impacts of this work.
17

---

C Examples of Found Theorem by POETRY
C.1 Examples in miniF2F Dataset
theorem amc12b_2020_pp6 fixes nat
h0: \<le> n"
shows "X<xisst>>x: :nat. (real nat x) (fact (n fact (n 1)) / fact n"
proof
from
show?thesis
unfolding @aver2_eq_sqaaa
by (intro exI "n + 1"]) (auto simp: field_eimps)
simps)
qed
theorem mathd mathd_algebra. aal_abalggaaa_ 422:
fixes x :: real and <eigma>:: "real \<Rightarrow> real" assumes "bij \<sigma>" and <<sigma> :>aaa>;"<<<> <foorlll>>>>> <<sigma> 5 12" and "\<sigma> shows "x 47 24"
1) (Hilbert Choice. inv \<sigma>) x"
proof
from assms
"bij \<sigma>"
by (auto intro!: bijI simp: bij_def)
show?thesis
proof (rule ccontr)
"x K<oteeq> 47/24"
False using assms
by (subat (aam) bij inv_iiigg__. inv_eq_iff)) auto
qed ged
theorem mathd laae__llgabaa___ae 441:
fixes real "x \<noteqp (x"4 (14 x)) (35 x)) 10"
shows "12 proof
from assms
show?thesis apply (simp add: divide_simps)
apply algebra
by (simp add: power4_ _ere__e___x__ xxxx pover2_eq_aquaze
qed
18

---

theorem mathd_ :: real assumes "b a22
fixes algebra_ 487:
and "a b 1" and and "c + d 1"
c22"
and "a /<oteeq c" shows "sqrt ((a 2 (b 2)) sqrt 10" proof (rule real, real_ sqrt_ unique) sqqqquq
show "(sqrt 10)p2s (a c) c)\c>sup>2 + (b d) d>ps""u>>2" proof
let?r real_of_rat
show?thesis
proof (rule power2_eg imp__q)
show "((sqrt aup>>>) << <usu>> = ((a c)\<<uu>>2 + (b =d)(<aup>2))
\<"su>>""
proof
from assms
show?thesis
unfolding poxer2_eq_aqual
apply simp
apply (auto simp: field_ simps) by sos
qed
ged (auto simp: gigebra_simpa
qed
qed (simp add: pover__eq_squrr
C.2 Examples in PISA Dataset
lemma rev rev_morphs: "two "two_binary" proof
(rev_map map g) (rev_may map h)
show Srev_map (u <<dot>> v) = rev rev_map g \<ddot> rev rev_map v" for proof (simp add: rev_map_deff
show "rev (g (rev \<edot> rev u)) rev (g (rev w)) \<edot> rev (g (rev v))"
using swap by (simp add: g. g.morph)
qed
Kedot>> v) rev h u \<edet> rev rev_map v" for proof (simp add: rev rev_map_ _e__p__eee)
show "rev "rev_map
show "rev (h (rev \<edot> rev w)) rev (h (rev u)) \<edot> rev (h (rev v))"
using swap by (simp add: h.morph)
qed qed
19

---

lemma 1set_ :te__tterates:
"Iset (iterates x) {(f n) xln. True]"
proof
show "Iset (iterates x) \<subseteq> {(f ~n n) In. True)"
proof (cases "x A<in> laet (iterates f x)
case True
thus?thesis by (auto simp add: lalllsstcoon,. lnth)
next
case False thus?thesis
by (auto simp: in
qed show "{(f -" In. True} \<subseteq> lset (iterates x)
proof safe
fix
show "(f n) \<in> 1set (iterates f x)"
proof (induct n arbitrary: x)
case 0
thus?case
by (subst iterates) simp
next
case Suc thus?case
by (subst iterates) (simp add: o o_def (anpow_swapp)
ged
qed
qed
lemma neg_distr, cond_bset bset_eeeeeeeee eq: www.ddiiddcccc diw.dd_coddddd_.eeeed bset (=) (=) tytok"
unfolding neg_ jig_distr_connd cast__coonbbbe_dee_____eee
eeply(rul predicate2I)
apply transfer subgoal for
(rule bexI [where x=B])
subgoal
apply safe subgoal
unfolding sel_set_00
by (auto simp add: rel_set, def 00 def)
subgoal
unfolding rel_set_00 by (auto simp add: rel_ses set__et 00_def)
done
by (simp)
done
20

---

lemma
"frag_cmul (c+d) a frag_cmul cmul frag_cmul a"
proof
show?thesis
proof (rule poly_mapping_eq(]
fix show "lookup (frag_cmul (c d) a) lookup (frag_cmul c a + frag_ cmul
a) x"
proof (cases "x <<nn> keys a")
case True
thus?thesis unfolding lookup_add cmul
using by (auto simp: algebra_simpa
qed (auto simp: in in_keys_itt iff lookup_ado add in_keys_iff) qed
qed
lemma SETId: assumes "x |Kin>> shows "(Id |0l x proof
have "x \<in> Obj (0p S
using assms
apply (simp add: OppositeCategory.cooo
by (simp add: SET SET_dee def SET' def MakeCat_def. thus?thesis
proof
assume 1: "x \<in> obj \< bsub>2p 3ET\<"esub>* show?thesis
proof (simp add: SET def) show "id)< babk<bbbbaaaaeCat SET' X |@] x x"
proof (cases "x \\iin> x") True
thus?thesis
(simy add: SET' _def
apply (simp add: MakeCat_deff) by (rule ZFfunApp)
ged qed
(simp add: assms)
qed
qed
21

---

lemma (in encoding_wi wrt,
indRelRSTPO lerps_wttbbbrrrreee barbs)
fixes Sãel "('procS \<times> 'procS) set"
and TRel "('procT \<times> 'procT) set"
assumes reflection: "rel_ veel_veekly_reflettt.mooo barbb (indRelRSTPO SRel TRel) STCalWB SWB TWE)
shows feel_wekll__d reflects barbs barbs SRel SWB"
rreakly_reflects
and rel__veakly_refletee barbs TRel TWB"
proof
have "rel "rel_weakly www.eeyeeelllets_aeeeeeeee barbs SRel SWB \<and> rel_weaaly_reflects..mn
TRe1 TWB"
proof (rule conjI)
show "rel_ weel_waakl__efleeeee barbs SRel SWB"
using reflection rel_with_soune sourbesssuueeeeeee impl Smmp_SRell___ SRell _Ree_weeklly_eeeeeeeeeeeeaeeeeee
barbs [where
Rel="indRelRSTPO SRel TRel" and SRel="SRel"] by (simp add: indRe1RSTPO. source (eeeree[wrr [where SRel="SRel" and TRel="TRel")) show "rel_ pel__waaky_rrfeeec barbs TRel TWB"
weakllyyyrffleett using reflection rel_ with target_ impl Beel__Tee__see feakyy rww.eeefect...o baakects__babbbbte barbs [where Rel==indRelRSTPO SRel TRe1" and TRel="TRel"] by (simp add: indRelRSTPO target [where SRel="SRel" and TRel="TRel"])
qed
thus "rel_weake sel__waaklyrrffetttt.. barbs SRel SWB" and "rel_ ree__eeaky_refeetts_po barbs
TRel TWB" by simp_alls
qed
22

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
The abstract and the introduction clearly state the contributions of POETRY, the recursive proving method that enables proof search to find substantial longer proof. POETRY achieves superior performance on benchmarks like miniF2F and PISA, which align with the paper's content.
Justification:
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification:
The paper discusses the limitations in Section 6.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The au- thors should reflect on how these assumptions might be violated practice and what the implications would be.
The authors should reflect the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the ap- proach. For example, a facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because fails to handle technical jargon.
The authors should discuss the computational efficiency the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to ad- dress problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't it acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
23

---

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 cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theo- rems.
The proofs can either appear the main paper or supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be comple-
mented by formal proof' provided in appendix supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
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 conclu- sions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: The paper provides detailed steps of the methodology. including the data extraction process, the training details in Section 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 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 novel architecture, describing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary either make it possible for others replicate the model with the same dataset, or provide access to the model. In general. releasing code and data 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 sub- missions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results way to re- produce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case au- thors 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 (c.g., to registered users), but it should be possible for other researchers to have some path to reproducing verifying the results.
24

---

5. Open access to data and code
Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
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.
Justification:
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nig) cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so No is acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (c.g., for a new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https: //nips wwtpccccpp/cccctccccccccccccccct
cooollccggidesse guwdee/dde///e / ssionPolicy) for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they chosen, type of optimizer, etc.) necessary understand the results?
Answer: [Yes]
The paper specifies the experimental details, including data splits, hyperpa- rameters, model configurations, and evaluation metrics necessary to understand the results in Section and Appendix A.
Justification:
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 level of detail that is necessary appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment Statistical Significance
Question: Does the paper report error bars suitably and correctly defined or other appropri- ate information about the statistical significance of the experiments?
Answer: [Yss]
Justification: As our beam search generation of GPT is deterministic. error bars 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.
25

---

The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the enror bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall
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 the standard error of the mean.
is OK report I-sigma error bars, but one should state it. The authors should prefer- ably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that out of range (e.g. negative error rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification:
This information can be found in Appendix A.2.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount compute required for each of the individual experimental runs well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't t make it into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics https: //tps::////erreee/ http//nnuripp.ppe httpp//tttps..pppllii/i/c//////t ctcc/puubbcc/ccccccciieeeellll
Answer: [Yes]
Justification: This 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 the authors have reviewed the NeurlPS Code of Ethics. If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g.. if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification:
The paper discusses this aspect in Appendix B.
26

---

Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact spe- cific 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 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 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 mitiga- tion strategies (e.g., gated release of models, providing defenses addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data or models that have high risk for misuse (e.g.. pretrained language models, image generators, or scraped datasets)?
Question:
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 high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by re- quiring 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 require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
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?
Question:
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 existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
27

---

For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
assets are released, the license, copyright information, and terms use in the pack- age should be provided. For popular datasets, paperswi thcode com/ datasets has curated licenses for some datasets. Their licensing guide can help determine the cense of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information is not available online, the authors encouraged to reach out to the asset's ' creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documenta- tion provided alongside the assets?
Answer: [Yes]
Justification: All code, datasets and models are documented and will be provided alongside the assets facilitate further research.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
For crowdsourcing experiments and research with human subjects, does the pa- per include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Question:
Answer: [NA]
Justification:
The paper does not involve crowdsoureing or research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing research with human subjects.
Including this information in the supplemental material is fine, but if the main contri- bution of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, cura- tion, or other labor should paid at least the minimum wage the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: The paper does not involve research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
28

---

Depending on the country in which research is conducted, IRB approval (or equiva- lent) 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 include any information that would break anonymity (if applicable), such as the institution conducting the review.
29


Reviews:
[{"review_id": "bV1JfItnZR", "reviewer": "Reviewer_eTZY", "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).", "questions": "Please see weaknesses section above.", "limitations": "Yes", "rating": 7, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "The paper is very well structured and clearly written. Intuitions, method details, connection to existing methods, limitations, and take away messages from experiments are all very well articulated.\n\nThe idea seems simple but is apparently novel (see 'weaknesses' below, related to this). \n\nThe gains over several baselines are notable, of 5% or more (absolute).\n\nI am assuming the authors will publicly release the code of their POETRY system for further research on this topic.", "weaknesses": "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.\n\nI 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)?\n\nJust 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "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.\n\n## Weaknesses\n### w1. Novelty on the recursive method.\nTo 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.\n\n### w2. The necessity of the novel recursive best-first search\nThere are various options to handle recursive proving approaches, and we chose to use recursive best-first search (rBFS) for the following reasons:\n\n- **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.\n- **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.\n- **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.\n- **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.\n\nAs 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.\n\nRegarding 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.\n\n\n### w3. The performance on miniF2F with large language model.\nWe 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.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "RX4KMM1rUA", "reviewer": "Reviewer_BhWC", "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.", "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?\n2. In your training procedure, do you fine-tune on any theorems in the miniF2F dataset?", "limitations": "Yes.", "rating": 5, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "While the idea of a proof sketch is not novel, the combination of the data curation process to enable the construction of proof sketches is. This takes a step towards generating conjectures which would be crucial to making progress on neural theorem proving.", "weaknesses": "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. \n2. 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.\n3. 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?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your detailed and constructive comments. We hope our responses and rebuttal material (RM) address your concerns.\n\n## Clarification on strengths.\nThere 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`:\n\n- 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.\n- 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.\n\n## Weaknesses\n### w1. Dataset construction.\nPlease 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.\n\n### w2. Context explaining the comparison with Lean result against Isabelle.\nThe 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:\n- We follow previous work like [Li et al](https://arxiv.org/abs/2404.09939v1). to provide a comprehensive demonstration of the benchmark results in miniF2F.\n- 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.\n\n### w3. Details on Pros and Cons of POETRY\nWe have followed your advice and conducted a more thorough analysis of POETRY.\n\n- **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.\n\n- **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`:\n\n  ```isabelle\n  lemma terminates_tl_raw: \n    assumes \"terminates g\"\n    shows \"terminates (tl_raw g)\"\n  proof\n    fix st :: \"bool \\<times> 'a\"\n    obtain n s where \"st = (n, s)\"\n      by (cases st) blast+\n    from assms have \"s \\<in> terminates_on g\"\n      by (metis terminatesD)\n    thus \"st \\<in> terminates_on (tl_raw g)\"\n      unfolding \\<open>st = (n, s)\\<close>\n      apply(induction s arbitrary: n)\n      by(case_tac [!] n)(auto intro: terminates_on.intros)\n  qed\n  ```\n  Here, the top-level sketch instantiates n and s and proceeds with proving conjectures, with the actual verification of the condition deferred.\n  \n- **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.\n\nFigure 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.\n\n## Questions\n### q1. Relations between proof sketches and the tree of conjectures.\nProof 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.\n\n### q2. Finetuning on miniF2F.\nNo, 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.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "V0azUuAuyE", "reviewer": "Reviewer_9pow", "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.", "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?\n* For problems that both POETRY and the GPT-f baseline solve, does POETRY tend to generate longer proofs?\n* 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?\n* 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?\n* What is Thor without sledgehammer? It sounds like a different thing other than Thor.\n* 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": "Yes, adequately addressed.", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The paper is well motivated and tackles a timely topic, using a standard, hard benchmark (minif2f) for methods in this space. The writing is mostly clear (though see some notes below).\n\nPOETRY is a simple, sound and novel method to structure the proof generation process. It should be adaptable to other interactive theorem provers with some work. POETRY allows the prover model to get more intermediate feedback from the environment compared to methods that try to produce the whole proof at once. It also uses this feedback in a way that is complementary to proof repair methods (generally what the standard when we consider using intermediate feedback).", "weaknesses": "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.\n\nAs 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).\n\nThe 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your detailed and constructive comments. We hope our responses and rebuttal material address your concerns.\n\n## Clarifications on the summary\nThere 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.\n\n## Weaknesses\n### w1. Clarification on the baseline\nBoth `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`.\n\n### w2. Pass@1 metric\nPOETRY, `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.\n\n### w3. On \"Can POETRY find longer proof?\"\nIt 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.\n\nWe 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.\n\n## Question\n### q1. The condition of a sketch being valid\nWhen 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`.\n\n### q2. Proof length differences\nAccording 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.\n\nOccasionally, 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. \n\nTherefore, 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.\n\n### q3. Example in LEGO-Prover\nHere is an example from the LEGO-Prover GitHub:\n```Isabelle\ntheorem aime_1983_p9:\n  fixes x::real\n  assumes \"0<x\" \"x<pi\"\n  shows \"12 \\<le> ((9 * (x^2 * (sin x)^2)) + 4) / (x * sin x)\"\nproof -\n  define y where \"y = x * sin x\"\n  have \"12 \\<le> (9 * y^2 + 4) / y\"\n  proof -\n    have c0: \"y > 0\"\n      by (simp add: assms(1) assms(2) sin_gt_zero y_def)\n    have \"(9 * y^2 + 4) \\<ge> 12 * y\"\n      by sos\n    then show ?thesis\n      using c0 by (simp add: mult_imp_le_div_pos)\n  qed\n  then show ?thesis\n    by (simp add: power_mult_distrib y_def)\nqed\n```\nConjectures 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.\n\n### q4. The search algorithm used in the baselines\n`Thor w/o sledgehammer` and `GPT-f Baseline` use the best-first search algorithm described in the original GPT-f paper.\n\n### q5. Explanation with Thor w/o sledgehammer\nPlease refer to w1.\n\n### q6. Confusion in Figure 5(b)\nThis 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.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "NQNlvZd6T6", "reviewer": "Reviewer_p8XS", "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.", "questions": "-\tIn 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": "The authors adequately addressed the limitations and potential negative societal impact.", "rating": 7, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "-\tThe POETRY algorithm is neat and novel by mimicking how human write mathematical proofs hierarchically. \n-\tThis paper is well written and easy to follow.\n-\tThe POETRY algorithm has potentials to be further improved by incorporating premise-selection techniques such as sledgehammer or Magnushammer.", "weaknesses": "-\tFrom 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "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.\n\n## Weaknesses\n### w1. How POETRY scales with more computing resources.\nIndeed, 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.\n\nRegarding 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.\n\nMoreover, 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.\n\nTherefore, 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.\n\n## Question\n### Q.1 Cause of complex proof in Figure 5(b).\nThe 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.\n\nWhile 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.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:
Dear Reviewers and ACs,

Thank you very much for the time and effort you have dedicated to reviewing our paper. We appreciate the thorough suggestions and constructive feedback on our manuscript.

We are also grateful for the positive recognition from the reviewers regarding our motivation (eTZY, 9pow, p8XS), contribution (eTZY, BhWC, 9pow, p8XS), and strong results (eTZY, p8XS), as well as the potential future impact of our work (eTZY, BhWC, 9pow, p8XS). We acknowledge the concerns raised by reviewers BhWC and 9pow, which may stem from some previously incomplete observations in our work. Reviewer 9pow raised concerns about our baseline comparison, which appear to stem from misunderstandings of our methods and baseline. POETRY operates step-by-step, like GPT-f Baseline, within each proof sketch, without incurring extra computation costs compared to the baseline method, ensuring a fair comparison. We will provide further explanations in our revised manuscript.

We have carefully considered all the suggestions provided by the reviewers and included the additional information requested in our one-page rebuttal. We have denoted the attached PDF document as rebuttal material, abbreviated as RM. The key updates are as follows:

- **(BhWC)** Table 1 compares the constructed training corpus for GPT-f Baseline and POETRY, providing a clear view of the differences in training data.
- **(eTZY)** Table 2 illustrates benchmark results using a large language model. These results are not comparable but are presented for demonstration purposes.
- **(BhWC and 9pow)** Figure 1 shows a histogram of the number of problems solved by `GPT-f Baseline` and POETRY based on the length of the ground truth proofs. This analysis reveals that POETRY tends to solve more complex problems and excels at solving problems requiring structural reasoning.
- **(BhWC and 9pow)** Figure 2 provides two failure cases showcasing issues caused by the greedy exploration process, which can lead POETRY to find proofs with redundant steps or fail to find shallow proofs. However, these occurrences are sparse.

Additionally, we outline our paper's main contributions, including additional conclusions drawn during the rebuttal:

- We propose POETRY, a novel approach for neural theorem proving. Addressing a long-standing issue in previous step-by-step approaches, we introduce a recursive proving approach to find proofs hierarchically within the proof. **To our knowledge, we are the first to explore the recursive proving paradigm in neural theorem proving.**
- We introduce a novel recursive best-first algorithm that naturally aligns with the idea of recursive theorem proving. Additionally, it has good extensiveness and the potential for parallel computation.
- Experiments conducted on the miniF2F and PISA datasets demonstrate significant performance gains with our POETRY approach over state-of-the-art methods. POETRY achieves an average proving success rate improvement of 5.1% on miniF2F.
- A substantial increase in the maximum proof length found by POETRY is observed, from 10 to 26. Through thorough analysis, we confirm that POETRY is capable of solving more complex problems and excels at solving problems requiring structural reasoning.

We thank all the reviewers again for their time and effort in reviewing our paper and are committed to addressing every issue raised.

Meta-review: 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.
Decision: Accept (poster)