More Details, Please: Improving Autoformalization with More Detailed Proofs

Authors: guillem  tarrach
albert q jiang
daniel  raggi
wenda  li
mateja  jamnik
Venue: ICML_cc_2024_Workshop_AI4MATH
Published: 2024-06-01 11:28:40

Abstract: The formalization of mathematical theorems and their proofs is a time-consuming and tedious process which, despite recent advances in the reasoning capabilities of AI systems, remains a challenging task for computers. Existing attempts to automate the process with language models struggle with the difference in level of detail between formal and informal proofs. Successful autoformalization requires models to understand and be able to explain the nuances of logical arguments, a critical aspect of reasoning that is often overlooked in existing research. In this work, we introduce Sketch, Prove, Add Detail & Repeat (SPADeR), an approach that enhances proof autoformalizers by using language models to infer and explicitly incorporate implicit details from informal proofs. With the same number of autoformalization attempts, our method increases the percentage of successfully formalized problems in the miniF2F test dataset from 34.8% to 38.1%.

Main paper: 
 introduction: 
 A significant body of recent work has investigated the reasoning capabilities of Large Language Models (LLMs), particularly in the context of solving mathematical problems. One frequently studied task is Automated Theorem Proving (ATP), which involves automatically generating formal proofs of mathematical theorems. However, few studies have investigated the ability of LLMs to understand and explain mathematical arguments. In this work, we introduce an approach that leverages this capability to construct more detailed informal mathematical proofs, thereby improving the process of autoformalization -the translation of informal proofs into formally verifiable formal proofs. Informal proofs lack many details that are necessary to verify their correctness. While formal proofs do not suffer from this issue, in practice the focus on low-level details makes formal automated theorem provers less successful at high-level planning. As a result, autoformalization systems struggle with the discrepancy in the level of detail in formal and informal proofs (Jiang et al., 2023, Section 5.2 and Appendix C) . Our approach uses LLMs to explain informal proofs by inferring and incorporating implicit details, thereby bridging the gap between informal and formal proofs.To plan ahead and focus on the overall proof strategy, mathematicians usually write proofs in a non-linear, hierarchical manner: They start by writing a high-level proof draft and iteratively add more detail until the proof is considered complete. Previous work on language model-based ATP has studied such hierarchical set-ups (Li et al., 2021; Jiang et al., 2023; Mikuła et al., 2023) , but has not explored adding detail to informal proofs. For example, in Draft, Sketch and Prove (DSP) (Jiang et al., 2023) , a high-level informal proof draft is used to inform a more detailed formal proof sketch, which is later completed by an automated theorem prover. A common error case occurs in the process of translating informal drafts into formal sketches. This process happens in a single step: the model must decide which steps in the draft need further argumentation, add the missing details, and translate the informal draft to the formal language all at once. Therefore, the approach could benefit from using specialized models for each of the three stages, particularly adding the missing details as it is especially complex.Our main contribution is SPADER, a method that enhances autoformalizers through the use of LLMs to construct more detailed informal mathematical proofs by incorporating the implicit reasoning steps into them. The approach is illustrated in Figure 1 . Starting with a theorem statement and an informal proof, we use an autoformalizer to generate a formal proof sketch. We attempt to complete the sketch using an automated prover. If some steps cannot be proved, we use an LLM to provide more details about them and re-attempt the process with a new, more detailed, informal proof. The process succeeds if the additional detail is correct and offers a good explanation for the problematic step.Our experiments show that SPADER increases the success rate of autoformalization systems. With the same number of autoformalization attempts, adding detail to informalProblem. Expand the product (x+1) 2 •x. Show that it is x 3 + 2x 2 + x.Solution. We have (x + 1) 2 = x 2 + 2x + 1.Multiplying this by x gives x 3 + 2x Problem. Expand the product (x + 1) 2 • x. Show that it is x 3 + 2x 2 + x.Solution. We have (x + 1) 2 = (x + 1)(x + 1)= x • x + x • 1 + 1 • x + 1 • 1 = x 2 + 2x + 1.Multiplying this by x gives x 3 + 2x Given formal and informal statements of a theorem and an informal proof, we attempt to autoformalize the proof and then formally verify it. Whenever a particular step cannot be proved, we add more details to it using a language model. We re-attempt the formal verification with the more detailed informal proof. The inclusion of more details into informal proofs improves the performance of the autoformalizer.proofs with GPT-4o increases the number of successfully verified problems in the miniF2F test from 85 (34.8%) to 93 (38.1%).In conclusion, we make the following contributions:• We propose a method for using LLMs to construct more detailed proofs by inferring implicit details in informal mathematical proofs.• We demonstrate the usefulness of the presented method for autoformalization.Our work shows that LLMs can provide detailed mathematical proofs by inferring and explaining implicit reasoning steps. This ability helps bridge the gap between informal and formal mathematical proofs and enables LLM-based autoformalization systems to verify more theorems. 
