A Language-Agent Approach to Formal Theorem-Proving

Thank you for your valuable feedback. We respond to your comments and questions below:

1. “Why define the problem as an RL task, if this is not used in the methodology proposed?”

Ans. Our approach is inspired by recent “verbal RL” approaches [1, 2] that use LLMs to perform control tasks (like game-playing) that were traditionally solved using RL. The big idea here is that unlike in traditional deep RL, there is no gradient-based policy update descent. Instead, RL-style exploration is combined with in-context learning: the agent interacts with the world, collects information, and then updates the LLM's prompt to elicit new behavior.

The MDP formulation associates our approach with this perspective. The MDP captures interactions between our LLM and the external world (the proof environment), which form the primary difference between our approach and prior LLM-based approaches to theorem-proving. The sentence "Instead, we consider a fixed policy..." captures this essential difference between our method and classical RL approaches where one updates the policy iteratively.

2. “The structure of the framework proposed is not very clear. The algorithm in Fig. 3 is quite high-level. The calls and interactions with the LLMs are not discussed in much detail.”

Ans. Figure 4 shows some of the interactions with the LLMs, we can add more details in the appendix. Please mention any specific detail you would like to see, and we would be happy to add that information to the paper.

3. "What is sophisticated about the search algorithm used in COPRA?”

Ans. The search algorithm maintains a stack and keeps track of previous failures, and current execution feedback. This information is then added back to the prompt helping the guidance model (GPT-4) to better direct the search. The algorithm also uses a partial order over goals (originally introduced in Proverbot) to ensure that tactics actually simplify the proofs. Most of the previous approaches tend to use a stateless best-first search strategy, but our search uses a form of stack-based DFS and is stateful (by backtracking when the model starts repeating the same failed steps for any given proof state). This not only optimizes the number of inference steps needed to find a proof but also lets us fail fast when the proof is too hard to find (see Tables 1 and 2 for comparison).

References:

[1] Noah Shinn, Federico Cassano, Beck Labash, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. Reflexion: Language agents with verbal reinforcement learning. arXiv preprint arXiv:2303.11366, 2023.

[2] Guanzhi Wang, Yuqi Xie, Yunfan Jiang, Ajay Mandlekar, Chaowei Xiao, Yuke Zhu, Linxi Fan, and Anima Anandkumar. Voyager: An open-ended embodied agent with large language models. arXiv preprint arXiv:2305.16291, 2023.

Thank you for your valuable feedback. We address your main points below. Due to the 5000 characters limit, we split our response into multiple comments.

1. Questions about novelty and differences from existing retrieval-based LLM approaches like ReProver.

Ans. Our approach is based on the new paradigm of Language Agents, where one uses LLMs to perform control tasks and interact with and external world. In particular, we were inspired by Reflexion [2], which uses language agents to solve natural language RL tasks, and Voyager [3], which uses language agents to play Minecraft. This approach is different from traditional deep RL because there is no gradient-based policy update. Instead, RL-style exploration is combined with in-context learning.

In the proof synthesis setting, an LLM agent needs to have human-like interactions with the underlying interactive theorem prover (ITP) and generate a proof step-by-step along with using external knowledge and tools. In approaches like ReProver, Baldur, PACT, etc., the model is not trained to interact with the ITP. The proof steps are either generated all at once or one at a time, but there is no use of execution feedback, history of proof so far, or known failed proof steps.

Specifically, in the case of ReProver, there is no use of error feedback from ITP. Most of the current work uses a guidance model to carry out a search for completing the proof in a step-by-step manner. The guidance model is trained to predict the next step and the search is carried out using the best-first strategy. Some other methods generate the whole proof in one shot. Other approaches use informal proofs, for example in Draft-Sketch-Proof (DSP) [4]. While DSP might be using external knowledge (like generating informal proofs, hammer), there is no interaction with the ITP. The proof sketch is generated all at once and then a powerful automatic reasoning tool (like hammer) is used to fill the holes. Also, it is important to note that in certain situations like software verification (e.g. CompCert) the notion of informal proof is not well defined and there is no informal statement to begin with (which is required for approaches like DSP).

2. “It seems that the proposed method does not significantly outperform ReProver.”

Ans. It is true that the set of theorems that COPRA eventually discovers is not much larger than what Reprover discovers. However, COPRA finds the proofs much faster than ReProver at least 9x faster in absolute wall clock time. COPRA also fails faster when it is not able to find the proofs. We weren't able to run COPRA on a very large number of timesteps because of the high cost of GPT-4 queries; however, we expect that doing so would improve COPRA's performance even more.

