Lyra: Orchestrating Dual Correction in Automated Theorem Proving

Dear Reviewer bwwN,

Thank you for appreciating our approach. We address your comments below.

Q1: Add the contribution of DSP.

A1: The part is shown on the first page of the Appendix. Because of the paper page limit, we have added the sledgehammer+heuristic description to the Appendix.

Meanwhile, compared to sledgehammer+heuristics in DSP, our proposed Tool Correction has a different motivation and implementation. For example, if “by (simp add: div mult mod eq)” fails, the DSP will immediately stop validating, while our proposed Tool Correction will try all other potential tools. With Tool Correction, we would like to present one important point: the post-process of formal proof can significantly further improve performance, and future work could try to design a more powerful post-process method. And the following is the number of fixed wrong steps via Tool Correction.

For more details, please kindly check our answer in The difference between Tool Correction and sledgehammer+heuristic in Author Response to All Reviewers.

Q2: Baldur is very similar to the conjecture correction with error messages and should be noted.

A2: We have added Baldur to our reference. And the difference between Baldur and Lyra Conjection Correction is the following. Compared to Baldur which needs a training process, Lyra Conjection Correction is training-free, and it can reset the initial solution after several failure rounds. Please refer to the more detailed answer to The difference between Lyra and other works in the Author response to all reviewers.

If you think our comment and update address your concerns, could you please consider raising your rating of the paper? Thank you!

Dear Reviewer NmsF,

Thank you for the detailed review. We will address your concerns below.

Q1: The technical or empirical insights.

A1: Tool Correction presents the importance of post-processing LLM response to improve performance, and Conjecture Correction proposes a framework that can extend the non-refinement framework to a refinement framework.

The Insight of Tool Correction

• Experiment Observation. LLM formal proof can not prove a simple conjecture x = 19∗(x div 19)+4. After our analysis, this is caused by LLM hallucination that LLM wrong believes by (simp add: div mult mod eq) can prove x = 19∗(x div 19)+4. To mitigate the hallucination, we propose to post-process the LLM-generated formal proof by predefined rules, which is called Tool Correction.
• Following this direction, the automated theorem proving performance can be further improved, if there are better rules to post-process the generated formal proof. And this is one of the important points that we want to present and prove by Tool Correction.

The Insight of Conjecture Correction

• The motivation of Conjecture Correction: propose a technique that can change a non-framework (such as DSP) to a refinement framework (such as Lyra), without too many modifications.
• Experiment Observation. If directly appends the error message at the end of the prompt, the LLM response is various. For example, after appending error at the end of (informal Proof 1, formal Proof 1, informal Proof 2, formal Promal 2) to get (informal Proof 1, formal Proof 1, informal Proof 2, formal Proof 2, error), and then ask LLM to refine formal Proof 2, the response may begin with LLM’s comments of formal proof 2, but not a formal proof.
• Solution. Conjecture Correction adds “proof -” at the end of the instruction as an indicator. As most of the formal proofs begin with “proof -”, adding such an indicator could ask LLm to generate a formal proof.

Q2: Are the heuristics used for TC transferable to other theorem proving tools and datasets.

A2: The proposed Tool Correction can be transferable to other theorem proving tools and datasets. The corresponding heuristics can be transferable to other datasets, and the heuristics need to be designed for different provers as they have different syntaxes.

We discuss how can we transfer Tool Correction to other theorem proving tools, using Lean Prover as an example.

• The Lean Prover has proving tools, such as simp, linarith, ring, and so on (these are its heuristics). When proving a conjecture, we can also try these different proving tools (heuristics) in Lean if the current tactic fails. Hence. Tool Correction is transferable to Lean Prover with Lean.
• Tool Correction and heuristics are not related to datasets, but related to a prover (such as Isabelle or Lean). Hence, as long as we adapt Tool Correction to a prover, the proposed Tool Correction and heuristics can be transferable to other datasets.
• Therefore, the Tool Correction and heuristics are transferable to other theorem proving tools datasets.
• Finally, Tool Correction provides the following insights to overcome LLM hallucination. First, decompose the LLM response into different parts. Then, employs predefined rules to post-process the parts.

Q3: How do we know that these heuristics are not overfit to the miniF2f dataset?

A3: These heuristics are not overfit to the miniF2F dataset because they are related to a prover, but not a dataset.

