ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Authors: Haoxiong Liu
Jiacheng Sun
Zhenguo Li
Andrew C Yao
Venue: ICML 2025 poster (2025)
Keywords: Neural Theorem Proving
Large Language Models
Primary area: deep_learning->large_language_models
TL;DR: We propose a novel NTP method ProofAug that achieves new SOTA (66.0%) on miniF2F-test Isaballe through equipping proof-generation LLMs with automation methods in different granularities via fine-grained structure analysis.

Abstract: The synergy between deep learning models and traditional automation tools, such as built-in tactics of the proof assistant and off-the-shelf automated theorem provers, plays a crucial role in developing robust and efficient neural theorem provers~(NTPs).
However, for proof synthesis with LLMs, previous work applies automation tools either only when explicitly invoked by the model or at a single granularity level, failing to fully exploit their power. 
To solve this issue, we propose ProofAug, a procedure that equips LLMs with automation methods at various granularities through fine-grained structure analysis of model-generated proof proposals. 
ProofAug also serves as a versatile plug-and-play module that seamlessly integrates with any tree-search algorithm, enabling our construction of an efficient recursive proving (ERP) module to further enhance performance.
The superiority of our method is validated on the miniF2F benchmark using the open-source deepseek-math-7b-base model and the Isabelle proof assistant.
Notably, by additionally employing a mixed prompting strategy, we achieve a cumulative pass rate of 66.0% after curation of the dataset (61.9% for the original version) with 2100 queries to the model per problem (In contrast, the previous SOTA in Isabelle, Subgoal-XL, only achieves 56.1% using 16384 queries per problem).
We also implement a Lean 4 version of ProofAug that can improve the pass@1 performance of Kimina-Prover-Preview-Distill-1.5B from 44.3% to 50.4% on miniF2F-test. 
Our code is available at https://github.com/haoxiongliu/ProofAug.

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Haoxiong Liu
Jiacheng Sun
Zhenguo Li Andrew C Yao 1.
Abstract
1. Introduction
The synergy between deep learning models and traditional automation tools, such built-in tac- ties of the proof assistant and off-the-shelf auto- mated theorem provers, plays a crucial role in developing robust and efficient neural theorem provers (NTPs). However, for proof synthesis with LLMs, previous work applies automation tools either only when explicitly invoked by the model at single granularity level, failing fully exploit their power. To solve this issue, we propose ProofAug, a procedure that equips LLMs with automation methods at various granularities through fine-gres greigga structure analysis of model- generated proof proposals. ProofAug also serves as versatile plug-and-phl module that seam- lessly integrates with any tree-search algorithm, enabling our construction of an efficient recursive proving (ERP) module to further enhance perfor- mance. The superiority of our method is validated on the miniF2F benchmark using the open- spencsource deepseek-mane math-77b-bscc model and the Isabelle proof assistant. Notably, by additionally employ- ing a mixed prompting strategy, we achieve a cumulative pass rate of 66.0% after curation of the dataset (61.9) 1.% for the original version) with at most 2100 queries to the model per problem (In contrast, the previous SOTA in Isabelle, Subgoal- XL (Zhao et al., 2024), only achieves 56.1% us- ing 16384 queries per problem). We also imple- ment Lean 4 version of ProofAug that im- prove the pass @1 performance of Kimina-Prover Preview-Distill-1.5BB from 44.3% to 50.4% on miniF2F-test. Our code is available at https: www./////wwiooooooooo.oooooooooa
Automated theorem proving is field that not only appeals to mathematicians looking for efficient formalization and proof automation for mathematical theorems, but also finds significant applications in real-world industries such as inte- grated circuit design and software engineering (Bibel, 2013; Schumann, 2013). Early applications of machine learn- ing methods on automated theorem proving focus on tasks such as premise selection (Irving al., 2016) and proof search (Loos et al., 2017) in SMT solvers resolution/- superposition provers, often interleaved with handcrafted heuristics. Recently, rapid progress in mathematical rea- soning with large language models (LLMs) has awoken a flourishing interest for directly synthesizing formal proofs using generative language models.
In literature, there are primarily two paradigms for direct proof synthesis: the proof-step generation paradigm and the whole-proof generation paradigm, each corresponding to a distinct proof style. For proof assistants where proofs are mainly in the procedural style (or tactic-style), such as MetaMath (Megill & Wheeler, 2019) and HOL Light (Harri- son, 2009), previous work adopts the proof-step generation paradigm (Polu & Sutskever, 2020; Lample et al., 2022; Han et al., 2022; Polu al., 2022), where in each iteration the model is requested to generate one tactic to be applied in the interactive theorem prover (ITP) Then the ITP provides information on the updated proof state, which sometimes could be indispensable for people to finish the remaining proof. Proof-step generation methods typically use tree- search algorithms guide the proof process. inspired by the success of AlphaGo (Silver et al., 2016). In contrast, for proof systems where declarative style proofs are common, such as Isabelle and Lean 4, computation-efficien whole- proof generation methods become possible. However, the efficiency in this paradigm is not free. Any incorrect appli- cation of a proof method that bridges the gap between two proof terms (or goals/conjectures) will cause the proof to fail to pass the ITP verification check.
github. com hww.iiaoiiiiooooooo ongl wu/proo FAug.
'Institute for Interdisciplinary Information Sci- ences. Tsinghua University "Huawei Noah's Ark Lab Shhnghaa Qi Zhi Institute. Correspondence to: Haox- iong Liu <liuhx20@mattn wel.22@@aii..tsinnnnee www.ssssiinnuuuuenm.m Zhenguo Li <li.zhenguo @ huawei.com>>
We use the terms 'interactive thcorem prover' and 'proof assistant' interchangeably with a nuance: the former emphasizes the formal system aspects, while the latter highlights its role in assisting users.
Proceedings of the 42nd International Conference Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
To avoid this issue, the Draft, Sketch, and Prove (DSP) framework (liang et al., 2023) proposes to let the model first write formal proof sketch (Wiedijk, 2004) according to an informal proof draft, then offload the proofs of in- termediate conjectures to off-the-shelf ATPs² and heuristic proof methods. Many subsequent works (Wang et al., 2023a; Zhao et al., 2023; Zheng et al., 2024; Zhao et al., 2024) also follow the practice of DSP when designing their few-shot prompts: The proof methods in the original proofs of the demonstration examples are replaced with a placeholder, which signifies that ATPs are responsible for completing the task. We observe that while this approach can signifi- cantly enhance performance compared to direct full-proof generation, it may also result in proof failures in unintended ways:
issue in the first place. For the generated proof proposal, we first find its corresponding maximal compatible semi- proof (MCSP) that maintains most structural information yet can pass the check of ITP. Then, departing from it, we recursively resort to a more coarse semi-proof whenever ATPs fail to fill in some gap in the current one. This proce- dure solves the 'Complicated Draft' issue, thus significantly improving the sample efficiency. We call this procedure ProofAug. Figure 1 shows an example flow of our method.
We also demonstrate that the application of proof structure analysis is not restricted to single- single-pass generation. In fact, ProofAug can be incorporated into any tree-search algorithm to expand the candidate node set at each iteration. This will become evident in our unified view of theorem proving introduced in Section 2.1. In Section 3.3, we illustrate its application in constructing sample-efficien recursive proving (Wang et al., 2024) module on top of ProofAug.
(Hard Conjectures) In DSP, the in-context learning ability of LLMs makes them follow the style of the few-shot prompt to generate rough sketches according to the informal proof, refusing to dive into the neces- sary details. As a result, the generated intermediate conjectures could be too hard for ATPs to solve.
We list our contributions with corresponding key evalua- tion results below. All experiments use the open-source deepscek-male math--b-bbscc model (Shao et al., 2024) if not otherwise specified.
(Complicated Draft) Due to common inconsistencies between informal proof and formal system, there are conjectures that despite being easy to be solved by ATPs, humans need to write complicated informal proofs for them. The unnecessary intermediate steps could be translated into formal conjectures that are in- appropriate in syntax even harder than the original theorem.
We propose a versatile plug-and-play procedure ProofAug that can significantly enhance the perfor- mance of neural theorem provers, based on fine iin-grrined proof structure analysis. On minis2F-ttstt (Zheng et al., 2021), ProofAug achieves a pass rate of 52.5% with no more than 100 queries to the model. Abla- tion results show that when compared with the DSP baseline, the improvement brought by ProofAug imple- mentation for Isabelle is 7.8%, 4.1 and 3.3% under sample budgets of 1, 10 and 100, respectively.
Here, a dilemma appears. On one hand, instructing the model to produce rough sketch increases the risk of miss- ing critical details, making it challenging for ATPs to bridge the gaps. On the other hand, directing the model to gener- ate highly detailed sketches can exacerbate formalization issues. Neither way is ideal for fully leveraging the power of off-the-shelf automation methods.
ProofAug can be incorporated into any tree-search al- gorithms under our unified view of existing genera- tive LM based theorem proving methods. We show- case that when integrated with our Efficient Recursive Proving (ERP) module, O-shot ProofAug performance improves from 54.5% to 56. 56.1% with a limit of 500 queries per problem. For comparison, RMaxTSS (Xin et al., 2024b) only shows an advantage of < 0.2% over naive single-pass retrying under a sample budget of 3200.
In this paper, we propose to address this dilemma through performing fine-grained structural analysis on the proof proposals generated by LLMs, based on the observation that regardless of correctness, full proofs contain rich struc- tural information from which valid semi-proofs* of varying granularities can be derived. Specifically, given a theorem statement, instead of instructing the model to generate proof sketch as previous work does, we choose to start from generating a full proof to suppress the 'Hard Conjectures'
Moreover, using a mixture of strategies with different prompting methods, we achieve a total pass rate of 61.9% within 1700 model queries. After curating the miniF2F-test data, we manage to prove 66.0% of the theorems with no more than 2100 requests, setting new state-of-the-art across methods using the Isabelle proof assistant.
FFor simplicity, we follow the practice of Jiang et al. (2023) to use the abbreviation ATP to refer to any automated method, including SMT solvers and what traditionally known as automated thcorem provers.
We also build a Lean implementation of ProofAug and
'We refer the readers to Appendix B for two concrete examples
that illustrate these two issues.
'We use 'miniF2F-test to refer to the miniF2F test split Isabelle data included in the code repository of Jiang et al. (2023). See Section 4.1 for detailed discussion on the versions of miniF2F.
'By semi-proofs, we refer to proofs that possibly contain sym- bols indicating pending proof, such as sorry in Isabelle and Lean.
2

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Coopeneed
Conjectore 2
Conjecture
Proof method
Conjecture
Step into/out block
Cesjechue1
Conjecture
Conjecture
Eagjrtes
to next proof step
Cogaster
Hil
Red: Failed
Green: Passed
Cusjecsuo
Coejectoe
Corjechre
Orange: Posiponed
OLD
QB.
QU-
[a)
(b)
(e)
Thaoren Stemmnng
Conjectan
Suavesse
Therre
Corjecture
Theoren
Thereem
CapateckE
CAT
proof
<AT
Conjecuro
Corgecture
Corjectore
Certeree
mirpltion praw
Conpetiue
Cesjethur
Cappttar 2
QRI
QBa
(d)
(2)
Figure 1: Illustration example of ProofAug. Each box in the flowchart corresponds to a proof step. (a) The initial proof encounters an error when proving Conjecture 1-0. (b) We replace the original proof of Conjecture 1-0 with a sorry and continue, until syntactic error occurs Conjecture 1-1. (c) The proof of Conjecture is replaced by sorry and we obtain semi-proof with two sorrys. (d) Automation tools called to prove Conjecture 0 and Conjecture 1, but failing the
latter one. (e) The ERP module (introduced in Section 3.3) sends completion request Conjecture 1. (I) The generated ERP proof still fails at Conjecture 1. (g) We finally resort to more coarse level of proof and successfully find proof with automation tools. Refer to Algorithm 2 for a pseudo-code description of ProofAug.
shows that the pass @1 accuracy of Cimiina-Prover- miniF2F-test can be improved from 44.3% to 50.4%, exhibiting the generality of ProofAug for various proof systems.
T: S x S is the state transition function of the ITP.
For any string E Σ", we use 8 to denote T(so, 2),, where we have lifted the notation T to express consecutive state transitions, i.e., for s E S,
2. Preliminaries
T(8, = am)) T(: 1)) 1))................... c.... ........... ((,,
2.1. A Unified View of Theorem Proving with Generative Language Models
if Parse(x) = (a(1), a[2), ... ,.fn))
We first formulate the task of theorem proving in the context of language modeling and introduce our notations. We assume there is a global alphabet Σ. An ITP is formulated as triple S,)), where:
Given a theorem statement (with context) 2y Σ*, we say yʃ E Σ' is proof of x if Szyllyy -inishh = True, where || denotes the concatenation of two strings. A generative lan- guage model (with a decoding strategy) is a map that outputs a distribution x (-12x) on Σ* when conditioned on a prompt x E Σ' response is a sample y ~ T(-(z). The task of theorem proving is to find proof yy of the given theorem statement xy using the black-box distribution generator Some benchmarks also provide a corresponding informal statement x; and informal proof y/ for each theorem.
A C E- is the set of proof steps. There is also a parser Parse: Σ - A" that transforms a string into a sequence of proof steps.
S is the set of states. A state s E S represents our ab- straction of the proof object underlying the ITP, which contains all information the ITP needs to proceed with the proof, including s.state, s.error, s. sfnissh, etc., varying depending on the specific ITP environment. Additionally, there is special element sp, which rep- resents the initial state.
We state our unified view of existing generative- -aarriiee-L---aare LM-based theorem proving methods as follows. In each round, an algorithm completes three steps:
1. (State Selection) Select state to work with in this round. (Prompt Formation) Form a prompt and present it to
AA" denotes the set of all finite lists (or sequences) of elements from A, including the empty list.
3

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Table 1: A summary of current theorem proving methods using generative language modeling under our unified view, including DSP (Jiang et al., 2023), LEGO-Prover (Wang et al., 2023a), Lyra (Zheng et al., 2024), GPT-f (Polu & Sutskever, 2020), HTPS (Lample et al., 2022), ReProver (Yang al., 2023), Lean-STaR (L.in et al., 2024), POETRY (Wang et al., 2024), RMaxTS (Xin et al., 2024b). We use the terms node and state interchangeably.
Method State Selection
Prompt Components
Expected Output
Response Processing
Single-pass generation methods
Naive
Always Say
full proof
verify the proof in ITP call ATPs to fill the gaps call ATPs + update skill library tool correction call ATPs
DSP
Always Sxy
zf informal draft
proof sketch
LEGO
Always Say
r draft + skills
skill comple. proof sketch
Lyra
Always Bag
Ji last attempt error
proof sketch
Proof-step generation methods
GPT-f
max logprob goal max PUCT value goal
the selected goal the selected goal retrieved prem. ps proof state context + proof state context + proof state
tactic tactic
expand the goal- roal-based search tree expand and backprop the hypertree expand the state- based search tree proceed the step in ITP update the recursive proof tree add new node for cach valid step
HTPS
ReProver
max logprob state
tactic
Lean-STaR
current state
a proof step with rationale proof step (with 'sorry") proof completion
POETRY
max logprob state discounted UCB
RMaxTS
Ours
ProofAug
Always Sxy the first ATP failure
+ informal draft context + proof state
a full proof proof of this conjecture
FindMCSP + Proof Augmentation
ERP
new nodes for each block
the model.
theorem " ((AA - B)
A) A"
3. (Response Processing) Use the response of the model to interact with ITP to generate new states.
proof
assume (A B)
A
show A
Compared typical views of tree-search algorithms, our ap- proach integrates their expansion step and proppaaatattionn step with the process of interacting with the ITP into a sin- gle response processing module. We isolate the prompt formation procedure into a single module to emphasize its importance, as proof-step generation methods and whole- proof generation methods differ fundamentally at this point. Besides, this allows to place not only these two lines of work, but also methods that lie in between, under unified view.
proof (rule classical)
assume "- A"
have "A - 3" proof
assume
with (- A) show B by contradiction
qed
with ((A B) A) show ... qed
qed
Table 1 summarizes and compares different methods under this view. Our view disentangles the different modules of algorithm design, naturally motivating us to optimize exist- ing algorithms the module-level. Our method ProofAug, which will be introduced in Section 3.2, is a procedure belonging to the response processing step. Thus, can integrate effective practices in other modules with ProofAug to make further improvements. We showcase such an ap- plication in Section 3.3. Moreover, since the goal of theo- rem proving is to improve the overall pass rate rather than the success rate of each attempt, an appropriate 'portfolio' of different strategies for each module could significantly improve the pass rate than single strategy. Such a phe- nomenon has been observed in the CoT & non-CoT mode combination (Xin et al., 2024b; Zhao et al., 2024). In Sec- tion 4.4, we explore this idea across additional combinations
Figure 2: An example proof in Isar with hierarchical proof...qed block structures.
and demonstrate its superiority.
2.2. The Isabelle/saar Proof Language
Although the basic idea of our method in general fits any ITP, the implementation details vary depending on specific features of the proof assistant. In this paper, we use Is- abelle/Isar (Wenzel al., 2004) as an example introduce the spirit of ProofAug and how to implement it in spe- cific proof system. In this section, we introduce some basic knowledge and unique features that ease the implementation
See Appendix C for a detailed explanation of why our method is generic across different systems and a brief summary of our Lean implementation.

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
of our method in Isar.
Algorithm Find the Maximal Compatible Semi-Proof
The specific object corresponding tion formulated in Section 2.1 is Isar/VM transition. The transitions are typed with different modes, including proof(prove), proof(state) and proof(chain). We find that identifying the mode proof(prove) particularly useful for the analysis of proof structure since indicates that a goal has just been declared and the next proof step is required to contain a proof method. In Isar, proof methods are only allowed to be invoked after the keywords proof and qed. As a result, a typical proof in Isar is organized by hierarchical proof...qed blocks.
'state' abstrac-
Input: initial proof vf. ITP (A)
a + Parse(y])
s <- Null] x len(a)
> States before each step
1, StAss f 1, 50
while len(a) do
s[i] t Sthie
Sneat T(Sthis; ali))
if Snent. then
if Sthis = proof(prove) then
a(i] t- sorry
else > Error in other modes, skip the block
block + InnermosiBlock((, a)
Figure shows an example of Isar proof. Users are allowed to have or show are keywords that Isabelle allows to appear in the proof(state) mode to introduce new local goals. To prove goal with some proof method m, one single clause 'by m', which is an abbreviation of 'proof m qed'. The other keywords, assume and with, serve exactly the same purpose as they do when used in natural language proofs. Benefiting from the above properties, Isar proofs are readable even for people unfamiliar with Isabelle, thus easy to be analyzed just like how we analyze the structure of informal proof.
if block Null then
return Null afi] not in any block, terminate end if
(tt. a blblokk.edd t sorry
1)] +- Null
i, Sthis t block.end, sundsssblon s/block.start end if else
i, Sthis f- i 1, Sneat end if end while if finish then
Finally, we specify the attributes we can access from state through the ITP environment used in this work. We can have proof state string s.state that corresponds to the "proof state' Isabelle shows to the user, a corresponding mode s. mode, a list of all available facts s.facts that can be obtained by the print_ facts command in Isabelle, and two boolean-type attributes s.error and s.finish indicating whether 'an error has occurred' and whether 'a theorem is proved', respectively. We say = $2 for two states 81, 82 E S if all the values these five attributes are equal.
return Concat(a) end if
semi-proof y is compatible to 7/ if each sorry in matches proof...qed block a by clause in v/ and the remaining parts are equal. Thus, by MCSP, we refer to the particular compatible semi-proof لرو from which all compatible semi- proofs (w.r.t. B9) can be obtained by substituting some proof...qqd blocks or by clauses of y with sorrys.
3. Method
Algorithm 2 describes our method, ProofAug. It mainly consists of three parts: finding the Maximal Compatible Semi-Proof (MCSP), proof augmentation, and an optional Efficient Recursive Proving (ERP) module, In this section, we state each of them in detail. For an illustrative walk- through example of ProofAug, refer to Figure
The FindMCSP routine is descrihed in Algorithm 1. Firstly, v is parsed into sequence of proof steps Then we create a pointer i indicating the current position and an array indicating the states before the ith step. In each iteration, we first try to proceed the current proof step a[i] from the current state s|i] in the ITP. this step succeeds, we continue to the next proof step; otherwise, according the proof mode of s(i], we take different strategies: if s mode is proof(prove),
3.1. Find the Maximal Compatible Semi-Proof
Given a proof proposal of sampled from क (-1p(x;llus x))) (where .) is a few-shot/zero-shot prompter that ap- propriately combines its arguments), the first procedure of ProofAug is to find the Maximal Compatible Semi- Proof (MCSP) of vf-
replace ali] with sorry; otherwise, find the innermost proof...qed block of y that contains the i-th step and substitute the whole block with a single sorry step, then move the pointer accordingly. The algorithm terminates when a failed step occurs outmost or all steps pass the check of the ITP.
We first explain what the MCSP is. Recall that a semi-proof refers to a proof that possibly contains sorry steps. We say
5

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Algorithm 2 Proof Augmentation (ProofAug)
we encounter a sorry step as we progress with the proof, we try predefined set of Isabelle built-in heuristic methods and Sledgehammer to find a proof of the current goal. This procedure can be seen as a special proof method <ATP> created by us, similar to the built-in proof method try. If this <ATP> method fails, we can rule out the possibility that the final proof contains the innermost proof...qed block in which this sorry lives and replace the block with sorry. We iteratively perform this operation until we finish the proof, or the semi-proof degrades into single sorry step and <ATP> fails to directly prove the original theorem.
Input: theorem statement y,,, informal statement & draft 2y Me prompter p(t:)), LM <T--)), ITP (A
0f ~ (-lp((zillv; (
> Sample an initial proof & Apply Algorithm
< Parse(FindMCSPP(())
[Null] x len(a)
2, Sthie < So
while < (en(a) do
Speat f T (S ali))
if a[i] + sorry then
error= False
else
For a concrete example of ProofAug inducing a proof from a failed initial proof proposal, refer to Appendix I.
error + TSthis: <ATP>).error
>
Try ATPs
end if
if error and usEE then
> ERP module
3.3. Efficient Recursive Proving
stt f a []]lsuss--saat state vf ~ < =/1 )
Solving a complicated theorem from a single proof proposal generated by the language model π (-1--) (-) is challenging even with our ProofAug procedure. By simply sampling more proof proposals, we can probably get better results as long as there is some randomness underlying the decoding strategy of и. We ask the question: how can we outperform this naive retrying strategy, given fixed sample budget?
if ( vf) ) = Snezt then alil, + ff. False
else
yf + FaileedTaciissAATPP
if T(shiin uff) = neet then
error + vf. False
end if
On miniF2F, Wang et al. (2023a); Zheng et al. (2024) achieve better performance than the naive approach by mak- ing use of the previous error messages or proved lemmas in the previous attempts of proof'. Nevertheless, these meth- ods all belong to the whole-proet generation paradigm and benefit from the strong instruction-follwiin ability of GPT- series models. Here, we are more interested in going beyond whole-proof generation to investigate whether tree-search methods used in the proof-step generation paradigm can help improve the sample efficiency.
end if
end if
if error then
> Resort to the last level
block <- IInermostBlock(i, a)
if block is Null then return Null
a jillokk bblock..tart..blocceeeee - 1)] t Null
a [block.end] + sorry
i, Sthis + block.end, siblock.
else
Sthia + i 1, Snezt end if end while
To the best of the authors' knowledge, RMaxTS(Xin et al., 2024b) is the only successful attempt to integrate some tree- search algorithm with whole-proof generation. However, the advantage of RMax only becomes clear when the sample budget comes to 4 x 6400. Our explanation for this inefficiency is that, for proofs that deviate from the correct paths at a very early stage, RMaxTS could spend much time in searching after the proof steps that have already misled the direction of proof. We argue that this can be largely avoided if we can first check whether the proof pro- posal forms a valid reasoning path. POETRY et al., 2024) is a top-down approach that satisfies this property through fine-tuning the model to never step into the next proof level. However, POETRY falls in the proof-step gener- ation paradigm and requires fine-tuning the model follow their special proof-step generation strategy.
return Concat(a)
> The final proof
3.2. Proof Augmentation
The goal of ProofAAg is to determine whether there exists a compatible semi-proof that can be completed into a valid proof using ATPs or built-in heuristic proof methods to fill the sorry gaps. Instead of first finding out all compatible semi-proofs and trying them sequentially, we should design more efficient way that makes use of the overlap among these semi-proofs to avoid waste of computation resources spent on calling ATPs. The resulting proof augmentation algorithm is shown in Algorithm 2 (Ignore the ERP module for now).
In order to achieve more sample efficient and fine-tuning free recursive proving method, we design our algorithm in a modularized way under the unified view described in
Specifically, we first parse the MCSP and create a pointer and a corresponding state array as in Algorithm 1. When
6

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Section 2.1. Firstly, for the prompt design module that deter- mines the expected output content, we borrow the proof com- pletion module of RMaxTS to replace the proof-generation step of POETRY; then, for the response processing module, we perform proof structure analysis as in the proof augmen- tation procedure and try <ATP> for the failed proof...qed blocks or by clauses. A new node is added if the <ATP> method fails solve the corresponding conjecture. For the state selection strategy, we follow the best-first strategy, but the priority is modified from the cumulative log-probability to the end position of the failed proof block, i.e., if one node is an ancestor of another, we prioritize the descendant; otherwise, we prioritize the one that appears first in the semi-proof.
for each problem compared to the OpenAl miniF2F 9. While both versions contain many mistakes and various extents of inaccuracies in the formal statements, previous work (Wang et al., 2023a; Zheng et al., 2024; Wang et al., 2024; Zhao et al., 2024) in general chooses to use this DSP-version for a fair comparison between different methods. Thus, in order to show the superiority of our ProofAug, we first fol- low previous work do experiments on the DSP-version miniF2F-test.
However, as the performance of neural theorem provers has significantly improved recently, the ratio of unprovable theorems resulting from the mistakes to the total number of statements that provers fail to provide proofs becomes no longer ignorable, and is one of the possible reasons that ssabelle-basee provers have fallen behind Lean-based ones this cross- tross-anggaage benchmark. So, we build curated dataset and part of our experiments are done on the curated version." 10
In practice, to simplify the algorithm and suppress the sam- pling cost wasted in low-level details, only try <ATP> and add new nodes for failed conjectures belonging to the original MCSP. Such simplifications make the above procedure become a plug-and-play ERP module over our ProofAug, as shown in Algorithm 2. This coincidence can be interpreted as that each conjecture naturally inherits one proof try from the original proof proposal. In other words, the ProofAug without ERP module is already implicitly recursive proving method, in the sense that each compatible semi-prod proof exactly corresponds to one proof tree during the search process of POETRY if the two methods share the same final proof.
4.2. Experimental Setup
The Isabelle version we use is Isabelle2022. We use the PISA environment (Jiang et al., 2021) to inter- act with Isabelle. Our <ATP> method is the combi- nation of 8 Isabelle proof methods (auto, simp, auto, blast, fastforce, eval, sos, arith, simp:field,simps simp add:mod simps) and Sledgehammer. Following Jiang et al. (2023), we set the timeout for any proof step and Sledge- hammer as 10s and 120s, respectively. During verifica- tion, we run 12 PISA instances in parallel on one In- tel(R) Xeon(R) Gold 6326 CPU @ 2.90GHz
For an illustrative example of how the ERP module works in ProofAug, one can refer to Figure
4. Experiments
The language model we use across all our experiments is deepseek-math math-7b-base (Shao et al., 2024), run on Nvidia GeForce RTX 3090 with vLLM (Kwon al., 2023). Unless otherwise specified, we follow Jiang et al. (2023) to use sampling temperature T 0.6 with top-p 0.95. The default max number of tokens of the response is set to 2048, and when the length of the prompt exceeds 2048, we adjust the max number of tokens to 4096 #token of the prompt.
A summary of our experimental results and comparison with previous methods is shown in Table 2. Below, we state the experimental setup and describe how different parts of the results are obtained and provide additional ablation study results. For the results in Lean implementation, please refer to Appendix C.
4.1. Benchmark
For few-shot prompting (and similarly for zero-shot prompt- ing), we prepare few-shot examples that are the same as those of Jiang al. (2023) except that the proof sketches are modified to new full proofs written by us. For n-shots
We evaluate methods the Isabelle part of miniF2F (Zheng et al., 2021), a benchmark for formal Olympiad-level mathematics problems across four differ- ent formal languages. Unless otherwise specified, we use 'miniF2F-test' or 'the original version of miniF2F-test' or 'the DSP-version miniF2F-test" to refer to the dataset in- cluded in the code repository* of Jiang et al. (2023), which provides an additional informal statement and informal draft
Phttps:/ wwtphhh....co.aaaaaaaaaaaaamaaaa main/ issbeele
"You can find our curated version here: https:// github. con i isabelle_sse wwtp/atteette///eeeeeeeeeeeeeeet wttp://ttteiiiiittttttt-e-eee-ee curettedd jsoni. See also Appendix H for the details of how we curate miniF2F
hhttps://githut com/co///////.. 1ibttti ang/draft. draft_ sketch grove/blcb/natt waaiaaaaiinnneaeeeeeeaaeaaeeeeee aaligedddd problens/ new pew_complete mini. isonl
"To reproduce our results, using the same CPU necessary requirement. See Appendix D for more discussion on the repro- ducibility issues.
7

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Table 2: Comparison of methods using Isabelle as the proof assistant on MiniF22-tesst For BFS methods, the sample budget x S corresponds to N attempts of S expansion with T iterations. As to tree-search methods, it becomes N T, with the same meanings for the symbols. Results with 't' are obtained using mixed strategy.
Method
Model
Sample Budget
miniF2F-test
Methods using Isabelle
DSP (Jiang et al., 2023)
CodeX Fine-tuned Llama-SB
100
39.3%
Subgoal-XL. (Zhao al., 2024)
64
39.3%
16384
56.1% %
LEGO-Prover (Wang et al., 2023a) Lyra (Zheng et al., 2024)
mixed GPTs GPT-4
100
50.0%
100
47.1%
51.2%
POETRY (Wang et al., 2024)
Fine-tuned ProofGPT (1.3B)
1 x 32 x 128
42.2%
Our Experiments (using Isabelle)
DSP baseline
deepseck-matt-77-bel
28.7%
40.6%
100
49.2%
ProofAug
deepseek-math- 7b-bas
7.8%)
10
44.7% (+4.1 1.6)
52.5% (43.3%)
ProofAug (0-shot) ProofAug (0-shot) + ERP
deepseek-mane -abbbbb-ae 7b-base
500
54.5%
deepseek- mateee--ttth-------a 7b-bee
500
56.1% %
ProofAug + Mixed Strategy
deepseek-mane maateeekk-mt------ase bb-bae
1400
61.9%
ProofAug + Mix. Dataset Curation
2100
66.0% %
Methods using Lean
HTPS (Lample et al., 2022)
Evariste (600M)
64 x 5000
41.0%
RMaxTS (Xin et al., 2024b) BFS CG (Wu al., 2024)
DeepSeek-Prover-VV VI.5RL (7B)
32 6400
63.5%
InterL.M2.55 Strepp.....-SeeProoerrr (7B)
256
600
65.9%
prompting, we randomly sample n examples from the candi- dates. By default, we use 1-shot prompting. See Appendix E for our specific prompt text, the reason for choosing 1-shot, and more details on the prompt construction process.
100.
For multiple attempts of proof, we record the checked semi- proofs and skip them when obtaining them in the subsequent attempts. This, in fact, harms the final performance since some tactics and Sledgehammer do not always give the same result under the same conditions. Nevertheless, this practice can help us significantly reduce the elapsed time of the experiments.
#Proved Theorems
Our prompt ProofAng
60
Our prompt
DSP prompt ProofAug
DSP
40
0-shot ProolAng
0-shot
20
4.3. Results of ProofAug
20
40
60
100
Number of Attemps
We do ablation studies to validate the effectiveness of ProofAug (without the ERP module). We first get the DSP baseline results our setting. Compared the performance 2iniF22-ttst, our
Figure 3: Ablation of three different prompting ways.
of the original DSP implementation DSP baseline is 9.9% higher (49. 2% 39.3% in 100 at- tempts) due to differences in proving environments choice of the prompting methods and model selection. Then we compare ProofAug results with our DSP baselines. Under sample budgets of 1, 10 and 100, ProofAug achieves per-
formance of 36.5%, 44.7% and 52.5%, significantly outper- forming the baseline by 7.8%, 4.1% and 3.3%, respectively.
Note that ProofAug also be applied to the proof sketches generated by DSP. Figure 3 shows how the number of proved theorems changes as the number of attempts in- creases w/ or w/o ProofAug for three prompting methods: DSP prompting, full proof prompting, and the more token- usage friendly zero-shot prompting. By w/o ProofAug,
See Appendix D for discussion on the differences of theorem proving environment between ours and that of Jiang al. (2023).
8

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
mean the 'Prove' step in DSP, i.e., <ATP> tried at the sorrys in the proof sketch. It be seen that while the performance of our few-shot prompting and zero-shot prompting w/o Puo is much lower than that of DSP prompting, ProofAug helps them achieve a comeback. This justifies our choice of generating full proofs instead of proof sketches.
through its ability to operate across various granularities and the fallback mechanism. Robustness is highly desirable property for systems lacking inherent verification mecha- nisms, such as informal mathematical gubblem-ollvnng and software engineering. Therefore, we are also highly inter- ested in exploring the effective application of ProofAug in these domains.
4.4. Results of the ERP module
Impact Statement
We tr 500 attempts of proof for each problem, using zero- shot prompting for ProofAug w/ and w/o ERP module. When the ERP module is turned on, we record the cumula- tive number of queries and stop verifying when it reaches 500 for fair comparison.
This paper presents work whose goal is to advance the field of Machine Learning. There are many potential societal consequences of our work, none of which we feel must be specifically highlighted here.
The result shows that the ERP module can bring an extra 1.6% performance gain. If we do not restrict the number of queries, we can achieve a pass rate 57.4%(+2.9% compared to the ProofAug without ERP).
References
Avigad, J.. De Moura, L., and Kong, S. Theorem proving in lean, 2021. URL htt.htt///eeeaprroeeee hawpaaaprreeee.ttthhh.o git..b. wo/theoree__provingg.toot
4.5. Cumulative Results of Mixed Strategy Experiments
Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliätre, J.-C., Giménez, E., Herbelin, H., et al. The coq proof assistant reference manual. INRIA, version, 6(11), 1999.
During the completion of this work, we have tried various se- tups to search for the best recipe. While some setups fail to achieve the best performance on the benchmark compared to results present above, diverse ways of generating proofs help prove more theorems. The setups include: 1) Different versions of prompts. We have three versions of demon- stration examples for few-shot prompt generation, and two versions of zero-shot prompt are used in our experiments. 2) Whether to include Informal drafts. The informal drafts could mislead LLMs. Although ProofAug can sometimes be rescue, it is not always the case.
Bibel, W. Automated theorem proving. Springer Science & Business Media, 2013.
Dong, K., Mahankali, A., and Ma, T. Formal theorem proving by rewarding ilms to decompose proofs hier- archically, 2024. URL https: htttps://arxi...... /ttp///awivo..//.aeee//./..ooeee abs/ 2411. 01829.
First, E., Rabe, M. N., Ringer, T., and Brun, Y. Baldur: Whole-proof generation and repair with large language models, 2023. URL https: /aaxiaa..ooorr//.. abs/ 2303.04910
In total, we try each problem of the original miniF2F-test under a sample budget of around 1400 in total, and 2100 for the two versions in total. See Table 3 in Appendix F for a breakdown of these two numbers. On the original miniF2F- test, we solve 61.9% of the problems, which 5.8% higher than the previous Isabelle SOTA. On the curated version, the solving rate comes to 66.0%.
Goertzel, A., Jakubúv, J.,, Kaliszyk, C., Olšák, M., Piepen- brock. J., and Urban, J. The isabelle enigma, 2022. URL attps://arxer org/ hbt://bs/22200 2205 01981.
Han, M., Rute, J., Wu, Y., Ayers, E. W., and Polu, Proof artifact co-training for theorem proving with lan- guage models, 2022. URL https://arxiv.. 211222222.2.....
5. Discussion and Future Directions
Although this work demonstrates that our ProofAug method significantly improves the performance of the neural the- orem prover on the miniF2F benchmark, there remains notable gap in tackling IMO-level problems or research- level challenges within formal systems. How to incorporate ProofAug into expert iteration methods (Xin et al., 2024a) or online learning methods (Lample et al., 2022) to further improve the performance is one direction of future work.
Harrison, J. Proof style. In International workshop on types for proofs and programs, pp. 154-172. Springer, 1996.
Harrison, J. Hol light: An overview. In International Conference on Theorem Proving in Higher Order Logics, pp. 60-66. Springer, 2009.
We believe that another important direction for future work fully leverage the robustness introduced by ProofAug
Irving, G., Szegedy, C., Alemi, A. A., Eén, N., Chollet, F,, and Urban, J. Deepmath-deep sequence models for

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
premise selection. Advances in neural information pro- cessing systems, 29, 2016.
Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. Formal mathematics statement eur- riculum learning, 2022. URL ptttps://arxiv...t
Jiang, A. Q., Li, W., Han, J. M., and Wu, Y. Lisa: Language models of isabelle proofs. 6th Conference on Artificial Intelligence and Theorem Proving, 2021.
abs / 2202.22222222 01344.
Schumann, M. Automated theorem proving in software engineering. Springer Science & Business Media, 2013.
Jiang, A. Q. Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M.. Lacroix, T., Wu, Y., and Lample, G. Draft, sketch, and prove: Guiding formal theorem provers with infor- mal proofs, 2023. URL https::///// http://axvvvv..//o wwwp:iii.orr..oooooo abs/ 2210. 12283.
Shao, Z., Wang, P., Zhu, Q., Xu, R., Song. J., Bi, X., Zhang, H., Zhang, M., Li, Y. K., Wu, Y., and Guo, D. Deepseekmath: Pushing the limits of mathemat- ical reasoning in open language models, 2024, URL https: http/vaaivvv/v.a///iv///..a...aa org. wwaaaassaaa 22202240.3333
Kwon, W., Li, Z., Zhuang, S., Sheng, Y., Zheng, L., Yu, C. H., Gonzalez, J. E.., Zhang, H., and Stoica, I. Efficient memory management for large language model serving with pagedattention. In Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles, 2023.
Silver, D., Huang, A., Maddison, J., Guez, A., Sifre, L., Van Den Driessche, G., Schrittwieser, J., Antonoglou, Panneershelvam, V., Lanctot, M., et al. Mastering the game of go with deep neural networks and tree search. nature, 529(7587):484 488 2016.
Lample, G., Lacroix, T., Lachaux, M.-.,, Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. Hyper- tree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337-26349, 2022.
Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., and Chaud- huri, S. An in-context learning agent for formal theorem- proving, 2024. URL https: arxiv org/ /bs/ 2310 04353.
Wang, H., Xin, H., Zheng, C., Li, L.,, Liu, Z., Cao, Q. Huang, Y., Xiong, J., Shi. H., Xie, E., Yin, J., Li, Z., Liao, H., and Liang, X. Lego-prover: Neural theorem proving with growing libraries, 2023a. URL https: / //a //arxiv.com wwgoorgg///oo abs /a.bbb//// 2211 10.00..0 00656.
Limperg. J. and From, A. H. Aesop: White-box best- first proof search for Ican. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 253-266 2023.
Lin, H., Sun, Z., Yang. Y., and Welleck, S. Lean-star: Learning to interleave thinking and proving, 2024. URL https:/ /arxivv.vvvv org/ abs 007 10040.
Wang, H., Yuan, Y., Liu, Z., Shen, J., Yin, Y.. Xiong, J.. Xie, E., Shi, H., Li, Y., Li, L., et al. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume I: Long Papers), pp. 12632-12644) 2023b.
Loos, S. M., Irving, G., Szegedy, C., and Kaliszyk, C. Deep network guided proof search. In LPAR, volume 46 of EPiC Series in Computing, pp. 85-105. EasyChair, 2017.
Lu, M., Delaware, B., and Zhang. T. Proof automation with large language models. In Proceedings of the 39th IEEE/ACM International Conference on Automated Soft- ware Engineering, pp. 1509-1520, 2024.
Wang. H., Xin, H., Liu, Z. Li, W., Huang, Y., Lu, J., Yang, Z., Tang, J., Yin, J., Li, Z., and Liang, X. Proving theo- rems recursively, 2024. URL https: /ttp:///axvvvvvv abs/2405 14414.
Megill, N. D. and Wheeler, D. A. Metamath: A Com- puter Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. URL htt.h:tt//// //us. metamath.orr downloads, belaadd/meetann /ttp//ttttaaa..ammma/maamaa ..f..
Wang. H., Unsal, M.. Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., et al. Kimina-prover preview: Towards large formal reason- ing models with reinforcement learning. arXiv preprint arXiv:2504 1154, 2025.
Mikuta, M., Tworkowski, S., Antoniak, S., Piotrowski, B., Jiang, A. Q., Zhou, P., Szegedy, C., Łukasz Kucifiski Miloš, P., and Wu, Y. Magnushammer: A transformer- based approach to premise selection, 2024. URL https: //arxiv. / abs/ 0aas/2300 2303. ......4444 04488.
Wang, M., Tang, Y., Wang, J., and Deng, J. Premise selec- tion for theorem proving by deep graph embedding, 2017. URL https:tt/////. arxii. v.v.orr worgorrg/ooo //g/////////./...//.// abs 709. 09994.
Wenzel, M. et al. The isabellc/isar reference manual, 2004.
Polu, S. and Sutskever, I. Generative language modeling for automated theorem proving, 2020. URL https: //arxis //aaxivvorrg///..//.////...ooola abs///bs/20099 03393.
Wiedijk, F. Formal proof sketches. In Types for Proofs and Programs: International Workshop, TYPES 2003, Torino,
10

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Italy, April 30-May 4, 2003, Revised Selected Papers, pp- 378-395 Springer, 2004.
Zheng, K., Han, J. M., and Polu, S. Minif2f: cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2 10, 2021.
Wiedijk, F. The seventeen provers of the world: Foreword by Dana S. Scott, volume 3600. Springer, 2006.
Wiedijk, F. A synthesis of the procedural and declarative styles of interactive theorem proving. Logical Methods in Computer Science, Volume 8, Issue 1, March 2012. ISSN 1860-5974, doi: 10.2116//mcc-- //dx. doi org.////g...o....oo 2168 211.//00..1121202022
URL http: (1: 30) 2012.
Wu, Y. Jiang, A. Q., Li, W., Rabe, M. N., Staats, C., Jam- nik, M., and Szegedy, C. Autoformalization with large language models, 2022. URL https: /atp:s///axvvvooo 12615.
Wu, Z., Huang. S., Zhou, Z., Ying, H., Wang, J., Lin, D., and Chen, K. Intermimn2.--stapprooeer, Advancing automated theorem proving via expert iteration on large-scale lean problems, 2024. URL https: /ttp///axxvvv///a org/ / 2410.15700
Xin, H., Guo, D., Shao, Z., Ren, Z., Zhu, Q., Liu, B., Ruan, C., Li, W., and Liang, X. Deepseek-prover. Ad- vancing theorem proving in ilms through laale-scale synthetic data, 2024a. URL https::///// /arp:v.//xxvv.o/// abs/2405. 14333.
Xin, H., Ren, Z. Z.,, Song, J., Shao, Z., Zhao, W., Wang, H., Liu, B., Zhang, L., Lu, X., Du, Q. Gao, W., Zhu, Q. Yang, D., Gou, Z., Wu, Z. F., Luo, F., and Ruan, C. Harnessing proof assistant feed- back for reinforcement learning and monte-carlo tree search, 2024b. URL atttss://axxt www/arrg//.....oooo............. 2408. 08152.
peepseek-prover-ve
Yang. K., Swope, A. M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., and Anandkumar, A. Leandojo: Theorem proving with retrieval-augmented language models, 2023. URL abb/ 15626.
Zhao, X., Li, W., and Kong, L. Decomposing the enigma: Subgoal-bare based demonstration learning for formal the- orem proving, 2023. URL ptttps://axiv.... org/ abs/2305. 16366.
Zhao, X., Zheng, L., Bo, H., Hu, C., Thakker, U., and Kong, L. Subgoalxl: Subgoal- based expert learning for theorem proving, 2024. URL httpttttt///tm htttap:://axxivoooo 0tt//2088.11172
Zheng, C., Wang, H., Xie, E., Liu, Z., Sun. J., Xin, H., Shen, J., Li, Z., and Li, Y. Lyra: Orchestrating dual correction in automated theorem proving, 2024. URL ittps:://rxxt arg/abs/2309 15806.

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
A. Other Related Work
In the main body, Table and Table 2 only include representative neural theorem proving methods that are most related to this work: they all focus on solving Olympic-level mathematical problems with generative language models. Below we introduce other related work.
Premise Selection. One line of work uses embedding models to facilitate the selection of premises for automation tools (Irving et al., 2016; Wang et al., 2017; Goertzel et al., 2022; Yang et al., 2023). The machine-learning enhanced automation tools can be used to strengthen the power of the <ATP> method in our ProofAug algorithm. For example, the et al., 2024) is an ideal substitution for the sledgehammer, whose solving rate on miniF2F is 34.0% (against 20.9% of sledgehammer) and has a mode that does not require GPU or TPU accelerators. We believe that access to such tools can help ProofAug achieve better performance on theorem proving.
Magnushammer
Hierarchical Theorem Proving. We note that the idea of hierarchically proving theorems in declarative ITP systems has been explored in several previous works. Besides the proof-step based recursive proving method POETRY (Wang et al., 2024) discussed in Section 3.3, LEGO-Prover (Wang et al., 2023a) uses a skill library to record the previously proved lemmas and retrieves relative skills when instructing GPT series models to synthesize its proof based on decomposed informal draft. It is hicrarchical proving method in the sense that the lemmas used for proving the current theorem can be built on more low-level lemmas. From another point of view, LEGO-Prover uses all previous queries to solve the current theorem hierarchically. In contrast, Dong et al. (2024) does not record a skill library, but finishes the hierarchical proving from seratch. The key difference between these hierarchical proving methods and our ProofAug (without ERP module) is that we work in bottom-up fashion to best exploit the power of traditional automation tools, contrary to their top-down frameworks that all require extra queries to the model when stepping into the next level proof. We argue that bottom-up fashion aligns more with the pre-trained corpus, thus making best use of the theorem proving knowledge possessed by the model. In contrast, top-down methods require in-context learning or fine-tuning to control the behavior of LMs, which could hurt the intrinsic ability of the model and bring extra complexity to the problem. This is likely the underlying reason why ProD-RL (Dong et al., 2024) fails to make significant improvements over the simple SFT method on miniF2F-test Whereas our ProofAug serves as a play-and-plug module and can fall back to naive single-pass generation, being superior in efficiency, robustness, and flexibility. Moreover, by adding the ERP module, we integrate the top-down and bottom-up fashions in a sample-efficient way.
While finalizing this paper, the authors became aware of concurrent and independent work Lu et al. (2024), which proposes PALM, that shares similar high-level ideas with ProofAug. However, our work is distinct in several key aspects: 1) PALM works in Coq (Barras et al., 1999), a procedural proof language where declarative modes (such as the 'Mathematical Proof Language' introduced in the Coq reference manual) are less common. Since tactics in the procedural style proof languages designed in the spirit that the user decides what tactic to use next by observing the resulting goal or proof state after using the last tactic, it is often the case that new variables facts are introduced by one tactic and the subsequent tactics need to specify the names of these facts. Thus, performing whole-proof generation as PALM does for Coq is generally harder than in the declarative style proofs and could be detrimental to the performance. Besides, in Coq proof', there are few explicit intermediate conjectures or block structures as in those in Isar or Lean 4. Thus, for each tactic, the backtracking procedure of PALM simply goes back to the proof state before the unrepairable error and continues backtracking, except for the bullet point structure that equivalent to the 'case" structure in Isabelle/Tsar (rather than the more common 'have' method). Consequently, the proof's found by PALM mostly show scarce high-level structures as we can observe from the results provided in its code repository 13, In contrast, our ProofAug departs from the DSP framework and takes an 'augmentation" perspective to solve the issues of DSP. We first determine all compatible semi- eemi-proofs, then sequentially prune the semi-proofs that become impossible to be extended into a full proof after each time we apply <ATP > to an intermediate conjecture. This procedure makes ProofAug fit with the 'sketch' procedure of DSP that translates the informal proof into intermediate conjectures, and each semi semi-proof is expected to align with the corresponding part of the informal proof. Note that such correspondence is hard to achieve for procedural proofs and obligating the LLMs to use the uncommon declarative mode or 'assert' keywords in Coq could be detrimental to the performance. Although in Appendix C we also discuss how to transform procedural style proof language into declarative one in the spirit described in Wiedijk (2012) and then train models and apply ProofAug accordingly, this procedure needs to fine-tune a model on enough data, which is in general expensive. In total, ProofAug is the choice for theorem proving models such as the DeepSeek- Pervvere----errreeo series and the Kimina- Prover (Wang et al., 2025) series that achieve SOTA performance on the cross- benchmark miniF2F, and provide detailed solutions
Phttps:/ // //t///ttttt thub. cww
12

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
and code. 2) Our work further explores the Efficient Recursive Proving module and shows it can boost the performance with relatively small number of queries. In fact, the counterpart of the ERP module for procedural-style proofs should be some kind of truncate-and-resume tree-search algorithm (that only adds new nodes based on the initial proof proposal) proposed in Xin et al. (2024b). However, since the proof style adopted by Deepseek-Prover- V1.5 series models is rather declarative, Max'SS becomes inefficient for them due to the potential reasons we analyzed Section 3.3. 3) We make extra contributions such as exploring extended mixture of strategies to enhance the performance, curating the Isabelle version of miniF2FFttst and finally achieving a cumulative pass rate of 66.0% on this benchmark, while the performance of Coq-based methods remains unclear on the problems of miniF2F since the Coq version is not included by now.
Declarative versus Procedural. The discussion of proof styles dates back to Harrison (1996). Wiedijk (2006) compares the proof styles of a wide range of different systems. Wiedijk (2012) discusses how to convert from procedural system to declarative one. Avigad et al. (2021) introduces the two styles of proof in Lean and provides concrete examples.
Other proof-step generation works. Aside from works introduced in Table 1, such as Polu & Sutskever (2020): Lample et al. (2022), Han al. (2022); Polu et al. (2022); Wang et al. (2023b) are also valuable explorations on what practice beneficial for tree-search proof-step generation methods. Thakur al. (2024) designs an agent that makes use of the history ITP feedbacks in a serialization way.
Other whole-proof generation works. Xin et al. (2024a); Wu et al. (2022) verify the effectiveness of expert iteration on neural theorem proving using the naive whole-proof generation method. They build the first-round theorem statements through autoformalization of the informal problems, First et al. (2023) employs Isabelle error messages to enhance the direct full proof synthesis ability of LLM.
B. Examples of the DSP Issues
Figure 4 and Figure 5 show examples of the 'Hard Conjecture' issue and the 'Complicated Draft' issue described in Section 1.
theorem mumbertheory nurterrtheorry.ssmdddilool.. sgnodBin00d::
fixes int
shows "a"2 mod 3 \<or> a"2 med 3 1"
proof
(* Let be an integer, then \pmod 3 Vin {0, 1, 2). *)
have c0: "a mod \<i>> (0, 2)" by fastforce
(* Using that a'2 \pmod 3 (a \omoo 3) "2 \pmod *)
have "a"2 mod (a mod 3) mod 3" by (simp add: power_mod
(+ we have a \pmod 3 \in {0, 1). *)
then show ?thesis using c0 sledgehameer qed
Isabelle Info: Sledgehammering... No proof found
Figure 4: An example of the 'Hard Conjectures' issue. In this example, although the informal draft is reasonable to human, sledgehammer fails to find proof for the final step.
C. Discussion of Implementing ProofAug for Other Proof Assistants
Lean. Although Lean proofs can be completely tactic-based, block-structures starting with by are very common as well, especially for the proofs of Olympics-level math problems (refer Xin et al. (2024b); Wang et al. (2025) for the example proofs they find). As a result, Lean proofs are also amendable for proof structure analysis, so we also build simple implementation of ProofAug in Lean. As to the substitution of the <ATP> method, we use the combination of Aesop(Limperg & From, 2023), omega and our hand-made heuristic try norm num [x]; try field d s simp [*] at *; try ring nf at *; try nl miiinniitii th For the proof structure analysis process, given a line of code, we manually infer whether is intended to be part of a statement or tactic from its indent and context. Our experiment result shows that ProofAug improves the performance of Kimina- Pronna--rrve--eee Pereeer-reveew-eee Preview-Distill---. Distill-1..B from 44.3% to 50.4% on miniF2F. The improvement can be further enhanced if we can obtain more proper control of the parsing and structure analysis
13

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
theorem
"god 180 168 (12: mat) by eval
theorem
"god 180 168
- (12::nat))
proof
(* If number divides into both 180 and 168 *)
have "god 180 168 dvd 180" sledgehammer
moreover have "god 180 168 dvd 168" sledgehammer
(* it must also divide into their difffernce.. *)
finally have "god 180 168 dvd 12" sledgehanmer
qed
Isabelle Info: Sledgehammeringg.. No proof found
Figure 5: An example of the *Complicated Draft' issue. In this example, while the eval proof method can prove the theorem easily in Isabelle, the translation of informal draft into formal proof fails to pass the verification due to the lack of explicit type annotations, which is a typical error the language models could make in autoformalization.
process and get better substitutions of the <ATP> method. Readers may refer to our code for more implementation details.
For procedural ITPs that work mostly in tactic-based way and do not have block structures in the proofs explicitly, in principle, one follow Wiedijk (2012) to build proof interface that supports declarative style proofs upon the original system. Since Wiedijk (2012) also provides generic way to convert the proofs in the original procedural language to declarative ones, one may obtain data for training language models on this new language by conversion of the corpora in the original language. Then one can perform ProofAug on this new declarative language.
D. Theorem Proving Environment Setup Details and Discussion on the Reproducibility
Our theorem proving environment setup mainly follows that described in Jiang al. (2023), but there some subtle differences. For the setup of PISA, set the candidate provers of Sledgehammer to CVC4 vampire verit spass 23 2 pperpos inn, with 30s timeout for each and 120s in total, as in Jiang et al. (2023). However, we find that in their PISA source code, they use cvc5 instead of CVC4 and the actual total timeout for Sledgehammer is around 35s instead of the intended 120s, scemingly due to an implementation bug. We fix this bug and still use CVC4 since evc5 is not integrated Isabelle 2022. We do not compile the Archive of Formal (AoF) library due to lack of disk space to simultancously run 12 instances possessing compiled AoF heaps on our server. As a result, we do not import the Symmet c_Pol c_Polynom ymomi als. Vieta theory in Jiang et al. (2023). Besides, The heuristics used in our <ATP> method and those in Jiang et al. (2023) differ in that we add an extra simp: add mod.si imps, remove force since we already have fastforce and remove presburger, linarith th since arith integrates the two in rough sense.
To reproduce the results that involve the use complex built-in proof methods or off-the-shelf ATPs, one has to make sure to run PISA instances on the same CPU since the performance of these automation methods heavily rely on the computational power of the CPU.
Nevertheless, even using the same environment, still hard produce exactly the same results due the inherent randomness of these automation methods. The good news, however, is that for theorem proving, have made some progress when new theorems get proved, no matter whether this is completely reproducible not. So we focus on making sure the obtained proofs are correct by verifying them again in Isabelle. We provide the found proofs in attachment to our code. Note that although there are cases where the reconstructed proof fails due to the timeout Isabelle built-in methods such as smt and met is, it does not mean that the theorems are not proved. is only the limitation of these tactics.
confident that
14

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
E. Prompt Construction
The prompts in our experiments are all constructed from three components: prompt template, few-shot demonstration examples. and a prompter. The prompt template is JSON file that contains different roles as names and corresponding templates as values. Each example is also an JSON object whose names occur in the templates. prompter mainly consists of a chat template that maps the sampled examples conversation consisted by messages according the prompt template.
For example, for few-shot prompting for ProofAug, we use the prompt template shown in Figure 6. The examples contain names xi, yi, x yf, corresponding to an informal statement, an informal draft, the formal statement, and the formal full proof. For zero-shot prompting (possibly with ERP), we use the prompt template Figure 8, which has two extra fields ps and yf. For non-ERP prompting. they are set to null string. For ERP prompting state s, they corresponds to the 'proof state' s.state and the partial proof that have been verified this state.
As to the chat template, simply use three newlines to separate pairs of user-assistant messages and concatenate the user message and assistant message in each pair. Nevertheless, we mainly expect the response to stop at the end of the Isabelle code block.
Figure shows an example of the sampled 1-shot prompt.
"user": "Please complete the following Isabelle proof. \n Visabellela Informal statement: (nattemnnt:n(xi]]] (nnxzi/n/nInfformal \n(ii) x) Anfxff(n", "assistant": (n "stop": [">*", "Antheorem", "\nend"]
Figure 6: The prompt template we use for few-shot prompting.
As to the choice of the number of shots to use, in Jiang et al. (2023), they set #shot=3 when prompting the model to translate a draft. We find that since the maximum sequence length of deepseck-math-7bee -b-base is only 4096, few-shot prompting can lead to failure of proofs that are long in nature. As a consequence, DSP with 3-shots prompting solves 117/244, 2-shots 1 11/244, both smaller than 1-shot (120/244). Thus, across the paper, we use 1-shot prompting unless otherwise stated.
F. Breakdown of the Mixture of Strategies
Table 3 shows the breakdown of the mixture of strategies in Section 4.4. Below some explanations of the options appearing in Table 3.
As to the prompt version, we have 3 versions of few-shot prompting and two versions of zero-shot prompting. The three versions of few-shot prompting share the same prompt template shown in Figure 6, but differ in examples: 'DSP' refers to the examples in Jiang al. (2023), and 'few-shot' refers to examples used for ProofAug, where we write full proofs that strictly match the informal proofs provided in the miniF2F dataset of Jiang al. (2023). In contrast, many of the informal proofs of DSP few-shot prompting examples are just descriptions of formal sketches prepared in advance. We also have 'few-shot-legacy version where we first write the simplest proof (rather than a proof sketch) we can come up for each theorem, then write a natural language description for it as an informal proof. Although it turns out that the 'few-shot' version is the best one for 1-shot prompting, the three sets of examples form a complement to each other. Since zero-shot prompting do not involve examples, the two versions of our zero-shot prompts only differ in the instruction text and format. For the O-shot-legacy prompt, we do not have the 'Below is complete proof statement in Isabelle/lsar, translated from the informal proof.' text in the "user" field shown in Figure 8.
A x in the 'Draft' column means that informal statement and the informal proof are not included in the prompt.
For the experiments using the ERP module, we only count the proved theorem using fewer than 700 and 200 requests to the model, for the experiments with 500 attempts and 100 attempts, respectively. As to the pass rates of these experiments, since we only evaluate on the previously unproved theorems for the curated version dataset, we put N/As for them.
For further information, such as the contents of the examples, please refer to our code.
15

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Please complete the Following Isabelle proof.
(* Informal statement:
When Rachel divides her favorite mumer by 7, she gets a remainder of 5.
What will the remainder be if she miltiplies her favorite number by 5 and then divides by 7?
Show that it is 4.
Informal proof:
Let 71 be Rachel's s favorite number. Then n (mod 7), so 5n 5.5 25 (mod 7)- *)
theorem methd_ haahhhh_uumbeethrryyBaa
fixes nat
assumes h0 "n mod 7 5"
shows (5 n) mod 4"
proof
(* so 5m = 5-5 5- = 25 = 4 (mod 7). *)
have c0: (5 n) mod 7 (5 mod 7" proof
have c00: "(5 n) mod (5 mod (n mod 7)) mod by (auto simp: mod_simps then show ?thesis unfolding ho by autc
ged
also have "... mod 7" by auto
finally show 2thesis by auto
qed
Please complete the following Isabelle proof.
(* Informal statement: (informal statement of the problem)
Informal proof:
(informal draft of the problem) *)
ifomal statement of the problen)
Figure 7: An example of final 1-shot prompt for ProofAug.
G. Additional Experimental Results
On miniF2F-valid, ProofAug w/ and w/o ERP module achieve 58.6% and 57.0% in 100 attempts of proof respectively. During the experiment, we make sure the problem to prove is not in the candidate examples.
H. Curation of the Isabelle part of miniF2F
Our curation of DSP-version miniF2F test split mainly includes two types: Typo fix: Statements with typos in variable names or numbers are mostly completely wrong and unprovable. 2) Modifying the type of the variables from nat to int for theorems that could potentially involve the minus operation in the proofs. This is important because, for example, the operation :2:: nat)
(3: :ntt) is valid and expected to be (0:: :nat) in Isabelle/HOL. Although sometimes the sense that the resulting also satisfies the constraints in the statement, it does not express the intent of the original problem. Figure 9 shows such an example.
original statement can still be proved
After finishing the curation process, the authors get learn about that there is FAIR version repository of miniF2F!4 that is actively in maintenance and most of the typos and inappropriate uses of minus of nat type numbers we find in the DSP-version have been fixed in the latest commits. Nevertheless, several typos and some inappropriate use of nat type remain. Thus, we still make a pull request to the FAIR miniF2F repository to update part of our curation to the upstream.
"https://gt hhtpps: pttttps://itt //g htt.d:/cwwo.cccoooooeeeeeeeeecie
com
16

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
"user": "Please complete the following Isabelle proof. An " "isabelle\n Informal statement: :ntttementtn(xx)/Miaa "assistant":
proof: (n(o) x) "n(nnf LL(f
"stop": [">*", "Antheorem", "Anend", "Anlemna")
Figure The prompt template we use for zero-shot prompting for efficient recursive proving (ERP) module.
Table
Breakdown the mixture strategies introduced in Section 4.4.
#attempts
Prompt Ver.
#shots
Draft
ERP
#queries
Curated Ver.
Pass Rate
500
O-shot
X
500
V
N/A
500
0-shot
700
57.4%
100
few-shot
X
52.5%
100
fow-shot
V
X
100
V
N/A
100
few-shot-legacy
X
X
100
X
48.4%
100
few-shot-legacy
V
100
50.8%
100
DSP
V
100
49.2%
0-shot-legacy
X
V
N/A
100
O-shot-legacy
V
X
100
X
50.8%
100
O-shot-legacy
V
200
X
52.0%
An Example of How ProofAug Induce a Proof
Figure 10 shows an example of ProofAug inducing proof from failed proof proposal generated by the model.
17

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Differences:
theorem 200__2001___________111
fixes a b с ::nat
fixes
::int
assumes "0
<<and> <<and> \<and> 0
and "d c"
and "c < b"
and "b < a" and "a
c) c d)
and "a + shows "\<not> prime (a c d)
* (a b
d)
a
Figure 9: How we fix the imo 2001_6000pp DSP-version miniF2F-test. The "a + c + c) " constraint does not express what intends in the original statement when +
(b + d
c) (b
18

---

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
theorem algebra sqineq at2ralti init proof:
fixes :real
shows (2 a) \<le> 1"
proof
have "(a 1) \<" "suup> \<ge> 0" for ar:roal proof
have "C \<le> (a
1)*
using zero zero_le__cte _______u_urreeeeee by auto then show (a 1) suppp l<ge> 0" by (sirp add: power2 eq square))
qed
then have "a (2 <lee> 1" for a: :real
proof
have " (2 - a) - 2 * al< sup="" by (simp add: pover2_eq_aquane
also have "...
1) s'sup>2
a a sup=2" by (aimp add: algebra_simps)
also have <<le> 1"
using <<open>0 \<le> (a 1) 2 by lirarith
finally show ?hesis qed
then show ?thesis
qed
theorem algeora sqineg ataanetlgattaaaaaaaa fixes a::real
shows "a * (2 a) \<le> 1"
proof
have "(a \< ssupo2 V<ge> for at:real proof
have "C \<le> (a - * (a - 1)*
using zero_le__quaa square by auto then show (a 1) \<" supup \<ge> 0"
by (simp add:
ged
then have "a * (2 - a) !<le> 1" for a::real proof
have "a
a) =
ak< sup=2" sorzy
also have "... (a 1) supe2
"spps sorry
also have "... \<le> 1"
using <<oper> \<le> (a 1) '<' <cspp sorry
finally show ?thesis ged
then show ?thssis qed theorem
fixes treal
shows "a (2 \<le> 1"
proof
have "(a - 1) \<" supp2 \<ge> 0" for ar:real
proof
have "C \<le> (a - (a 1)*
using nero_le_squar by auto then show (a i< supe2 \<ee> by (simp add: power2 eq square)
ged then have "a (2 Kle 1" for treal by sos then show 7thesis
qed
Figure 10: An example of ProofAug inducing a proof from a failed initial proof proposal. It can be seen that the initial proof fails inside the proof...qee block of proving al2 a) < due the wrong intermediate claim a a² (a 1)2 1 a², ProofAug finds that a(2 a) < 1 can be directly proved with the proof method given the previous proved fact (a 1)2 2 0.
19