mathematical reasoning with language models: 
 With recent advances in language models, particularly the introduction of LLMs, there has been an increase in research into their reasoning capabilities, particularly in the context of mathematical problem-solving (Hendrycks et al., 2021; Drori et al., 2022; Welleck et al., 2021) . While alternative prompting methods (Wei et al., 2022; Yao et al., 2023; Zheng et al., 2023a) help improve the accuracy of reasoning arguments, language models still frequently make mistakes. These challenges highlight the need for robust verification methods to complement informal reasoning.Furthermore, the ability of LLMs to understand and explain existing arguments remains largely unexplored. In this work, we investigate these abilities and their evaluation through autoformalization and formal verification.To address the limitations of reasoning with language models, recent work has explored the combination of informal reasoning with formal verification through autoformalization. While early approaches to autoformalization with deep learning took inspiration from Neural Machine Translation (Wang et al., 2018) , it has been observed (Wu et al., 2022) that LLMs are better suited for this task because of their incontext few-shot learning capabilities (Brown et al., 2020) and the scarcity of parallel informal-formal data. Draft, Sketch and Prove (DSP) (Jiang et al., 2023) approaches automated theorem proving by autoformalizing computergenerated informal proofs. Autoformalization proceeds in two stages. The first stage uses an LLM to generate a formal sketch that follows the informal proof. The formal sketch is not a complete formal proof; instead, it outlines the overall proof strategy by describing intermediate conjectures. In the second stage, an off-the-shelf formal theorem prover is employed to prove the intermediate conjectures in the sketch, thus completing the proof. However, in many cases, the informal proof does not contain enough detail for the automated prover to fill in the gaps. Don't Trust: Verify (Zhou et al., 2024) applies a similar method to open-ended mathematical problems. The method consists of generating an informal chain-of-thought reasoning argument to find the answer to a problem, which is considered valid only if it can be autoformalized and formally verified by an automated prover. This approach suffers from the same problem, where informal solutions sometimes fail to be verified despite being correct. Lyra (Zheng et al., 2023b) addresses this issue by prompting LLMs to repair errors in the formal proofs. In our approach, we instead prompt LLMs to add more detail to the informal proofs. We note that informal solutions to the test problems used to evaluate the methods in Lyra, as well as ours, may be part of the training data for the LLMs used (GPT-4 and GPT-4o. respectively). Therefore, these methods are better understood as methods for autoformalization rather than theorem-proving.The construction of mathematical proofs in non-linear ways, where detail is dynamically added to problematic steps, has been more widely studied in the context of formal theorem proving. IsarStep (Li et al., 2021) introduces a benchmark for the task of generating intermediate steps in a formal proof. Magnushammer (Mikuła et al., 2023) combines a premise selection model with formal proof generators (Jiang et al., 2022) . The premise selection model is employed to find premises that imply the intermediate conjectures generated by the proof generator, which together constitute a proof of the theorem. Baldur (First et al., 2023) approaches ATP by generating a full formal proof with a pre-trained language model and using a specialized model to repair any errors with it. However, unlike the methods in Section 2.2, none of these methods make use of informal mathematical data, which is significantly more abundant than formal data. 
