ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis

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:

Q1: Experimental results of the ERP module make it seem like it produces only a marginal gain.

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.

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.

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.

Q3: (Suggestions on the writing and some specific expressions)

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.

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'?

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.

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?

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:

1. 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.
2. 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.

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

As 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".

Finally, we would like to thank you for your time and consideration. We hope that our responses have addressed your concerns.

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:

Q1: (On the major experimental claims: The improvement seems minimal, and correction of data might cause unfairness)

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:

• Through ablation study, we show that ProofAug can improve pass rate given a relatively small sample budget. (as you mentioned)
• 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.
• 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.

We will modify our claims to more clearly reflect these points in the revised version.

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

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?

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.

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?

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.

Finally, we thank the reviewer for the time and consideration. We hope that our responses have addressed your concerns.

We thank the reviewer for the constructive feedback. Below is our response to your concerns:

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.

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. In 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. We 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.

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

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?

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.

Q3: The experiments are limited to Isabelle, and though the authors talk about other systems in the Appendix, some concrete experiments would be helpful.

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.

Again, we thank the reviewer for the valuable comments. We hope that our responses have addressed your concerns.

We thank the reviewer for the clear and constructive feedback. As to your questions, we address them as follows:

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.

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.

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

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.

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:

Differences:
--- Original
+++ Fixed
@@ -1,8 +1,8 @@
 theorem imo_2001_p6:
-  fixes a b c d ::nat
+  fixes a b c d ::int
   assumes "0 < a \<and> 0 < b \<and> 0 < c \<and> 0 < d"
     and "d < c"
     and "c < b"
     and "b < a"
-    and "a * c + b * d = (b + d + a - c) * (b + d - a + c)" 
+    and "a * c + b * d = (a + b - c + d) * (- a + b + c + d)" 
   shows "\<not> prime (a * b + c * d)"
HTML diff saved to xf_diffs/imo_2001_6_diff.html

The "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.

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?

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. As 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'. You may also refer to our response to Q5 of Reviewer vgEx for the obstacles we are facing when trying to implement ProofAug on Lean.

Again, 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.