The proposed Tool Correction focuses on post-processing the formal proof which is written in Isabelle in this work. Therefore, the heuristics are related to Isabelle (in this work), but not any dataset, such as the miniF2F dataset.

Q4: Are the presented techniques overfit to miniF2F dataset and Isabelle? In particular, I am afraid this might be the case for TC.

A4: The presented techniques are not overfit to miniF2F or Isabelle.

For Tool Correction,

• We can easily adapt it to other provers, such as Lean. And this is illustrated in Q2.
• Also, Tool Correction implementation is dataset-agnostic, and it is not related to any datasets, including miniF2F.

For Conjecture Correction,

• Conjecture Correction needs formal proof and the corresponding error message, which can come from Isabelle (in this work) and other provers (such as Lean)
• Conjecture Correction is also not overfit to miniF2F, because its implementation is dataset-agnostic.

Q3: Do the authors have any hypotheses for why the LLMs are even able to understand Isabelle error messages (for instance, does the publicly available Isabelle proof corpus also have examples of error messages)

A3: There are two hypotheses for why the LLMs are even able to understand Isabelle error messages.

Let’s start from an easy point: the LLMs can understand English and Isabelle syntax.

• LLMs can understand English. This is approved by OpenAI. Therefore, this conclusion is obvious.
• LLMs can understand Isabelle syntex.
  • There are publicly available Isabelle proof corpus. For example, The entire AFP library, the largest formal library that contains most of Isabelle proofs, is 180MB in size [2].
  • LLMs can understand Isabelle's syntax, and this is proved by previous works [2-5].

Hypothesis 1: The publicly available Isabelle proof corpus also has examples of error messages.

• The training dataset of GPT-3 [6] contains Common Crawl datasets [7], which contain Stackflow.
• On the Stackflow, we find examples of error messages.
  • Example 1: Failed to apply initial proof method: using this: [ ] ∈ ns_public goal (1 subgoal): 1. ∀A B X. Says A B X ∉ set_of_list [ ]
  • Example 2: Failed to apply proof method: using this: (y, x) ∈ r^* (z, y) ∈ r goal (1 subgoal): 1. (z, x) ∈ r^*
  • Example 3: Failed to apply initial proof method: using this: n < a n < b goal (1 subgoal): 1. n * n < a * b
• Therefore, the publicly available Isabelle proof corpus may also have examples of error messages.

Hypothesis 2: the LLMs may understand Isabelle's error message if they understand English and Isabelle's syntax, but do not have to see Isabelle's error messages before.

• First, we show what Isabelle's error messages look like. The error message is written in English, such as “Failed to apply proof method using this: 0 < y goal (1 subgoal): 1. 9 * (x * sin x) + 4 / (x * sin x) = (9 * (x * sin x)<^sup>2 + 4) / (x * sin x) At command “by” “.
• According to the error message, we can find that the error message only contains English words and Isabelle syntax (such as <^sup>).
• Therefore, to understand Isabelle's error message, the proposed LLM may not need to see Isabelle's error message before, but just has to understand English and Isabelle's syntax.

If you think our comment and update address your concerns, could you please consider raising your rating of the paper? Thank you!

[1] Thakur, A., Wen, Y., & Chaudhuri, S. (2023). A Language-Agent Approach to Formal Theorem-Proving. arXiv preprint arXiv:2310.04353.

[2] Wu, Y., Jiang, A. Q., Li, W., Rabe, M., Staats, C., Jamnik, M., & Szegedy, C. (2022). Autoformalization with large language models. Advances in Neural Information Processing Systems, 35, 32353-32368.

[3] Jiang, A. Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóźdź, T., Miłoś, P., ... & Jamnik, M. (2022). Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35, 8360-8373.

[4] Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., ... & Lample, G. (2022). Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283.

[5] Zhao, X., Li, W., & Kong, L. (2023). Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving. arXiv preprint arXiv:2305.16366.

[6] Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J. D., Dhariwal, P., ... & Amodei, D. (2020). Language models are few-shot learners. Advances in neural information processing systems, 33, 1877-1901.

[7] Raffel, C., Shazeer, N., Roberts, A., Lee, K., Narang, S., Matena, M., ... & Liu, P. J. (2020). Exploring the limits of transfer learning with a unified text-to-text transformer. The Journal of Machine Learning Research, 21(1), 5485-5551.

