NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving

Authors: laetitia  teodorescu
guillaume  baudart
emilio  jesús
gallego  arias
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-25 21:50:54

Abstract: Formal theorem proving is challenging for humans as well as for machines. Thanks to recent advances in LLM capabilities, we believe natural language can serve as a universal interface for reasoning about formal proofs. In this paper, 1) we introduce Pétanque, a new lightweight environment to interact with the Coq theorem prover; 2) we present two interactive proof protocols leveraging natural language as an intermediate representation for designing proof steps; 3) we implement beam search over these interaction protocols, using natural language to rerank proof candidates;  and 4) we use Pétanque to benchmark our search algorithms. Using our method with GPT-4o we can successfully synthesize proofs for 58% of the first 100/260 lemmas from the newly published Busy Beaver proofs.

Main paper: 
 introduction: 
 The general knowledge and reasoning abilities of frontier large language models (LLMs) makes them practical as a backbone for building agents able to interact with interactive theorem provers (ITP). These agents should iteratively build proofs with help from proof engine feedback. While previous work (e.g. Yang et al. [2023] ) used a costly data collection procedure to finetune modestly sized language models, we believe that reasoning in natural language before outputting tactics will lead to better and more interpretable results. Recently, Thakur et al. [2024] showed promising preliminary results by using GPT-4 as an agent proposing tactics inside a backtracking search and using rich feedback from the proof environment.In this work, we develop infrastructure to allow communication between a GPT-4o-based agent and the Coq proof environment [The Coq Development Team, 2024] . Our key idea is to rely on natural language as much as possible when generating proofs. Using natural language leverages the strength of LLMs, and allows us to use chain-of-thought [Wei et al., 2022] by asking for an informal mathematical proof before generating the formal proof, making it more intuitive and comprehensible compared to purely automatic formal techniques. Additionally, partial proofs expressed in natural language are easier for humans to understand, adapt, or reuse, allowing for greater flexibility and collaboration between machine-generated suggestions and human mathematicians.We present the following contributions: 1) Pétanque: A new fast and lightweight environment to interact with the Coq theorem prover. 2) Two interactive proof protocols both leveraging natural language reasoning: tactic-by-tactic proof construction, and hierarchical proof templating. 3) We couple both protocols with standard search algorithms leveraging feedback from the ITP and using natural language to rerank proof candidates. 4) We evaluate this agent on a new dataset of textbook 4th MATH-AI Workshop at NeurIPS'24 (2024) 2 Pétanque: a lightweight interactive environment for CoqA common difficulty when interacting with interactive proof assistants in the context of machine learning is inadequate tooling (see for example [Reichel et al.] ). Following existing work [Gallego Arias et al., 2016 , Gallego Arias, 2019 , Yang and Deng, 2019 , Sanchez-Stern et al., 2020] , we have built a new environment for machine to machine interaction for the Coq proof assistant, particularly tailored for interactive, high-throughput, low-latency learning applications. Pétanque is based on Flèche [Gallego Arias, 2024] , a new document manager for Coq. We extend Flèche by enabling Pétanque to access the Coq proof engine directly without requiring edits in the associated document. This makes our environment fast and lightweight. A Python interface provides easy access to the API. See Appendix B for more information on Flèche and Pétanque. 
