LEGO-Prover: Neural Theorem Proving with Growing Libraries

Thanks for your detailed and constructive comments. We respond to all the issues you pointed out in detail below. We hope our response and rebuttal revision will address your concerns.

Many of the weaknesses you've identified correspond directly to the questions you've raised. To provide a cohesive and concise response, and to avoid repetition, we will address them simultaneously.

Weaknesses & Questions

W1Q1. Question on miniF2F split.

We have adopted the approach outlined in 'Draft, Sketch, Prove', and 'Subgoal-based Learning' to present the performance of the miniF2F dataset on both the validation and test sets separately. Our method does not require training, and these two splits are actually treated identically by our approach. The separate display of results for each split is solely for the purpose of facilitating a more detailed comparison with previous methods

W2Q2. Performance gap between miniF2F-valid and miniF2F-test

We have updated the performance of LEGO-Prover on the miniF2F-test set, which achieves a 50.0% pass rate on the miniF2F-test with human-written informal proofs and 45.5% with model-generated informal proofs. It's important to note that the performance gap between the validation and test sets is not unique to our method. Similar performance gaps are observed in other methods, including "Draft, Sketch, Prove" (42.6% and 38.9%), "Subgoal-based Learning" (48.0% and 45.5%), and "Hyper-tree Proof Search." (47.5% and 40.6%). This gap is likely attributable to variations in problem difficulty between the two splits.

W3Q3. 100 proof attempts for the Subgoal-based Learning method.

The paper "Subgoal-based Learning" by Zhao et al. (2023) does indeed utilize 100 proof attempts per problem. This can be verified by examining Figure 2 in their paper, where they demonstrate that the performance achieved with 100 sketches (proof attempts) corresponds to the 45.5% success rate reported in Table 1.

W4Q4. Missing cells in Table 1.

As mentioned in our general response, we encountered technical issues that prevented us from producing the results on time. These problems have been resolved, and we have completed Table 1 accordingly. For the result of the ablation study in the miniF2F-test, we intentionally conducted the ablation only on the validation set to conserve our budget (we mentioned this setting in section 4.1 baseline methods).

Additional Questions

Q5. The performance gap between LEGO-Prover and the ablation becomes stable.

We have extended our ablation setup to include 100 proving attempts per problem, where the LEGO-Prover achieves a success rate of 55.3% and the ablation setup achieves 50.4%. When compared to the previous 50-attempt setup, the performance gap has increased from 3.3% (LEGO-Prover 50.4%, ablation 47.1%) to 4.9%. We have also updated Figure 3(a) in our rebuttal revision to reflect these 100 attempts. It is evident from the figure that the LEGO-Prover's performance progressively improves in comparison to the ablation setup.

Q6(minors). Minor suggestions.

Thank you for your valuable suggestions on improving the presentation of our paper. We have significantly improved our figures and captions as well as the overall writing in this rebuttal revision, striving to make each figure and its explanation as clear as possible within the space constraints. You can review all the revisions we have made in the general response.

Dear Reviewer Nn2P,

We have posted our response to your comments since 3 days ago. Did our rebuttal sufficiently address your concerns? Is there anything we can present that will convince you to increase your rating? We look forward to hearing from you.

Many thanks, Authors

We sincerely thank Reviewer Nn2P for the positive feedback. Thank you again for your time and effort in reviewing this paper! Sorry for our oversight, the explanation for why the miniF2F-valid dataset is used is included in our new rebuttal revision.

Thanks for the detailed explanation. I will update my score according to the impression for the revision. I still recommend explaining why the miniF2F-validaiton dataset is used in the revision to avoid confusion (Sorry if it has been added, but I cannot find it in the revision).

Dear Reviewer Nn2P,

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

We have significantly enhanced our figures and captions, as well as the overall writing quality. We strive to ensure that each figure and its explanation are as clear as possible within the space constraints. Specifically, here are our revisions:

• In Figure 1(b), the 'evolver' is now elaborated to show the directional transformer and request solver. The corresponding caption has also been improved to better explain the overall architecture.
• We have corrected all missing citations and incorrect references. For instance, 'Figure 3(b)' on page 9 has been corrected to 'Figure 4'.
• We have addressed the misuse of cite and citep commands. As an example, 'Subgoal-Learning Zhao et al. (2023)' on page 7 has been corrected to 'Subgoal-Learning (Zhao et al., 2023)'.
• In Appendix A.2, we have included additional algorithmic descriptions, which greatly enhance clarity.
• An additional table describing the prompt outline has been included in Section 3 to enhance readability.

We sincerely thank you for your positive feedback. Your writing suggestions have been very helpful in improving the presentation of our paper. Thank you again for your time and effort in reviewing this manuscript!

Questions

Q1. Computational cost of skill library.

We have included an additional section in Appendix A.3 in our rebuttal revision to discuss the computational cost of the evolver and we run additional experiments on ablation, validating the effectiveness of our growing skill library. The results are detailed as follows:

• The average token consumption ratio is 1:0.89 for the prover and evolver. Therefore, we conducted an additional 100 proving attempts for the ablation setup, which approximates the tokens used by the evolver to those used by the prover. The results show that our method still outperforms the ablation setup by 2.1% under 189 proving attempts (the number of proving attempts with balanced computational cost). Thus, the extra tokens used for more attempts at solving the original problems do not close the gap. Furthermore, LEGO-Prover acquires a significantly large skill library containing various verified proofs, while the prover-only method only accumulates proved problems, which are of no use for other problems or any future applications.

• As the proposer of the concept of utilizing a growing skill library in neural theorem proving, we also believe that this skill library represents the future of ATP. However, in our exploration of employing the skill library for theorem proving, we identified certain limitations that inevitably hinder the performance of the skill library's application in theorem proving. These limitations also contribute to increased token consumption by the evolver to maintain the skill library.

  • Limitations of LLM’s capabilities. The LLM struggles to produce correct proofs, with the evolver's average proof success rate being only 24.1%. Moreover, the evolver might generate proofs that are either trivial or too similar to existing lemmas in the library. After filtering, an average of only 9.1% of the generated proofs are added to the lemma vector store.
  • The task of extracting useful lemmas applicable to other problems is challenging. Identifying useful and non-trivial common lemmas for a specific problem set is difficult, even for humans. The LLM often yields lemmas that are either overly trivial or too specific, lacking generality.
  • Characteristics of the dataset. The miniF2F dataset, comprising only 488 problems, includes many that are simple enough to solve without additional lemmas. Others may require unique solving techniques, not sharing common intermediate lemmas.

  Thus, the 4.9% performance gap is not easily attainable. There are of course some promising future directions for exploration, such as improving the performance of the directional transformer, enhancing the accuracy of the request solver, and increasing retrieval efficiency, all of which present potential avenues for reducing these additional computational costs. However, as the first work to utilize a skill library in neural theorem proving and propose the use of a block-by-block manner for theorem proof, we believe our paper already makes a significant contribution.

Thanks for your detailed and helpful comments. We respond to all the issues you pointed out in detail below. We hope our response and rebuttal revision will address your concerns.

Weaknesses

W1. Figure and text quality.

We have significantly improved our figures and captions as well as the overall writing in this rebuttal revision, striving to make each figure as clear as possible within the space constraints. You are invited to review all the revisions we have made in the general response.

W2. Fairness of comparison to the baseline.

We adhered to "Draft, Sketch, and Prove" and "Subgoal-based Learning" papers to include Thor, Thor+expert iteration, and Draft, Sketch, and Prove as baselines for comparison. These methods represent the state-of-the-art in the miniF2F benchmark for the Isabelle theorem prover. Specifically, Thor and Thor+expert iteration utilizes a fine-tuned, small language model (770 million parameters), demonstrating the performance of search-based neural theorem proving methods. The LLM employed in Thor+expert iteration is only used for auto-formalizing additional problem statements used for data augmentation.