Dear Reviewer NmsF,

Thank you very much for the reply, and thank you very much for updating the score.

We have incorporated the discussion on why LLMs might be able to understand error messages in the paper (please check the updated version). We will explain the question of TC in detail below.

Q1: However, my point was simply that there is no guarantee that the performance gains due to TC will be larger than zero for any dataset.

A1: Our claim and this point does not have conflict. There is a guarantee that TC does not cause any reduction in performance, and there is no guarantee that the performance gains due to TC will be larger than zero for any dataset. And we prove that there does not exist that “there is a guarantee that the performance gains due to Algorithm A will be larger than zero, compared to baseline sledgehammer+heuristics, for any dataset (the pass rate limit is 100%), for any Algorithm A”. We will explain it below.

• Recall when TC works. As described in previous Q1, TC is employed to reduce the occurrence of “The Conjecture is correct, but the proving tool is incorrect”.
  • For a very easy dataset, if any automated proving tool can prove the formal proof from the dataset, then TC may not further improve performance.
  • For a very difficult dataset, if all conjectures are incorrect for the proof from the dataset, then TC may not further improve performance.
  • For other datasets (have the occurrence of “The Conjecture is correct, but the proving tool is incorrect”), the proposed TC has the potential to further improve the performance.
• Therefore, both the following two claims are correct:
  • There is a guarantee that the performance gains due to TC will be larger than zero or equal to zero.
  • There is no guarantee that the performance gains due to TC will be larger than zero.

Meanwhile, as we both agree that “there is a guarantee that the performance gains due to TC will be larger or equal to zero, for any dataset”, we want to prove that there does not exist “there is a guarantee that the performance gains due to TC will be larger than zero, for any dataset”.

• We already know that both TC and sledgehammer+heuristics (baseline) can solve some problems.
• Then, we can select a subset, so that the subset’s problem can be solved by both TC and sledgehammer+heuristics.
  • Therefore, the pass rate of sledgehammer + heuristics is 100%.
  • If “there is a guarantee that the performance gains due to TC will be larger than zero, for any dataset”, then the pass rate of TC will be larger than 100%, which is a contradiction.
• Therefore, there does not exist “there is a guarantee that the performance gains due to TC will be larger than zero, for any dataset”.
• Actually, it is also easy to prove that there does not exist that “there is a guarantee that the performance gains due to Algorithm A will be larger than zero, compared to baseline sledgehammer+heuristics, for any dataset(the pass rate limit is 100%), for any Algorithm A”.
• Hence, it is good enough that “there is a guarantee that the performance gains due to TC will be larger or equal to zero, for any dataset.”

Q2: The reason TC helps for miniF2F might be because the heuristics in TC are tailored to this dataset.

A2: We do not tailor the heuristics for the miniF2F dataset.

These heuristics tools (such as sledgehammer, by simp and so on) are mentioned by the DSP paper (ICLR 2023, Oral). To have a fair comparison, we directly use and keep the same heuristics tools from DSP. Hence, we do not optimize the heuristics tools set for the miniF2F dataset, but directly use these mentioned heuristics tools from the DSP paper.

Though TC and sledgehmmaer+heuristics employ the same heuristics, we both agree that there is a guarantee that TC is better than sledgehammer+heuristics (larger or equal to zero performance gains). Therefore, compared to baseline DSP’s sledgehammer+ heuristics, the improvement of TC is not caused by tailoring the heuristics for the miniF2F dataset.

Q3: Is there a reason to believe that these heuristics will also be useful for other datasets?

A3: There are two reasons to believe that these heuristics will also be useful for other datasets:

• For any given formal proof (dataset), the TC always gets non-negative performance gains, compared with baseline sledgehammer +heuristics (we both agree).
  • That TC is helpful and good enough. Because there does not exist that Algorithm A always gets positive performance gains for any dataset (the pass rate limit is 100%), compared to baseline sledgehammer+heuristics, for any Algorithm A (proved in Q1).
• We do not tailor or optimize the heuristics set for the miniF2F dataset (proved in Q2).

If you think our comment and update address your concerns, could you please consider raising your rating of the paper? Thank you!

Dear Reviewer NmsF,

Thank you very much for your reply. We will address the concerns of TC's general applicability in the following.

Empirical Results