spader: enhancing autoformalization with more detailed informal proofs: 
 We now describe SPADER (Sketch, Prove, Add Details & Repeat), our approach to autoformalization and formal verification. This approach enhances the performance of autoformalizers by using LLMs to construct more detailed proofs that guide the autoformalization and formal verification process. The approach is illustrated in Figure 1 and summarized in Algorithm 1. We assume the user has access to an autoformalizer and an automated theorem prover or proof assistant. Given an informal proof -a proof draft in the terminology of DSP (Jiang et al., 2023) -the approach consists of the following stages:Stage 1 (Sketch). The informal proof draft is translated into a formal sketch using an autoformalizer. The formal sketch need not be a complete formal proof; it may contain open conjectures that will be handled in the next stage.The formal sketch should follow the high-level structure of the informal draft. For example, in Figure 1 , the different intermediate conjectures in the formal proof can be mapped to steps with the same color in the informal draft. This may be achieved through the use of comments in the sketch.Stage 2 (Prove). An automated theorem prover attempts to fill in the missing details in the formal sketch, thus completing the proof. If a proof is found, the process has been successful. If the theorem prover is unable to prove an intermediate step, the step is flagged as not proven, and the theorem prover proceeds with the rest of the proof, assuming that the step is true.Stage 3. (Add Detail). The steps in the formal sketch that could not be proved are mapped to the corresponding steps in the informal draft. A separate model, typically an LLM, is then prompted to provide more details on the steps in question and to generate a more detailed informal draft.Repeat. The process is repeated starting from Stage 1 with the new draft.In Figure 1  
experiments: 
 Next, we describe the experiments we conducted to evaluate whether adding detail to informal proofs with SPADER improves the performance of autoformalizers.We evaluate SPADER on the miniF2F dataset (Zheng et al., 2021) . The miniF2F dataset comprises 488 mathematical problems (244 validation problems and 244 test problems). Each problem consists of a collection of formal statements in different formal languages: Isabelle (Paulson, 1988) , Lean (de Moura et al., 2015) , MetaMath (Yu et al., 2024) and HOL Light (Bansal et al., 2019) . This dataset was expanded in DSP (Jiang et al., 2023) to include an informal statement and a human-written informal solution for each formal statement. Our goal is to correctly autoformalize and formally verify the informal solution in Isabelle. We evaluate the performance of our method according to the number of test problem solutions that can be correctly formalized and verified.We performed our experiments with the Isabelle proof assistant (Paulson, 1988) . We have considered M = 1 and M = 2 detailing passes. This allows us to compare the effect of multiple detailing passes.As our autoformalization model, we use GPT-4o 1 . We prompt the model through the OpenAI API to translate the informal proof into a formal Isabelle/HOL sketch with 1 https://openai.com/index/hello-gpt-4o/ 3-shot prompting. We prompt the model to include the original proof as comments before the corresponding steps in Isabelle. We also prompt the model to include a comment concluding the informal proof (with "The result follows") so that the end of the proof can be marked as needing more detail in the next stages. We include 3 in-context examples, randomly sampled from a list of 17 hand-labeled samples, which are modified versions of those from (Jiang et al., 2023) . They have been modified to break down the informal proofs (included as comments in the formal proof) into smaller steps. We hope that segmenting informal proofs into smaller steps makes it easier to pinpoint the problematic steps later. To generate a diverse set of sketches across multiple runs, we generate them with temperature sampling with a temperature parameter of 0.6 as in DSP (Jiang et al., 2023) .We attempt to complete the sketch using the Isabelle theorem prover. Whenever Isabelle fails to prove an intermediate conjecture, we attempt to prove it with several heuristics, as in DSP (Jiang et al., 2023) , and Sledgehammer (Paulson & Blanchette) , a collection of automated theorem provers. If these fail to prove a conjecture, we add a sorry statement, which tells Isabelle to assume that the step has been proven and allows it to continue verifying the rest of the proof. If the verification process encounters an error (e.g. if the formal sketch contains syntax errors), we abort and stop the run. If a proof is parsed correctly but contains sorry statements, we add an 'unproven' flag to the last comment before each such statement. Since the comments contain the original informal proof, the flagged steps are those that require more detail. We concatenate all the steps to recover the original proof and surround the flagged steps with the strings <MORE_DETAIL> and </MORE_DETAIL>.To add detail to the proof, we prompt GPT-4o to rewrite the proof with more detail in the marked steps. We use temperature sampling with a temperature parameter of 0.4. We have used a lower temperature parameter than before to prioritize accuracy over diversity since only one detailed draft is generated per sketch. We generate either one (if M = 2) or two (if M = 1) formal sketches for each of the new drafts and re-attempt the formal verification. If M = 2, we repeat the process of adding detail to unproven steps, generating a formal sketch, and attempting to complete it.We ensure that the number of autoformalization attempts is consistent across the different experiments (M = 1, M = 2 and the baseline) by implementing a modified version of Algorithm 1, which is described in the appendix.We have run each experiment N = 100 times and consider a problem solution to be successfully autoformalized whenever one of these succeeds. To avoid confusion in our discussion, we will distinguish between individual runs (each run of an experiment) and autoformalization attempts (each time the autoformalizer is called). Each individual run may generate up to three sketches with different levels of detail, so the process involves at most 300 autoformalization attempts. Since we stop a run whenever a formal proof is found or the verification encounters an error, this bound is rarely reached in practice (with the average number of attempts being 108).As a baseline, we compare our approach against our implementation of the autoformalization method presented in DSP (Jiang et al., 2023) : we first generate a formal sketch, which we try to formally verify in Isabelle using the same procedure described above. We refer to this baseline as Sketch and Prove since it does not include the Draft stage in DSP: we conduct our experiments exclusively with humangenerated proofs. These proofs, unlike computer-generated ones, are known to be correct and contain no errors. This allows us to isolate the effect of additional detail on autoformalization more accurately. As discussed above, for each individual run, we use the same number of autoformalization attempts in the baseline and the other approaches.The results of our experiments on autoformalization are displayed in Table 1 . With the same number of autoformalization attempts, SPADER achieves a higher success rate than the Sketch and Prove baseline. We note that SPADER is able to solve the same number of problems with M = 1 and M = 2, which suggests that adding even more detail to detailed sketches does not improve performance. Figure 2 shows how the number of successfully solved problems changes with the number of individual runs N . 