In the "Draft, Sketch, and Prove" approach, GPT-3.5 achieves approximate results of 41.8% and 38.5% on the miniF2F validation and test sets, respectively, as reported in the ablation study of the Subgoal-based Learning paper. By removing their proposed subgoal-based demonstration and diffusion re-ranking components, the Subgoal-based Learning method becomes nearly identical to Draft, Sketch, and Prove, thereby providing an approximate performance benchmark for DSP runs on GPT-3.5. LEGO-Prover significantly outperforms these results.

W3. Request for algorithmic presentation of LEGO-Prover.

Thank you for your valuable suggestions on improving the presentation of our paper. We have included a detailed description of the LEGO-Prover algorithm in Appendix A.2 in our rebuttal revision.

W4(minor). Minor suggestions.

We have fixed the missing cross-ref on p. 8. in our rebuttal revision.

Dear Reviewer SGTy,

We have posted our response to your comments since 3 days ago. Did our rebuttal sufficiently address your concerns? Is there anything we can present that will convince you to increase your rating? We look forward to hearing from you.

Many thanks, Authors

Dear reviewer SGTy:

We include a tabular presentation of the results here for enhanced clarity. We have updated the experimental results in Table 2. The Draft, Sketch, and Prove* runs with ChatGPT using model-informal proofs is an approximate result reported in the ablation study of the Subgoal-based Learning paper (As mentioned in W1). Since Subgoal-based Learning is a method optimized for model-informal proofs and orthogonal to our work, a more fair comparison for LEGO-Prover (model-informal proof) is Draft, Sketch, and Prove*. Compared to Draft, Sketch, and Prove*, LEGO-Prover improves the pass rate by 10.6% (41.8% vs 52.4%) and 7% (38.5% vs 45.5%) in the miniF2F valid and test set, respectively. Our method significantly surpasses all baselines when using LEGO-Prover with human-written informal proofs.

The pass rate for miniF2F-test (human informal proof) has been updated from 47.1% to 50.0%. Compared to the state-of-the-art methods, our method now demonstrates a significantly greater performance gain. The previous result, with a 47.1% pass rate, was primarily due to a bug in our code that incorrectly added false lemma codes to the skill library. As these incorrect lemmas accumulated, the performance of the prover was adversely affected by the faulty lemmas. We have now fixed the bug and reported the full result.

Table 1. Revised proving success rates on the miniF2F dataset with Isabelle, updated values are highlighted in bold, and the best results are in italics. LEGO-Prover* denotes the cumulative pass rate of the miniF2F dataset, considering the total number of problems solved using model-generated and human-written informal proofs.

Another strong baseline is from the recently released paper “Lyra” (Zheng et al., 2023) $1$ , which was published after our submission deadline and therefore is not included in our paper. Lyra extends 'Draft, Sketch, and Prove' with GPT-4's auto-correction ability, prompting GPT-4 to revise the formal proof based on error messages produced by Isabelle. To evaluate how well our method performs in human-informal proof, we compared LEGO-Prover with Lyra, and the results are shown in Table 2. By comparing 'Draft, Sketch, and Prove' using GPT-4 with those using Codex and ChatGPT, we can see that GPT-4's formal mathematics capability has substantially improved (51.2% vs 42.6% and 43.0% vs 39.3%). LEGO-Prover, using ChatGPT, achieves better performance (+4.1% and +7.0%) compared to 'Draft, Sketch, and Prove' using GPT-4. Moreover, LEGO-Prover also outperforms Lyra using GPT-4 (+3.3% and +2.9%) and even achieves comparable results when Lyra is extended to 200 proving attempts with GPT-4. This result is remarkable since the performance of GPT-4 in formal mathematics is substantially better than that of Codex and ChatGPT.