• Experiment Setting. Our experiment setting follows previous work, including DSP (ICLR 2023) and Sub-goal learning, which all only conduct experiments on the miniF2F dataset. To the best of our knowledge, the miniF2F is the only dataset that has both informal problem, informal proof and formal statement. And all DSP, subgoal-learning and Lyra need informal problems for inference.
• To better analyze the TC, we modify the miniF2F to build an IMO problem set (which has 40 IMO problems). The IMO problem set is much more challenging than common automated theorem proving problems, which can effectively prove the TC generalization. The results are the following.

This proves that: for the other datasets, such as IMO problem set, Tool Correction can still improve the performance. And the emperical results also prove the previous conclusion: the performance gains of TC are larger or equal to zero, compared to baseline sledgehammer+heuristics, for any dataset.

Theoretical Analysis

The following is the analysis of TC's general applicability.

• The miniF2F is a common and widely used dataset which contains different-level problems and various problem types, so that it can sufficiently evaluate the method. And DSP and subgoal-learning also use the dataset for all their experiments.

• The TC presents an important idea: post-process LLM response to further improve the performance, which can be widely used for other datasets or tasks.

• TC generalization. We both agree that the performance gains of TC are larger or equal to zero, compared to baseline sledgehammer+heuristics, for any dataset (TC does not cause performance reduction).

• Reviewer NmsF’s requirement of generalization. the performance gains of TC are larger than zero, compared to baseline sledgehammer+heuristics, for any dataset.

• Obvious point: as proved in Q2 of Nov 18 response, there is no model/algorithm that can fullfills the Reviewer NmsF’s requirement of generalization.

According to both Empirical Results and Theoretical Analysis, the concern of TC's general applicability is addressed.

If you think our comment and update address your concerns, could you please consider raising your rating of the paper? Thank you!

Dear Reviewer 1Jjk,

Thank you for appreciating our approach. We address your comments below.

Q1: the innovation of TC appears slightly limited.

A1: TC implementation reveals an important point: post-process of formal proof can significantly further improve performance, which does not get enough attention in previous work. Future work can explore how to design better post-process rules or techniques to improve the formal proof quality. And this is one important point that we want to present and prove via Tool Correction. For more details, please refer to The difference between Tool Correction and sledgehammer+heuristic in Author Response to All Reviewers.

Q2: I would love to see a comparison between Baldur and Lyra if possible.

A2: The following is our comparison between Baldur and Lyra. We have clarified this in our general response to all reviewers. Please kindly check our answer in The difference between Lyra and other works in Author Response to All Reviewers.

Compared to Baldur which needs a training process, the proposed Lyra is training-free. As Baldur does not release code or conduct experiments on miniF2F, currently we cannot directly compare their performance. However, we can compare Baldur, Thor [1] and Lyra to draw a conclusion between Baldur and Lyra.

Fortunately, we can 1) first compare Baldur with Thor [1] on AFP topic classification; 2) then compare Thor with Lyra on miniF2F; 3) finally, conclude: that Lyra is significantly better than Thor, while Thor is better or comparable to Baldur.

Q3: In the tool correction part, it appears that LLMs are prompted to produce a full mechanised proof including the tactic 'by (simp add: div mult mod eq)', which is considered as LLM hallucination by the authors. Is that the case? If so, it might be a good idea to make the distinction clear as this may affect the ablation study.

A3: Yes, that is the case. And we update the following to make the distinction clear.

• Page 1: “ As shown in the observation in Figure 1, prover fails to prove conjecture x = 19 ∗ (x div 19) + 4 because LLM wrongly believes that by (simp add: div mult mod eq) can prove x = 19 ∗ (x div 19) + 4” —> “ As shown in the observation in Figure 1, prover fails to prove conjecture x = 19 ∗ (x div 19) + 4 because by (simp add: div mult mod eq) generated by LLM cannot prove x = 19 ∗ (x div 19) + 4 (considered as LLM hallucination)”
• Figure 1: “The prover fails because LLM wrongly believes that by (simp add: div mult mod eq) can prove x = 19∗(x div 19)+4” —> “The prover fails because by (simp add: div mult mod eq) generated by LLM cannot prove x = 19∗(x div 19)+4, which is considered as the hallucination.”
• Moreover, we have highlighted that this is the LLM hallucination in our paper in Page 4: “For instance, consider the statement x = 19 ∗ (x div 19) + 4, where LLM proposes to utilize the tactic by (simp add: div mult mod eq), leading to failure. This is the LLM hallucination…”