More generally, we believe that as foundation models get more and more capable and cheaper (think of OpenAI's recent announcement regarding GPT-4-turbo, which significantly boosts GPT-4's context window while slashing costs), the benefits of COPRA-like approaches will become even clearer.

3. “Ablation studies might be needed to understand the role played by the RL component.”

Ans. Please let us know any specific ablations that you would want to see, and we would be happy to run them.

References:

[1] Zheng, Chuanyang, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. "Lyra: Orchestrating Dual Correction in Automated Theorem Proving." arXiv preprint arXiv:2309.15806 (2023).

[2] Noah Shinn, Federico Cassano, Beck Labash, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. Reflexion: Language agents with verbal reinforcement learning. arXiv preprint arXiv:2303.11366, 2023.

[3] Guanzhi Wang, Yuqi Xie, Yunfan Jiang, Ajay Mandlekar, Chaowei Xiao, Yuke Zhu, Linxi Fan, and Anima Anandkumar. Voyager: An open-ended embodied agent with large language models. arXiv preprint arXiv:2305.16291, 2023.

[4] Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothee´ Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022.

3. “Why does GPT-3.5 perform better than GPT-4 as indicated in Table 2? Does this suggest that there might be overfitting of prompts for different LLMs?”

Ans. GPT-3.5 doesn’t perform better than GPT-4. Table 2 compares the average wall clock time taken to find proofs using various approaches. What we observe is that GPT-3.5 response time is usually faster than GPT-4 per inferences which makes sense because it is presumably a smaller model than GPT-4. However, Copra agent with GPT-4 still finds proofs faster than GPT-3.5 because the search guidance provided by GPT-4 is more effective.

4. “How can it be verified that theorems are proved sufficiently?”

Ans. COPRA generates formal proofs. Formal proofs are machine-checkable and Interactive Theorem Provers (ITP) like Lean are used for the purpose of verifying the correctness of formal proofs. Often formal proofs are much more rigorous and pedantic than informal proofs.

6. “Why is COPRA claimed to be "the first LLM-agent approach to formal theorem-proving" when previous works like REPROVER and Decomposing the Enigma [1] might also be considered as LLM-agent approaches?”

Ans. Proof agents, like other Language Agents, need to have more human-like interactions with the interactive theorem prover (ITP) and generate proof step-by-step along with using external knowledge and tools. In approaches like ReProver, Baldur, PACT, etc., the model is not trained to interact with ITP. Instead, it is trained to either generate the whole proof all at once or one proof step at a time. Also, there is no use of execution feedback, history of proof so far, or known failed proof steps.

Specifically, in the case of ReProver, there is no use of error feedback from ITP. Most of the current work uses a guidance model to carry out a search for completing the proof in a step-by-step manner. The guidance model is trained to predict the next step and the search is carried out using the best-first strategy. Some other methods generate the whole proof in one shot. Other approaches use informal proofs, for example in (Draft-Sketch-Proof) DSP [4]. While DSP might be using external knowledge (like generating informal proofs, hammer), there is no interaction with the ITP. The proof sketch is generated all at once and then other symbolic techniques (like hammers) are used to fill these holes. Also, in applications like software verification (e.g. our CompCert benchmark), the notion of informal proof is not well defined and there is no informal statement to begin with (which is required for approaches like DSP).

Language Agents are used to perform control tasks (naturally framed using an MDP) through “verbal RL” [2, 3]. This is different from traditional deep RL because there is no gradient descent. Instead, the method synthesizes RL-style exploration with in-context learning. Neither ReProver nor “Decomposing the Enigma” frame theorem-proving as a control/MDP task.

7. “The authors seem to overstate their claim of having 'state-of-the-art' performance.”

Ans. Thank you for this point. We will make our claim of being state-of-the-art more nuanced, as we recognize that there are many versions of the state-of-the-art depending on how the problem is formulated (for example, whether the use of informal proofs is allowed or not).

8. “What is the average API cost for COPRA per proven theorem?”

Ans. It depends on the number of inferences needed, the model used, and the length of the proof. It is somewhere from $0.75-$5 per theorem on miniF2F and CompCert datasets.

References:

[1] Zhao, Xueliang, Wenda Li, and Lingpeng Kong. "Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving." arXiv preprint arXiv:2305.16366 (2023).

[2] Noah Shinn, Federico Cassano, Beck Labash, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. Reflexion: Language agents with verbal reinforcement learning. arXiv preprint arXiv:2303.11366, 2023.