Table 2. Comparison of proving success rates with GPT-4. All methods listed, except for 'Lyra (200 attempts),' involve 100 proving attempts.

Reference:

[1] Zheng, Chuanyang, et al. "Lyra: Orchestrating Dual Correction in Automated Theorem Proving." arXiv preprint arXiv:2309.15806 (2023).

We sincerely thank Reviewer SGTy for the positive feedback. The suggestion of including a discussion on computational cost is very insightful and essential. Thank you again for your time and effort in reviewing this paper!

Thanks for your detailed and constructive comments. We respond to all the issues you pointed out in detail below. We hope our response and rebuttal revision will address your concerns.

Weaknesses

W1. Request for pseudo code.

Thank you for your valuable suggestions on improving the presentation of our paper. We have included a detailed description of the LEGO-Prover algorithm in Appendix A.2 in our rebuttal revision.

Questions

Q1. Question on request vector store.

Your understanding is correct: the request vector store maintains a list of conjectured statements proposed by the decomposer. There is a possibility that these proposed statements could be incorrect, and the evolver will attempt to prove them if they are selected. However, these incorrect conjectures definitely cannot be proven and will be rejected by the Isabelle theorem prover. We have integrated a simple grammar check with the Isabelle theorem prover to filter out grammatically incorrect conjectured statements. For other statements that are correct grammatically, there are no trivial ways to filter them out, since disproving a conjecture is an unpredictable problem. To our knowledge, methods like those described in Yutaka et al. (2018) can reject simple conjectures, but we consider exploring these methods as part of our future work.

Q2. Problem statements used in evolver.

In the directional transformer, we retrieve relevant problem statements using the selected lemma generated by the formalizer or the directional transformer itself. These problem statements are used as reference problems and are added to the prompt to guide the LLM in generating new skills. By presenting the problem and explicitly instructing the LLM to try to evolve the skill that would help solve the problem, the LLM is directed to produce new skills that are more helpful in solving these specific problems, rather than generating arbitrary skills.

Q3. Explanations on minimally solved requests.

LEGO-Prover maintains a list of lemma statements within the request vector store. Each statement is associated with a specific counter that records the number of times it has been selected to solve by the request solver. When attempting to address a request, we prioritize those with the lowest solve count. In cases where multiple requests share the minimal solve count (e.g., 0), we randomly select one of these to solve.

Q4. Explanations on reference examples in request solver.

The term 'server as a reference' might be too vague to elucidate how these retrieved skills are utilized in the request solver. We have reformulated the retrieved lemma into in-context learning (ICL) examples, which helps to prompt the large language model (LLM) to solve the selected request. A detailed usage example can be seen in Figure 7 in Appendix B. We have improved our expression in the paper to make this clearer and more illustrative.

Q5. Open-source request.

Yes, we will release our code after the anonymous review period.

Q6(minor). Minor suggestions.

We have incorporated the temple-based lemma conjecturing into the related work section in our revised rebuttal and corrected the reference errors on pages 5 and 8.

References:

[1] Nagashima, Yutaka, and Julian Parsert. "Goal-oriented conjecturing for Isabelle/HOL." Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11. Springer International Publishing, 2018.

We sincerely thank Reviewer UPjC for the positive feedback. Your suggestions have helped us identify many unclear presentations in our paper. Thank you again for your time and effort in reviewing this paper!

W2. Comparison to ablation is not very strong.

We have included an additional section in Appendix A.3 in our rebuttal revision to discuss the computational cost of the evolver and we run additional experiments on ablation, validating the effectiveness of our growing skill library. The results are detailed as follow:

• We have extended the number of proving attempts for ablations of LEGO-Prover without a skill library to 100 proving attempts (up from 50). The results show that the gap between using the skill library and not using it gradually and consistently enlarges. The initial 3.3% performance gap increases to 4.9% when the LEGO-Prover reaches 100 proving attempts. Thus, the advantage of the growing skill library will become more apparent as the number of skills in the library increases.