Reviews:
[{"review_id": "cUK3Cpg6Ta", "reviewer": "Reviewer_rCPC", "summary": "The paper proposes ProofAug, a method for achieving efficient neural theorem proving by combining LLMs with automated theorem proving (ATP). The paper conducts extensive experiments comparing ProofAug with baseline methods, categorizing them by different proof styles.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the clear and constructive feedback. As to your questions, we address them as follows:\n\n**Q1**: Regarding lines 261-263 in Section 3.2: Instead of replacing the outer block with sorry, have the authors considered generating more fine-grained drafts from the exact inner theorem containing sorry? It seems counterintuitive that an advanced Isabelle tactic would be more effective on a coarse theorem than on a finer one.\n\n**A1**: Yes! We think what you describe is exactly our ERP module introduced in Section 3.3. We apologize for the unclearness in our description of ERP module. A clearer version of description of ERP is that, for each conjecture (inner theorem) in the Maximal Compatible Semi-Proof that <ATP> fails to prove, we ask the model to generate a new draft for it, given the corresponding proof state in the comment in hope that this information can help it draw a more fine-grained draft. You can refer to line 290-300 in Algorithm 2 and our code (the proof_aug_1dp method) for more details.\n\nIn the revised version, we will modify the line 311-315 in Section 3.3 to 'In practice, to simplify the algorithm and suppress the sampling cost wasted in low-level details, we only try $\\verb|<ATP>|$ and add new nodes for failed conjectures belonging to the original MCSP' to make our description clearer.\n\n\n**Q2**: Regarding the curation of the miniF2F-test dataset: How are the incorrect theorems classified as incorrect? Are they unprovable in principle, or are there formalization errors that make them trivially provable? Providing concrete examples would improve clarity.\n\n**A2**: We only checked the theorems that cannot get proved in our initial experiments, so we think our curation does not include theorems that are made trivially provable due to formalization errors. There are mainly two types of our curation: 1.Fix Typos. Statements with typos in variable names or numbers are mostly completely wrong and unprovable. 2. Modifying the type of the variables from Nat to Int for theorems that perform division on the variables. This is important because, for example, the operation \"(2::Nat) - (3::Nat)\" is valid and expected to be \"(0::Nat)\" in Isabelle. Although sometimes the original minif2f statement can still be proved in the sense that the resulted 0 also satisfies the constraints in the problem, but it is not expressing what the original problem intends. Below is an example:\n```html\nDifferences:\n--- Original\n+++ Fixed\n@@ -1,8 +1,8 @@\n theorem imo_2001_p6:\n-  fixes a b c d ::nat\n+  fixes a b c d ::int\n   assumes \"0 < a \\<and> 0 < b \\<and> 0 < c \\<and> 0 < d\"\n     and \"d < c\"\n     and \"c < b\"\n     and \"b < a\"\n-    and \"a * c + b * d = (b + d + a - c) * (b + d - a + c)\" \n+    and \"a * c + b * d = (a + b - c + d) * (- a + b + c + d)\" \n   shows \"\\<not> prime (a * b + c * d)\"\nHTML diff saved to xf_diffs/imo_2001_6_diff.html\n```\nThe \"a * c + b * d = (b + d + a - c) * (b + d - a + c)\" constraint does not express what it intends in the original statement when $a > b+d$ or $c > b +d+a$. We will also provide several typical examples in our revised version of the paper.\n\n\n**Q3**: Why was Isabelle selected over Lean for evaluation? Is it due to the authors’ familiarity with the proof language, or does Isabelle have an advantage in terms of automation tactics or ATP integration?\n\n**A3**: Mostly the latter one. Isabelle/HOL has the most powerful proof automation across all proof assistants, and the sledgehammer is a built-in tool for Isabelle that have been developed for years. In comparison, Lean does not include an built-in SMT implementation or access to external ATP/SMTs with it, and the related community projects were mostly still in beta during our work. \nAs a result, it is most appropriate to try out our method in Isabelle/HOL first to verify its effectiveness, or in other words, to obtain a 'proof of concept'. \nYou may also refer to our response to Q5 of Reviewer vgEx for the obstacles we are facing when trying to implement ProofAug on Lean.\n\n\nAgain, we appreciate your constructive feedback and will make the necessary changes in our revised version. We hope that our responses have addressed your concerns and clarified the points you raised. Thank you for your time and consideration.", "claims_and_evidence": "Yes. The paper addresses the trade-off between generating hard conjectures and producing overly complicated drafts, particularly in the DSP framework. It claims to propose a solution that effectively balances the two. The proposed algorithm demonstrates its effectiveness through experiments, including ablation studies, which show that ProofAug improves performance over DSP by a significant margin.", "methods_and_evaluation_criteria": "The method is evaluated on the miniF2F test dataset (in Isabelle), which is a widely accepted benchmark for theorem proving. The dataset includes theorems of varying difficulty levels, making it a reasonable choice for evaluating theorem-proving methods.", "theoretical_claims": "The paper does not contain theoretical claims.", "experimental_designs_or_analyses": "The paper begins by categorizing different baseline approaches and then evaluates the performance of the proposed method, ensuring that the sampling budget aligns with baseline methods for a fair comparison. The evaluation results on the miniF2F test dataset show a clear improvement in performance. The paper also conducts ablation studies on the Efficient Recursive Proving (ERP) module and mixed proof strategies to validate the necessity of each component.", "relation_to_broader_scientific_literature": "The paper reviews existing work in neural theorem proving, categorizing approaches into whole-proof generation, proof-step generation, and hybrid methods. By building on these existing paradigms and introducing a framework that improves performance through fine-grained proof structure analysis, the paper advances the state of the art in this field. Additionally, the integration of ProofAug into tree-search algorithms aligns with recent advances in proof synthesis and recursive theorem proving.", "essential_references_not_discussed": "None.", "other_strengths_and_weaknesses": "Strengthes and weaknesses are fully discussed in other sections.", "other_comments_or_suggestions": "I don't have other comments.", "questions_for_authors": "1. Regarding lines 261-263 in Section 3.2: Instead of replacing the outer block with sorry, have the authors considered generating more fine-grained drafts from the exact inner theorem containing sorry? It seems counterintuitive that an advanced Isabelle tactic would be more effective on a coarse theorem than on a finer one.\n\n2. Regarding the curation of the miniF2F-test dataset: How are the incorrect theorems classified as incorrect? Are they unprovable in principle, or are there formalization errors that make them trivially provable? Providing concrete examples would improve clarity.\n\n3. Why was Isabelle selected over Lean for evaluation? Is it due to the authors’ familiarity with the proof language, or does Isabelle have an advantage in terms of automation tactics or ATP integration?", "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": "kQH9M8RvqU", "reviewer": "Reviewer_u8sL", "summary": "This paper introduces ProofAug, a novel theorem-proving method that enhances the sample efficiency of proof synthesis by integrating automation tools at multiple granularity levels. Unlike prior approaches that use automation tools either selectively or at a single level, ProofAug applies fine-grained structure analysis to better leverage built-in tactics and automated theorem provers. Additionally, the method is designed as a plug-and-play module compatible with any tree-search algorithm, allowing the construction of an efficient recursive proving (ERP) module for further performance gains. Evaluated on the miniF2F-test benchmark using the deepseek-math-7b-base model and the Isabelle proof assistant, ProofAug achieves a new state-of-the-art (SOTA) performance, reaching a 66.0% cumulative pass rate with dataset curation (61.9% without) using only 2100 samples, aided by a mixed prompting strategy.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the constructive feedback, especially the concise and accurate comments on our ProofAug method. Below is our response to your concerns:\n\n**Q1**: (On the major experimental claims: The improvement seems minimal, and correction of data might cause unfairness)\n\n**A1**: Thank you for the summary of our major claims from the experimental results. We apologize for the confusion caused by lack of explanation of the goals of the experimental comparisons and possibly inappropriate claims. We in fact want to claim the following three points through the experimental results:\n- Through ablation study, we show that ProofAug can improve pass rate given a relatively small sample budget. (as you mentioned)\n- When compared with previous Isabelle-based methods, our methods can achieve significant improvement on the pass rate, remarking a new SOTA and showing the overall superiority of the designs introduced in this work.\n- As to the comparison with methods based on other proof assistants, we agree with your opinion that a 0.1% improvement is not that significant. However, the main goal of our comparison is to show that, given that previous Isabelle-based methods have been largely outperformed by Lean-based counterparts, our method is still competitive with the state-of-the-art Lean-based methods under a far smaller sample budget. \n\nWe will modify our claims to more clearly reflect these points in the revised version.\n\nAs to the concern of the possible unfairness caused by our curation, we also report our results on the original Isabelle version of minif2f and show that our method is superior to other methods using Isabelle. The goal of curating the dataset is for the comparison with results evaluated on the Lean versions of minif2f. Our curation mainly consists of two types: 1. Fix typos. 2. Modify the type of the variables from Nat to Int for theorems that perform division on the variables (refer to our response to Q2 of Reviewer rCPC for detailed explanation of this type of curation). We have manually checked a large part of the Lean version of minif2f and find that no issues falling into these two types appear. Thus, we believe that using the evaluation result on our curated Isabelle version of minif2f to compare with the Lean version result is more fair.\n\n\n**Q2**: One thing I personally find counterintuitive is that in ProofAug the ATPs are essentially being tried first for smaller (i.e., innermost) subgoals and then larger ones. Usually one would expect that ATPs are better at solving low-level small goals and would struggle with larger ones. The fact that ProofAug works seems to suggest the opposite. This can be due to the fact that MiniF2F-test problems mainly suffer from the problem of “complicated draft”, where small goals are actually not suitable for ATPs, or it may just be accidental?\n\n**A2**: Our observation is that, for models comparable to or stronger than deepseek-math-7b-base, ATPs are actually better at solving low-level goals proposed by the models. We feel sorry that the specific 'complicated draft' example might have misled you. Note that the performance of sledgehammer on minif2f-test is only 20.9\\%, which already indicates that the ATPs struggles to prove high-level competition-math theorems (since they are not designed to solve such problems). As to their performance on low-level model-proposed conjectures, during the experiments, we record at which stage ProofAug helps find a new proof, as you can observe in the results provided in the supplementary material together with the code. We classify the success stages into 3 types: 1. The initial proof succeeds; 2. The Maximal Compatible Semi-Proof succeeds after substituting all 'sorry's with <ATP>s; 3. Some coarse semi-proof succeeds after substituting all 'sorry's with <ATP>s. The rough observation is that , for deepseek-math-7b-base, type 2 success is more common than type 3, which means that the lowest-level conjectures it propose are at least quite 'useful' for the ATPs.\n\n\n**Q3**: Section 3.3 mentions POETRY extensively and adopts part of its approach. Maybe add a high-level description in the very paragraph to briefly explain how the components work?\n\n**A3**: Thank you for the suggestion. We thought that POETRY appears in the Table 1 in the preliminary section so we chose not to describe it extendedly in Section 3.3. We apologize for the confusion and will add a high-level description to briefly explain how the components work in the revised version.\n\n\nFinally, we thank the reviewer for the time and consideration. We hope that our responses have addressed your concerns.", "claims_and_evidence": "There are two major claims:\n\n- ProofAug (based on proof structure analysis) improves pass rate given a relatively small sample budget.\n\n- The cumulative pass rate when adopting a mixed prompting strategy achieves SOTA given a small sample budget.\n\nThe first claim is well demonstrated by detailed explanation of the system design and experiments. Table 2 shows clear differences between ProofAug and the DSP baseline when given the same amount of sample budget.\n\nThe second claim is weaker in my opinion. MiniF2F-test is a relatively small dataset, and a 0.1% improvement (66.0% vs 65.9%) is perhaps not significant enough to claim the crown (if not an error at all). \n\nMoreover, since some MiniF2F-test problems are corrected (as reported in section 4.4), the performance of other existing approaches may also vary a bit. So it isn’t entirely fair to compare the numbers directly.  \n\nThe small amount of sample budget does seem nice.", "methods_and_evaluation_criteria": "The proposed methods make sense. It roughly follows the line of DSP but is much more carefully engineered to maximally exploit the capability of the built-in ATPs in Isabelle, aiming to balance the problem of hard conjectures and complicated draft (as described on page 2.). The evaluation criteria also makes sense. Pass rate with respect to sample budget is the standard metric in this area.", "theoretical_claims": "The paper is mostly emprical.", "experimental_designs_or_analyses": "The experimental designs and analyses look valid to me. I do find that the cumulative pass rate (with dataset curation) being the best is less convincing given that the test dataset is slightly modified / corrected and that the improvement is minimal. But the major part of this submission, namely the improvement in performance of vanilla ProofAug over DSP baseline is reasonable.", "relation_to_broader_scientific_literature": "The approach proposed in this paper can potentially benefit provers other than Isabelle that have strong built-in ATPs.", "essential_references_not_discussed": "The references seem reasonable.", "other_strengths_and_weaknesses": "I appreciate the amount of effort put into the careful engineering in this work. The presentation is also generally clear and the content is well-organized. \n\nOne thing I personally find counterintuitive is that in ProofAug the ATPs are essentially being tried first for smaller (i.e., innermost) subgoals and then larger ones. Usually one would expect that ATPs are better at solving low-level small goals and would struggle with larger ones. The fact that ProofAug works seems to suggest the opposite. This can be due to the fact that MiniF2F-test problems mainly suffer from the problem of “complicated draft”, where small goals are actually not suitable for ATPs, or it may just be accidental?", "other_comments_or_suggestions": "Section 3.3 mentions POETRY extensively and adopts part of its approach. Maybe add a high-level description in the very paragraph to briefly explain how the components work?", "questions_for_authors": "Nothing in particular.", "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": "tWJIAY7aes", "reviewer": "Reviewer_vgEx", "summary": "Recursive theorem decomposition and rebuilding to obtain SOTA scores on miniF2F-test\n\n## update after rebuttal\nSatisfied with responses to questions : Rating remains \"4: Accept\"", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We appreciate the valuable comments from the reviewer, and especially thank you for recognizing and expressing interest in the experimental details in our code. Below is our response to your concerns:\n\n**Q1**: Experimental results of the ERP module make it seem like it produces only a marginal gain.\n\n**A1**: We agree with you that the 1.6\\% improvement seems like only a marginal gain. However, a 1.6\\% improvement under a sample budget (number of calls to LLM for each problem) of 500 is already a significant improvement when compared with RMaxTS, which only improves around 0.1\\% for Deepseek-Prover-V1.5-SFT under a sample budget of 3200 (Even when the sample budget comes to 16×6400, the improvement is only 1.6\\% as well). It is the overall difficulty of using tree-search methods to outperform simple resampling under small sample budgets that make you surprised at the seemingly marginal gain. \n\n\n**Q2**: While the overall claims are supported, the headline SOTA result (since it is based on a 'Mixed Strategy' rather than solely the proposed technique in isolation) somewhat weakens the overall idea.\n\n**A2**: We agree that the overall idea will be strengthened if the SOTA result is reported without using mixed strategies. For 'Pure' ProofAug (with ERP module), we have also achieved SOTA within isabelle-based methods (note that the previous SOTA Isabelle-based method, SubgoalXL, also uses 'mixed strategies' that even include using multiple trained checkpoints), which justifies the superiority of the proposed technique in isolation. We will highlight this in the revised version.\n\n\n**Q3**: (Suggestions on the writing and some specific expressions)\n\n**A3**: Thank you for the suggestions. We will modify \"with a total sample budget of only 2100\" to \"restricting the number of LLM queries to 2100 for each problem\" in the abstract and fix other typos and grammar issues in the revised version.\n\n\n**Q4**: Section 4.4 : \"Besides, we find some incorrect theorem statements in the miniF2F-test dataset during our experiments, so we build a curated dataset and part of the experiments are done on the curated version.\" : Have these been reported 'upstream'?\n\n**A4**: Thank you for the suggestion, and we agree that it is important to report them upstream. However, since there is a gap between the verification style of DSP (which always imports a same set of theories for every theorem) and that of the original minif2f dataset (where different theories are imported for each theorem), extra efforts are needed to make a pull request to the minif2f repository. We will report our curation upstream as we finish the transfer to the original minif2f dataset style.\n\n\n**Q5**: While Appendix C discusses the generic applicability, are there concrete plans to implement and evaluate ProofAug on other proof assistants beyond Isabelle, such as Lean? If so, what are the main challenges anticipated in porting ProofAug to a different ITP environment, and how might the performance differ?\n\n**A5**: Yes, we are currently conducting our plans to implement and evaluate ProofAug on Lean. The main challenges we are facing are the engineering complexities involved in the implementation. To name a few:\n1. The hammer tools (such as the lean-smt project) for lean are still in beta. So it takes time to make the whole pipeline work. \n2. We need to adapt many implementation details from Isabelle/HOL to Lean. For example, there are no concepts like 'proof mode' in Lean so our Lean version implementation could no longer rely on them. \n\nWe anticipate that the performance improvement might be less than that in Isabelle to some extent, since the current Lean hammers are weaker, and Lean proofs are usually in the mixed declarative and procedural style rather than being mostly declarative like Isabelle/Isar proofs. Modifications to ProoAug are probably needed to make it behave well for Lean if we do not choose to derive a completely declarative proof language from Lean as described in Appendix C. \n\nAs a result, we feel like ProofAug should better represent the overall idea of 1. get a list of semi-proofs from the proof proposal 2. apply hammers for the semi-proofs in an organized way 3. an optional recursive proving module, while the specific implementations differ for different proof systems. If you think this statement can help people understand the idea of ProofAug better, we can add it to the revised version, and refer to Algorithm 2 as the \"Implementation of ProofAug in Isabelle/HOL\".\n\n\nFinally, we would like to thank you for your time and consideration. We hope that our responses have addressed your concerns.", "claims_and_evidence": "* Claim: ProofAug enjoys superior sample efficiency.\n  + Table 2 shows that ProofAug outperforms the DSP baseline at sample budgets of 1, 10, and 100 queries on miniF2F-test. \n* Claim: ProofAug achieves a new SOTA on miniF2F-test.\n  + Table 2 compares ProofAug's performance to previous SOTA methods on miniF2F-test, though this 66.0% figure appears to have been achieved through a 'mixed strategy', i.e. throwing a variety of techniques at the solution (explained in Appendix F), rather than 'pure' ProofAug.\n* Claim: ProofAug is a versatile plug-and-play module and integrates well with tree-search algorithms, exemplified by the ERP module.\n  + The paper describes ProofAug as a module within a unified view of theorem proving (Section 2.1) and demonstrates its integration with an ERP module (Section 3.3, Algorithm 2). Experimental results though (surprisingly) make it seems like it produces only a marginal gain.\n* Claim: ProofAug addresses the \"Hard Conjectures\" and \"Complicated Draft\" issues.\n  + Starting from full proof generation aims to mitigate \"Hard Conjectures\" and the recursive coarsening of semi-proofs addresses \"Complicated Draft\", this important aspect is left to two Figures in Appendix B.", "methods_and_evaluation_criteria": "Benchmarks/evaluations make sense - and obtaining good miniF2F-test scores coupled with an eye to efficiency is good.", "theoretical_claims": "The paper is primarily empirically driven and does not make significant theoretical claims that require formal proof verification.", "experimental_designs_or_analyses": "* Control of Variables: The paper mentions using the same `deepseek-math-7b-base` model, Isabelle version, and PISA environment across experiments, which ensures fair comparisons. The discussion in Appendix D regarding reproducibility and CPU dependency is also important for experimental validity.\n* Query Limits and Sample Budgets: The paper clearly reports sample budgets and query limits, allowing for a fair assessment of sample efficiency.\n* Ablating ProofAug from different prompting strategies (DSP, full proof, zero-shot) effectively demonstrated the contribution of ProofAug across various prompting approaches.", "relation_to_broader_scientific_literature": "* Builds upon DSP Framework (Jiang et al., 2023): ProofAug directly addresses limitations observed in the Draft, Sketch, and Prove (DSP) framework\n* Addresses Sample Efficiency in Whole-Proof Generation: The paper acknowledges the sample inefficiency in whole-proof generation methods and positions ProofAug as a solution to improve. This relates to the broader challenge of making LLM-based theorem provers more practical\n* Integrates Automation Tools (ATPs): ProofAug strategically integrates off-the-shelf ATPs\n* Related to Tree-Search in Proof Proving (AlphaGo, etc): The paper explicitly connects ProofAug to tree-search algorithms and demonstrates its compatibility with such approaches through the ERP module", "essential_references_not_discussed": "References seem comprehensive", "other_strengths_and_weaknesses": "Strengths:\n\n* Originality: The core idea of fine-grained proof structure analysis and MCSP for enhancing neural theorem proving is novel and offers a distinct approach compared to existing methods.\n* Significance: The significant improvement in sample efficiency and achieving good results on miniF2F-test demonstrates the practical impact and potential of ProofAug. \n* Comprehensive Evaluation: The paper provides a thorough experimental evaluation with ablation studies.  The overall claims are supported.\n\nWeaknesses\n\n* SOTA Result: While the overall claims are supported, the headline SOTA result (since it is based on a 'Mixed Strategy' rather than solely the proposed technique in isolation) somewhat *weakens* the overall idea : The recursive decomposition is interesting enough...", "other_comments_or_suggestions": "* Abstract: \"with a total sample budget of only 2100\" :: No sense of units here : Is this cumulative number of calls to the LLM?  Over how many questions?  (Abstract should stand alone)\n* Figure 3 label : \"Number of Attemps\" -> \"Number of Attempts\"\n* Section 4.1: \"For multiple attempts of proof,\" -> \"For multiple attempts of a given proof,\" (my understanding here)\n* Section 4.1: \"do not always give the same result under the same condition\" -> \"do not always give identical results under the same conditions\"\n* Section 4.4: \"During the completion of this work, we have tried various\" -> \"During the completion of this work, we tried various\"", "questions_for_authors": "* Section 4.4 : \"Besides, we find some incorrect theorem statements in the miniF2F-test dataset during our experiments, so we build a curated dataset and part of the experiments are done on the curated version.\" : Have these been reported 'upstream'?\n* While Appendix C discusses the generic applicability, are there concrete plans to implement and evaluate ProofAug on other proof assistants beyond Isabelle, such as Lean? If so, what are the main challenges anticipated in porting ProofAug to a different ITP environment, and how might the performance differ?", "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": "IObd6S0lIu", "reviewer": "Reviewer_6tf8", "summary": "The paper introduces ProofAug, a novel approach for enhancing neural theorem proving (NTP) by integrating large language models (LLMs) with traditional automation tools. Unlike prior approaches such as the Draft, Sketch, and Prove (DSP) framework, which generate rough proof sketches and rely on automation tools to fill gaps at a single granularity, the paper proposes starting with a full proof generated by an LLM and employs a fine-grained analysis to derive a maximal compatible semi-proof (MCSP)—a structurally intact proof verifiable by an interactive theorem prover (ITP) like Isabelle, with some unproven parts marked as \"sorry.\" These gaps are iteratively refined using automation tools at varying levels of detail, with the process repeating recursively until a complete proof is achieved or deemed infeasible. The method is enhanced by an efficient recursive proving (ERP) module, which integrates with tree-search algorithms to boost sample efficiency, achieving a notable 66.0% pass rate on the miniF2F-test benchmark after dataset curation (up from 61.9% originally), surpassing previous state-of-the-art results of 50-60%.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the constructive feedback. Below is our response to your concerns:\n\n**Q1**: The authors discuss limitations of the DSP framework in the introduction and as motivation for their approach. However, aside from a couple of examples, there doesn't seem to be any quantitative evidence of these being primary limitations. To be clear, intuitively these do make sense but there doesn't seem to be any quantitative evidence.\n\n**A1**: Thank you for raising the concerns about quantitative evidence. This is a nuanced issue here. Firstly, we would like to clarify that the two limitations we discuss in our paper are not meant to classify the error reasons of the failed verification in DSP and claim which ones are primary. Instead, as stated in line 59, our argument is that \"it(DSP) may also result in proof failures in unintended ways\". By 'unintended', we mean the situations where the there is a chance for the direct whole-proof completion counterpart to generate a correct proof, while the DSP method leads to the failure. \nIn fact, any syntactically correct DSP sketch that fails to pass the verification must fall into either or both of the following two categories: 1. some provable intermediate conjecture cannot be solved by <ATP>. 2. some intermediate conjecture (which is intended to be the translation of a step in the informal draft in DSP) is unprovable in Isabelle/HOL due to being incorrect or being improperly expressed in Isabelle/HOL. The first situation corresponds to our 'Hard Conjecture' issue, and direct whole-proof completion always has a chance to solve the conjecture. As to the second one, for direct whole-proof completion, there is also always a chance that if we do not follow the informal draft to propose this intermediate conjecture, we will get rescued.  This is the 'Complicated Draft' issue. As a result, the two issues we propose can almost cover 100\\% of the 'unintended' failures of DSP.\nWe apologize for the confusion caused by the lack of clarification of what 'unintended' means in our paper and will add more details to the revised version.\n\nIf you are interested in how many such intended failures can be rescued by ProofAug, i.e. cases where the chances are actually realized in practice (the function of <ATP> in ProofAug can be seen as to help find the alternative proof), Figrue 3 can be a reference (DSP v.s 0-shot/Ours+ProofAug for different number of attempts). Remember that it does not reflect the ratio of different types of failures in DSP.\n\n\n**Q2**：(State-of-the-art performance with a mixed strategy). The authors acknowledge that this number is on a curated version of the data, however, the baselines numbers as far as I can tell are not computed on this curated data. This makes the comparison unfair and consequently the claim of SoTA seems unsubstantiated. Moreover, it is not clear what the curation procedure is exactly. Could you please clarify the choices for curation, and what is the rationale behind the comparison to other methods on a different dataset?\n\n**A2**: In Table 2, we have also reported our results on the original Isabelle version of minif2f (61.9\\%) and show that our method is superior to other methods using Isabelle (previous Isabelle SOTA on minif2f-test is 56.1\\%). The goal of curating the dataset is for the comparison with results evaluated on the Lean versions of minif2f. Our curation mainly consists of two types: 1. Fix typos. 2. Modify the type of the variables from Nat to Int for theorems that perform division on the variables (refer to our response to Q2 of Reviewer rCPC for detailed explanation of this type of curation). We have manually checked a large part of the Lean version of minif2f and find that no issues falling into these two types appear. Thus, we believe that using the evaluation result on our curated Isabelle version of minif2f to compare with the Lean version result is more fair.\n\n\n**Q3**: The experiments are limited to Isabelle, and though the authors talk about other systems in the Appendix, some concrete experiments would be helpful.\n\n**A3**: We are currently conducting our plans to implement and evaluate ProofAug on Lean. Preliminary results show that using heuristic tactic combinations as the <ATP> to build a Lean version of ProofAug can help improve about 3\\% on the pass@1 rate for Deepseek-Prover-V1.5-SFT, but hard to make improvements for pass@128 or higher number of attempts. Integration with hammer tools in Lean, such as lean-smt, is necessary for further improvements. Also, some additional modifications might be needed (You can refer to our response to Q5 of Reviewer vgEx for more details). In the revised version, we will update some progress and results we finish by then. \n\n\nAgain, we thank the reviewer for the valuable comments. We hope that our responses have addressed your concerns.", "claims_and_evidence": "C1: Limitations in DSP where generated proofs may produce overly difficult intermediate conjectures or overly complex formal proofs\n\nThe authors discuss limitations of the DSP framework in the introduction and as motivation for their approach. However, aside from a couple of examples, there doesn't seem to be any quantitative evidence of these being primary limitations. To be clear, intuitively these do make sense but there doesn't seem to be any quantitative evidence. \n\nC2: Novel approach ProofAug which improves sample efficiency and can be seamlessly integrated with tree search algorithms. \n\nThe method discussed in Section 3, is evaluated on miniF2F and achieves better performance than DSP given the same budget. Additionally, the results with the ERP module also demonstrate strong performance.  \n\nC3: State-of-the-art performance with a mixed strategy\n\nI find this claim a bit problematic. The authors acknowledge that this number is on a curated version of the data, however, the baselines numbers as far as I can tell are not computed on this curated data. This makes the comparison unfair and consequently the claim of SoTA seems unsubstantiated.", "methods_and_evaluation_criteria": "I am not an expert on the topic but miniF2F is a standard dataset used for evaluating neural theorem provers.", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "As mentioned above, I believe the results on the curated data with a mixture strategy are compared unfairly as the numbers for the proposed method are computed on a different (curated) version of the data. Moreover, it is not clear what the curation procedure is exactly but I appreciate the authors including the curated dataset with the submission. Additionally, the experiments are limited to Isabelle, and though the authors talk about other systems in the Appendix, some concrete experiments would be helpful.", "relation_to_broader_scientific_literature": "The paper improves upon a widely used approach of DSP for neural theorem proving and provides a new interesting approach for combining LLMs with existing automated theorem provers.", "essential_references_not_discussed": "N/A", "other_strengths_and_weaknesses": "* (Strength) The unified perspective on theorem proving with language models in Section 2.1 was quite interesting and insightful.\n* (Strength) The authors include code to reproduce the experiments.", "other_comments_or_suggestions": "N/A", "questions_for_authors": "Could you please clarify the choices for curation, and what is the rationale behind the comparison to other methods on a different dataset?", "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:

Meta-review: The paper presents ProofAug, a novel approach to neural theorem proving that enhances sample efficiency by integrating large language models (LLMs) with traditional automation tools at multiple granularity levels. The method is evaluated on the miniF2F-test benchmark, achieving a new state-of-the-art (SOTA) performance with a 66.0% cumulative pass rate after dataset curation, surpassing previous results.

(+) The method shows significant improvements in sample efficiency, making it a valuable contribution to the field of neural theorem proving.  
(-/=) The field of neural theorem proving is moving so fast, Kimina-Prover is already at 80%+ on miniF2F.  
(+) The paper is very clear and provides ample ablations.

Comments to Authors:
* Consider providing more quantitative evidence for the limitations of the DSP framework as discussed in the introduction.
* Clarify the curation process of the miniF2F-test dataset and ensure that comparisons with baseline methods are fair and transparent.
* Explore the implementation and evaluation of ProofAug on other proof assistants, such as Lean, to demonstrate its generalizability and potential impact across different systems.

Overall, the paper presents a valuable contribution to the field and is recommended for acceptance at ICML 2025.
Decision: Accept (poster)