An In-Context Learning Agent for Formal Theorem-Proving

Authors: amitayush  thakur
george  tsoukalas
yeming  wen
jimmy  xin
swarat  chaudhuri
Venue: colmweb_org_COLM_2024_Conference
Published: 2024-03-22 23:43:12

Abstract: We present an in-context learning agent for formal theorem-proving in environments like Lean and Coq. Current state-of-the-art models for the problem are finetuned on environment-specific proof data. By contrast, our approach, called COPRA, repeatedly asks a high-capacity, general-purpose large language model (GPT-4) to propose tactic applications from within a stateful backtracking search. Proposed tactics are executed in the underlying proof environment. Feedback from the execution is used to build the prompt for the next model query, along with selected information from the search history and lemmas retrieved from an external database. We evaluate our implementation of COPRA on the miniF2F benchmark for Lean and a set of Coq tasks from the CompCert project. On these benchmarks, COPRA significantly outperforms few-shot invocations of GPT-4. It also compares favorably against finetuning-based approaches, outperforming REPROVER, a state-of-the-art finetuned approach for Lean, in terms of the pass@1 metric. Our code and data are available at https://github.com/trishullab/copra

Main paper: 
 introduction: 
 The ability of large language models (LLMs) to learn in-context (Brown et al., 2020) is among the most remarkable recent findings in machine learning. Since its introduction, in-context learning has proven fruitful in a broad range of domains, from text and code generation (OpenAI, 2023b) to image generation (Ramesh et al., 2021) to game-playing (Wang et al., 2023a) . In many tasks, it is now best practice to prompt a general-purpose, black-box LLM rather than finetune smaller-scale models.In this paper, we investigate the value of in-context learning in the discovery of formal proofs written in frameworks like Lean (de Moura et al., 2015) and Coq (Huet et al., 1997) . Such frameworks allow proof goals to be iteratively simplified using tactics such as variable substitution and induction. A proof is a sequence of tactics that iteratively "discharges" a given goal.Automatic theorem-proving is a longstanding challenge in computer science (Newell et al., 1957) . Traditional approaches to the problem were based on discrete search and had difficulty scaling to complex proofs (Bundy, 1988; Andrews & Brown, 2006; Blanchette et al., 2011) . More recent work has used neural models -most notably, autoregressive language models (Polu & Sutskever, 2020; Han et al., 2021; Yang et al., 2023) -that generate a proof tactic by tactic.The current crop of such models is either trained from scratch or fine-tuned on formal proofs written in a specific proof framework. By contrast, our method uses a highly capable, general-purpose, black-box LLM (GPT-4-turbo (OpenAI, 2023a) * ) that can learn in context. We show that few-shot prompting of GPT-4 is not effective at proof generation. However, one can achieve far better performance with an in-context learning agent (Yao et al., 2022; Wang et al., 2023a; Shinn et al., 2023 ) that repeatedly invokes GPT-4 from within a higherlevel backtracking search and uses retrieved knowledge and rich feedback from the proof environment. Without any framework-specific training, our agent achieves performance comparable to -and by some measures better than -state-of-the-art finetuned approaches.Figure 1 : Overview of COPRA. COPRA takes as input a formal theorem statement and performs a stateful proof search through an in-context learning agent. At each step of search, the agent has access to the search history, error feedback from the proof environment, and relevant lemmas retrieved from a database, which are formatted according to a prompt serialization protocol.Figure 1 gives an overview of our agent, called COPRA. † The agent takes as input a formal statement of a theorem and optional naturallanguage hints about how to prove the theorem. At each time step, it prompts the LLM to select the next tactic to apply. LLM-selected tactics are "executed" in the underlying proof assistant. If the tactic fails, COPRA records this information and uses it to avoid future failures.Additionally, the agent uses lemmas and definitions retrieved from an external database to simplify proofs. Finally, we use a symbolic procedure (Sanchez-Stern et al., 2020) to only apply LLM-selected tactics when they simplify the current proof goals (ruling out, among other things, cyclic tactic sequences).Our use of a general-purpose LLM makes it easy to integrate our approach with different proof environments. Our current implementation of COPRA allows for proof generation in both Lean and Coq. To our knowledge, this implementation is the first proof generation system with this capability.We evaluate COPRA using the miniF2F (Zheng et al., 2021) benchmark for competition-level mathematical reasoning in Lean, as well as a set of Coq proof tasks (Sanchez-Stern et al., 2020) from the CompCert (Leroy, 2009) project on verified compilation. In both settings, COPRA outperforms few-shot calls to GPT-4. On miniF2F, COPRA outperforms REPROVER, a state-of-the-art finetuned approach for Lean theorem-proving, in terms of the established pass@1 metric. Using a refinement of the pass@1 metric, we show that COPRA can converge to correct proofs with fewer model queries than REPROVER as well as PROVERBOT9001, a state-of-the-art approach for Coq. Finally, we show that a GPT-4-scale model is critical for this setting; an instantiation of COPRA with GPT-3.5 is less effective.To summarize our contributions, we offer: (i) a new approach to formal theorem-proving, called COPRA, that combines in-context learning with search, knowledge retrieval, and the use of rich feedback from the underlying proof environment; (ii) a systematic study of the effectiveness of the GPT-4-based instantiation of COPRA, compared to few-shot GPT-4 invocations, ablations based on GPT-3.5, and state-of-the-art finetuned baselines; (iii) an implementation of COPRA, which is the first open-source theorem-proving system to be integrated with both the Lean and Coq proof environments. 
problem formulation: 
 A (tactic-based) theorem-prover starts with a set of unmet proof obligations and applies a sequence of proof tactics to progressively eliminate these obligations. Each obligation o is a pair (g, h) , where g is a goal and h is a hypothesis. The goal g consists of the propositions that need to be proved in order to meet o; the hypothesis h is the set of assumptions that can be made in the proof of g. The prover seeks to reduce the obligation set to the empty set.(a) theorem mod_arith_2 (x : N) : x % 2 = 0 → (x * x) % 2 = 0 := begin intro h, rw mul_mod, rw h, rw zero_mul, refl, end (b) x: N h: x % 2 = 0 ⊢ x * x % 2 = 0 (c) (de Moura et al., 2015) , of a basic theorem about modular arithmetic (the proof is automatically generated using COPRA). The first step of the proof is the intro tactic, which changes a goal P → Q to a hypothesis P and a goal Q. The next few steps use the rw (rewrite) tactic, which applies substitutions to goals and hypotheses. The last step is an application of the refl (reflexivity) tactic, which asserts definitional equivalences.In code generation settings, LLMs like GPT-4 can often generate complex programs from one-shot queries. However, one-shot queries to GPT-4 often fail at even relatively simple formal proof tasks.Figure 2-(c ) shows a GPT-4-generated incorrect Lean proof of our example theorem.By contrast, we follow a classic view of theorem-proving as a discrete search problem (Bundy, 1988) . Specifically, we offer an agent that searches the state space of the underlying proof environment and discovers sequences of tactic applications that constitute proofs. The main differences from classical symbolic approaches are that the search is LLM-guided, history-dependent, and can use natural-language insights provided by the user or the environment. Now we formalize our problem statement. Abstractly, let a proof environment consist of: where w e is some feedback that explains the error. Error states (O, w) satisfy the property that T((O, w), a) = (O, w) for all a. • A set of global contexts, each of which is a natural-language string that describes the theorem to be proven and insights (Jiang et al., 2022b) about how to prove it. The theorem-proving agent can take a global context as an optional input and may use it to accelerate search.Let us lift the transition function T to tactic sequences by defining:T(O, α) = T(O, a 1 ) if n = 1 T(T(O, ⟨a 1 , . . . , a n-1 ⟩), a n ) otherwise.The theorem-proving problem is now defined as follows: Problem 1 (Theorem-proving). Given an initial state O in and an optional global context χ, find a tactic sequence α (a proof ) such that T(O in , α) = QED.In practice, we aim for proofs to be as short as possible. 