• "Simply using all those extra tokens for more attempts at solving the original problems would likely provide a lot of benefits and could conceivably close the 3.3% gap." In response, we conducted an additional experiment to disprove this (Detailed in Appendix A.3 in our rebuttal revision). Specifically, the average token consumption ratio is 1:0.89 for the prover and evolver. Therefore, we conducted an additional 100 proving attempts for the ablation setup, which approximates the tokens used by the evolver to those used by the prover. The results (Figure 5 in A.3) show that our method still outperforms the ablation setup by 2.1% under 189 proving attempts (the number of proving attempts with balanced computational cost). Thus, the extra tokens used for more attempts at solving the original problems do not close the gap. Furthermore, LEGO-Prover acquires a significantly large skill library containing various verified proofs, while the prover-only method only accumulates proved problems, which are of no use for other problems or any future applications.

• As the proposer of the concept of utilizing a growing skill library in neural theorem proving, we also believe that this skill library represents the future of ATP. However, in our exploration of employing the skill library for theorem proving, we identified certain limitations that inevitably hinder the performance of the skill library's application in theorem proving. These limitations also contribute to increased token consumption by the evolver to maintain the skill library.

  • Limitations of LLM’s capabilities. The LLM struggles to produce correct proofs, with the evolver's average proof success rate being only 24.1%. Moreover, the evolver might generate proofs that are either trivial or too similar to existing lemmas in the library. After filtering, an average of only 9.1% of the generated proofs are added to the lemma vector store.
  • The task of extracting useful lemmas applicable to other problems is challenging. Identifying useful and non-trivial common lemmas for a specific problem set is difficult, even for humans. The LLM often yields lemmas that are either overly trivial or too specific, lacking generality.
  • Characteristics of the dataset. The miniF2F dataset, comprising only 488 problems, includes many that are simple enough to solve without additional lemmas. Others may require unique solving techniques, not sharing common intermediate lemmas.

  Compared to improvement (w.r.t SotA on miniF2F-valid) made by other approaches such as DSP (37.3% -> 42.6%, Δ=5.3%) and Subgoal-base Learning (42.6% - > 48%, Δ=5.4%), the improvement shown in our ablation study (50.4% -> 55.3%, Δ=4.9%) is comparable. We also point out that it becomes harder and harder to make even a 1% improvement when the base pass rate (e.g. 50.4%) is larger.

  There are of course some promising future directions for exploration, such as improving the performance of the directional transformer, enhancing the accuracy of the request solver, and increasing retrieval efficiency, all of which present potential avenues for reducing these additional computational costs. However, as the first work to utilize a skill library in neural theorem proving and propose the use of a block-by-block manner for theorem proof, we believe our paper already makes a significant contribution.

W3. Paper readability.

Thank you again for these prompt advisories for improving the paper's presentation. All the suggestions (including minor and very minor ones) on writing have been addressed to the best of our ability. We have significantly improved our figures and captions as well as the overall writing in this rebuttal revision, striving to make each figure as clear as possible within the space constraints. You can review all the revisions we have made in the general response.

Weaknesses

W1. Comparison to the baseline is not very strong.