Q4: Informal proof and the formal sketch are quite different. Elaborate a bit on the discrepancy between the informal proof and the formal one.

A4: The informal proof is a guide to formal proof, and it is not necessary that the informal proof steps and formal proof steps are one-to-one. The detailed explanation is the following.

• Why Informal proof and the formal sketch are quite different? $Reason$: The informal proof is a guide to formal proof generation. According to the original DSP paper, the informal proof only needs to be useful for producing a sketch in the next stage.
• Why the formal one does not cover continuity or limit? $Reason$: Actually, the formal one covers the limit. For example, the formal proof has shown that "ultimately have "1 < ?S" by simp [ATPWithTC]", which covers the limit. The limit is proved via the ATP and Tool Correction.

Dear Reviewer 1Jjk,

Thank you very much for your reply. The following is one of the potential extensions of TC for ‘apply'-style proofs. The difference between "by" and "apply" is in a pdf named "The Isabelle/Isar Reference Manual", while "by" is mainly introduced on Page 148 and "apply" is introduced on Page 167.

• Recall the core idea of TC: replace potential incorrect tools/tactics with predefined correct ones. In this setting, we replace incorrect "apply"-style tactics with 12 predefined "apply"-style tactics.
• Step 1: Check whether we need to process the "apply" tactics. If we need and the previous tactic does not begin with "apply", then we directly change ‘apply'-style proofs to single-step method, which is sledgehammer+11 tactics. And if succeed via sledgehammer+11 tactics, then we continue. That is, if succeed via sledgehammer+11 tactics, for the next tactic, if it still begins with “apply”, we directly ignore it. If fails, we move to Step 2
• Step 2: Try the given "apply"-style tactics. If fails, we move to Step 3.
• Step 3: If Step 2 fails, then try sledgehammer+11 tactics. And if it succeeds, we continue. And if it fails, we try all 12 predefined "apply"-style tactics.
• If Step 3 fails, then the prover fails.

The following is the Python-like pseudocode.

#tactic_list: list of the tactics of formal proof
#prover: Isabelle Prover 
#TCUsage: whether employ Tool Correction
tool_heuristics=['by auto','by arith','by blast', 'by simp',
'by fastforce', 'by force', 'by eval', 'by presburger', 'by sos',
'by linarith', 'by (auto simp: field_simps)', 'sledgehammer']


# can be other heuristics, such as dynamic heuristics.
apply_heuristics=['apply auto','apply arith','apply blast', 'apply simp',
'apply fastforce', 'apply force', 'apply eval', 'apply presburger', 'apply sos',
'apply linarith', 'apply (auto simp: field_simps)', 'apply assumption']


output={}
previous_tactics="None"
for tactic in tactic_list:
    use_heuristics=False
    
    if tactic.strip().startswith("done") and output.has_key('ignore_apply'): #solve "apply"-style via "by".
        previous_tactics="done"
        continue

    # Step 1 Begin
    if tactic.strip().startswith("apply") and TCUsage:
        if output.has_key('ignore_apply') and previous_tactics.startswith("apply"): 
            # solved by previous tactics, such as single-step
            continue
        elif not (previous_tactics.startswith("apply")) #If previous one is not "apply"
            for tool_try in tool_heuristics: # try single-step
                output = prover.run_tac(tool_try)
                if output['error'] is None:
                    break
            if output['error'] is None: 
                #go to next tactic, and ignore the following "apply" 
                #becuase already finish the proof
                output['ignore_apply']=True #solve the proof
                continue
        else:
            #do nothing
    # Step 1 End
            

    previous_tactics=tactic
    
    #Step 2 Begin        
    output = prover.run_tac(tactic)
    #Step 2 End

    if output['error'] is not None:
        if TCUsage: # Use Tool Correction or Not
            if tactic.strip().startswith("by") or tactic.strip()==("."):
                use_heuristic=True
    
        if ("sledgehammer" in tactic) or use_heuristic:
            for tool_try in tool_heuristics:
                output = prover.run_tac(tool_try)
                if output['error'] is None:
                    output['ignore_apply']=True
                    break
                    
                    
        # Step 3 Begin
        if TCUsage and tactic.strip().startswith("apply"):
            for tool_try in tool_heuristics:
                output = prover.run_tac(tool_try)
                if output['error'] is None:
                    output['ignore_apply']=True #solve the proof
                    break
            
            if output['error'] is not None:
                for apply_try in apply_heuristics:
                    output = prover.run_tac(apply_try)
                    if output['error'] is None: 
                        # if not use by-style tactic, 
                        # not sure whether the whole proof is solved or not here. 
                        # So that NO output['ignore_apply']=True
                        break
        # Step 3 End
                    
        
    if output['error'] is not None:
        return "tactic_failed", output
    if output['tactic_state'] == 'no goals':
        return "success", output
        