[3] Guanzhi Wang, Yuqi Xie, Yunfan Jiang, Ajay Mandlekar, Chaowei Xiao, Yuke Zhu, Linxi Fan, and Anima Anandkumar. Voyager: An open-ended embodied agent with large language models. arXiv preprint arXiv:2305.16291, 2023.

[4] Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothee´ Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022.

Thank you very much for providing valuable feedback. We answer your questions below. Due to the 5000 characters limit, we split our response into multiple comments.

1. Comparison with the method “Decomposing the Enigma” [1]. Comparison of COPRA's absolute performance with Proverbot on the CompCert dataset.

Ans. “Decomposing the Enigma” [1] is based on Draft-Sketch-Proof (DSP) [4] style approaches, which uses informal proofs to find formal proofs. Having access to informal proofs (human-written or LLM-generated) simplifies the problem of synthesizing the formal proof into more of a translation problem, and that is one of the reasons why DSP-like approaches perform well on miniF2F datasets. It is important to note that these numbers are not comparable across different languages, [1] uses Isabelle which has powerful automatic reasoning tools like Sledgehammer, unlike Lean. As we mentioned in the related work section of our paper, this idea is orthogonal to the ideas in our paper, and we will explore ways to combine it with our methods in future work.

That said, we also note that informal proofs are hard to get in real-world mathematical reasoning settings such as software verification like CompCert. Also, the approach prescribed in [1] starts with a manually written subgoal-based proof, and then subsequently refines it. By contrast, our approach is completely automatic.

We agree that COPRA doesn’t outperform Proverbot on CompCert dataset in absolute numbers, but it uses much fewer inferences to find those proofs. It is quite possible that COPRA could do more proofs if we allowed more inference steps, but we are limited by our cost and API budget for GPT-4.

2. “It is unfair to compare the number of inferences made with REPROVER in Figure 5, as COPRA utilizes GPT-4 to prove theorems, while REPROVER employs a much smaller LLM. One query from GPT-4 is far more powerful than a single inference from REPROVER's LLM.”

Ans. Our objective for comparing the number of inferences is as follows:

a. We want to test the hypothesis of whether one can match the performance of fine-tuned models using just in-context learning. There is a recent trend of using Language Agent [2, 3] for performing control tasks using in-context “verbal RL”. We wanted to explore this idea in the context of theorem proving. It is important to note that ReProver is finetuned on proof-state and tactic pair data, but our approach is completely in-context.

b. The intention behind pass@k-inferences is to assess the speed of the proposed method and the effectiveness of the LLM or neural network to guide the proof search. To avoid any confusion we plan to rename this metric as pass@k-guidance budget, which is a reasonable metric as it does the right trade-off in accounting for the time taken to complete a proof and at the same time ignores very low-level hardware details. Even if ReProver uses a smaller model, it can make a lot more inferences in a given time. However, we observe that ReProver is slower in finding proofs even with the wall clock time. This means that the effectiveness of the guidance model is important in quickly finding the proof. We think that Coq/Lean ITP run time contributes more significantly when the guidance model is not effective search-wise (i.e. predicts wrong tactics). We can present an argument for ReProver as to why it is slower. We know that on average the time taken per inference (which includes time to run on ITP as well) is around 1.55 seconds for ReProver and 6.73 seconds for Copra (From Table 2). Even if we assume ReProver doesn’t take any time (zero time) to run the inferences and spends all of 1.55 seconds running the tactic on ITP, then we can assume that about 5 seconds (6.73 - 1.55) is the average response time for GPT-4. However, we see that the number of inferences used by ReProver is about 46x higher on success. This interestingly shows up in the wall clock time too which is around 9x higher (~46x/5) for ReProver on success, so there is a tradeoff between the two, but the number of inferences dominates when the guidance model is not good. So, if the guidance model is good (it may be as big as GPT), we can empirically argue that asymptotically the search will converge to proof faster (given that it can be found using that guidance model).

References:

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

[2] Shinn, Noah, et al. "Reflexion: Language agents with verbal reinforcement learning." Thirty-seventh Conference on Neural Information Processing Systems. 2023.

[3] Wang, Guanzhi, et al. "Voyager: An open-ended embodied agent with large language models." arXiv preprint arXiv:2305.16291 (2023).

[4] Jiang, Albert Q., et al. "Draft, sketch, and prove: Guiding formal theorem provers with informal proofs." arXiv preprint arXiv:2210.12283 (2022).

Thank you for meticulously reviewing our paper and giving valuable feedback. Due to the 5000 characters limit, we split our response into multiple comments. We respond to the important questions that you have raised below.