• Subgoal-based Learning (Zhao et al., 2023) indeed uses model-generated proofs. However, Subgoal-based Learning is an approach that is specifically optimized for model-generated proofs. In contrast, our approach focuses on the usage of a skill library and block-by-block formalization, all based on human informal proofs (as is the case for DSP). We do not extensively explore methods of model-generated proof in LEGO-Prover, as this task is more pertinent to Math Word Problems and not the primary focus of our work. We have outlined the differences in handling model-generated proofs between LEGO-Prover and Subgoal-based Learning in the table below. Each row is explained in detail in the following:

  	LEGO-Prover	Subgoal-based Learning
  Pass rate	The 52.4% produced by LEGO-Prover is NOT a cumulative pass rate.	The 48% IS a cumulative pass rate that integrates the pass rates from both the data collection stage and the inference stage.
  Demonstration examples	Decomposer produces the step-by-step proof directly on top of the informal proof. Only 20 demonstration examples come with DSP used for Decomposer and Formalizer.	The step-by-step informal proof undergoes 15 iterations of refinement using a cross-verification strategy, culminating in 61 demonstration examples to prove the theorem.
  Number of model-generated informal proofs	Use up to 20 model-generated informal proofs per problem (on average 12.13)	Use 100 model-generated step-by-step informal proofs per problem

  In conclusion, the Subgoal-based method is actually orthogonal to our approach. The novel approaches proposed by Subgoal-based Learning, such as subgoal-based demonstration and diffusion re-ranking, are both directly applicable to LEGO-Prover without any conflict. We believe this will definitely improve our results with model-informed proof and further enhance our approach. Unfortunately, Subgoal-based Learning has not been open-sourced to date.

• We believe that a more accurate and direct comparison would involve DSP with model informal proof runs on ChatGPT. An approximate result would be the ablation outcome for the Subgoal-based Learning method, which yields 41.8%(miniF2F-valid) and 38.5%(miniF2F-test). By removing their proposed subgoal-based demonstration and diffusion re-ranking components, the Subgoal-based Learning method becomes nearly identical to Draft, Sketch, and Prove, thereby providing an approximate performance benchmark for DSP runs on GPT-3.5. In comparison to these figures, our LEGO-Prover achieves a notable improvement with 52.4%(+10.6%) and 45.5%(+7.0%) on valid set and test set with model-generated proof.

• Another strong baseline is from the recently released paper "Lyra" (Zheng et al., 2023) $1$ , which was published after the submission deadline and therefore is not included in our paper. Lyra enhances DSP by letting GPT-4 to auto-correct the formal proof with the error message provided by Isabelle. As a result, Lyra achieved pass rates of 55.3% and 51.2% on the miniF2F validation and test sets, respectively, using human-written informal proofs and attempting each problem 200 times with GPT-4. In contrast, LEGO-Prover achieves pass rates of 55.3% and 50.0% with only 100 attempts using only ChatGPT (gpt-3.5-turbo). Thus, our pipeline, with a growing skill library, is able to achieve results comparable to GPT-4 using half the number of proving attempts with ChatGPT. We believe this is a remarkable achievement.

• In response to your comments regarding LEGO-Prover*, your understanding is accurate. We included the result solely to demonstrate performance, and it is highlighted in the abstract to attract attention. However, if you think this is misleading, we are more than willing to revise it accordingly.

Thank you for your detailed and very constructive comments. Your suggestions have been very helpful in enhancing the overall quality and clarity of our paper. We are truly grateful for the improvement suggestions provided in your review and have made every effort to incorporate these into our revisions. We believe that our rebuttal revision is now far more robust, better written, and easier to read compared to the previous version. In the general response, we have outlined all the changes made in this rebuttal revision. Here, we respond to all the issues you pointed out in detail below. We hope our response and rebuttal revision will address your concerns.

Clarifications on the summary

Clarification 1: Your understanding regarding the request vector store and lemma vector store is correct. However, the problem vector store is exclusively utilized in the Directional Transformer. It is employed for similarity searches to identify potentially relevant problems that the selected lemma might aid in solving. As for handling the unsolved problems in miniF2F for prover processes, we utilize a multi-processing shared queue that maintains a list of pending problems. A detailed description is added in Appendix A.2.

