An In-Context Learning Agent for Formal Theorem-Proving
Authors: Amitayush Thakur
George Tsoukalas
Yeming Wen
Jimmy Xin
Swarat Chaudhuri
Venue: COLM (2024)
Keywords: theorem proving, formal methods, large language models, agents
TL;DR: We present an LLM agent for formal theorem proving which capitalizes on rich error feedback from the proof environment and proof search history. Our agent conducts an in-context proof search and outperforms state-of-the-art fine-tuned methods.

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

Published as a conference paper at COLM 2024
An In-Context Learning Agent for Formal Theorem-Proving
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin & Swarat Chaudhuri
Department of Computer Science The University of Texas at Austin {ami tayush, george. tsoukalas, ywen, jxin31415]@utexas. edu, swarat@cs, utw.as.eeea.oooo.ua edu
Abstract
We present an in-context learning agent for formal theorem-proving in environments like Lean and Coq. Current state-of-the-an models for the problem are finetuned on environment-specife proof data. By contrast, our approach, called COPRA, repeatedly asks high-capacity, general- purrpose large language model (GPT-4) to propose tactic applications from within a stateful backtracking search. Proposed tactics executed in the underly- ing 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 evalu- ate 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-basee approaches, outperforming REPROVER, hate-offtheeart finetuned approach for Lean, in terms of the pass@1 metric. Our code and data are available at https:/ htt///gtttbbooomoo /tris/ulllbb////// tttshullabbcopra,
Introduction
The ability 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 (OpenAl, 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 p a purposs,, 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 al., 2015) and Coq (Huet al. 1997). Such frameworks allow proof goals to be iteratively simplitied using tactics such as variable substitution and induction. A proof is a sequence of tactics that iteratively "discharges" given goal.
Automatic theorem-proving is a longstanding challenge in computer science (Newell 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 s
most notably, autoregressive language models
(Polu & Sutskever, 2020
Han al. 2021 Yang al. 2023) that generate proof tactic by
tactic.
The current crop of such models is either trained from scratch or fine-tuned on formal proofs written in specific proof framework. By contrast, our method uses a highly capable, general-purpose, black-box LLM (GPT-4-turbo (OpenAl 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 higher- level backtracking search and uses retrieved knowledge and rich feedback from the proof
"For brevity, refer to GPT-4-turbo as GPT-4 in the rest of this paper.

---

Published as a conference paper at COLM 2024
environment. Without any framework-specift training, agent achieves performance comparable to - and by some measures better than state-of-the-art finetuned approaches.
Figure gives an overview of our agent, called COPRA. The agent takes as input a formal statement of theorem and optional natural- language hints about how to prove the theorem. At each time step, prompts the LLM to select the next tactic apply. LLM--slected tac- tics are "executed" in the under- lying proof assistant. the tactic fails, COPRA records this informa- tion and uses avoid future fail- ures.
Formal theorem informal hints (aptional)
COPRA
3. Execute the tactic environment (Lean, Coq)
1. Prompt
Tactic
Synthesis
Parsing
Lemma Database
Feedback
4. Augment the prompt: Backtrack if needed
5. Query lemma database
QED
Additionally, the agent uses lem- mas and definitions retrieved from an external database to simplify proofs. Finally, use 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).
Figure 1: Overview of COPRA. COPRA takes as input 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 his- tory, error feedback from the proof environment, and relevant lemmas retrieved from database, which are formatted according to prompt serialization protocol.
Our use of a general- 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-leve mathematical reasoning in Lean, as well as set of Coq proof tasks (Sanchez- SSanchez-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, state-of-the-art finetuned approach for Lean theorem-proving, in terms of the established pass@1 metric. Using refinement of the pass@l metric, we show that COPRA can converge to correct proofs with fewer model queries than REPROVER well as PROVERBOT9001, state-of-the-art approach for Coq. Finally, we show that 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) new approach to formal theorem-provingg, 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 sfate-of-the-art finetuned baselines; (iii) an implementation of COPRA, which the first open-source poooee--roving system be integrated with both the Lean and Coq proof environments.
2 Problem Formulation
A (tactic-based) theorem--rooeer starts with set of unmet proof obligations and applies sequence of proof factics to progressively eliminate these obligations. Each obligation o is pair (g. kt, where g is goal and is a hypothesis. The goal g consists of the propositions that need to be proved in order to meet 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 the empty set.
COPRA is acronym for "In-context Prover Agent".
2

---

Published as a conference paper at COLM 2024
Figure (a) shows formal proof, in the Lean language (de Moura et al. 2015), of
(a)
(c)
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 goal Q. The next few steps use the rw (rewrite) tactic, which applies substitutions to goals and hypothe- ses. The last step is an application of the refl (reflexivity) tactic, which asserts defi- nitional equivalences.
theorem
begin
mod_arin arith_2
intro h,
(x N) x % 2
have h1
=
2)
(x x)
(nat. mul div_cancel
=0 :=
begin
h) symm,
intro h,
h1, rw nat. mul_div__ae
mul_mod, h,
rw zero_mul, refl,
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.
(show 2, from dvd_refl _) [mul_assoc, nat.
end
(b)
x: NN
mul mod mod_mod_riie right 1,
Figure (c) shows GPT-A-generater incor- rect Lean proof of our example theorem.
h: x %
x
end
By contrast, follow classic view of theorem-proving as a discrete search prob- offer
Figure 2: (a) A Lean theorem and correct proof found by COPRA. (b) Proof state after the first tactic. (c) An incorrect proof gener- ated by GPT-4.
lem (Bundy 1988). Specifically, agent that searches the state space of the un- derlying proof environment and discovers sequences of tactic applications that con- stitute 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 proof environment consist of:
A set of states O. Here, state is either a set O {o1,...,o ox} of obligations or of the form (O,w), w), where
set of obligations and to is textual error message. States of the latter form are error states, and the set of such states is denoted by Err.
A set of initial states, each consisting of a single obligation (gin/ hm) extracted from user-provided theorem.
A unique goal state QED is the empty obligation set.
A finite set of proof tactics.
A transition function a(O,a), which determines the result of applying tactic a to a state O. If a can be successfully applied at state O, then T(O, a) is the new set of obligations resulting from the application. If a is "bad" tactic, then T(O, a) is an error state (O, w,), where W. is some feedback that explains the error. Error states (O, w) satisfy the property that ((O,w),a) = (O,w) w) for all
A set of global contexts, each of which is natural-language string that describes the theorem to be proven and insights (Jiang et al. (202bb) about how to prove it. The theorem-provine agent can take global context as an optional input and may use accelerate search.
Let lift the transition function T to tactic sequences by defining:
T(O,a1) if = T(T(O, (a,,..,, A an) otherwise.
T(O,a)
The theorem-proving problem now defined as follows:
Problem 1 (Theorem-provingg Given initial state On and an optional global context X find a tactic sequence (a proof) such that T(Omp a) = QED.
In practice, aim for proofs to be short as possible.
3

---

Published as a conference paper at COLM 2024
3 The COPRA Agent
The COPRA agent solves the theorem-proving problem via a GPT-4-directed depth-first search over tactic sequences. Figure 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 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 (ad(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 "t least as hard" as another. Formally, for states O, and O2 with Og É Err and O2 & Err, O, 2 O2
Vo; (gi E Oz.
30x = (gx h4)) O₁ 8k A (Ax h;).
Intuitively, O₁ O2 for every obligation in O2, there is stronger obligation in Oj. 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.
As shown in Figure 3 the COPRA pro- cedure uses the relation to only take actions that lead to progress in the proof. Using our progress check, Co-
COPRA(O,A PUSH(sI, O) p RETRIEVE(())
for j < 1 to
PRA avoids cyclic tactic sequences that would cause nontermination.
do + PROMPTIFY(st, Bad (a.((O))).)))) p.x) PARSETACTIC(LLM(p)) O' T(O,a)
The rou- tines PROMPTIFY and PARSETACTIC to- gether constitute the prompt serialization protocol and critical to the success of the policy. Now we elaborate on these procedures.
Prompt Serialization.
if = QED
then terminate successfully else O' Err
30" E st. O' = O" then add to Bad(O) else COPRA(O', x)
10
11
12
PoP(st)
PROMPTIFY carefully places the differ- ent pieces of information relevant to the proof in the prompt. It also in- cludes logic for trimming this informa- tion 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 search procedure in COPRA. T is the environment's transition function; sf is a stack, initialized to be empty. (ad(O) is set of tactics, initialized to Ø, that are known to be bad at O, LLM an LLM, PROMPTIFY generates a prompt, PARSETACTIC parses the output of the LLM into 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 On and an optional global context X.
Figure 3:
The agent prompts are synthetically generated using context-free gram- mar 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 grammar (distinct from the one for agent prompts) that we expect the LLMs to follow when
4

---

Published as a conference paper at COLM 2024
Serialized
[GOALS]
[GOALS]
Proof State
[GOAL]
[GOAL]
x x % 2
x 0x 2
[YPOOTHSSE]]
[HYPOTHESES]
HYPOTHESIS] X:
[HYPOTHESIS] x:
[YPOTTESIS)] h: 0
[MPPTTHSSS)] 1:x%2=0
Stack & Fallure
[LAST STEP]
[TEPS]]
[STEPS] [STEP] intro h,
[STEP]] [STEP] intro h,
intro h,
[STEP] intro
Dictionary
[LAST STEP)
[INCORRECT STEPS]
[LAST STEP]
[STEP] rw h,
nat.mul_man _mod_
[LAST STEP] apply nat.mul wat.mullmoddttte mod_right,
Interaction Result
[SUCCESS] [END]
[ERROR MESSAGE] Got error in 'Tw hi: error: rewrite tactic failed, did not find instance of the pattern target expression [END]
[ERROR MESSAGE]
[SUCCESS]
Got error in
[END]
'apply
nat.mul. mod right,:
error: invalid apply tactic,
failed to unify
=
with
2mm_1"2m____ [END]
LLM
Query #1
Query #2
Query #3
Query #4
Response
[RUN TACTIC] [END]
[RUN TACTIC] apply nat.mul_mod mod_right, [END]
[RUN TACTIC] nat.mul_moot [END]
[RUN MUUTICCIC]
h. [END]
Figure A "conversation" between the LLM and the search algorithm in COPRA. Query #1, Query # represent queries made as the proof search progresses. The column labeled Query #i depicts the prompt at time step and the corresponding LLM response. The LLM response is parsed into tactic and executed, with the error feedback incorporated into the next prompt.
...
proposes 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.
Filureeiillustrates typical "conversation" between the LLM and COPRA'S A's search algorithm via the prompt serialization protocol. Note, 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 miniF2F-
test (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 's ability to work with multiple proof frameworks, we perform sec- ondary set of experiments on the Coq platform. Our benchmark here consists of set of theorems drawn from the CompCert compiler verification project (Leroy 2009). The dataset was originally evaluated on the PROVERBOT9001 system (Sanche7-Stern et al. 2020). Due to budgetary constraints, our evaluation for CompCert uses 118 the 501 theorems used in the original evaluation of PROVERBOT9001. For fairness, we include all 98 theorems proved by PROVERBOT9001 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 ground between quality and affordability. Because of the substantial cost of GPT-4 queries, cap the number of queries that COPRA make at 60 for the majority of our experiments.
middle-

---

Published as a conference paper at COLM 2024
In both Lean and Coq, we instantiate the retrieval mechanism to be 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 CompCert- based 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 natural- language (informal) proot 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 exam- ples, 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 m 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 theorem- proving 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 retrieval- augmented open-source system that is part of the LeanDojo project (Yang et al., 2023). We also compare against LLEMMA-76 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 CodeL (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 budget of k proof atfempts; the method is considered successful if one of these attempts leads to success. We consider a refinement of this metric called wus-@e--ithh---quurres. Here, we measure the number of correct proofs that a prover can generate given k attempts, each with a budget of л queries from the L.LM 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).
6

---

Published as a conference paper at COLM 2024
COPRA Few-Shot LLM Queries. Statistics for the two approaches, as well as comparison with the few- shot GPT-3.5 and GPT-4 baselines, appear in Table [ As we see, Co- PRA offers significant advantage over the few-shot approaches. For example, COPRA solves more than twice as many problems the few- shot GPT-4 baseline, which indicates that the state information positively assists the search. Furthermore, we find that running the few-shot base- line with 6d4 attempts (provided nonzero temperature), exhibits con- siderably worse performance com- pared to COPRA. This indicates that COPRA makes more efficient use of queries to GPT-4 than the baseline, even when queries return single tac- tic (as part of a stateful search), as opposed to full proof. We include further details in Appendix(A.1.1
Evaluation on miniF2F-test
pass@k
% proved
Approach
-willl-n-queries k x n (Timeout)
Few-Shot (CodeLlama)
1 (600)
0.0%
Few-Shot (GPT 3.5)
1 x 1 (600)
2.8%
COPRA (aad)
1 x 500 (600)
5.73%
COPRA (GPI-3.5)
1 60 (600)
9.02%
Few-Shot
1 1 (600)
13.52%
Few-Shot (T 0.7)
60 1 (600)
15.98%
REPROVER Retrieval)
1076 (600)
22.13%
COPRA (- Backtracking)
1 x 60 (600)
24.59%
REPROVER
1 x 3751 (600)
25.00%
LLEMMA-34b
1 x 3200 (600)
25.82%
LLEMMA-7b
1 3200 (600)
26.23%
COPRA
1 60 (600)
26.63%
COPRA (+ Retrieval)
1 60 (600)
29.09%
COPRA is capable of improving the performance of GPT-3.5, Lam over its few-shot counterpart. We note that the use of GPT-4 seems es- sential, weaker models like GPT- 3.5 or CodeLlama have a reduced ability to generate responses follow- ing the specified output format.
COPRA
1 60 (600)
29.92%
(4 Retrieval Informal)
COPRA
100 (1200)
30.74%
(+ Retrieval Informal)
Table 1: Aggregate statistics for COPRA and the base- lines on miniF2F dataset. Note the various ablations of COPRA with and without retrieval or informal proofs. The timeout is wall-clock time budget in seconds allocated across all attempts. Unless other- wise specified, (i) COPRA uses GPT-4 the LLM (ii) the temperature (T) is set to 0.
Comparison with Finetuned Ap- proaches on miniF2F. Figure 5 shows our comparison results for the miniF2F domain. With a purely in-context learning approach, Co- PRA outperforms REPROVER, prov- ing within just 60 queries theorems that REPROVER could not solve after thousand queries. This is remarkable given that REPROVER was finetuned on curated proof-step dataset derived from Lean's mathlib library. For faimesss we ran REPROVER multiple times with 16, 32, and 64 (default) 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 miniF2F- test Lean. COPRA proves 29, 29.09% of theorems in miniF2F-tes: theorems, which exceeds that of LLEMMA-7b & LLEMMA-344 A-4b, [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 wall- clock time in Figure B 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 The average time per query includes the time taken to execute the generated proof step by the interactive theorem prover. Hence, more
Too ensure fairness we matched the number of attempts for Few-Shot (GPT-4) baseline with the number of queries COPRA took pass fail for each theorem.
7

---

Published as a conference paper at COLM 2024
effective model can be slow in generating responses while still proving faster compared to model with quicker inference, by avoiding the waste 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. Fig- (in Appendix A.2 show that COPRA proves more theorems in most of the cat- egories and takes fewer steps consistently across all categories of problems in miniF2F as com-
pass@l-wwith-nnqqerrie
33
ure and Figure 9
Number of Theorems Proved
pared to REPROVER. Additionally, we find that certain kinds of problems, for example, Interna- tional Mathematics Olympiad (IMO) problems and theorems that require induction, are difficult for both approaches.
COFRA (GPT-4-turbo)
evall
ReProver (with Ratrivall
From our qualitative analysis, there are certain kinds of problems where our language- agent approach seems especially helpful. For instance, Figure 7 shows problem in the 'numbertheory' category that REPROVER could not solve. More examples of interesting proofs that COPRA found appear in the Appendix A.2
COPRA (GPT44 turbo)
(withou: Retrevaa)
ReProyeet
(withou: Retrieval)
Number Queries (m)
Figure 5: COPRA vs. REPROVER on the miniF2F benchmark.
in Figure 10
Effectiveness of Backtracking, Informal Proofs, and Retrieval. We show the ablation for the backtracking feature of COPRA in Table [ We find that backtracking is useful when proofs are longer or more complex, as COPRA is more likely make mistakes which require amending. We include additional examples in Figure 12 (in Appendix A.2
From Table 1 we see that retrieval helps in prov- ing more problems. Retrieval reduces the ten- dency of the model to hallucinate the lemma names and provides the model with existing lemma definitions otherwise may not have known. We include proof generated by COPRA that uses a retrieved lemma in Figure 7
pass@n-seconds
Number Theorems Proved
We experiment with adding model-generated in- formal proofs as global context in COPRA'S search. As evidenced in [ COPRA is able to outperform PACT (Han et al., 2021) and the -fate-of-the-art (29.6%) expert iteration method (Polu et al.) 2022) in a pass@1 search through the incorporation of informal proofs. Further- more, increasing the maximum query count to 100 enables further increase in COPRA'S perfor- mance to 30.74%. An example of proof found when incorporating informal proofs is shown in Figure 15 (see Appendix A.5).
COPRA (GPT-4 turbol
(with Retr evail
RePhover
(with Retrievall
COPRA (GPT-/)
ReProver
(withou: Retrivval)
200
300
40
500
Wall-Clock Time in Seconds (n)
Figure 6: COPRA vs. REPROVER on the miniF2F benchmark on the passon- seconds metric.
Test-Set Memorization Concerns. Given that the pretraining corpus of GPT-4 is not publicly available, it is imperative to assess for the pos- sibility 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 be found in detail in Ap- pendix A.1.4 As seen in Table we find that COPRA reproduces none of the "long" proofs
8

---

Published as a conference paper at COLM 2024
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 proots in miniF2F, or proof has been checked in. We provide examples of proots generated by our approach compared to those included in miniF2F in Figure 11
Coq Experiments COPRA can prove significant portion of the theorems in our Cog evaluation set. As shown in Figure [6 (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 few- shot baselines utilizing GPTT-4 and GPT- 3.5, which could prove 36 and 10 the- orems, respectively, on our CompCert- based evaluation set. Some example Coq proofs generated by COPRA are shown in Appendix A.5 Figure
theorem mathd__umbbetthorr
(n IN)
(ho 0 <<n)
(h1 nat.gcd 40 10)
(h2 : nat.lcm 40 280)
70 :=
begin
have hg n 40 10 280 by rw =[nat. ged_ gec__mc__mlllln exact (nat. ef_oee___mllll ____u__________________________e ee_______iihhhh ( by norm_num 0 40) h2),
40, h1, h2],
end
Figure 7: theorem that requires retrieval. Co- PRA used BM25 to find the lemma "ged mmmmlmmlmm (n NN) (ged n m) x (lcm m) = n m" which led to the proof while REPROVER failed to prove this theorem. is important note that just retriev- ing the correct lemma is not sufficient, but knowing how to use it correctly is equally important. The Figure shows how COPRA utilizes the capabili- ties of LLM to correctly use the retrieved lemma in the proof.
5 Related Work
Neural Theorem-Proving. There is sizeable literature on search-based theorem-proving techniques based on supervised learning. Neural models are trained to predict proof step given context and the proof state, then employed to guide 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 GPTT- (Polu & Sutskever 2020), have used language models trained proof data.
2021 enhanced the training of such models with a set of self-supervised Lample et al. (2022) introduced Hyper'Tree Proof Search, which uses language model trained on proots to guide an online MCTS-inspired, search algorithm.
PACT Haa et al.
auxiliary tasks.
Among results from the very recent past, REPROVER trains retrievallauugmeneed trans- former for proof generation in Lean. LLEMMA performs continued pretraining of the CodeLlamma 7B & 34B
math-focused corpus. Baldur (First et al. 2023) generates the whole proof in one-shot using an LLM and then performs a single repar step by passing error feedback through an LLM finetuned on (incorrect proof, error message, correct proof) tuples. AlphaGeometry (Trinh et al. 2024) integrates transformer model trained on synthetic geometry data with 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 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 & Bjorer 2008 to prove goals. Thor (Jiang et al. 2022a) augmented the PISA dataset (Jing et al. 2021 to include successful Sledgehammer invocations, and trained language model to additionally predict hammer applications. Integrating these ideas with the COPRA approach is an interesting subject of future work.

---

Published as a conference paper at COLM 2024
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 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 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. 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 domain- agnostic 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-Graviaas 2023 Yao et al. 2022 Shinn et al. 2023 Wang
et al. 2023a). These models combine an LLM's capability to use Gools/Schic et al. (2023).
decompose task into subtasks (Wei et al. 2022 Yao al. 2023), and self-reflect (Shinn
let al. 2023 However, COPRA is the first in-context learning agent for theorem-proving.
6 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 theorem- proving techniques by performing a Iritory-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 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, 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, use our code, one must use their own OpenAl API keys. An issue with reproducibility in our setting is that the specific models served via the GPT-4 and GPT-3.55 APIs may change over time. our experiments, set the "temperature" parameter to zero to ensure the LLM outputs are 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.
10

---

Published as a conference paper at COLM 2024
References
Andrews, P. B. and Brown, C. E. Tps: A hybrid automatic-interactiiee system for developing proofs. Journal of Applied Logic, 4(4):367-395, 2006.
Azerbayev, Z., Schoelkopt, H., Paster, K., Santos, M. D., McAleer, S., Jiang, A. Q., Deng, J., Biderman, S., and Welleck, Llemma: An open language model for mathematics, 2023.
Blanchette, C., Bulwahn, L., and Nipkow, T. Automatic proof and disproof in isabelle/ /hol. In Frontiers of Combining Systems: 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings 8, pp. 12-27. Springer, 2011.
Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J. D., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al. Language models are few-shot learners. Advances in neural information processing systems, 33:1877-1901, 2020.
Bundy, A.
The use of explicit plans to guide inductive proofs. In 9th International Conference on Automaled Deduction: Argonne, Illinois, USA, May 23-26 1988 Proceedings 9, pp. 111-120. Springer, 1988.
De Moura, L. and Björner, N. Z3: an efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08/ /OAAS0////TPSS00 pp. 337-340, Berlin, Heidelberg, 2008 Springer Verlag. Verilg. iSBN 3540787992.
de Moura, L.,, Kong, S., Avigad, J., Van Doorn, F,, and von Raumer, The Lean theorem prover (system description). Automated Deduction-CADE-22 25th International Confer- ence Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378-388. Springer, 2015.
First, E., Rabe, M. N., Ringer, T., and Brun, Y. Baldur: whole-proof generation and repair with large language models. arXiv preprint ar arXiv:2003.04910 2023.
Han, J. M., Rute, J., Wu, Y., Ayers, E. W., and Polu, S. Proof artifact co-training for theorem proving with language models. arXiv preprint ar Xrxe:2102.06203 2021.
Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., and Steinhardt, J. Measuring mathematical problem solving with the math dataset. 2021.
Huang, D., Dhariwal, P., Song, D., and Sutskever, Gamepad: A learning environment for theorem proving. In ICLR, 2019.
Huet, G., Kahn, G., and Paulin-Mohring, C. The coq proof assistant a tutorial. Rapport Technique, 178, 1997.
Jiang, A. Q., Li, W., Han, M., and Wu, Y. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pp. 378-392, 2021.
Jiang, A. Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóždz, T., Miloš, P., Wu, Y., and Jamnik, M. Thor: Wielding hammers integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35:8360-8377 8373008-333,8400 2022a.
Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., and Lample, G. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arxiv preprint ar Xr::::2200 12283,, 2022b.
Lample, G., Lacroix, T., Lachaux. M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. Hypertree proof search for neural theorem proving, Advances in Neural Information Processing Systems, 35:26337-26349, 2022.
Leroy, X. Formal verification of a realistic compiler. Communications of the ACM, 52(7): 107-115, 2009.
11

---

Published as a conference paper at COLM 2024
mathlib Community, T. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL 20. ACM, January 2020. doi: 10.11453382285.3333335 /ttp///////////////////ooo/oo/// 1145333788883888888888 33738885333388844 3373824
www. org/
Newell, A., Shaw, J. C., and Simon, H. A. Empirical explorations of the logic theory machine: case study in heuristic. In Papers presented at the February 26-28, 1957, western joint computer conference: Techniques for reliability, pp. 218-230, 1957.
OpenAL. GPT-4 technical report, 2023a.
OpenAL. GPT-4 and GPT-4 turbo, 2023b. UKLnntps:/bllafoomm.peen ccm//aaa.ccmm/bcc///mmee/e
3pt-4-and-got-4-Uun ------pt---4-b--
Paulson, L. and Blanchette, J. Three years of experience with sledgehammer, practical link between automatic and interactive theorem provers. 02 2015. doi: 10.29007/tnfd.
Paulson, L. C. Isabelle: A generic theorem prover. Springer, 1994.
Polu, S. and Sutskever, 1. Generative language modeling for automated theorem proving. Xiv preprint ar Xix::2009.03333, 2020.
Polu, S., Han, M., Zheng, K., Baksys, M., Babuschkin, I,, and Sutskever, I. Formal mathematics statement curriculum learning. arviv preprint ar xrXi:2202.001344 2022.
Ramesh, A., Pavlov, M., Goh, G., Gray, S., Voss, C., Radford, A., Chen, M., and Sutskever, I. Zero-shot text-to-image generation. In International Conference on Machine Learning, pp- 8821-8831. PMLR, 2021.
Roziere, B., Gehring, J., Gloeckle, F., Sootla, S., Gat, I,, Tan, E., Adi, Y., Liu, J., Re- mez, T., Rapin, J,, et al. Code llama: Open foundation models for code. arXiv preprint arXiv:2308.1298 2023.
Sanche7-Stern, A., Alhessi, Y., Saul, I.., and Lerner, S. Generating correctness proofs with neural networks. Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, pp. 1-10, 2020.
Schick, T,, DwwiediiYYu. J,, Dessi, R., Raileanu, R., Lomeli, M., Zettlemoyer, L., Cancedda, N., and Scialom, T. Toolformer: Language models can teach themselves to use tools. arXiv preprint ar (rXiv:2302.447 047661, 2023.
Schulz, S. E brainiac theorem prover. Al Commun., 15(2,3):111-126, aug 2002. ISSN 0921-7126.
Shinn, N., Cassano, F,, Labash, B., Gopinath, A., Narasimhan, K., and Yao, S. Reflexion: Language agents with verbal reinforcement learning. arXiv preprint ar XxX6o:2303.11366, 2023.
Significant-Gravin Gravitts,. Autogpt. http::///hhhaaaaaaagSaaaaaaaataa
2023.
Touvron, H., Lavril, T., Izacard, G., Martinet, X., Lachaux, M.-A., Lacroix, T., Rozière, B., Goyal, N., Hambro, E., Azhar, F., et al. Llama: Open and efficient foundation language models. Xrx preprint ar 2rXin:2302.33971, 2023.
Trinh, T. H., Wu, Y., Le, Q V., He, H., and Luong, T. Solving olympiad geometry without human demonstrations, Nature, 67777995) 2024.
Wang, G., Xie, Y., Jiang, Y., Mandlekar, A., Xiao, C., Zhu, Y., Fan, L., and Anandkumar, A. Voyager: An open-ended embodied agent with large language models. arXiv preprint arXiv:2305.16291, 2023a.
Wang, H., Xin, H., Zheng, C., Li, L., Liu, Z., Cao, Q., Huang, Y., Xiong, J., Shi, H., Xie, E., Yin, J., Li, Z., Liao, H., and Liang, X. Lego-prover: Neural theorem proving with growing libraries. 2023b.
12

---

Published as a conference paper at COLM 2024
Wei, J., Wang, X., Schuurmans, D., Bosma, M., Xia, F., Chi, E., Le, Q. V., Zhou, D., et al. Mhain-of-thoughi prompting elicits reasoning in large language models. Advances in Neural Information Processing Systems, 25:24824-24831) 2022.
Yang, K. and Deng, Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, pp. 6984-6994, PMLR, 2019.
Yang, K., Swope, A. M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., and Anandkumar, A. Leandojo: Theorem proving with retrieval-augmented language models. Xiv preprint ar orXio:2306.16626 2023.
Yao, S., Zhao, J., Yu, D., Du, N., Shafran, I., Narasimhan, K., and Cao, Y. React: Synergizing reasoning and acting in language models. ar preprint ar XrX::22100.0662, 2022.
Yao, S., Yu, D., Zhao, J., Shafran, I,, Griffiths, T. L., Cao, Y., and Narasimhan, K. Tree of thoughts: Deliberate problem solving with large language models. arXiv preprint arXio:2305.1060) 2023.
Zhao, X., Li, W., and Kong, L. Decomposing the enigma: Subgoal-baser demonstration learning for formal theorem proving. 2023.
Zheng, C., Wang, H., Xie, E., Liu, Z., Sun, J., Xin, H., Shen, J., Li, Z., and Li, Y. Lyra: Orches- trating dual correction in automated theorem proving. arXiv preprint ar Xrxo:22399.5806, 2023.
Zheng, K., Han, J. M., and Polu, S. Minif2f: a cross-system benchmark for formal olympiad- level mathematics. Xiv preprint ar wrXr:210090001111 2021.
13

---

Published as a conference paper at COLM 2024
A Appendix
A.1
Evaluation Details
A.1.1 COPRA Implementation Setup Details
We introduce 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 support more proof languages.
COPRA provides support for various LLMs other than the GPT-series, including open- sourced LLMs like Liama (Touvron al., 2023) and Code Llama (Roziere al.) 2023). For most of our experiments, all the theorems are searched within timeout of 600 seconds (10 minutes) and with maximum 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 ual queries focus on single proof step and cannot see the original goal, yet measures a useful experiment which indicates the benefits of COPRA'S 's stateful search under fixed budget of APT calls to GPT-4.
We use GPT-3.5, GPT-4 (OpenAl 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 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 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 algebraíc manipulation which can be easily handled with powerful tactics like linarit th in Lean. Table 5hoows the number of tokens used our prompts for different datasets.
A.1.2 Metric: pass@l-viit--u-qquerress
We consider the metric pass@k-witth- to assess the speed of the proposed approach and the effectiveness of the LLM or neural network to guide the proof search. It reasonable metric because it does 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 different amount of guidance from neural model to find the right proof. For example, approaches like Baldur (First et al.) 2023), DSP [Tiang 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 step-by-step fashion. We argue that pashhk--wthh--
14

---

Published as a conference paper at COLM 2024
Evaluation on miniF2F-test
Approach
Avg. Query in Total
Avg. Query on Failure
Avg. Query Pass
REPROVER (- Retrieval)
350.7
427.24
81.6
REPROVER
1015.32
1312.89
122.62
COPRA
21.73
28.23
3.83
COPRA (+ Retrieval)
37.88
50.90
7.38
Table 2: Aggregate effectiveness statistics for COPRA and the baselines on miniF2F dataset. We can see the various ablations of COPRA with and without retrieval.
Approach
Avg. Time Seconds
Per Proof
Per Query
On Pass
On Fail
All
On Pass
On Fail
All
ReProver (on CPU retrieval)
279.19
618.97
543.78
3,42
1.45
1.55
ReProver (on GPU retrieval)
267.94
601.35
520.74
2.06
0.44
0.48
ReProver (on GPU retrieval)
301.20
605.29
529.27
2.46
0.46
0.52
COPRA (GPT-3.5)
39.13
134.26
122.21
15.97
9.43
9.53
COPRA (GPT-4)
67.45
370.71
289.92
17.61
13.09
13.34
COPRA (GPT-4 retrieval) 117.85
678.51
510.78
15.97
13.33
13.48
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 a fairer metric compare these different types of approaches because it correlates with the effectiveness of the proof-finding algorithm in implementation-agnnsii way. the effectiveness because of
Since the exact time might not always be good reflection hardware differences, network throttling, etc., it makes sense to not compare directly 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).
A.1.3 pass@k-wiith-n-qqrriis versus wall-clock time
We show that pus@@k-with-n-qqurriss correlates well with wall-clock time for finding proofs by using the metric pass@k-seconile pass@k-seconda measures the number of proofs that an approach find in less than & seconds. The plot in Figure 6 shows that pass@k-seconds follows the same trend as maas@k-withh---quee
as shown in Figure
We can use the comparison of COPRA with REPROVER Yang et al. 2023 the miniF2F dataset to explain the correlation between finding proots fast and mais@kk-withh---querie 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 REPROVERS guidance LLM 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 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 tradeoff between the two, but the number of queries dominates when the guidance model is of low quality. Hence, given high-quality guidance model, we can empirically argue that asymptotically the search will converge to a proof faster (assuming proof is achievable with the guidance model).
15

---

Published as a conference paper at COLM 2024
A.1.4 Data Leakage in GPT-4
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 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 general- purpose 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 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 model of Lean's kernel, which is highly unlikely. It is also improbable that GPTT4 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 comples completely different from the manually written proofs in the miniF2F test dataset (including the first step mismatch). TableAshowe 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 1 linarith, nlinarith, th, 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 proof mentioned in the mini dataset. Out of all proofs generated by COPRA about 25.33% proofs are for theorems that have 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
Finally, the ability of agent interactions to enhance the basic LLM approach seems to transcend OpenAl'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 L.M.-agostic.
A.1.5 Comparison with methods using Isabelle and informal proofs
An interactive theorem prover (ITP) is a software tool to assist with the development of formal proofs by numan-machine collaboration. This involves sort of interactive proof editor, or other interfaces, with which human can guide the search for proofs. A formal proof written in 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 dilfer-
16

---

Published as a conference paper at COLM 2024
Proofs found in minsP2F-test
Proofs miniF2P
Total
Longer Complex Proofs
Single-Tactic Simple Prooff
Two-Tactic Proofs
Total
Tactics Used
tactics
OR
linarith
nornunum
nlinarith
two tactics
tactic multi-args
sorry
Proof Count
Proof
16
164
Count
Match
5
22
COPRA
Count
1a Tactic
Match
7
10
8
29
0
CoPRA
Count
Distinct
33
COPRA
2
9
34
70.67%
Count
Distinct
COPRA
53 /
Count
9
17
34
19
91.37%
Single-Tactic
COPRA
11
12
14
56
19
73
Count
Table 4:
Analysis of proof generated by COPRA (GPT-4 Retrieval + Informal) on miniF2F test dataset for Lean. See Table for details about various ablations.
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 patthematics-competiin benchmarks like miniF2F, it is less applicable to domains such as software verification, where there often no informal specification, as well as domains that use customized, domain-specife formalizations. Furthermore, having access to informal proofs (human-written or (LM--enerated) shifts the problem of synthesizing the formal proof towards an autoformalization problem, as the LLM likely to have seen correct natural language proofs of miniF2F problems in its training. Additionally, unlike DSP-like approaches which tend to use mass@100 pass@200, only use pass@1.
A.2 Example Proofs Generated for miniF2F
Figure 10 shows dataset. Figure 8 and Figure shows the breakdown of theorems proved in various cat- egories by COPRA versus REPROVER. Figure 10 shows some interesting miniF2F proofs as done by COPRA.
other interesting proofs generated by approach miniF2F
IT 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.
A.3 System Prompts For miniF2F
Parts of the 'system prompt' used by COPRA for theorem proving in Lean are shown in Fig.
13
17

---

Published as a conference paper at COLM 2024
40
COPRA
35
Number of Theorems Proved
20
15
10
matha algebra
matha numbertheory
amc
aime
algebra
imo
induction
numbertheory
Problem Category
Figure 8: Breakdown of theorems proved in various categories by COPRA (GPT-4 + retrieval + inforrmll proof): Problems solved in different categories in miniF2F test dataset. Notice that 'IMO' and 'Induction' problems are hard for both approaches. COPRA does more problems than REPROVER in most of the categories.
1750
ReProver
COPRA
1500
Avg. Number of Queries (n)
1000
750
250
ino
induction
algebra
slgees 2 Samne
Problem Category
Figure Breakdown of theorems proved in various categories by COPRA (GPT-4 + retrieval + informal proof): Number of queries needed in different categories in miniF2F test dataset. Notice that COPRA takes very less queries to solve the problems in each category.
18

---

Published as a conference paper at COLM 2024
(a)
(c)
(e)
theorem wathd_numberrthoryy.ue
thearem mathd_algebra_
theorem amc 2b_2002_p7
(a N)
(a b c IN
(n IN)
(ho even a)
(hu 0 < A < A c)
(ho 0 0<
(h1 1 k in finset.
(h: b
1)
(h1 nat.ged 40 10)
range 8, (2 * k 1)
(h2 : c=
(h2 : nat.lcm
280)
1Σ k in finset.
(h3 a = (a +
range 5,
k)
+ c))
70 :
(4:2))
a" (b'2 c'2) 77
begin
a = begin
begin
have hg
rw [h,, h2] at h3
280 := by rw +[nat.
simp only [finset.
ring_nf at hs,
ged_mul_1cm n 40, h1, hz], exact (nat. mo__of_mi_eq__ull eew.e__rmiihhht.oeeeeeeeee (by norm_num 0 40) h2),
sum_range_suce
rw [h1, h2].
finset. www_range__eeeeeeeeeee add_zero, finset. sum_const, finset. card_range, nsmul_eq_muv finset. end sun_add_distrib Finset.mul_st kinset.sum_mul) at h1,
ring_nf, simp [h1, h2] at *, ring_nf at 8, nlinarith,
end
norm_num at h1, linarith, end
(b)
(d)
theorem
theorem mathern theory334
batth__nuberrtheory..kk
Σ k in finset. filter (" x, (a c N) [3x) (finset. Icc
(ha a <
49), (k 10) 78 :
S 9)
begin
(hi nat digits 10
norm_num [finset. sum_filter, finset. Icc
((5'100) 1000) = [c.
b,a]) :=
a b begin
ring, end
norm_num at hj
cases h1, linarith, end
Figure 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 not easy to synthesize without knowing the exact execution feedback from the environment which often contains the hint fix the rewrites.
19

---

Published as a conference paper at COLM 2024
(a.1)
(a.2)
theorem mathd_number theory__
theorem range 10, ((x 1) 2))
( in finset. range 10, ((x 1)^2)) x
cΣ x range
10
:=
10 :
begin dec_trivial!, end
begin
simp only rannee finset. sun_suuun____eeeee_____ add_zero, pow_twol, norm_num, end (b.2)
(b.1)
theorem mathd_algebr a_29
(o : equiv R R)
(he 0.2 2 = 10)
(h: 0.2 10 1)
theorem mathd_algest (0: equiv R R)
(h2 : 0.2 1 2)
0.1 (o.1 10) = :=
(hg 0.2 10)
begin
(h1 0.2 10 1)
rw +[ ho. + h2],
(h2 0.2 1 2)
simp,
0.1 (0.1 10) = =1 :
end
begin
(c.1)
apply_ fun œ. inv_fun at h1 rw equiv. www.:iii__uussccooc at h rw the at h, rw +h2 at h,, +ho. hwt.viin__fu_as_ccc at ho
theorem thmfhd_nmmbertoory...oo (5'30) begin
have five_to_ dive_to_thirty.. thirtt_is__one:
(5'30 zmod 7) = 1 begin
apply_fun oe at h1 rw equiv.inv_fun_as_cm at h rw +h2,
have
sithe_ssiiis_oee (5"6
zmod 7) = 1, by dec_ trivial
sequiv.iv_ffu_aate fuu_as__co at h2,
have break_power : (5 30 zmod 7)
simp [equiv. sympaappyy_apply]]
(5*6) ", by norm_num, break_power,
end
rw dive__tt_the__i__is____ norm_num,
(c.2)
theorem ma sid__umbberrteeeeeeeeedddreerrdd theory_22 (5 (5"30) := begin
end, change 5 30 [MOD 7], =zmod, Lfffmmoeeq_at. exact_mod_cast five_to_ thirtttiiit_onnee end
norm_num,
end
Figure 11: Some proofs found by COPRA compared to the proofs mentioned in the miniF2F test dataset. It is interesting to see that the proofs generated by COPRA are different from the proofs mentioned in the repository. This is especially true when the proofs are longer. It is also worth noting that occasionally COPRA can find very simple proofs for longer proofs mentioned in miniF2F test dataset. (a.1), (b.1), and (c.1) show the proofs as mentioned in the miniF2F dataset, while (a.2), (b.2), and (c.2) show the corresponding proofs generated by COPRA.
20

---

Published as a conference paper at COLM 2024
(a)
(c)
(e)
theorem
theorem aime_1990_pp
theorem mathd_algebra,
mathd_algebra_115
(x IR)
(x R)
(a
IN)
(hg : 0 < x)
x x 7'2 14
(ho even a)
(hi x 10 * x 29
3
(h1 1E k in finset.
0)
begin
range 8, (2
1) (h2 x
45
apply le_of_sub_nonneg, ring_nf,
1Σ k in finset.
range 5, (a 2 * k) (hg
x - 10 x x 69
have (x 14) 49
* 0)
- 2, by ring, rw this, apply now_two__noneee
:=
(h4 / (x'2 - 10
begin
29)
(x"2
simp only [finset. sum_range_succ, finset.
10 * x 45) 2
end
(x'2 - 10 x 69)
0)
sum_range_zerg
13
add_zero, finset. sum_const, finset. card_range, nsmul_eq_mul, finset. sum musset, finset.summmml] at h,, norm_num at h
begin
ring_nf at h44
have h3 (x 2
10
29) (x
10
45)
(x
10
69) # 0 :=
mul nul_ne_zero
mul_ne jil_n_zeen zero h1 h2) h
3, field_simp [hy] at
linarith, end
ring at h4, nlinarith,
(b)
theorem mathd_algebra._e end
(s t R) (ho s
(d)
t)
(h, t
theorem b NN)
t 4
begin
(ho a
split,
<)
rw h1 at hp. rw hp, linarith,
(h: bb 1)
(h2 c 1)
(hs aa
8 (a
rw ho at hy,
+b+ c))
rw h at ho.
a'2 + (b'2 + c²2) 77
linarith,
end
begin
rw [hj, h2] at h3, ring_nf at hy, rw [h,, hz], ring_nf, simp [h,, h2] at *, ring_nf x, nlinarith,
end
Figure 12: Some interesting proofs generated for miniF2F dataset which were generated because of COPRA'S backtracking capabilities.
21

---

Published as a conference paper at COLM 2024
You are proficient formal theorem-proving agent in Lean 3. You are tasked with predicting the next proof step given the current proof state, which
is described in the following format:
1. All the goals are described under the "[GOALS]" keyword. Each goal following [GOALS]] is described under the keyword [GOAL]] i', where
"i" is positive integer. For example, [[GOAL] 1", [[GOAL] 2", etc.
2. Within each [[GOA]] i keyword, the goal is described
human-readable serialized version of the proof state as shown while running the "lean" command. Each goal may be accompanied by hypotheses, which are described under the keyword [[HYPOTHESES] i' Each hypothesis following [[HYPOTHESES] i starts with the prefix [HYPOTHESIS]] Apart from goals and hypotheses, the OPTIONAL keywords [DEFFNITIONS]] i" and [[HEOOEMM]] i may appear, which respectively describe the relevant definitions of symbols and terms used in that goal and some potentially useful theorems or lemmas which might help in proving the goal. Each definition within "DEFFINTTIONS]" starts with the prefix "[DFFINITION"". Similarly, each theorem/lenma within [[THEOREMS]" starts with the prefix "[THEOREM]". If you choose to be SURE that it applies and is useful for proving the goal.
theorem described in [[THEOREMS] i',
3. The [[STEPS]" keyword is used to describe the proof-steps which were used to obtain the current proof state from the original theorem. Each proof step starts with the prefix [[STEP]' and is valid Lean tactic. For example, [[SEPS][STEPPIr h at h2, [ITEP][(iinnr)
4. Sometimes the [[INCOREECT STEPS] keyword will appear, which describes proof-steps which should NOT be generated. For example, *[INCORRECT
STEPSJ[STEP]apply , [STEP]rw thi.. **DO NOT** generate these
"[INCORRECT STEPS] again, they are failed proof steps which have
already been tried. Re-generating such proof steps will cause backtracking and early termination of your proof search.
5. There is also an optional [[AST STEP] keyword which describes the
proof-step generated last time. If the proof-step was incorrect, then it is also followed by an error message from Lean environment
described with the *[ERROR MESSAGE] keyword. For example, [LAST STEP]linarith, \n[ERROR MESSAGE]linarite failed to find
contradictionvnstatee Anx y R, Anh; x 2 y, \nh2 x 1\ni false' You can use the error message guidance in predicting correct proof-step. Do not generate tactics which you believe will result in the same error. If the proof-step was correct then it is followed by the keyword [SUCCESS]] For example, [[LAST STEP]linarith, [SUCCESS]', Do NOT generate the last proof-step again if it was NOT successful, this will also cause early termination of your proof search.
6. Sometimes there can be errors in the format of the generated response. This is reported using the keyword [[ERROR]" followed by the message. For example, [ERROR]\nInvall] complete.", AnStopping Reason: 'stop', An Please respond only in the format specified. [END]* This means that the response generated by was not in the specified format.
response: \n 'Great! The proof is
Start your response with "[RUN TACTIC] followed by the tactic which will help in proving the current proof state, and then [[END]" For example, "CRUN TACTIC] induction c, [END]*. Do NOT finish the proof in one shot ending with "end", which signifies the end of Lean proof. Generate exactly ONE proof-step. Multiple proof steps are more error prone, because you will not get chance to see intermediate proof state descriptions.....
Figure 13: Parts of "system prompt" used by COPRA for Lean.
22

---

Published as a conference paper at COLM 2024
Prompt Token Statistics for different settings
Setting
Min. Token Count
Max. Token Count
Avg. Token Count
miniF2F
33
1828
322.61
miniF2F (+ Retrieval)
181
4355
824.21
miniF2F (+ Retrieval Informal)
192
4355
955.20
CompCert (+ Retrieval)
292
116574
3219.79
Table Aggregate prompt token statistics for COPRA on miniF2F and CompCert dataset.
A.4
System Prompts For CompCert
Parts of the 'system prompt' used by COPRA for theorem proving in Coq are shown in Fig.
14
A.5 Example Proofs generated For CompCert
Figure 16 shows the number of proofs done by COPRA versus PROVERBOT9001 varying with the number of queries CompCert benchmark. Figure 17 shows some interesting proofs generated by our approach on the CompCert dataset.
23

---

Published as conference paper at COLM 2024
You are proficient formal theorem-proving agent in Coq. are tasked with predicting the next proof step given the current proof state, which
"> is described in the following format:
1. All the goals are described under the "[GOALS]" keyword. Each goal
following [GOALS]] is described under the keyword [GOAL] i", where
"i" is positive integer. For example, [[GOAL] 1 [[GOAL] 2", etc.
2. Within each [GGOA]] i keyword, the goal is described as human-readable serialized version of the proof state as shown while running the "lean" command. Each goal may be accompanied by hypotheses, which described under the keyword [[HYPOTHESES] i Each hypothesis following [[HYPOTHESES] i starts with the prefix [HYPOTHESIS] Apart from goals and hypotheses, the OPTIONAL keywords [DEFFINITIONS] i' and [[THEOREMS] i" may appear, which respectively describe the relevant definitions of symbols and terms used in that goal and some potentially useful theorems or lemmas which might help in proving the goal. Each definition within "[DEFINITIONS]" starts with the prefix [DEFIINIIINN" Similarly, each theorem/lemma within [[THEOREMS]" starts with the prefix "[THEOREM]". If you choose to use a theorem described be SURE that it applies and is useful for proving the goal.
[[THEOREMS] i',
3. The [[STEPS]" keyword is used to describe the proof-steps which were used to obtain the current proof state from the original theorem. Each proof step starts with the prefix "[STEP]", and is a valid Coq tactic ending with ... For example, [STEPS][STEP]intros a. [[STEP]induction a.
4. Sometimes the "[INCORRECT STEPS] keyword will appear, which describes proof-steps which should NOT be generated. For example, "[INCORRECT STEPS][STEP]appLY mul_assoc. [STEP]rewrite <- H." **DO NOT** generate these [INCORRECT STEPS] again, as they are failed proof steps which have already been tried. Re-generating such proof steps will cause backtracking and early termination of your proof search.
5. There is also an optional [[LAST STEP] keyword which describes the
proof-step generated last time. If the proof-step was incorrect, then it is also followed by error message from Coq environment described with the [ERROR MESSAGE] keyword. For example, "[LAST STEP]reflexivity [ERROR MESSAGE]Error: In environment'nn nat'nUnable to unify "n" with "n + 0".". You can use the error message as guidance in predicting correct proof-step. Do generate tactics which you believe will result in the same error. If the proof-step was correct then it is followed by the keyword "[SUCCESS]' For example, "[LAST STEPJreflexivity [SUCCESS]*. Do NOT generate the last proof-step again if was successful, this will also cause early termination your proof search.
6. Sometimes there can be errors in the format of the generated response. This is reported using the keyword [[ERRO]]" followed by the error message. For example, [[RROR] response: 'Great! The proof is complete.", \nStopping Reason: 'stop". An Please respond only in the format specified. [END]* This means that the response generated by you not in the specified format.
Start your response with "[RUN TACTICI', followed by the tactic which will help in proving the current proof state, and then [[END]" For example, "[RUN TACTIC]destruct c. [END] NOT finish the proof in one shot ending with "Qed", which signifies the end of Coq proof. Generate exactly ONE proof-step. Multiple proof steps are more error prone, because you will not get chance to see intermediate proof state descriptions. particular, not generate tactics which could split into smaller tactics you will not be able to view the intermediate proof states during these rewrites. The tactic "admit" NOT valid proof step, do NOT generate it.
Ensure that the proof step you generate is (1) valid (2) helpful
Figure 14: Parts of "system prompt" used by COPRA for Coq.
24

---

Published as a conference paper at COLM 2024
theorem Baathdaageeba_10 107
(x R)
(ho : x 8 y'2 6 y 0)
(x + 4) + (y-3)"2 5'2 1=
begin
have h1 (x + 4) 2
2
16 := by ring,
have h2
y
9 by ring,
rw [hi, h2], ring_nf, linarith,
end
Figure 15: An interesting proof generated by COPRA while using informal proofs hints generated GPT-4.
pass@l-with---querries
50
Number of Theorems Proved
COPRA (GPT-4-turbo)
(with retrieval)
Proverbott0011
10
3:
80
Number of Queries (n)
Figure 16: COPRA vs. PROVERBOT9001 the CompCert benchmark.
25

---

Published as a conference paper at COLM 2024
(a)
gss
forall V m,
1 match 1 with R (c)
(set
r =>
disjoint_cons_rige
v sl ofs ty
(e)
Val. 1ead_oad_rr result
forall a 11 12,
set lelllllllllssseeee
_chunk_of_type ty) v end.
disjoint 11 (a ::
forall e1
12) -> disjoint
e2,
Proof.
11 12.
env lessdef e1
intros 1 m.
Proof. intros 12
e2 -> forall
destruct
s t]
il,
unfold set.
H.
env mnw_lessdef
destruct (Loc.eq (R r) (R
unfold disjoint.
localo il
r)); [reflexivity
e1) localoocas il
contradiction).
intros x1 x2 H2.
unfold set.
e2).
destruct (Loc.eq eq sS
apply H. assumption. right. assumption.
Proof.
(S t));
intros el e2 H.
[reflexivity
induction il
contradiction].
[] a il'].
Qed.
Qed.
apply H.
(b)
(d)
intros.
apply
eq forall (p q: loc), {p-
eq_int_type
set_var_ le_ssde..
q) + (p q).
forall (x y:
apply IHil'
Proof.
int_type),
apply
decide equality.
(x=y) (xcy).
Val, lessdef_rell.
apply mreg_eq.
Proof.
Qed.
decide equality.
decide
decide equality.
equality.
apply Pos. dec.
Qed.
decide equality.
decide equality.
Qed.
Figure 17: Some other interesting proofs generated for CompCert by COPRA. We can see that these proofs are long, and often use 'apply' tactic which shows that COPRA effectively use the retrieved information to discharge given proof states.
26

---

Published as a conference paper at COLM 2024
[GOALS]]
[GOAL]] 1
70
# The goal we want to prove (or proof state)
[HYPOTHESES] 1 # Assumptions about the goal
[HYPOTHESIS]
N
[HYPOTHESIS] ho 0 <
[HYPOTHESIS] h1 n.ged 40 10
[HYPOTHESIS]" h2 n.lcm 40 = 280
[THEOREMM]] The retrieved lemmas from BM25 which can help prove goal"
(n m N+) (ged n m) * (lcm m) = =n * [THEOREM] ieriii.is_prrmm_heeee : (n : IN) (h1 : < n) (h2
[THEOREM]
nat fit_mmin_fccc n) nat.prime n
[THEOREM] pnat.lcm_coe (n m.m: NN)
[INCORRECT STEPS] # Previous mistakes the given proof state" # Each mistake is listed with the 'STEP' keyword." "[STEP]" apply nat.eq_of 1at_oo__u__ee_mullleee (by norm_num 0 40), rw +pnat. mirattccd_mul_cmm repeat { rw pnat.gcd_com }, repeat [ rw pnat. lcm_ce }, norm_num,
[[STEP]" have hg n 40 nat.ged 40 nat.lcm 40, from cest.gcd_mul__1 ((n, h₂)) (40, dec_trivial), [[STE]] rw www.:cddmul_leee [[STEP] mmat.gc_mmul_0 mam_mml__c at h1,
[LAST STEP] # Last prediction have ha
280, from mat.gcd_mul_lon (subtype. .nk ho) (subtype. mk 40 dec_trivial), linarith,
[[RROR MESSAGE] # Error message the last step" Got error 'have ha : n 40 10 2...': error: invalid type ascription, term has type
pnat.god (n, ho) (40, _> pnat. lcm (n, hy) (40, _> (n, ha) (40, _ [[END]'
Prediction by GPT-4
[RUN TACTIC] have ha linarith, [[END]
10 280, by rw [-nat. sonat.gcd_mull.e 40, h, h2],
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 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 also important to note that 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 can act as per the rich feedback it gets from the environment. Another interesting idea one try is to let COPRA create search query to control the retrieved lemma, which can make simple BM25 search more effective than DPR.
Figure 18:
27


Reviews:
[{"review_id": "Py52ycwnte", "reviewer": "Reviewer_G5kH", "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. \n\nCOPRA has several unique features. \n- 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. \n- COPRA fixes runtime errors via self-critique.\n- CORPA could retrieve and get benefits from lemmas and definitions and informal texts.\n- COPRA could work on both Lean and Coq, two tactic-based proof assistants. \n\nOn 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.", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your thorough feedback. We answer your main questions below. \n\n**Q**: More details about input and output in the step of retrieval.\n\n**A**: The retrieval works by: (i) first tokenizing the proof state, then (ii) performing a BM25 search on the lookup repositories (Mathlib in case of miniF2F) to find the top k lemmas (we use k=7). These lemmas are then added to the prompt along with the proof state. The following example shows the retrieval prompt:\n```\nGoals to prove:\n[GOALS]\n[GOAL] 1\nn = 70\n[HYPOTHESES] 1\n[HYPOTHESIS] n : ℕ\n[HYPOTHESIS] h₀ : 0 < n\n[HYPOTHESIS] h₁ : n.gcd 40 = 10\n[HYPOTHESIS] h₂ : n.lcm 40 = 280\n[THEOREMS] 1\n[THEOREM] pnat.gcd_mul_lcm : ...\n...\n[THEOREM] pnat.lcm_coe : ...\n...\n[INCORRECT STEPS]\n...\n[STEP] have h₃ : 10 * 280 = n * 40, by rw [←h₁, ←h₂],\nlinarith,\n...\n[LAST STEP]\nrw [←h₁, ←h₂] at h₃,\n[ERROR MESSAGE]\n....... failed, unknown 'h₃' local\n[END]\nResponse:\n[RUN TACTIC] \nhave h₃ : n * 40 = 10 * 280, by rw [←nat.gcd_mul_lcm n 40, h₁, h₂],\nlinarith,\n[END]\n```\n**Q**: Did we run ReProver?\n\n**A**: The results we report are those we obtained from running ReProver ourselves. We chose to run ReProver ourselves to obtain more fine-grained information to allow for a comparison of the number of queries and wall-clock time.\n\n**Q**: What is the format of ICL exemplars?\n\n**A**: We use fixed exemplars in all our prompts. The simple examples are intended to demonstrate the prompt format to the LLM. For miniF2F we use 6 examples, these are simple examples with no overlap with the miniF2F test set. The format is shown below:\n```\n`example_user`\nGoals to prove:\n[GOALS]\n[GOAL] 1\nx = 1 ∧ y = 1\n[HYPOTHESES] 1\n[HYPOTHESIS] x y : ℝ\n[HYPOTHESIS] h₁: x = 3 - 2 * y\n[HYPOTHESIS] h₂: 2 * x - y = 1\n[END]\n`example_assistant`\n[RUN TACTIC]\nlinarith,\n[END]\n`example_user`\nGoals to prove:\n[GOALS]\n[GOAL] 1\nx = 1 ∧ y = 1\n[HYPOTHESES] 1\n... \n[LAST STEP]\nlinarith,\n[ERROR MESSAGE]\nlinarith failed ...\n[END]\n`example_assistant`\n[RUN TACTIC] split, [END]\n```\n**Q**: Statistics on the prompt sizes.\n\n**A**: The statistics for the number of tokens in the prompt sizes for some of our settings are as follows: (this is for GPT-4-turbo model which allows at max 128k tokens)\n```\nSetting         | Min  |  Max  | Avg\nminiF2F         | 33   | 1828  | 322.61\nminiF2F + ret   | 181  | 4355  | 824.21\nminiF2F + inf   | 192  | 4355  | 955.20\nCompcert + ret  | 292  |116574 | 3219.79 \n```\nOur system prompts typically have 2-2.5k tokens -- examples can be found in the Appendix.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "Similar to code agents, theorem proving can be tackled by AI agents. This paper brings such a method, which should be beneficial to the AI/TP community. \nThe proposed proving agent is well-designed, combining the guidance from LLM with the search algorithm. The proposed progress check seems to be a clever and effective approach.\nThe experiment protocol and evaluation metric are sound and solid. The results are positive to show the power of ICL for theorem proving. Ablation demonstrates the importance of retrieval.", "reasons_to_reject": "I didn't find major issues for this submission, except for a few questions to be clarified below.", "questions_to_authors": "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?\n2 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?\n3 Do you have ICL exemplars in prompts? If so, what is the format of ICL exemplars? \n4 Can you provide some statistics for the size of our prompts and LLM responses, like the mean, min, max, per request, and per proof?", "extra_scores": {}}, {"review_id": "WEbA8xxzRM", "reviewer": "Reviewer_Ub88", "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.", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": true, "final_justification": "", "rebuttal": "Thank you for your valuable feedback. We address your main points below.\n\n\n**Concern**: The novelty is limited, given ReProver already suggests tactics given goals/premises.\n\n**Answer**: Our proof search procedure goes beyond Reprover in using additional signals not present at Reprover's training time, including error messages, memoization of proof search history, and additionally retrieved lemmas. Also, Copra handles both Coq and Lean, and we demonstrate its applicability in two quite different domains: competition mathematics and software verification. By contrast, other AI-based approaches to formal mathematics tend to be restricted to specific proof environments and applications. Also, compared to ReProver and Proverbot, we find that COPRA is more query-efficient. Our wall-clock time analysis also shows that the COPRA can find proofs faster than ReProver. Finally, we believe the use of in-context learning in difficult reasoning tasks is a subject of intrinsic interest to the language-models community. Copra is the first system to exploit in-context learning in formal theorem-proving. \n\n\n\n**Question**: Examples of problems that ReProver cannot solve but COPRA could. In-depth analysis of tactics used in proofs.\n\n\n**Answer**: Figure 6 shows one example where ReProver fails while COPRA succeeds. Figure 9 shows the breakdown of theorems proved in various categories by REPROVER and COPRA, we can see that COPRA proves more than ReProver in almost all categories (while in some categories they both fail like induction proofs). Particularly, COPRA is generally more capable of handling problems in the algebra category. Table 4 (in the appendix) sheds some light on the types of tactics used by COPRA, however, we can do a more in-depth analysis beyond the basic tactics in subsequent revisions.\n\nFinally, thank you for the stylistic suggestions. We will incorporate them into the next version of the paper.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "Theorem proving is a unique problem because you can get feedback on whether you've solved it by checking for remaining goals. Additionally, you receive feedback on intermediate execution through frameworks like LeanDoJo, which prevents incorrect tactics. This is an interesting problem setting to integrate the feedback in an self-improving way.\n\nThe analysis is thorough. Experiments compared the accuracy with few-shot LLM queries and fine-tuned baselines. The qualitative analysis is also interesting.\n\nI appreciate the discussion on test-set memorization concerns, as addressing memorization issues in black-box large language models is crucial.", "reasons_to_reject": "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.\n\nThe 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)?\n\nStylistic suggestions:\nFigure 2 would look better if (a) and (c) were aligned vertically.\nFigure 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).", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "yn0rueBF3w", "reviewer": "Reviewer_eJQk", "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.\n\nAs 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.", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": true, "final_justification": "", "rebuttal": "Thank you for your thoughtful review! Below are the responses to your queries.\n\n\n**Q**: Impact of omitting error feedback.\n\n\n**A**: These would indeed be interesting ablations, and we would be happy to add these ablations to the paper.\n\n**Q**: Limited evaluation and possible contamination.\n\n**A**: While including additional eval-sets would certainly strengthen our paper, we already go beyond most prior work on AI for theorem-proving by handling multiple languages (Coq, Lean) and two distinct application domains (competition mathematics and software verification). We could add an evaluation on a subset of the LeanDojo benchmark if necessary.  \n\nFor contamination issues, we performed a deep assessment of the proofs found by COPRA, generally showing no duplication (Table 4 in App.). No notable results popped up when we looked up the (longer) proofs generated by COPRA.\n\n**Q**: Combining smaller models with feedback abilities of GPT-4. \n\n**A**: We tried out two smaller models -- CodeLlama and GPT-3.5 -- for in-context tactic selection. We found to often fail to adhere to the prompt format. However, using a larger-scale model as a critic for such a smaller model -- and combining finetuned and in-context models --are  interesting ideas for future work. \n\n\n**Q**: Limited boost from informal proofs and results still fall behind SoTA\n\n**A**: HTPS and DSP use pass@64 and pass@100 respectively, while we use pass@1. SoTA depends on higher value of k in pass@k.\nIn the DSP paper (https://arxiv.org/pdf/2210.12283), from Figure 3 we can see that their pass@1 for combined miniF2F test + valid set is around 70. Thus, the test set number should be around 35 (test and valid set are same size). While we could do 75 proofs (30.74%) on the test set alone.\n\n\n**Q**: Can LLM also provide feedback on the retrieval?\n\n**A**:  In our experiments, the LLM does not. However, using the LLM in this way is an interesting idea for future work.\n\nThank you for the suggestion regarding Fig. 8. We will move it to the main paper.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "- COPRA is a new, agent-based search approach for tackling the problem of formal theorem proving. Their method beats strong baselines such as ReProver and Llemma, even without retrieval.\n- The search procedure is intuitive and straightforward. It shows good results compared to GPT-4, ReProver, and Llemma.\n- To my knowledge, this is the first work to incorporate theorem prover feedback into the process without fine-tuning. \n- The authors provide a relatively comprehensive set of experiments, comparing not just query count but also wall-clock time (which is important because ReProver is likely much faster than GPT-4 for every single query). They also ablate backtracking, informal proofs, and retrieval and also give an analysis of contamination.", "reasons_to_reject": "- 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. \n- 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.\n- 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_to_authors": "- 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).\n- 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. \n- 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?\n- Can the LLM also provide feedback on the retrieval, to identify whether a retrieval was helpful for the next step?\n- 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.", "extra_scores": {}}, {"review_id": "ruU3RUbrV6", "reviewer": "Reviewer_BSYj", "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).", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your review. We address your main points below. \n\n\n**Question**: page 3, ‘we have an efficient ….’: Elaborate a bit on how to check if one proof obligation is stronger than another.\n\n**Answer**: The line you quoted does not appear in our submission. We presume you are referring to our discussion of Progress Checks on Page 4. In that section, we describe a procedure that is used to eliminate some straightforward cases where we can compare the difficulty of two proof states. Summarized, these cases are when goals match exactly and one set of hypotheses contains the other. We are happy to elaborate further on this if you have further questions.\n\n\n**Question**: Comparison with ReProver and Proverbot9001.\n\n**Answer**: Our approach is faster than ReProver both in terms of wall-clock time as well as the number of queries. We used Proverbot9001 because it is the best model for the CompCert dataset. Given the use of extra signals like error feedback, and proof history, we induce faster proof completion while searching for proofs. It is important to note that our approach is completely in-context and doesn’t need any domain-specific training data. Being We have shown that it works on both miniF2F and CompCert, while ReProver and Proverbot are limited to specific languages and the specific domains from which their training data is drawn.\n\n\n**Concern**:  We need to see the effectiveness of Copra when equipped with less capable models.\n\n**Answer**:   Prior work has shown that some of the in-context reasoning capabilities of LLM agents only kick in when the model is of GPT-4 scale. For example, Voyager, which used LLM agents to play Minecraft, needed GPT-4 as the actor. We do not believe that our use of GPT-4 should count against Copra, especially as in the future, GPT-4-scale models will get cheaper.\n\nAlso note that smaller models have smaller context windows and sometimes cannot fit in all feedback signals. Generating the feedback data (error signals, proof history, etc.) to train the smaller models is harder because we don’t have data with error signal annotation to begin with. Our use of ICL/GPT-4 lets us get around the need to train on feedback data.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "Strength: the paper is well written and easy to follow. I especially appreciate that the authors attempt to validate their idea on two diverse datasets (miniF2F and CompCert) from two systems (Lean and Coq). I also like the introduction of the metric that incorporates the number of queries to the LLMs.", "reasons_to_reject": "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_to_authors": "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?", "extra_scores": {}}]

Author rebuttal:

Meta-review: 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.
Decision: Accept