the copra agent: 
 The COPRA agent solves the theorem-proving problem via a GPT-4-directed depth-first search over tactic sequences. Figure 3 shows pseudocode for the agent. At any given point, the algorithm maintains a stack of environment states and a "failure dictionary" Bad that maps states to sets of tactics that are known to be "unproductive" at the state.At each search step, it pushes the current state on the stack and retrieves external lemmas and definitions relevant to the state. After this, it serializes the stack, Bad(O), the retrieved information, and the optional global context into a prompt and feeds it to the LLM. The LLM's output is parsed into a tactic and executed in the environment.One outcome of the tactic could be that the agent arrives at QED or makes some progress in the proof. A second possibility is that the new state is an error. A third possibility is that the tactic is not incorrect but does not represent progress in the proof. We detect this scenario using a symbolic progress check as described below. The agent terminates successfully after reaching QED and rejects the new state in the second and third cases. Otherwise, it recursively continues the proof from the new state. After issuing a few queries to the LLM, the agent backtracks.Progress Checks. Following Sanchez-Stern et al. (2020) , we define a partial order ⊒ over states that indicates when a state is "at least as hard" as another. Formally, for states O 1 andO 2 with O 1 / ∈ Err and O 2 / ∈ Err, O 1 ⊒ O 2 iff ∀o i = (g i , h i ) ∈ O 2 . ∃o k = (g k , h k ) ∈ O 1 . g k = g i ∧ (h k ⊆ h i ). Intuitively, O 1 ⊒ O 2 if for every obligation in O 2 ,there is a stronger obligation in O 1 . While comparing the difficulty of arbitrary proof states is not well-defined, our definition helps us eliminate some straightforward cases. Particularly, these cases include those proof states whose goals match exactly and one set of hypotheses contains the other.COPRA(O, χ) 1 PUSH(st, O) 2 ρ ← RETRIEVE(O) 3 for j ← 1 to t 4 do p ← PROMPTIFY(st, Bad(O), ρ, χ) 5 a ∼ PARSETACTIC(LLM(p)) 6 O ′ ← T(O, a) 7 if O ′ = QED 8 then terminate successfully 9 else if O ′ ∈ Err or ∃O ′′ ∈ st. O ′ ⊒ O ′′ 10 then add a to Bad(O) 11 else COPRA(O ′ , χ) 12 POP(st)Figure 3 : The search procedure in COPRA. T is the environment's transition function; st is a stack, initialized to be empty. Bad(O) is a set of tactics, initialized to ∅, that are known to be bad at O. LLM is an LLM, PROMPTIFY generates a prompt, PARSETACTIC parses the output of the LLM into a tactic (repeatedly querying the LLM in case there are formatting errors in its output), and RETRIEVE gathers relevant lemmas and definitions from an external source. The overall procedure is called with a state O in and an optional global context χ.As shown in Figure 3 , the COPRA procedure uses the ⊒ relation to only take actions that lead to progress in the proof. Using our progress check, CO-PRA avoids cyclic tactic sequences that would cause nontermination.The routines PROMPTIFY and PARSETACTIC together constitute the prompt serialization protocol and are critical to the success of the policy. Now we elaborate on these procedures.PROMPTIFY carefully places the different pieces of information relevant to the proof in the prompt. It also includes logic for trimming this information to fit the most relevant parts in the LLM's context window. Every prompt has two parts: the "system prompt" (see more details in Appendix A.3) and the "agent prompt."The agent prompts are synthetically generated using a context-free grammar and contain information about the state stack (including the current proof state), the execution feedback for the previous action, and the set of actions we know to avoid at the current proof state.The system prompt describes the rules of engagement for the LLM. It contains a grammar (distinct from the one for agent prompts) that we expect the LLMs to follow when it Figure 4 : A "conversation" between the LLM and the search algorithm in COPRA. Query #1, Query #2, . . . represent queries made as the proof search progresses. The column labeled Query #i depicts the prompt at time step i and the corresponding LLM response. The LLM response is parsed into a tactic and executed, with the error feedback incorporated into the next prompt.proposes a course of action. The grammar carefully incorporates cases when the response is incomplete because of the LLM's token limits. We parse partial responses to extract the next tactic using the PARSETACTIC routine. PARSETACTIC also identifies any formatting errors in the LLM's responses, possibly communicating with the LLM multiple times until these errors are resolved.Figure 4 illustrates a typical "conversation" between the LLM and COPRA's search algorithm via the prompt serialization protocol. Note, in particular, the prompt's use of the current goals, the stack, and error feedback for the last executed tactic. 