discussion: 
 LLMs Can Understand and Explain Informal Proofs.In our experiments, we have asked LLMs to provide more details on specific steps in mathematical proofs. For 8 prob- lems in the miniF2F dataset, the new, more detailed proofs could be formalized, while the original proofs could not. Therefore, the details added by the LLM must be correct (since they have been formally verified) and must provide a good explanation of the arguments in the original proof (since they help verify the rest of the proof). We have included a few successful examples in the appendix.Additional Details do not Improve Autoformalization on Easy Problems. We observe from Figure 2 that for small numbers of runs (N < 20), the more detailed proofs do not improve the success rate of autoformalizers. All the problems that are proved by the baseline, but not by SPADER in this range, are solved in subsequent runs by SPADER on initial autoformalization attempts (i.e., by autoformalizing the original drafts, which do not contain additional details). This suggests that the process of adding detail is helpful only for difficult problems. Future research may explore distinguishing which proofs benefit most from additional detail so that resources can be allocated more effectively.Multiple Detailing Passes are not Necessary. Table 1 and Figure 2 indicate that adding detail twice (M = 2) does not yield better performance than adding detail once (M = 1).As discussed above, the performance of the baseline (which corresponds to M = 0) is similar to that of M = 1, 2 for small numbers of runs, suggesting that the similar trend for M = 1 and M = 2 might not hold for a very large number of runs (N ≫ 100). However, verifying or making use of this would require an impractical amount of computational resources. It is also possible that more detailing passes are beneficial for more complicated informal proofs, since they are usually less detailed.Use of Specialized Models for Adding Detail. We have experimented with using specialized models that retrieve relevant references or insert intermediate steps in proofs to provide more detail. However, these models have not proved successful at improving autoformalization. We believe this is due to the difference in distribution between the problems in the miniF2F dataset, consisting of high-school level mathematics and employing rich language in their solutions, and our training data, which is collected from ProofWiki 2 and consists of university-level mathematics using more rigid language. 