proof interaction protocols: 
 In this section, we present two approaches leveraging LLMs' ability to reason in natural language in order to find a formal proof with the help of a proof assistant. Tactic-by-tactic proof construction mimics the typical behavior of a standard Coq user: given the current goals, the agent generates one or several tactics that updates the goals and repeats this process until the proof is complete. By contrast, hierarchical proof templating tries to generate full proofs directly. Failed tactics are then replaced with holes to obtain a proof template. The agent repeats the process of filling each hole until the proof is complete. Our approach's originality is that although both protocols' inputs (goals) and outputs (tactics) are Coq code, the agent internally uses natural language as an intermediate representation to analyze the input and guide the code generation.An overview of the tactic-by-tactic proof construction agent is presented in Figure 1 . Given a Coq theorem, the agent first uses natural language to describe the goal and explain how to continue the proof (chain-of-thought). The last step synthesizes the corresponding Coq tactics. For instance, in Figure 1 , the goal is to prove that addition over natural numbers is commutative. The agent decides to try a proof by induction and correctly synthesizes a sequence of two tactics: intros n m. introduces two variables n and m of type nat (natural numbers), and induction n. starts an induction over n.The tactics are sent to the Pétanque environment, which parses and executes each tactic to update the current goal. A textual representation of the new goal is then fed back to the agent to make further progress in the proof. If the execution returns an error, the current goal does not change, but we augment the prompt with the failed tactics and ask the LLM to try something else for the next attempt. For instance, in Figure 1 , both tactics succeed and generate two new subgoals: the base case (for n=0, prove m + 0 = 0 + m) and the induction case (given the induction hypothesis Model Interface. In early experiments, we observed that conversation-style reasoning often diverges: after a few rounds, the output makes very little sense, and the agent never recovers. Following [Yang et al., 2024] -and similarly to [Thakur et al., 2024] -we use a synthetic interface to summarize at each goal the global objective (initial theorem), the current goal (in the middle of a proof), and failed attempts to solve the same goal.An example execution of the hierarchical proof templating agent is presented in Figure 2 . The agent pipeline is similar to the tactic-by-tactic method, but instead of focusing only on the next step, the agent generates a complete proof in natural language, before translating the proof in Coq syntax. For instance, in Figure 2 , the agent uses the inversion tactics on the hypothesis H which generate two subgoals with a simpler hypothesis H0, and then tries to solve each subgoals using this H0 hypothesis.The Pétanque environment then repairs the proof, replacing failed tactics by holes which admit and close the current subgoal, removing subsequent tactics until the focus moves to the next subgoal. Pétanque then checks that the resulting template is correct, i.e., assuming a valid proof for each holes, the proof is complete. A textual representation of each holes is then fed back to the agent which repeat the process to fill the holes one by one. For instance, in Figure 2 , apply H0 fails on both subgoals. The agent then repeats the process for each holes, using focused fine-grain reasoning to prove the corresponding subgoal. The proof is complete when there are no more holes. We combine our interactive protocol with the classic beam search algorithm. Inspired by [Yao et al., 2023] , we use the LLM to rank and sort the proposals at each step of the search. A simplified version of the code is presented on the right. At each step, agent.generate generates n_actions possible steps (tactics or proofs). Each step is then validated with petanque.step and the state of all the resulting candidates is stored. Then agent.sort calls the LLM to discuss, compare and finally rank and sort the candidates for the next step.For the tactic-by-tactic agent, the state contains the current goal obtained by running all the previous steps from the initial goal, i.e., the theorem statement. At each step, agent.generate generates multiple possible tactics for the current goal. For each tactic proposed by the LLM, petanque.step executes the tactic to compute the updated state. If the tactic is invalid, we log the failure and the state is not modified.For the template agent, the state contains a template, i.e. a proof with holes and a queue containing pointers to these holes and the associated goals. At each step, agent.generate generates multiple possible proofs for the first hole in the queue. For each proposed proof, petanque.step builds the corresponding sub-template. The updated state is obtained by replacing the current hole by the sub-template and adding the sub-templates holes to the end of the queue.As a baseline, our naive search corresponds to a beam search with n_action=1 and beam_size=1 (in which case, the sorting step is useless). 
evaluation: 
 Logical Foundations exercises: We extracted the exercises of Logical Foundations [Pierce et al., 2024] , the first volume of the Software Foundation textbooks series that is widely used to introduce Coq. We extracted 179 exercices. Given the popularity of this textbook the risk of data leak is high. We filtered out 66 "easy" exercises that are solved with one shot prompting. This dataset thus comprises 113 exercises.To avoid data leak issues, we extracted the 260 lemmas from the recent proof of BB(4) = 107 [ccz181078, 2024]. The repository was created in April 2024, long after the knowledge cutoff date of the current version of GPT-4o (October 2023). To provide the necessary context for the proof, for each lemma we augment the prompt with all the preceding definitions and lemmas.Evaluation. The results are presented in the following For both agents, we set n_actions=4 and beam_size=3, with n_steps=30 for the tactics agent and n_steps=10 for the template agent. While the tactics agent outperforms the template agent on the Logical Foundation benchmark, we observe that the template agent is significantly cheaper and faster than the tactics agent. By design the tactics agent requires much more interactions with the LLM to reach a full proof step by step.To limit the costs of our experiments, we only run the template agent on the first 100 Lemmas of the BB(4) benchmark. For the template agent, the gray numbers indicate the proportion of proofs that are correct at the first try (no holes). See Appendix A and Tables 1 and 2 for more details. 