1. "It seems highly restrictive to only allow the model to choose tactics. Why not use prompting to ask the model the most promising partial proof to attack next?"

Ans. If we understand your point correctly, you would like us to use the LLM to not just select a tactic for proving an obligation, but also for selecting the best obligation to prove. In most cases, the LLM has a large enough context window to see all obligations, this way there is an implicit choice available for the LLM to choose which obligation to attack first. In order to prove a theorem, all obligations have to be proved; in most cases, it might not matter which obligation is proved first (except for cases like induction where we prove the base case first).

2. Why are both scalar rewards and text feedback formalized as part of the reward? How does this compare to traditional RL / MDP setups? Why the departure from that? Where is the scalar reward actually used? What is the meaning of the sentence “A trajectory of policy …” in Section 2.

Ans. The scalar reward is there to incentivize correct proofs and disincentivize incorrect proofs within the MDP framework. (In principle, the scalar reward function can also be used to incentivize shorter proofs.) We agree that the use of text feedback as part of the reward is not standard in traditional RL. The justification of this idea is that just like reward functions in traditional RL, the text describes the effectiveness of an action at a given state. We borrow this idea from recent work on “verbal RL” [1], which uses LLM agents for solving certain natural language RL problems and uses text as a generalization of rewards. This line of work departs from traditional RL in not having explicit policy updates, but combining RL-style exploration with in-context learning.

We note, however, that the text feedback can also be modeled as part of the new environment state resulting from the action, as opposed to the reward signal. Such a model would make the reward function purely scalar just like in classical RL. If you think this is more natural, we would be happy to make this change.

In RL, the agent's goal is to maximize the expected reward aggregated over trajectories. This requires a definition of trajectories. The paragraph “A trajectory of policy ..,” offers this definition.

3. In the pseudo-code (Figure 3), is this entire protocol repeated up to k times, or is this all within one value of your j pseudo-code?

Ans. Thank you for pointing this out, the ‘k’ mentioned in the algorithm is not the same ‘k’ as in pass@k-inference. All inference calls to LLMs even for fixing formatting errors are counted in pass@k-inferences. This is done to ensure that COPRA doesn’t have any unfair advantage over other approaches when we cap the number of inferences allowed. You can assume that the ‘k’ in the pseudo-code is just a free hyperparameter, and has nothing to do with the overall inference cap. The inference cap is strictly enforced. For pass@k-inference, COPRA can never make more than ‘k’ API calls to the LLM including all calls for fixing the formatting errors, incomplete responses, etc.

4. The use of one-shot prompting along with the agent interactions for finding proofs dilutes the capabilities of the agent.

Ans. Our reasoning here was that the goal is to find proofs quickly and cost-effectively. If GPT-4 can do it in one shot, the problem is not hard enough to justify the more expensive agent interaction.

That said, if you like, we can run the Copra agent on 26 theorems which GPT-4 could do in one shot. Even in the most unlikely case of Copra not proving any of the 26 theorems, we can still say that COPRA does at least about 3% more proofs than what GPT-4 could do alone (which is evident from the numbers in Table 1).

References:

[1] Noah Shinn, Federico Cassano, Beck Labash, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. Reflexion: Language agents with verbal reinforcement learning. arXiv preprint arXiv:2303.11366, 2023.

Dear Reviewer,

We ran experiments to address the concerns raised by you. We are excited to share some findings with you, which we believe demonstrate significant progress:

1. Enhancement in Problem Solving Capability using Retriever: In response to the retriever disabled issue, we developed a BM25 retriever and re-ran our experiments. This gives us 27.45% i.e. 67/244 success rate on miniF2F. This outperforms notable systems like ReProver, Llemma, PACT, and Lean GPT-f.

2. Addressing Data Leakage Concerns: We undertook a thorough analysis of potential data leakage within the miniF2F dataset. Our findings indicate that of the 67 proofs our system generated, 68.65% are distinct from those mentioned in the miniF2F dataset or are cases where the dataset lacks a corresponding proof. Notably, the proofs matching with miniF2F are primarily simple ones, solvable with a single tactic like 'linarith', 'norm_num', or 'nlinarith'. Excluding these straightforward cases, we found that 92% of our generated proofs are unique compared to the miniF2F dataset. Additionally, 25.37% of the proofs generated by our approach are not mentioned in the miniF2F dataset, compared to 22.9% of for the ReProver.

We appreciate the opportunity to run additional experiments and hopefully address your concerns regarding retriever and data leakage.

Best regards,

Authors