conclusion: 
 To create successful autoformalization systems, it is essential to reconcile the lack of detail of informal proofs with the high detail requirements of formal verification systems.In this paper, we introduced SPADER, an approach that enhances autoformalizers by using Large Language Models (LLMs) to construct more detailed informal mathematical proofs. By inferring and incorporating implicit details in proofs, this approach improves the accuracy of language model-based autoformalizers. This shows that LLMs possess the ability to understand and explain existing mathematical arguments. 
 
 Appendix: This paper presents work whose goal is to advance the field of Machine Learning. There are many potential societal consequences of our work, none of which we feel must be specifically highlighted here.prompting the model to follow the informal proof very closely and make the informal steps (included in comments) as close as possible. The motivation behind this is that, with smaller steps, our approach will be able to more accurately zone in on the parts of the proof that are difficult for the automated prover. In contrast to (Jiang et al., 2023) , instead of prompting the model to invoke the Sledgehammer automated prover to prove intermediate conjectures whenever possible, we allow the model to predict premises that will prove it. The second prompt contains less detailed instructions.We sample 3 random examples from a list of 17 hand-labeled samples and include them as in-context examples. The examples contain the original informal proof as comments: for each step in the informal proof, a comment containing it is followed by the corresponding formal statement. The examples are based on the examples from (Jiang et al., 2023) ; however, we segment the informal proofs into smaller steps. For each set of examples and prompts, we have generated two outputs with temperature sampling with a temperature parameter of 0.6 and a maximum output context length of 1024 tokens. We did not observe any significant difference in the performance of the two prompts in our validation runs. For the following sketching stages (j > 0), we use only the first prompt and generate a single output per set of in-context examples, also with a temperature parameter of 0.6 and a maximum output context length of 1024 tokens.Whenever an intermediate conjecture in the formal sketch fails to be proved, we attempt to prove it with the following heuristics: auto, simp, blast, fastforce, force, eval, presburger, sos, arith, linarith, auto simp: field simps algebra simps. Note that, differently to DSP (Jiang et al., 2023) , we include algebra simps in the last one. If the heuristics fail, we attempt to prove the step with the Sledgehammer automated prover (Paulson & Blanchette) . We interact with Isabelle from Python scripts via Portal to ISAbelle (Jiang et al., 2021) .Below, we include four examples of problems whose original human-written solution could not be autoformalized with the Sketch and Prove baseline, but which could be autoformalized with the additional detail provided by GPT-4o with SPADeR. We include the original informal statement and original human-written informal solution, as well as the more detailed informal solution and complete formal solutions provided by SPADeR. We show two number theory problems (Figure 3 and Figure 4 ) and two algebra problems (Figure 5 and Figure 6 ). The first problem (Figure 3 ) was discussed in Appendix C of DSP (Jiang et al., 2023) as an example of a problem whose human-written solution could not be correctly autoformalized due to not containing enough detail, but for which a computer-written solution could. Problem. What is the units digit of the sum of the squares of the first nine positive integers? Show that it is 5.Original informal solution. We can reduce the amount of work we have to do in this problem by realizing that the units digit of the sum of the squares is the units digit of the sum of the units digits of the squares. In other words, the units digit of 1 2 + 2 2 + . . . + 9 2 is the units digit of 1 + 4 + 9 + 6 + 5 + 6 + 9 + 4 + 1 = 45, which is 5.Detailed informal solution. We can reduce the amount of work we have to do in this problem by realizing that the units digit of the sum of the squares is the units digit of the sum of the units digits of the squares. To find the units digit of 1 2 + 2 2 + . . . + 9 2 , we first compute the units digit of each square: -The units digit of 1 2 is 1.-The units digit of 2 2 is 4.-The units digit of 3 2 is 9.-The units digit of 4 2 is 6.-The units digit of 5 2 is 5.-The units digit of 6 2 is 6.-The units digit of 7 2 is 9.-The units digit of 8 2 is 4.-The units digit of 9 2 is 1. Summing these units digits, we get 1 + 4 + 9 + 6 + 5 + 6 + 9 + 4 + 1 = 45. Thus, the units digit of the sum 1 2 + 2 2 + . . . + 9 2 is the same as the units digit of 45, which is 5. University of CambridgeUniversity of Edinburgh. Correspondence to: Guillem Tarrach <guillem.tarrach@gmail.com>. AI for MATH Workshop at ICML 2024, Vienna, Austria. Copyright 2024 by the author(s). 


Decision: The paper proposes a novel method for autoformalization based on DSP, using an iterative manner to fix informal proof with failure details. The proposed method marginal improvement over the DSP baseline. The paper describes a natural modification to the DSP pipeline and the not generally positive results can be useful for the research community. To improve the paper, the author needs to clarify the GPT-4o results, Figure 3, and the statement about informal data usage in the related works section.