related work and conclusion: 
 LLMs and theorem provers Automatic theorem-proving is a longstanding challenge in computer science [Newell et al., 1957] . Recent work has used neural models based on autoregressive language model that generate a proof tactic by tactic. Most works use finetuned LLMs [Polu and Sutskever, 2020 , Han et al., 2021 , Wu et al., 2022 , Yang et al., 2023 , First et al., 2023] Reasoning in LLMs This work is also related to recent investigations on the reasoning abilities of LLMs [Plaat et al., 2024] . Chain-of-Thought (CoT) prompting [Wei et al., 2022] was shown to improve LLM's answers; subsequent work found that these reasoning abilities could be elicited zero-shot [Kojima et al., 2022] . Further work interleaved CoT with decision-making [Yao et al., 2022] , added search and complex control flow to reasoning [Chen et al., 2022 , Yao et al., 2023 , Besta et al., 2024] , incorporated refinement and feedback [Madaan et al., 2024 , Shinn et al., 2024] , and learned to generate novel reasoning traces that proved beneficial for further training [Zelikman et al., 2022 [Zelikman et al., , 2024]] . Like our work, many of these methods -especially the ones using search and refinement -make use of LLM-based scoring or ranking functions [Zheng et al., 2023] . A Detailed results 
 
 Appendix: For the template agent, the gray numbers indicate the proportion of proofs that are correct at the first try (no holes). We also report the average length of the generated proofs (number of tactics) and the size of the smallest and the biggest proofs. Details are presented in Table 1 In this section we will describe Pétanque, a new environment for lightweight interaction with formal proof documents. Pétanque targets machine-learning applications such as reinforcement learning and other agent-based use cases, providing zero-overhead, purely functional1 access to Coq's proof engine, along with some utilities to implement custom proof search routines.Flèche Pétanque is built on top of Flèche [Gallego Arias, 2024] , a new document manager for Coq. Flèche is both a formal document interpreter and a build system for Coq proof documents.A schematic view of Flèche's behavior when the document is edited is presented in Figure 3 . Flèche maintains an enriched representation of Coq proof documents, including the relevant Coq states associated to the interactive proofs and their dependencies. When an edit occurs, Flèche only invalidate the parts of the document that depend on that change, following standard incremental computing practices [Acar et al., 2005] .At any point, users can query Flèche for data about the document -for example information about the current proof obligations at a given point of the document -and Flèche will compute the requested information on-demand, as fast as possible.coq-lsp Flèche's edit / query interface accommodates seamlessly the Language Server Protocol (LSP) protocol, the standard way to provide programming language support in modern Integrated Development Enviroments (IDEs). The LSP server coq-lsp2 built on top of Flèche thus provides continuous real-time checking for Coq documents inside popular editors such as Emacs or VSCode. Pétanque Unfortunately the edit/query document model turns out to be too expensive for highthroughput, proof-search applications: while Flèche invalidation on edits is very efficient, the associated overhead starts to become a problem when the edit frequency is higher than a few times per second. Moreover, using IDE protocols such as LSP means that agents need to exchange message with the server multiple times per step, which again creates non-trivial overhead. To overcome the previous problems, Pétanque provides one-shot direct access to Coq's proof state and tactic engine.A simplified view of the Pétanque API is presented in Figure 4 . Using this API, agents can perform speculative proof checking without altering the original document.The start methods initialize a proof session where the initial Coq proof state correspond to the theorem statement thm in the document file. Then, given a state, the run_tac method executes a tactic tac and return the resulting state if successful. The goals method can be used to retrieve a human readable version of the proof goals (e.g., as in Figures 1 and 2 ). computations are treated as stateless functions, i.e., for equal inputs, we obtain equal outputshttps://github.com/ejgallego/coq-lsp 


Decision: The reviewers are mixed on this work. While the work has limited novelty and lacks a comparison with related approaches, it presents an interesting system for theorem proving in Coq. We suggest the authors consider the comments mentioned in the reviews when submitting the camera-ready version.

Reviews: review: title: title: Review of NLIR
main_review: main_review: Summary：
This paper presented a new agent Pétanque for building proofs leveraging chain of thought as an intermediate representation, which obtain good performance on a new evaluation set.

Strength:
1. NL as general interface for reasoning about formal proofs is natural and important.
2. Based on this insight, authors design a lightweight and powerful proof tool Pétanque.
3. The proposed method show the outstanding performance and importance for theorm proof.

Weakness:
NL as an intermediate representation for reasoning actually have been proposed by [1] in theorm proof. Authors maybe should disscuss the difference.

[1] Lean-STaR: Learning to Interleave Thinking and Proving
title: title: The paper is overall well-written and the main ideas are clearly explained.
main_review: main_review: Paper Summary:

This paper introduces a gpt4 math agent for the Coq prover, using either step-by-step interactive tactic generation and hierarchical proofs, as well as search. The authors evaluate Logical Foundations and Busy Beaver proof using a new environment.

Weakness and strengths:

(+) The paper is well-structured and presents the problem, methodology, and findings. 

(+) This paper studies an interesting and well-motivated research topic: Formal theorem proving using LLM techniques.

(-) It would be beneficial to add more benchmarks in the experiments to evaluate the performance of the proposed method.
title: title: Interacting between NL and Coq for theorem proving
main_review: main_review: Overall, I think this paper presents a useful tool for Coq theorem proving, and for bridging NL and Coq in this task. The novelty and significance of this work convinces me less. The idea of agent-based approaches, and more concretely, letting LLMs reason in informal languages via having access to the proof checking environment is not new, and has been realized already in other proof assistants (e.g. Lean). So is the idea of building Python interfaces. Below are some other specific comments:

1. Since Pétanque is directly based on Flèche, I was hoping for a more detailed and straightforward discussion of which things were done by which work.

2. When seeing failure proofs, the idea of leaving holes in it for further proving instead of just discarding it sounds interesting. However, I feel this is based on the assumption that the failure proofs at least have a right overall structure and direction, which may not always be the case. In cases where the generated proofs are just not along the right line, the hole (in some sense the subgoals broken down) may be bad subgoals at the first place, limiting the chance of finishing the proof subsequently by focusing on such holes.

3. The heuristic in the beam search is designed here as a LLM ranking. There are other works which simply use LLMs' likelihoods as the heuristic. It would be great to have a comparison between these two approaches.

4. I like how the authors make a successful effort to avoid data leakage in their evaluation. If they wish to continue this work and expand into a full conference paper, I would also recommend expanding the scope of experiments.
title: title: The paper introduces an innovative approach by leveraging large language models (LLMs) like GPT-4 as intermediaries for mechanized theorem proving using natural language, which enhances interpretability and collaboration. The introduction of the Pétanque environment and interactive proof protocols shows strong potential, with promising evaluation results on Logical Foundations and Busy Beaver datasets. However, the paper could benefit from deeper theoretical exploration, broader dataset evaluation, and a more thorough comparison with alternative systems. Overall, it is a strong contribution to the field with room for further development.
main_review: main_review: # Review for "NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving"

## Strengths

### 1. Innovative Approach
The paper introduces a novel approach to leveraging large language models (LLMs) such as GPT-4 to serve as intermediaries in mechanized theorem proving. By employing natural language as an intermediate layer, it simplifies interactions between users and theorem provers. This technique is a valuable contribution that brings interpretability and flexibility to the process of formal proof generation.

### 2. Lightweight Environment (Pétanque)
The introduction of Pétanque, a fast and lightweight environment for interacting with the Coq theorem prover, is highly commendable. The environment is tailored to high-throughput, low-latency applications, making it a valuable tool for both machine-machine and human-machine theorem proving interactions.

### 3. Interactive Proof Protocols
The authors present two proof construction protocols: *tactic-by-tactic* and *hierarchical proof templating*, both of which utilize natural language reasoning. These protocols allow for more interpretable proof generation compared to purely formal methods and promote greater collaboration between machines and human mathematicians.

### 4. Comprehensive Evaluation
The paper evaluates its approach on two datasets: Logical Foundations exercises and Busy Beaver proofs. The evaluation metrics are clearly presented, showing that the method achieves a 46% success rate on Logical Foundations and a 50% success rate on Busy Beaver proofs, which demonstrates the practical effectiveness of the approach.

## Weaknesses

### 1. Limited Theoretical Explanation
While the paper presents impressive empirical results, it lacks a deeper theoretical explanation of why natural language serves as an effective intermediate representation in formal theorem proving. More discussion on the theoretical underpinnings and benefits of this method would provide stronger validation.

### 2. Narrow Dataset Evaluation
The evaluation focuses on two specific datasets. Expanding the scope to include a broader variety of theorems, including more complex or abstract ones, would provide a better understanding of how generalizable the proposed approach is across different domains.

### 3. Over-reliance on LLMs
The paper does not thoroughly address the limitations of relying heavily on LLMs like GPT-4, especially for scaling to more complex mathematical problems. It would be beneficial to explore potential limitations or challenges that arise when applying the approach to larger or more complex proof tasks.

### 4. Lack of Comparative Analysis
While the paper references prior works, a more detailed comparative analysis with alternative systems or approaches (e.g., symbolic AI theorem proving) would provide a clearer context of how this approach stacks up against state-of-the-art methods.

## Suggestions for Improvement

- **Expand Theoretical Discussion**: A deeper discussion on why natural language works as an effective intermediary between humans and formal proof systems could improve the paper's impact and clarify its contributions.
  
- **Broader Dataset Evaluation**: Expanding the evaluation beyond Logical Foundations and Busy Beaver proofs to other complex theorems would showcase the flexibility and robustness of the approach.
  
- **Address LLM Limitations**: A discussion of potential pitfalls, such as the scalability of GPT-4 to more complex or abstract mathematical domains, would strengthen the validity of the proposed method.
  
- **Incorporate Comparative Studies**: Direct comparisons with alternative theorem proving systems or strategies could offer valuable insights into the strengths and weaknesses of this method relative to other state-of-the-art approaches.

## Conclusion

The paper presents a promising and innovative approach to theorem proving by integrating natural language and LLMs into formal systems like Coq. The introduction of Pétanque and the two proof protocols provide a foundation for future research in this space. With further development, particularly around theoretical exploration and broadening the scope of evaluation, this work has the potential to become highly impactful in the field of mechanized theorem proving.