return "proof_incomplete", output

Another direction could be dynamic heuristics. For example, though the given tactic is incorrect (such as the "by (simp add: div_ mult_mod_eq) in Figure 1), there is still some useful information (such as something like div_mult_mod_eq). We may design corresponding methods to utilize the information. For example, search the lemma that is similar to div_mult_mod_eq and replace it. Therefore, another direction of TC extension could be dynamic tactic creation.

If you think our comment and update address your concerns, could you please consider raising your rating of the paper? Thank you!

Q5: If we set a time limit for each question like 10 or 30 minutes, what would be the performance of TC/CC compared with the GPT4 baseline and DSP+GPT4 baseline

A5: The result depends on whether it allows the parallel process.

As there is no GPT4 baseline (for DSP paper, they also do not have experiment results of Codex/Minerva baseline, but have DSP+Codex and DSP+Minerva), we list the performance of Lyra and DSP+GPT4 in the following.

If allows the parallel process, then we can keep the performance (55.3% on validation and 51.2% on test), if the time limit is larger or equal to 10 minutes. For the relationship between time limit and performance, we can refer to Figure 2 on Page 8, which presents the relationship between the number of attempts and the performance. One attempt takes 2 minutes, if not allow the parallel process.

The following is the performance under different time limits for each question, for DSP(GPT-4) and Lyra.

Usually, it takes about 1～2 minutes to finish one attempt (we take 2 min/attempt here), where each problem is allowed to try 200 attempts(a total of 400 minutes), in our setting. For DSP, the 200 attempts can be processed in parallel. Hence, if allowing the parallel process, the maximum time cost is 2 minutes. For Lyra, these 200 attempts are divided into 40 patches, where each patch contains five attempts. The 40 patches can be processed in parallel. Hence, if allowing the parallel process, the maximum time cost is 10 minutes. If not allowing the parallel process, when the time limit is 10 mins, Lyra achieves 33.6% miniF2F-validation and 28.6% miniF2F-test. And if not allow the parallel process, when the time limit is 30 mins, Lyra achieves 40.1% miniF2F-validation and 36.0% miniF2F-test.

If you think our comment and update address your concerns, could you please consider raising your rating of the paper? Thank you!

Dear Reviewer Wc5t,

Thank you for the detailed review. We will address your concerns below.

Q1: novelty in terms of the approach.

A1: For Tool Correction, it provides this insight: post-process of formal proof can significantly further improve performance. Please refer to the The difference between Tool Correction and sledgehammer+heuristic in Author Response to All Reviewers.

And, we also show the The difference between Lyra and other works in Author Response to All Reviewers to present the innovation of Conjecture Correction.

Q2: I think one good baseline would be replace Minerva and Codex in DSP with GPT4. So we still have GPT4 to generate the proof sketch (the intermediate conjectures) but use 11 tactics + sledgehammer to close the open goals.

A2: We have shown the result in Table 2 in our paper. Our proposed Lyra degrades to DSP if removes both Tool Correction and Conjecture Correction. That is, $DSP+Tool Correction + Conjecture Correction = Lyra$, while the original DSP has sledgehammer + 11 tactics implementation (only works when the given tactic is "sledgehammer"), achieving 50.4% on miniF2F-valid and 42.6% on miniF2F-test.

Q3: Could you calculate the number of wrong proof steps fixed by each tactic in TC?

A3: The following is the number of wrong proof steps fixed by each tactic in TC.

• Proof comes from: the miniF2F validation set (pass rate 55.3%) and test set result (pass rate 51.2%), with GPT-4, human informal proof, Conjecture Correction and Tool Correction.
• The definition of proof step: a proof step is regarded as a tactic.
• Calculation protocol: if sledgehammer+heuristic or Tool Correction fails to validate the current tactic, then the current proving process will be terminated and we will turn to the next formal proof validation. Finally, we calculate how many correct tactics/proof steps.

On miniF2F-valid, sledgehammer+heuristics can help the prover successfully pass 2260 steps. After adding Tool Correction, the number increases to 3486 steps. Therefore, Tool Correction fixes 1226 wrong steps. On miniF2F-test, Tool Correction fixes 1293 wrong steps

Q4: The proposed method adds a lot more computation. How much time would be token by calling GPT4, TC and CC?

A4: There may be a slight misunderstanding here. Our method running time is similar to DSP.

Both tool Correction and Conjecture Correction do not add a lot more computing time. The upper bound of Tool Correction time cost is 120+11*10=230 seconds for each tactic (same as the sledgehammer+heuristics in DSP), and formal proof generation (Calling GPT-4 and CC) time varies from 10 seconds to 2 minutes. On average, Lyra takes about 2 minutes per attempt, including the time cost of TC, and GPT4+CC.

For the Tool Correction, it only works when the current tactics fail and begin with "by" or "." or “sledgehammer”. And it has the same timeout upper bound as DSP's sledgehammer+hsuristics. For sledgehammer, the timeout is 120 seconds. For every of the other 11 tactics, the timeout is 10 seconds. Hence, the upper bound of Tool Correction is 120+11*10=230 seconds. Usually, the prover validation with TC can be finished in 1 minute.

For the GPT-4+Conjecture Correction, it also does not add additional computing time. The proposed Lyra or DSP employs the aggressive model (Codex or GPT-4) to generate a formal proof. Hence, the time cost mainly depends on the length of the generated formal proof, which depends on different problems but not the Conjecture Correction. Depending on the difference of the problem, the formal proof generation is different for one attempt.

• If the formal proof is short (such as an easy proof), formal proof generation only needs less than 10 seconds. For example, the correct formal proof is only "by sos".
• If the formal proof is long (such as a difficult proof), formal proof generation needs several minutes. We have shown a long IMO formal proof example in Figure 3.

Therefore, both Tool Correction and Conjecture Correction do not add a lot more computing time. The Lyra has the same time complexity as DSP.

Dear Reviewer Wc5t,

The proposed Tool Correction can also be integrated with other Isabelle tactics besides "by"-style tactic (single-step method), while previous work (such as sledgehammer+heuristics in DSP) can not (only work when the given tactic is "sledgehammer"). In the following, we present the code that integrated TC with the "apply"-style tactic, which can make the TC more powerful.

• Recall the core idea of TC: replace potential incorrect tools/tactics with predefined correct ones. In this setting, we replace incorrect "apply"-style tactics with 12 predefined "apply"-style tactics.
• Step 1: Check whether we need to process the "apply" tactics. If we need and the previous tactic does not begin with "apply", then we directly change ‘apply'-style proofs to single-step method, which is sledgehammer+11 tactics. And if succeed via sledgehammer+11 tactics, then we continue. That is, if succeed via sledgehammer+11 tactics, for the next tactic, if it still begins with “apply”, we directly ignore it. If fails, we move to Step 2
• Step 2: Try the given "apply"-style tactics. If fails, we move to Step 3.
• Step 3: If Step 2 fails, then try sledgehammer+11 tactics. And if it succeeds, we continue. And if it fails, we try all 12 predefined "apply"-style tactics.
• If Step 3 fails, then the prover fails.

The following is the Python-like pseudocode.

#tactic_list: list of the tactics of formal proof
#prover: Isabelle Prover 
#TCUsage: whether employ Tool Correction
tool_heuristics=['by auto','by arith','by blast', 'by simp',
'by fastforce', 'by force', 'by eval', 'by presburger', 'by sos',
'by linarith', 'by (auto simp: field_simps)', 'sledgehammer']


# can be other heuristics.
apply_heuristics=['apply auto','apply arith','apply blast', 'apply simp',
'apply fastforce', 'apply force', 'apply eval', 'apply presburger', 'apply sos',
'apply linarith', 'apply (auto simp: field_simps)', 'apply assumption']


output={}
previous_tactics="None"
for tactic in tactic_list:
    use_heuristics=False
    
    if tactic.strip().startswith("done") and output.has_key('ignore_apply'): #solve "apply"-style via "by".
        previous_tactics="done"
        continue

    # Step 1 Begin
    if tactic.strip().startswith("apply") and TCUsage:
        if output.has_key('ignore_apply') and previous_tactics.startswith("apply"): 
            # solved by previous tactics, such as single-step
            continue
        elif not (previous_tactics.startswith("apply")) #If previous one is not "apply"
            for tool_try in tool_heuristics: # try single-step
                output = prover.run_tac(tool_try)
                if output['error'] is None:
                    break
            if output['error'] is None: 
                #go to next tactic, and ignore the following "apply" 
                #becuase already finish the proof
                output['ignore_apply']=True #solve the proof
                continue
        else:
            #do nothing
    # Step 1 End
            

    previous_tactics=tactic
    
    #Step 2 Begin        
    output = prover.run_tac(tactic)
    #Step 2 End

    if output['error'] is not None:
        if TCUsage: # Use Tool Correction or Not
            if tactic.strip().startswith("by") or tactic.strip()==("."):
                use_heuristic=True
    
        if ("sledgehammer" in tactic) or use_heuristic:
            for tool_try in tool_heuristics:
                output = prover.run_tac(tool_try)
                if output['error'] is None:
                    output['ignore_apply']=True
                    break
                    
                    
        # Step 3 Begin
        if TCUsage and tactic.strip().startswith("apply"):
            for tool_try in tool_heuristics:
                output = prover.run_tac(tool_try)
                if output['error'] is None:
                    output['ignore_apply']=True #solve the proof
                    break
            
            if output['error'] is not None:
                for apply_try in apply_heuristics:
                    output = prover.run_tac(apply_try)
                    if output['error'] is None: 
                        # if not use by-style tactic, 
                        # not sure whether the whole proof is solved or not here. 
                        # So that NO output['ignore_apply']=True
                        break
        # Step 3 End
                    
        
    if output['error'] is not None:
        return "tactic_failed", output
    if output['tactic_state'] == 'no goals':
        return "success", output
        
return "proof_incomplete", output

If you think our comment and update address your concerns, could you please consider raising your rating of the paper? Thank you!

The difference between Lyra and other works

The implementation difference between Lyra, Baldur [1], Coderl [2] and RustGen [3] is the following.

Baldur and Coderl need training, but Lyra is training-free. Compared with RustGen (designed for code generation) refining only with previous responses and error messages, the Lyra can sufficiently utilize problem information, informal proof information, previous response and the error message. Meanwhile, Lyra will reset the initial solution, if fails to refine the solution after several rounds. Also, Lyra utilizes “proof -” as the indicator to control the model response to be formal proof.

Meanwhile, the performance comparison between Baldur [1], Thor [4], and Lyra is the following.

As Baldur does not release code or conduct experiments on miniF2F, currently we cannot directly compare their performance. Fortunately, Baldur compared with Thor on AFP topic classification.

• Compared to Baldur, on AFP topic classification, Thor achieves better performance in Computer Science, Logic and Mathematics. Also, they achieve comparable performance on Tool AFP topic classification. This suggests that Thor can achieve better performance than Baldur.
• On the miniF2F dataset, our proposed Lyra is significantly better than Thor. Our Lyra achieves 55.3% on miniF2F-validation and 51.2% on miniF2F-test, while Thor achieves 28.3% on miniF2F-validation and 29.9% on miniF2F-test.
• Therefore, Lyra should be a more powerful model than Baldur in the automated theorem proving area.

[1] First, E., Rabe, M. N., Ringer, T., & Brun, Y. (2023). Baldur: whole-proof generation and repair with large language models. arXiv preprint arXiv:2303.04910.

[2] Le, H., Wang, Y., Gotmare, A. D., Savarese, S., & Hoi, S. C. H. (2022). Coderl: Mastering code generation through pretrained models and deep reinforcement learning. Advances in Neural Information Processing Systems, 35, 21314-21328.

[3] Wu, X., Cheriere, N., Zhang, C., & Narayanan, D. (2023). RustGen: An Augmentation Approach for Generating Compilable Rust Code with Large Language Models.

[4] Jiang, A. Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóźdź, T., Miłoś, P., ... & Jamnik, M. (2022). Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35, 8360-8373.