Reviews: review: paper_summary: paper_summary: The paper proposes a novel method for autoformalization, using language models to infer and explicitly incorporate implicit details from informal proofs. The percentage of successfully formalized problems increases from 34.8% to 38.1%.
strength_weakness: strength_weakness: More models should be tested.
questions: questions: The success rate in [DRAFT, SKETCH, AND PROVE](https://arxiv.org/pdf/2210.12283) paper with the "Human informal proof" setting is 39.3%, why does your paper have only 34.8%? Is GPT-4o weaker than Codex used in DSP? Can you reimplement the score of DSP?
paper_summary: paper_summary: This paper proposes a novel framework for autoformalization on top of DSP. The primary motivation comes from the misalignment between the reasoning steps in informal proofs and formal sketches, where one step in natural language might correspond to multiple formal codes in Isabelle. Therefore, the paper suggests adding an additional pipeline: whenever a specific conjecture in the proof sketch fails to pass Isabelle's proof checking, the LLM will be prompted to expand the informal proof of this sketch and extend the formalization of this step. The experimental results show that the proposed method is effective, improving the pass rate compared to the ablation counterpart.
strength_weakness: strength_weakness: The experimental result using GPT-4o is relatively low. In my understanding, the Sketch and Prove baseline is the same as DSP with a human-written informal proof. However, DSP achieves a 39.3% pass rate on the miniF2F test with the Codex model, whereas the Sketch and Prove baseline with GPT-4o achieves only a 34.8% pass rate. This is unlikely to happen, as GPT-4o has significant improvements compared to Codex and other models. One experimental result on GPT-4 (not GPT-4o) with DSP can be seen in the [Lyra](https://arxiv.org/abs/2309.15806) or [LEGO-Prover](https://openreview.net/forum?id=3f5PALef5B) papers, where GPT-4 achieves a 43.0% pass rate with model-generated proof (the result on human-written proof should be comparable). I don't understand why the pass rate for GPT-4o is so low with Sketch and Prove and SPADER.
questions: questions: Please justify the question I raised in the `Reasons To Reject`.
paper_summary: paper_summary: The paper introduces SPADER (Sketch, Prove, Add Details & Repeat), a method to enhance autoformalization of mathematical proofs using Large Language Models (LLMs). The approach aims to bridge the gap between informal and formal proofs by using LLMs to infer and incorporate implicit details from informal proofs, thereby increasing the success rate of formal verification. The method was tested on the miniF2F dataset, showing an improvement in the percentage of successfully formalized problems from 34.8% to 38.1%. The paper contributes by proposing a detailed-oriented approach to autoformalization and demonstrating its effectiveness in improving the accuracy of language model-based theorem provers.
strength_weakness: strength_weakness: n/a
questions: questions: Your results indicate that multiple detailing passes (M = 2) do not significantly improve performance over a single pass (M = 1). Could you discuss why this might be the case and whether there are scenarios where multiple passes could be more beneficial?
paper_summary: paper_summary: This paper describes a methodology for proof autoformalization using an iterative sketching and informal proof repair procedure. Given an informal theorem statement and proof, and a formal statement in Isabelle, they generate a formal sketch in the style of DSP. Automated reasoning tools attempt to fill in the sketch, and locations where failures occur are mapped to the informal proofs. The informal proofs are then rewritten with more detail and passed for another round of the process. They show marginal improvement over the (draft) sketch prove baseline, with no evidence as to the necessity of the iterativeness of the procedure.
strength_weakness: strength_weakness: 1. The results indicate marginal-at-best improvement over the sketching baseline. The iterative nature of the approach is not demonstrated to be useful. They mention Lyra in the related works, which also performs an iterative procedure based on amending formal proofs given erroneous data, which does yield some positive results with multiple passes. However, the alteration method here does not seem to help with multiple passes.
2. The idea of adding further detail to the informal proof is not new, and is done in Decomposing the Enigma (https://arxiv.org/abs/2305.16366) where the informal proof is enhanced at the start, rather than only making modifications after the automated reasoning tools fail.
questions: questions: 1. Could you include a baseline comparing Decomposing the Enigma vs. SPADeR? It seems that an additional informal proof refinement may be unnecessary, as you can begin with a refinement at the start of the process.
2. Can you clarify this sentence in the related works section: "None of these methods, however, can make use of informal mathematical data, which is significantly more abundant than formal data." Is the intended purpose to claim that SPADeR is capable of using informal data? If so, the same is true of all methods listed in the autoformalization section, yet I think an important distinction should be made with whether these methods are better understood as autoformalizers rather than theorem-provers due to potential test-set contamination.
3. The authors mention in the appendix that Figure 3 corresponds to a theorem which could not be proven in the DSP paper using a human proof, but can be with an automatically generated proof. Can the authors clarify whether they are using human-informal proofs, as there does not seem to be an initial drafting phase, and whether *their* implementation of the Sketch and Prove baseline is not capable of proving this theorem, but SPADeR is?