Clarification 2: "Concurrently with each pass through the dataset, for every 3 Problem Store problems attempted it makes 8 Request Store attempts, where an attempt is either a call to the Request Solver LLM or the Directional Evolution LLM, or perhaps both (please help clarify, thanks).". As shown in Algorithm 1 in Appendix A.2, we run the prover and evolver processes using the Python multiprocessing package, maintaining the number of processes at the ratio of 3:8. However, there is no synchronization mechanism among these processes except for a shared skill library. The time required for the prover to solve a problem, or for the evolver to transform (solve) a lemma (request), varies. Therefore, there is no guarantee that there will be 8 evolver attempts for every 3 prover attempts. For how the evolver calls to the request solver and the directional transformer. As detailed in Algorithm 3, when a call to the evolver is initiated, the evolver randomly selects either the request solver or the directional transformer to perform its task. Consequently, each pass of the evolver will utilize only one of these options.

Thank you for your detailed summary, the rest of the description is correct and needs no clarifications.

Questions

Q1. LEGO-Prover*’s proving attempts.

Yes, your understanding is correct. LEGO-Prover* technically equals the result of 200 proving attempts. We included this performance merely for demonstration purposes.

Q2. Entry for LEGO-Prover (model informal proof) in miniF2F-test.

We encountered some technical issues before submission, so the results in the miniF2F-test were either buggy or lost. We have updated the results for the miniF2F-test afterward. LEGO-Prover achieves 45.5% on model-generated informal proofs and 50.0% on human-written informal proofs.

Q3. Ablation explanation.

The ablation study runs with a human-written informal proof. Specifically, the prover functions as usual, but we ignore the requests provided by the decomposer and supply an empty list of reference skills to the formalizer. Consequently, the evolver is not utilized in this setup. Additionally, the autocorrect sledgehammer is also employed in the ablation setup.

• The ablation that directly produces the final proof actually degrades to DSP, with different prompt instructions. Due to a limited budget, we have not explored this ablation setup.

Q4. Prover procedure question.

Yes, in each of the 100 passes, LEGO-Prover runs the Decomposer once and then the Formalizer once on each problem. For a clearer algorithmic description, please refer to Appendix A.2 in our rebuttal revision.

Q5. Evolver procedure question.

For how the evolver calls to the request solver and the directional transformer. As detailed in Algorithm 3 in Appendix A.2, when a call to the evolver is initiated, the evolver randomly selects either the request solver or the directional transformer to perform its task. Consequently, each pass of the evolver will utilize only one of these options.

Q6. Question on skill usage.

As you mentioned, measuring the assistance that the retrievals provided in the prompt offer to generation under the retrieval-augmented generation paradigm is a challenging task. Therefore, we adopted a manual inspection method rather than an automated computational approach to judge the help provided by the lemma in the prompt to the formalizer. We only consider the extracted lemma to contribute to the formalizer if it is copied verbatim in the proof or if it provides a rewrite in a similar manner. This is in line with the two types of contributions mentioned in the paper. Other scenarios, where the generation results are irrelevant to the retrievals, are not considered as 'used to formulate new lemmas'. As described in Section 4.3.2, we manually examined all the correct solutions provided by LEGO-Prover in miniF2F-valid and calculated the number manually, instead of relying on any sort of computation of similarity.

Q7. Lemma usage frequency in created skill library.

Regarding how skills from the library are used in correctly solved problems, we have a detailed analysis in Section 4.3.2. As for the individual lemma usage frequency in the generated skill library, due to the small number of problems in miniF2F and the large number of skills generated (we generated more than 20,000 theorems while there are only 488 problems in miniF2F. Even if EVERY problem uses one generated skill, this would only result in a frequency of 488 / 20,000 ≈ 2.4%), the usage frequency remains low in our approach. We justify this as follows:

• Our objective in evolving theorems is not to solve the specific problems presented in the miniF2F dataset, but rather to enhance their mathematical value for more general purposes, such as through the parameterization process. Consequently, the outcomes of the evolution may not necessarily be adequately reflected in the proof tests of miniF2F. In Appendix C, we provide examples of theorems that have evolved, demonstrating their general mathematical significance without considering their relevance to the selected miniF2F problems.
• Increasing lemma usage frequency calls for a Reinforcement Learning (RL)-style system with usage frequency as feedback/reward. The strategies for the evolver in this work are hard-coded in the prompt and are mainly based on human intuition. No adjustment is integrated into the whole library learning process yet. And even if some of these strategies encourage the reusability of the generated theorems, there is no guarantee that the backbone LLM really follows the instruction in the intended direction (which requires a deep understanding of mathematical research). We think it is a very promising avenue to incorporate an RL-style system to dynamically learn the notion of "usefulness" for generated theorems/skills. This was already part of our plan for future research before this submission.

References:

[1] Zheng, Chuanyang, et al. "Lyra: Orchestrating Dual Correction in Automated Theorem Proving." arXiv preprint arXiv:2309.15806 (2023).

Dear reviewer oKSy:

We include a tabular presentation of the results here for enhanced clarity. We have updated the experimental results in Table 2. The Draft, Sketch, and Prove* runs with ChatGPT using model-informal proofs is an approximate result reported in the ablation study of the Subgoal-based Learning paper (As mentioned in W1). Since Subgoal-based Learning is a method optimized for model-informal proofs and orthogonal to our work, a more fair comparison for LEGO-Prover (model-informal proof) is Draft, Sketch, and Prove*. Compared to Draft, Sketch, and Prove*, LEGO-Prover improves the pass rate by 10.6% (41.8% vs 52.4%) and 7% (38.5% vs 45.5%) in the miniF2F valid and test set, respectively. Our method significantly surpasses all baselines when using LEGO-Prover with human-written informal proofs.

Table 1. Revised proving success rates on the miniF2F dataset with Isabelle, updated values are highlighted in bold, and the best results are in italics. LEGO-Prover* denotes the cumulative pass rate of the miniF2F dataset, considering the total number of problems solved using model-generated and human-written informal proofs.

To evaluate how well our method performs in human-informal proof, we compared LEGO-Prover with Lyra, and the results are shown in Table 2. By comparing 'Draft, Sketch, and Prove' using GPT-4 with those using Codex and ChatGPT, we can see that GPT-4's formal mathematics capability has substantially improved (51.2% vs 42.6% and 43.0% vs 39.3%). LEGO-Prover, using ChatGPT, achieves better performance (+4.1% and +7.0%) compared to 'Draft, Sketch, and Prove' using GPT-4. Moreover, LEGO-Prover also outperforms Lyra using GPT-4 (+3.3% and +2.9%) and even achieves comparable results when Lyra is extended to 200 proving attempts with GPT-4. This result is remarkable since the performance of GPT-4 in formal mathematics is substantially better than that of Codex and ChatGPT.

Table 2. Comparison of proving success rates with GPT-4. All methods listed, except for 'Lyra (200 attempts),' involve 100 proving attempts.

Dear Reviewer oKSy,

We have posted our response to your comments since 3 days ago. Did our rebuttal sufficiently address your concerns? Is there anything we can present that will convince you to increase your rating? We look forward to hearing from you.

Many thanks, Authors

Dear Reviewer oKSy:

Thank you immensely for your positive feedback and invaluable suggestions! Your insights into the ablation study and computational cost have been essential in enhancing the robustness of our work. Additionally, your writing suggestions are very helpful and have significantly improved the readability of our paper. We really like the idea of a color-coded Figure 2 and an additional table describing the prompt outline! We struggled to find a good way to present our work more clearly before, and your suggestions have helped a lot. Again, we're deeply grateful for your comprehensive review and the detailed responses provided. The discussion has been truly splendid!

Regarding the lemma usage frequency you mentioned, we apologize for our misunderstanding in our previous response. We will surely address this in our future work and continue to explore the area of library learning for automated theorem proving.

Thank you again for the truly splendid discussion and your recognition of our work!