evaluation: 
 Benchmarks. We primarily evaluate COPRA on the Lean proof environment using miniF2Ftest (Zheng et al., 2021) benchmark. This benchmark comprises 244 formalizations of mathematics problems from (i) the MATH dataset (Hendrycks et al., 2021) , (ii) high school mathematics competitions, (iii) hand-designed problems mirroring the difficulty of (ii). Broadly, these problems fall under three categories: number theory, algebra, and induction.To evaluate COPRA's ability to work with multiple proof frameworks, we perform a secondary set of experiments on the Coq platform. Our benchmark here consists of a set of a theorems drawn from the CompCert compiler verification project (Leroy, 2009) . The dataset was originally evaluated on the PROVERBOT9001 system (Sanchez-Stern et al., 2020) . Due to budgetary constraints, our evaluation for CompCert uses 118 of the 501 theorems used in the original evaluation of PROVERBOT9001. For fairness, we include all 98 theorems proved by PROVERBOT9001 in our system. The remaining theorems are randomly sampled.Implementing COPRA. Our implementation of COPRA is LLM-agnostic, and functions as long as the underlying language model is capable of producing responses which parse according to the output grammar. We instantiate the LLM to be GPT-4-turbo as a middleground between quality and affordability. Because of the substantial cost of GPT-4 queries, we cap the number of queries that COPRA can make at 60 for the majority of our experiments.In both Lean and Coq, we instantiate the retrieval mechanism to be a BM25 search. For our Lean experiments, our retrieval database is mathlib (mathlib Community, 2020), a mathematics library developed by the Lean community. Unlike miniF2F, our CompCertbased evaluation set is accompanied by a training set. Since COPRA relies on a black-box LLM, we do not perform any training with the train set, but do use it as the retrieval database for our Coq experiments.Inspired by DSP (Jiang et al., 2022b) , we measure the efficacy of including the naturallanguage (informal) proof of the theorem at each search step in our Learn experiments. We use the informal theorem statements in miniF2F-test to generate informal proofs of theorems using few-shot prompting of the underlying LLM. The prompt has several examples, fixed over all invocations, of informal proof generation given the informal theorem statement. These informal proofs are included as part of the global context. Unlike miniF2F, which consists of competition problems originally specified in natural language, our Com-pCert evaluation set comes from software verification tasks that lack informal specifications. Hence, we do not run experiments with informal statements and proofs for Coq.Initially, we run COPRA without access to the retrieval database. By design, COPRA may backtrack out of its proof search before the cap of 60 queries has been met. With the remaining attempts on problems yet to be solved, COPRA is restarted to operate with retrieved information, and then additionally with informal proofs. This implementation affords lesser expenses, as appending retrieved lemmas and informal proofs yields longer prompts, which incur higher costs. More details are discussed in Appendix A.1.1.Baselines. We perform a comparison with the few-shot invocation of GPT-4 in both the miniF2F-test and CompCert domains. The "system prompt" in the few-shot approach differs from that of COPRA, containing instructions to generate the entire proof in one response, rather than going step-by-step. For both COPRA and the few-shot baseline, the prompt contains several proof examples which clarify the required format of the LLM response. The proof examples, fixed across all test cases, contain samples broadly in the same categories as, but distinct from, those problems in the evaluation set.For our fine-tuned baselines, a challenge is that, to our knowledge, no existing theoremproving system targets both Lean and Coq. Furthermore, all open-source theorem proving systems have targeted a single proof environment. As a result, we had to choose different baselines for the Lean (miniF2F) and Coq (CompCert) domains.Our fine-tuned baseline for miniF2F-test is REPROVER, a state-of-the-art retrievalaugmented open-source system that is part of the LeanDojo project (Yang et al., 2023) . We also compare against LLEMMA-7b and LLEMMA-34b (Azerbayev et al., 2023) . In the CompCert task, we compare with PROVERBOT9001 (Sanchez-Stern et al., 2020) , which, while not LLM-based, is the best public model for Coq.Ablations. We consider ablations of COPRA which use GPT-3.5 and CodeLlama (Roziere et al., 2023) as the underlying model. We also measure the effectiveness of backtracking in COPRA's proof search. Additionally, we ablate for retrieved information and informal proofs as part of the global context during search.Metric. The standard metric for evaluating theorem-provers is pass@k (Lample et al., 2022) . In this metric, a prover is given a budget of k proof attempts; the method is considered successful if one of these attempts leads to success. We consider a refinement of this metric called pass@k-with-n-queries. Here, we measure the number of correct proofs that a prover can generate given k attempts, each with a budget of n queries from the LLM or neural model. We enforce that a single query includes exactly one action (a sequence of tactics) to be used in the search. We want this metric to be correlated with the number of correct proofs that the prover produces within a specified wall-clock time budget; however, the cost of an inference query on an LLM is proportional to the number of responses generated per query. To maintain the correlation between the number of inference queries and wall-clock time, we restrict each inference on the LLM to a single response (see Appendix A.1.2 for more details). Statistics for the two approaches, as well as a comparison with the fewshot GPT-3.5 and GPT-4 baselines, appear in Table 1 . As we see, CO-PRA offers a significant advantage over the few-shot approaches. For example, COPRA solves more than twice as many problems as the fewshot GPT-4 baseline, which indicates that the state information positively assists the search. Furthermore, we find that running the few-shot baseline with 60 ‡ attempts (provided a nonzero temperature), exhibits considerably worse performance compared to COPRA. This indicates that COPRA makes more efficient use of queries to GPT-4 than the baseline, even when queries return a single tactic (as part of a stateful search), as opposed to a full proof. We include further details in Appendix A.1.1.pass@k -with-n-queries k × n (Timeout) % proved Few-Shot (CodeLlama) 1 × 1 (600) 0.0% Few-Shot (GPT 3.5) 1 × 1 (600) 2.8% COPRA (CodeLlama) 1 × 500 (600) 5.73% COPRA (GPT-3.5) 1 × 60 (600) 9.02% Few-Shot 1 × 1 (600) 13.52% Few-Shot (T = 0.7) 60 ‡ × 1 (COPRA is capable of improving the performance of GPT-3.5, CodeLlama over its few-shot counterpart. We note that the use of GPT-4 seems essential, as weaker models like GPT-3.5 or CodeLlama have a reduced ability to generate responses following the specified output format.Comparison with Finetuned Approaches on miniF2F. Figure 5 shows our comparison results for the miniF2F domain. With a purely in-context learning approach, CO-PRA outperforms REPROVER, proving within just 60 queries theorems that REPROVER could not solve after a thousand queries. This is remarkable given that REPROVER was finetuned on a curated proof-step dataset derived from Lean's mathlib library. For fairness, we ran REPROVER multiple times with 16, 32, and 64 (default) as the maximum number of queries per proof-step. We obtained the highest success rates for REPROVER with 64 queries per proof-step. We find that COPRA without retrieval outperforms REPROVER.Our pass@1 performance surpasses those of the best open-source approaches for miniF2Ftest on Lean. COPRA proves 29.09% of theorems in miniF2F-test theorems, which exceeds that of LLEMMA-7b & LLEMMA-34b, (Azerbayev et al., 2023) and REPROVER (Yang et al., 2023) . It is important to note that these methods involve training on curated proof data, while COPRA relies only on in-context learning.We also establish a correlation between the number of queries needed for a proof and wallclock time in Figure 6 and Table 3 (more details are discussed in Appendix A.1.3). Although the average time per query is higher for COPRA, COPRA still finds proofs almost 3x faster than REPROVER. This can explained by the fact that our search is more effective as it uses 16x fewer queries than REPROVER (see Table 2 ). The average time per query includes the time taken to execute the generated proof step by the interactive theorem prover. Hence, a more effective model can be slow in generating responses while still proving faster compared to a model with quicker inference, by avoiding the waste of execution time on bad proof-steps. Qualitative Analysis of Proofs. We performed an analysis of the different categories of miniF2F problems solved by COPRA and REPROVER. Figure 8 and Figure 9 (in Appendix A.2) show that COPRA proves more theorems in most of the categories and takes fewer steps consistently across all categories of problems in miniF2F as compared to REPROVER. Additionally, we find that certain kinds of problems, for example, International Mathematics Olympiad (IMO) problems and theorems that require induction, are difficult for both approaches.From our qualitative analysis, there are certain kinds of problems where our languageagent approach seems especially helpful. For instance, Figure 7 shows a problem in the 'numbertheory' category that REPROVER could not solve. More examples of interesting proofs that COPRA found appear in the Appendix A.2 in Figure 10 .Effectiveness of Backtracking, Informal Proofs, and Retrieval. We show the ablation for the backtracking feature of COPRA in Table 1 . We find that backtracking is useful when proofs are longer or more complex, as COPRA is more likely to make mistakes which require amending. We include additional examples in Figure 12 (in Appendix A.2).Figure 6 : COPRA vs. REPROVER on the miniF2F benchmark on the pass@nseconds metric.From Table 1 , we see that retrieval helps in proving more problems. Retrieval reduces the tendency of the model to hallucinate the lemma names and provides the model with existing lemma definitions it otherwise may not have known. We include a proof generated by COPRA that uses a retrieved lemma in Figure 7 .We experiment with adding model-generated informal proofs as global context in COPRA's proof search. As evidenced in Table 1 , COPRA is able to outperform PACT (Han et al., 2021) and the state-of-the-art (29.6%) expert iteration method (Polu et al., 2022) in a pass@1 search through the incorporation of informal proofs. Furthermore, increasing the maximum query count to 100 enables a further increase in COPRA's performance to 30.74%. An example of a proof found when incorporating informal proofs is shown in Figure 15 (see Appendix A.5).Given that the pretraining corpus of GPT-4 is not publicly available, it is imperative to assess for the possibility of test-set leakage in our experiments. We perform an analysis of those proofs checked into the open-source miniF2F repository compared to those proofs COPRA discovers.We categorize those proofs available in miniF2F according to the number of tactics required and the complexity of the tactic arguments. These results can be found in detail in Appendix A.1.4. As seen in Table 4 , we find that COPRA reproduces none of the "long" proofs in miniF2F-test repository. Setting aside those cases where the proof consists of a single tactic, approximately 91.93% of the proofs generated by COPRA either bear no overlap to proofs in miniF2F, or no proof has been checked in. We provide examples of proofs generated by our approach compared to those included in miniF2F in Figure 11 . (n m : N+) : (gcd n m) * (lcm n m) = n * m" which led to the proof while REPROVER failed to prove this theorem. It is important to note that just retrieving the correct lemma is not sufficient, but knowing how to use it correctly is equally important. The Figure 18 shows how COPRA utilizes the capabilities of LLM to correctly use the retrieved lemma in the proof.Coq Experiments COPRA can prove a significant portion of the theorems in our Coq evaluation set. As shown in Figure 16 (in Appendix A.5), COPRA slightly outperforms PROVERBOT9001 when both methods are afforded the same number of queries. COPRA with retrieval is capable of proving 57 of 118 theorems within our cap of 60 queries. Furthermore, COPRA exceeds the fewshot baselines utilizing GPT-4 and GPT-3.5, which could prove 36 and 10 theorems, respectively, on our CompCertbased evaluation set. Some example Coq proofs generated by COPRA are shown in Appendix A.5 in Figure 17 . 
related work: 
 Neural Theorem-Proving. There is a sizeable literature on search-based theorem-proving techniques based on supervised learning. Neural models are trained to predict a proof step given a context and the proof state, then employed to guide a search algorithm (e.g. best-first or depth-limited search) to synthesize the complete proof.Early methods of this sort (Yang & Deng, 2019; Sanchez-Stern et al., 2020; Huang et al., 2019) used small-scale neural networks as proof step predictors. Subsequent methods, starting with GPT-f (Polu & Sutskever, 2020) , have used language models trained on proof data.PACT (Han et al., 2021) enhanced the training of such models with a set of self-supervised auxiliary tasks. Lample et al. (2022) introduced HyperTree Proof Search, which uses a language model trained on proofs to guide an online MCTS-inspired, search algorithm.Among results from the very recent past, REPROVER trains a retrieval-augmented transformer for proof generation in Lean. LLEMMA performs continued pretraining of the CodeLlama 7B & 34B on a math-focused corpus. Baldur (First et al., 2023) generates the whole proof in one-shot using an LLM and then performs a single repair step by passing error feedback through an LLM finetuned on (incorrect proof, error message, correct proof) tuples. AlphaGeometry (Trinh et al., 2024) integrates a transformer model trained on synthetic geometry data with a symbolic deduction engine to prove olympiad geometry problems. In contrast to these approaches, COPRA is entirely based on in-context learning.We evaluated COPRA in the Lean and Coq environments. However, significant attention has been applied to theorem proving with LLMs in the interactive theorem prover Isabelle (Paulson, 1994) . Theorem-proving systems for Lean and Isabelle are not directly comparable due to the substantial differences in automation provided by each language. Isabelle is equipped with Sledgehammer (Paulson & Blanchette, 2015) , a powerful automated reasoning tool that calls external automated theorem provers such as E (Schulz, 2002) and Z3 (De Moura & Bjørner, 2008) to prove goals. Thor (Jiang et al., 2022a) augmented the PISA dataset (Jiang et al., 2021) to include successful Sledgehammer invocations, and trained a language model to additionally predict hammer applications. Integrating these ideas with the COPRA approach is an interesting subject of future work.The idea of using informal hints to guide proofs was first developed in DSP (Jiang et al., 2022b) , which used an LLM to translate informal proofs to formal sketches that were then completed with Isabelle's automated reasoning tactics. Zhao et al. (2023) improved on DSP by rewriting the informal proofs to exhibit a more formal structure and employs a diffusion model to predict the optimal ordering of the few-shot examples. LEGOProver (Wang et al., 2023b) augmented DSP with a skill library that grows throughout proof search. Lyra (Zheng et al., 2023) iterated on DSP by utilizing error feedback several times to modify the formal sketch, using automated reasoning tools to amend incorrect proofs of intermediate hypotheses. DSP, LEGOProver, and Lyra heavily rely on Isabelle's hammer capabilities (which are not present in other ITPs like Lean) and informal proofs for formal proof generation (see Appendix A.1.5 for details). Moreover, the requirement for informal proofs in these approaches prohibits their application in the software verification domain, where the notion of informal proof is not well-defined. However, we propose a domainagnostic stateful search approach within an in-context learning agent which iteratively uses execution feedback from the ITP with optional use of external signals like retrieval and informal proofs.In-Context Learning Agents. Several distinct in-context learning agent architectures have been proposed recently (Significant-Gravitas, 2023; Yao et al., 2022; Shinn et al., 2023; Wang et al., 2023a) . These models combine an LLM's capability to use tools Schick et al. (2023) , decompose a task into subtasks (Wei et al., 2022; Yao et al., 2023) , and self-reflect (Shinn et al., 2023) . However, COPRA is the first in-context learning agent for theorem-proving. 
conclusion: 
 We have presented COPRA, the first in-context-learning approach to theorem-proving in frameworks like Lean and Coq. The approach departs from prior LLM-based theoremproving techniques by performing a history-dependent backtracking search by utilizing in-context learning, the use of execution feedback from the underlying proof environment, and retrieval from an external database. We have empirically demonstrated that COPRA significantly outperforms few-shot LLM invocations at proof generation and also compares favorably to finetuned approaches.As for future work, we gave GPT-4 a budget of at most 60 queries per problem for cost reasons. Whether the learning dynamics would drastically change with a much larger inference budget remains to be seen. Also, it is unclear whether a GPT-4-scale model is truly essential for our task. We have shown that the cheaper GPT-3.5 agent is not competitive against our GPT-4 agent; however, it is possible that a Llama-scale model that is explicitly finetuned on interactions between the model and the environment would have done better. While data on such interactions is not readily available, a fascinating possibility is to generate such data synthetically using the search mechanism of COPRA. 
reproducibility statement: 
 We are releasing all the code needed to run COPRA as supplementary material. The code contains all "system prompts" described in Section Appendix A.3 and Appendix A.4, along with any other relevant data needed to run COPRA. However, to use our code, one must use their own OpenAI API keys. An issue with reproducibility in our setting is that the specific models served via the GPT-4 and GPT-3.5 APIs may change over time. In our experiments, we set the "temperature" parameter to zero to ensure the LLM outputs are as deterministic as possible.Funding Acknowledgements. This work was partially supported by NSF awards CCF-1918651, CCF-2403211, and CCF-2212559, and a gift from the Ashar Aziz Foundation. 
 
 Appendix: We introduce a common proof environment for COPRA, which can also be used by any other approach for theorem-proving. The proof environment has a uniform interface that makes COPRA work seamlessly for both Lean and Coq. It also supports the use of retrieval from external lemma repositories and the use of informal proofs when available (as in the case of miniF2F). In the future, we plan to extend COPRA to support more proof languages.COPRA provides support for various LLMs other than the GPT-series, including opensourced LLMs like Llama 2 (Touvron et al., 2023) and Code Llama (Roziere et al., 2023) . For most of our experiments, all the theorems are searched within a timeout of 600 seconds (10 minutes) and with a maximum of 60 LLM inference calls (whichever exhausts first). To make it comparable across various LLMs, only one response is generated per inference. All these responses are generated with the temperature set to zero, which ensures that the responses generated are more deterministic, focused, and comparable. In one of our ablations with few-shot GPT-4, we use set the temperature to 0.7 and run more than 1 attempt. The number of attempts for few-shot GPT-4 matches the number of queries COPRA takes to either successfully prove or fail to prove a certain theorem. This comparison is not completely fair for COPRA because individual queries focus on a single proof step and cannot see the original goal, yet measures a useful experiment which indicates the benefits of COPRA's stateful search under a fixed budget of API calls to GPT-4.We use GPT-3.5, GPT-4 (OpenAI, 2023b), and CodeLLama (Roziere et al., 2023) to test the capabilities of COPRA. We find that it is best to use COPRA's different capabilities in an ensemble to enhance its performance while also minimizing cost. Therefore, we first try to find the proof without retrieval, then with retrieval, and finally with informal proofs (if available) only when we fail with retrieval. The informal proofs are used more like informal sketches for the formal proof and are generated in a separate few-shot invocation of the LLM. Thereafter, COPRA simply adds the informal proofs to its prompt which guides the search. To ensure fairness in comparison, we make sure that the number of guidance steps is capped at 60 and the 10-minute timeout is spread across all these ensemble executions. The use of a failure dictionary (see Section 3) enables fast failure (see Table 3 ) which helps in using more strategies along with COPRA within the 60 queries cap and 10-minute timeout. From Table 2 , it is clear that despite the significant overlap between the different ablations, the ensemble covers more cases than just using one strategy with COPRA. While extra lemmas are often useful, the addition of extra information from retrieval may also be misleading because the retriever can find lemmas that are not relevant to proving the goal, so the best performance is acquired by using the different capabilities in the manner we describe. Similarly, the use of informal proofs as a sketch for formal proofs can potentially increase the number of steps needed in a formal proof, decreasing the search efficacy. For example, an informal proof can suggest the use of multiple rewrites for performing some algebraic manipulation which can be easily handled with powerful tactics like linarith in Lean. Table 5 shows the number of tokens used in our prompts for different datasets.We consider the metric pass@k-with-n-queries to assess the speed of the proposed approach and the effectiveness of the LLM or neural network to guide the proof search. It is a reasonable metric because it does a more even-handed trade-off in accounting for the time taken to complete a proof and at the same time ignores very low-level hardware details.Different approaches need a different amount of guidance from a neural model to find the right proof. For example, approaches like Baldur (First et al., 2023) , DSP (Jiang et al., 2022b) , etc., generate the whole proof all at once. On the other hand, GPT-f (Polu & Sutskever, 2020), PACT (Han et al., 2021) , REPROVER (Yang et al., 2023) , Proverbot (Sanchez-Stern et al., 2020) , and COPRA generate proofs in a step-by-step fashion. We argue that pass@k-with-n- Table 3 : Average time taken by our approach (COPRA) and REPROVER on miniF2F dataset.We split the values according to the success of the proof search on that problem. We also report values per query.queries is a fairer metric to compare these different types of approaches because it correlates with the effectiveness of the proof-finding algorithm in an implementation-agnostic way.Since the exact time might not always be a good reflection of the effectiveness because of hardware differences, network throttling, etc., it makes sense to not compare directly on metrics like pass@k-minutes or pass@k-seconds. Not only these metrics will be brittle and very sensitive to the size, hardware, and other implementation details of the model, but not every search implementation will be based on a timeout. For example, PROVERBOT9001 does not use timeout-based search (and hence we don't compare on the basis of time with PROVERBOT9001).We show that pass@k-with-n-queries, correlates well with wall-clock time for finding proofs by using the metric pass@k-seconds. pass@k-seconds measures the number of proofs that an approach can find in less than k seconds. The plot in Figure 6 shows that pass@k-seconds follows the same trend as pass@k-with-n-queries as shown in Figure 5 .We can use the comparison of COPRA with REPROVER (Yang et al., 2023) on the miniF2F dataset to explain the correlation between finding proofs fast and pass@k-with-n-queries.From Table 3 , we know that on average the time taken per guidance (which includes time taken to execute the proof steps on ITP as well) is around 0.52 seconds for REPROVER and 13.48 seconds for COPRA. Given that REPROVER's guidance LLM is small, we can assume that REPROVER does not take any time (zero time) to query its LLM and spends most of the 0.52 seconds running the proof steps on ITP. Now, we can reasonably estimate GPT-4 average response time to be approximately 13 seconds from Table 3 . However, we see that the number of guidance used by REPROVER (from Table 2 ) is about 16x higher on success. Interestingly, this also shows up in the wall clock time, which is around 3x higher for REPROVER on success, so there is a tradeoff between the two, but the number of queries dominates when the guidance model is of low quality. Hence, given a high-quality guidance model, we can empirically argue that asymptotically the search will converge to a proof faster (assuming a proof is achievable with the guidance model).A key risk with closed-source pretrained models like GPT-4 is data leakage, i.e., overlaps between the evaluation set and the pretraining set. Naturally, we cannot be certain that COPRA does not benefit from such leakage. However, there are several reasons to believe that data leakage is not a significant contributor to our results.First, we note that COPRA significantly outperforms few-shot invocations of GPT-4. If the results on COPRA were significantly tainted by data leakage, we would have expected better performance from few-shot GPT-4.Second, it is highly unlikely that GPT-4 has been trained on proof-state and tactic pair generated by hooking up the Lean ITP. Not all the formal proofs of the miniF2F test dataset are available online (only 80 proofs are available in Lean). Furthermore, if one were to manually annotate (proof state, tactic) pairs, one would need ground truth tactics to annotate with, the majority of which do not appear in miniF2F-test. Given that GPT-4 is a generalpurpose LLM, it is highly unlikely that while training GPT-4 the miniF2F dataset was first manually annotated, and then proof-state and tactic pair information was collected by hooking up the Lean ITP.Also, in our agent interactions, we limit ourselves only to the goal at that point. There is no mention of the original theorem anywhere (except for the very first proof-state), so the chances that GPT-4 can correlate any intermediate state with the original theorem are slim, unless it has learned a model of Lean's kernel, which is highly unlikely. It is also improbable that GPT-4 has seen the proof-state in the same format that we use, let alone using the execution feedback which has not been used in any known previous works for Lean.One could hypothesize that some of the few-shot GPT-4 proofs might be influenced by potential training on the miniF2F dataset. However, this does not seem to be true because we see that most of the proofs we generated were either not mentioned in the miniF2F test dataset or completely different from the manually written proofs in the miniF2F test dataset (including the first step mismatch). Table 4 shows the detailed analysis of proofs generated by COPRA and the proofs mentioned in miniF2F test dataset for Lean. From the Table 4 , it is clear that most of the proofs generated by COPRA are different from the proofs mentioned in the miniF2F. The ones that are exactly the same are simple single-tactic proofs that just use exactly one of the linarith, nlinarith, or norm num tactics without any arguments. If we set aside these straightforward simple cases, then about 91.93% of the proofs generated by COPRA are either different from the proofs mentioned in the miniF2F or do not have a proof mentioned in the miniF2F dataset. Out of all proofs generated by COPRA about 25.33% proofs are for theorems that have no proofs mentioned in the miniF2F test dataset as compared to 22.95% for REPROVER. Some of the proofs generated by our approach as compared to proofs mentioned in the miniF2F test dataset are shown in Figure 11 .Finally, the ability of agent interactions to enhance the basic LLM approach seems to transcend OpenAI's LLMs. We ran COPRA on the recently released CodeLlama. From Table 2 , COPRA improved CodeLlama's capabilities to prove theorems by about 5% on miniF2F dataset. This indicates that the in-context learning capabilities that we build are transferable and LLM-agnostic.An interactive theorem prover (ITP) is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves a sort of interactive proof editor, or other interfaces, with which a human can guide the search for proofs. A formal proof written in an interactive theorem prover can be verified automatically by computers, whereas an informal proof is written in natural language can only be verified by a human. Generally, formal proofs are much more rigorous and pedantic than informal proofs. So informal proof can be loosely considered as a proof sketch based on which one can write rigorous machine-checkable formal proofs.Note that the accuracy numbers of DSP-like approaches (Jiang et al., 2022b; Zhao et al., 2023; Zheng et al., 2021) are not directly comparable to ours because they use a differ- ent proof language. These approaches use Isabelle, which, unlike Lean, allows the use of powerful automatic reasoning tools like Sledgehammer. Methods following the DSP pipeline use informal proofs for formal proof synthesis. While this strategy works well on mathematics-competition benchmarks like miniF2F, it is less applicable to domains such as software verification, where there is often no informal specification, as well as domains that use customized, domain-specific formalizations. Furthermore, having access to informal proofs (human-written or LLM-generated) shifts the problem of synthesizing the formal proof towards an autoformalization problem, as the LLM is likely to have seen correct natural language proofs of miniF2F problems in its training. Additionally, unlike DSP-like approaches which tend to use pass@100 or pass@200, we only use pass@1.Figure 10 shows some other interesting proofs generated by our approach on miniF2F dataset. Figure 8 and Figure 9 shows the breakdown of theorems proved in various categories by COPRA versus REPROVER. Figure 10 shows some interesting miniF2F proofs as done by COPRA. Figure 11 shows the comparison of proofs mentioned in the miniF2F repository versus the proofs discovered by COPRA. Figure 12 shows the proofs which were only possible because of our backtracking feature.Parts of the 'system prompt' used by COPRA for theorem proving in Lean are shown in Fig. 13 . (d) theorem mathd_numbertheory_341 (a b c : N) (h 0 : a ≤ 9 ∧ b ≤ 9 ∧ c ≤ 9) (h 1 : nat.digits 10 ((5ˆ100) % 1000) = [c, b,a]) : a + b + c = 13 := begin norm_num at h 1 , cases h 1 , linarith, end (e) theorem amc12b_2002_p7 (a b c : N) (h 0 : 0 < a ∧ 0 < b ∧ 0 < c) (h 1 : b = a + 1) (h 2 : c = b + 1) (h 3 : a * b * c = 8 * (a + b + c)) : aˆ2 + (bˆ2 + cˆ2) = 77 := begin rw [h 1 , h 2 ] at h 3 , ring_nf at h 3 , rw [h 1 , h 2 ], ring_nf, simp [h 1 , h 2 ] at *, ring_nf at *, nlinarith, endFigure 10 : Some other interesting proofs generated for miniF2F by COPRA. The length of the proofs generated shows that interaction with the environment helps in fixing the errors encountered while writing long proofs. These long sequences of rewrites are not easy to synthesize without knowing the exact execution feedback from the environment which often contains the hint to fix the rewrites. igure 18: We can see from this example that to be able to capitalize the well-retrieved lemmas, the models need to learn how to use those lemmas as well. In our case, BM25 does a very good job of retrieving the best lemmas, however, GPT-4 could not use it correctly in the first couple of tries. It was only because of our novel stateful backtracking approach that we could capture the previous mistakes along with the last error message all in the same prompt which dissuaded the GPT-4 from making repeated mistakes and getting to the right prediction. It is also important to note that we could not solve this problem without retrieval, but once we know the list of relevant lemmas, knowing how to use them becomes extremely important. Given this example, it should not be surprising that even when other retrieval methods like DPR perform better than BM25, COPRA has an edge because it can act as per the rich feedback it gets from the environment. Another interesting idea one can try is to let COPRA create a search query to control the retrieved lemma, which can make a simple BM25 search more effective than DPR.0 := mul_ne_zero ( mul_ne_zero h 1 h 2 ) h 3 , field_simp [h 5 ] at h 4 , ring_nf at h 4 , nlinarith, end (d) theorem amc12b_2002_p7 (a b c : N) (h 0 : 0 < a ∧ 0 < b ∧ 0 < c) (h 1 : b = a + 1) (h 2 : c = b + 1) (h 3 : a * b * c = 8 * (a + b + c)) : aˆ2 + (bˆ2 + cˆ2) = 77 := begin rw [h 1 , h 2 ] at h 3 , ring_nf at h 3 , rw [h 1 , h 2 ], ring_nf, simp [h 1 , h 2 ]† COPRA is an acronym for "In-context Prover Agent".‡ To ensure fairness we matched the number of attempts for Few-Shot (GPT-4) baseline with the number of queries COPRA took to pass or fail for each theorem. 


Decision: While there was not a complete consensus on the value of the paper, I believe overall its advantages are outweighing the faults it has. I highly recommend the authors to highlight to what extent they rely on GPT4 or the LLM for the proof, and to what extent their method adds value. Overall, good paper, perhaps requires a bit more polishing.

Reviews: review: paper_summary: paper_summary: This paper proposes an in-context learning approach for solving the task of automated theorem proving. An ICL agent, called COPRA is built to search for a proof in DFS by repeatedly running the proof step generated by GPT-4-turbo with backtracking. 

COPRA has several unique features. 
- COPRA filters out and avoid bad proof steps that result in new proof states weaker than old proof states, since we get no progress from these proof steps. 
- COPRA fixes runtime errors via self-critique.
- CORPA could retrieve and get benefits from lemmas and definitions and informal texts.
- COPRA could work on both Lean and Coq, two tactic-based proof assistants. 

On the Lean miniF2F and Coq CompCert benchmarks, COPRA achieves better performance than the few-shot prompting baseline that targets on generating the full proof in one LLM call. It also performs comparably to the finetuning baselines.
strength_weakness: strength_weakness: I didn't find major issues for this submission, except for a few questions to be clarified below.
questions: questions: 1 From the results, retrieval is very important, improving the pass rate from 26.63 to 29.09. Can you explain in more detail what the input and output are in the step of retrieval, and how do you get the output?
2 The numbers of ReProver listed in Table 1 are different from the numbers reported in LeanDojo paper (25 vs 26.5). Did you run ReProver by yourself and get the results?
3 Do you have ICL exemplars in prompts? If so, what is the format of ICL exemplars? 
4 Can you provide some statistics for the size of our prompts and LLM responses, like the mean, min, max, per request, and per proof?
paper_summary: paper_summary: This paper presents an in-context learning agent called COPRA for formal theorem-proving with Lean and Coq. This is achieved by calling general-purpose models like GPT-4 with the help of frameworks like LeanDoJo. During the tactics generation/proof search process, feedback from execution and search history is integrated to get better performance. On selected benchmarks, COPRA outperforms few-shot invocations of GPT-4 (without the help of theorem-proving environment) and fine-tuned baselines like ReProver.
strength_weakness: strength_weakness: The novelty of this paper is limited. Existing models like ReProver already suggest tactics given goals/premises, and it's known that powerful LLMs like GPT-4 have strong general capabilities, so simply integrating them isn't a major contribution.

The paper could benefit from more in-depth analysis. For example, what problems can GPT-4 solve that ReProver cannot? Since ReProver is trained on mathlib3, what logic types/tactics does it master better? Conversely, what logic types/tactics does GPT-4 master better, and why (could it be due to GPT-4 being trained on a broader range of web-scale data beyond mathlib3)?

Stylistic suggestions:
Figure 2 would look better if (a) and (c) were aligned vertically.
Figure 3 could be improved by placing the notations at the top of the algorithm description, which would enhance reader understanding and align with (more) standard practices (see Algorithm 1 of https://arxiv.org/pdf/2310.10625).
paper_summary: paper_summary: This paper introduces a new search algorithm, COPRA, to tackle the problem of theorem proving. COPRA uses a neat search algorithm, (branded as an "agentic approach") that incorporates elements such as execution feedback and a state comparison heuristic. Because it only uses in-context interactions, it is generally applicable to various domains and shows promising results on miniF2F and CompCert. Overall, the paper is clearly written, interesting, and the method is effective.

As I detail below, my two concerns are as follows. First, there is a limited evaluation, as the authors only test on two datasets. In general, this is fine, but I suspect miniF2F may be contaminated, as the problems are likely also on many mathematical websites. An additional dataset such as LeanDojo benchmark would be more convincing. Second, the method still falls behind SoTA, and it would be more convincing if the authors incorporated fine-tuned language models into their framework to achieve a better performance.
strength_weakness: strength_weakness: - While the authors give a contamination analysis on miniF2F, I don't find it unlikely that elements such as informal proofs or even the formal proofs themselves may be leaked somewhere on GitHub, not necessarily just in the miniF2F-test repository. This could give it an advantage over its baselines. 
- The work only evaluates two datasets. In light of this and the previous point, an additional dataset would be more convincing: for example, if the method can beat ReProver with retrieval at a subset of the LeanDojo benchmark.
- As the baselines included in the paper are mostly simple fine-tuned approaches, the results still fall behind SoTA. For example, HTPS achieve 35% with supervised fine-tuning, and 41% using their search algorithm, while COPRA is still at 31%. I acknowledge the in-context nature of COPRA compared to the fine-tuned setting of many of these works, but I believe the authors should have some comparison to methods like these, which have a better performance.
questions: questions: - What is the effect of including proof feedback? Can models like GPT-4 really learn from feedback? I would be interested in seeing an ablation study where error feedback is omitted when prompting (but still providing it the feedback that things are incorrect).
- Have the authors tried combining small, powerful models such as Llemma or ReProver with the feedback abilities of GPT-4 to further reduce the wall-clock time of proving theorems? As the authors mention, I don't find it unlikely that small models are relatively sufficient for theorem-proving, and I wonder if replacing some of the GPT-4 interactions with Llemma or ReProver would lead to better results. 
- The boost from using informal statements is less than I would have expected, especially in light of the success of DSP-like methods. Could the authors comment on this?
- Can the LLM also provide feedback on the retrieval, to identify whether a retrieval was helpful for the next step?
- Suggestion: I would consider bringing an example of how COPRA works (something like Figure 8) into the main text, which would help me understand the algorithm better than the formalism on pages 3-4.
paper_summary: paper_summary: This paper presents an in-context learning agent for formal theorem proving, where prompts will be revised according to the error messages from the formal environment. The effectiveness of the proposed approach named COPRA has been validated on both Lean (miniF2F) and Coq (CompCert).
strength_weakness: strength_weakness: Weakness: the effectiveness of the proposed approach is still a bit questionable, considering the ReProver baseline in Lean uses a much much smaller model and Proverbot9001 in Coq is not even based on language models and uses way less resources. It is also concerning to see the performance of Copra drops significantly when equipped with a less capable model (e.g., CodeLlamma and GPT-3.5). Admittedly, domain-specific fine-turning/training may explain some of the discrepancy between Copra (CodeLlamma/GPT-3.5) and ReProver, but I believe we still need to see the effectiveness of Copra when equipped with less capable models.
questions: questions: page 3, 'we have an efficient symbolic procedure that can check this relationship for any pair of states': could elaborate a bit on how to check if one proof obligation is stronger than another?

Comments: title: Thanks for the answers
Answers to your questions
Questions about "stateful backtracking"
Thanks for the rebuttal
comment: I appreciate the author's effort in addressing my questions. While I still have concerns about the novelty of this paper, their response has alleviated many of my initial reservations. Consequently, I have increased my score
Thank you for your comment!

Yes, like other work on LLM agents, we are inspired by traditional planning/RL. However, the use of LLMs puts us in a very different space in terms of capabilities. Specifically, while traditional symbolic planning and deep RL have been used for theorem-proving in the past, they haven't been able to scale to the kind of problems that Copra can solve.

It is true that the idea of LLM agents is also explored in efforts like Reflexion. However, the theorem-proving setting opens up some specific opportunities that the approaches you mention do not exploit. Specifically, formal proofs are driven by a rigorous ground-truth specification (the theorem's statement) and can offer detailed error messages explaining the failures of specific actions, and the Copra agent makes use of these. Also, the stateful backtracking search used in Copra is carefully designed to exploit specific characteristics of the theorem-proving setting (for example, we retain information about actions that failed in the past) and is more sophisticated than the sampling-based search in methods like Reflexion.
Thank you for your response. I noticed that your paper highlights stateful backtracking as a significant contribution. However, this approach appears similar to traditional planning methods in reinforcement learning. Additionally, recent works like Reflexion and Reasoning as Planning also employ a comparable strategy of using intermediate reasoning steps or checkpoints for self-improvement/planning. Could you clarify how your work differs from these methodologies?
Dear Reviewer,

Please let us know if you have any questions or clarifications about our response, we would be happy to address them.
Thank you, we are glad to hear that. Please let us know if you have any further questions, we would be happy to answer them.
Thank you for your comments. We would like to address some of those below:

**Question:** Comparison between COPRA and baselines with smaller models.

**Answer:** ReProver and Proverbot9001 are finetuning approaches and require training before use. For COPRA style use, it will need training on the feedback (error signals) data which is hard to generate. In general, in NLP, there has been a shift from finetuning to ICL. The power of ICL in theorem-proving is, in our opinion, a fundamental topic of interest to the COLM community. Open models are improving rapidly -- GPT-4 scale open models are not necessarily that far away.

**Question:** Is the significant performance drop from GPT-4 to GPT-3.5 solely a result of the difference in context width?

**Answer:** We believe that the drop from GPT-4 to GPT-3.5 is possibly because of the context window but also possibly because of the differences in the larger pretraining set. That said, we have thoroughly analyzed our results and found no evidence of leakage. Therefore, there seems to be a jump in the theorem-proving capabilities, and this is an intriguing phenomenon that the COLM community is well-positioned to study more deeply.

**Question:** Feasibility of implementing COPRA using open-source or more academically accessible models?

**Answer:** We evaluated COPRA on CodeLlama 2 (see Table 1) which is open for academic usage. This proves that our approach is agnostic of the underlying model. We show that using COPRA we could boost the performance of few-shot CodeLlama from 0% to 5.73%, which means the novel stateful backtracking search helps regardless of the underlying model. However, the performance is not comparable to GPT-4 because CodeLlama is a less powerful model. We would like to reiterate that open models at the level of GPT-4 are likely to be available in the future due to the rapid progress of the open-source community. For example, we can potentially incorporate a baseline where Llama 3 is used as the foundation model driving COPRA in subsequent revisions.

We would like to thank you for pointing out Graph2Tac, we were not aware of this work and we will cite it. We note that this is a fairly recent work, and we can include it as a baseline in subsequent revisions.
Thank you for the author's response, which addresses my questions.
I very much appreciate the authors' clarification. However, I am still concerned about the comparison between COPRA and the baselines (ReProver and Proverbot9001), where GPT-4 has been used to compete against small (or even none-LM based) models. Both ReProver and Proverbot9001 can be deployed locally, while GPT-4 is still too expensive. I am worried the advantages of COPRA might be diminished once ReProver and Proverbot9001 use stronger models. By the way, you can consider Graph2Tac (https://arxiv.org/abs/2401.02949) as a baseline in Coq, which is more recent and easier to adapt to LLM settings. Additionally, is the significant performance drop from GPT-4 to GPT-3.5 solely a result of the difference in context width? While I am open to the use of GPT-4, I would like to see a more comprehensive discussion on the specific model requirements for COPRA, as well as the feasibility of implementing COPRA using open-source or more academically accessible models.  Given the reasons outlined above, I will keep my rating unchanged.
Thank you for your comment. We would like to address your concerns as follows:

**Comment:** “Standard practice for self-improvement that leads to lack of novelty.”

**Response:** We go beyond just including the error response. The error message is incorporated with a stateful backtracking search. Statefulness helps avoid repeating similar mistakes and helps prune the search space further. Apart from the error message on the last step, the proof steps that were incorrect for the particular state are shown in the prompt, this reduces the search space dramatically, and triggers backtracking if the LLM chooses to repeat the same incorrect step. The stateful tracking of errors allows us to identify proof steps that eventually fail even while executing immediately which further helps in backtracking early and changing the direction of proof. We have included an example of this in the response to your next comment.

**Comment:** “ReProver uses DPR why BM25 works better in COPRA than ReProver”

**Response:** Retrieval helps get the useful lemmas needed to complete a proof, but the tactic prediction model needs to know the right way of using them. The model may fail to predict the right arguments for the lemma, and the proof search may fail despite the retrieval being correct. The ReProver paper doesn’t perform an ablation on how the quality of the retriever impacts its ability to do proofs. It studies the quality of the DPR vs BM25 retriever in terms of MRR but doesn’t have any ablations where ReProver uses BM25 instead of DPR for proof search, so it is hard to know the impact of the quality of retrieved results on the overall proof search.


For the example in Fig. 6, we had the following prompt just before GPT correctly predicted the next proof step:

```
[GOALS]
[GOAL] 1
n = 70   # The goal we want to prove (or proof state)
[HYPOTHESES] 1  # Assumptions about the goal
[HYPOTHESIS] n : ℕ
[HYPOTHESIS] h₀ : 0 < n
[HYPOTHESIS] h₁ : n.gcd 40 = 10
[HYPOTHESIS] h₂ : n.lcm 40 = 280


[THEOREMS] 1  # The retrieved lemmas from BM25 which can help prove goal
[THEOREM] pnat.gcd_mul_lcm : (n m : ℕ+) : (gcd n m) * (lcm n m) = n * m
[THEOREM] tactic.is_prime_helper : (n : ℕ)   (h₁ : 1 < n) (h₂ : nat.min_fac n = n) : nat.prime n
[THEOREM] pnat.lcm_coe : (n m : ℕ+) ....


[INCORRECT STEPS] # Previous mistakes on the given proof state
                  # Each mistake is listed with the ‘STEP’ keyword.
[STEP] apply nat.eq_of_mul_eq_mul_left (by norm_num : 0 < 40),
rw ←pnat.gcd_mul_lcm,
repeat { rw pnat.gcd_coe },
repeat { rw pnat.lcm_coe },
norm_num,
.... .... ....
[STEP] have h₃ : n * 40 = nat.gcd n 40 * nat.lcm n 40, from pnat.gcd_mul_lcm (⟨n, h₀⟩) ⟨40, dec_trivial⟩,
[STEP] rw nat.gcd_mul_lcm,
[STEP] rw pnat.gcd_mul_lcm at h₁,


[LAST STEP] # Last prediction
have h₃ : n * 40 = 10 * 280, from pnat.gcd_mul_lcm (subtype.mk n h₀) (subtype.mk 40 dec_trivial),
linarith,


[ERROR MESSAGE] # Error message on the last step
Got error in 'have h₃ : n * 40 = 10 * 2...':
 error: invalid type ascription, term has type
  pnat.gcd ⟨n, h₀⟩ ⟨40, _⟩ * pnat.lcm ⟨n, h₀⟩ ⟨40, _⟩ = ⟨n, h₀⟩ * ⟨40, _⟩ ...
[END]
```

```
# Prediction by GPT-4
[RUN TACTIC]
have h₃ : n * 40 = 10 * 280, by rw [←nat.gcd_mul_lcm n 40, h₁, h₂],
linarith,
[END]
```

It is easy to see that to be able to capitalize the well-retrieved lemmas, the models need to learn how to use those lemmas as well. In our case, BM25 does a very good job of retrieving the best lemmas, however, GPT-4 could not use it correctly in the first couple of tries. It was only because of our **novel stateful backtracking** approach that we could capture the previous mistakes along with the last error message all in the same prompt which dissuaded the GPT-4 from making repeated mistakes and getting to the right prediction. It is also important to note that we could not solve this problem without retrieval, but once we know the list of relevant lemmas, knowing how to use them becomes extremely important. Given this example, it should not be surprising that even when DPR performs better than BM25, COPRA has an edge because it can act as per the rich feedback it gets from the environment. Another interesting idea one can try is to let COPRA create a search query to control the retrieved lemma, which can make a simple BM25 search more effective than DPR.
I acknowledge that your work includes additional elements (such as error messages) compared to ReProver. However, these are standard practices for self-improvement, which is why I commented on the lack of novelty.

Regarding Figure 6, I'm finding it difficult to comprehend. ReProver also employs retrieval (Dense Passage Retriever) during the proof search process. Could you explain why a potentially weaker retriever like BM25 achieves better performance than ReProver?