LEGO-Prover: Neural Theorem Proving with Growing Libraries

Introduction

The automation of formal reasoning tasks, such as theorem proving and mathematical proof formalization, represents a formidable challenge and an active area of research within the domain of artificial intelligence (Polu & Sutskever, 2020a; Han et al., 2022; Jiang et al., 2022a; First et al., 2023; Bansal et al., 2019; Lample et al., 2022; Jiang et al., 2022b; 2021; Zhao et al., 2023; Yang et al., 2023; Wang et al., 2023b; Liu et al., 2023). The process of formalizing mathematical proofs typically relies on human experts to transcribe intricate mathematical concepts into structured formal languages verifiable by interactive theorem prover like Lean (de Moura et al., 2015) or Isabelle (Paulson, 1994). This process, while robust, is often labor-intensive and demands a high level of expertise.

In the past few years, large language models (LLMs) have emerged as a promising avenue, with their capacity to process and produce human-like text, opening doors to the idea of LLM-based neural theorem proving. Specifically, two predominant paradigms have been extensively explored in neural theorem proving. One stream of work involves step-by-step proof generation (Polu & Sutskever, 2020a; Han et al., 2022; Polu et al., 2022; Lample et al., 2022; Wang et al., 2023b; Yang et al., 2023; Jiang et al., 2022a), where fine-tuned models provide single-step proof actions coupled with search algorithms to find the complete proofs. Another paradigm leverages the coding capabilities of LLM to construct entire proofs in a single decoding process (Jiang et al., 2022b; Zhao et al., 2023; First et al., 2023). As shown in Fig. 1(a) left, these approaches share common proving strategies that synthesize the proof sequentially, with each step building upon the previous proof step, and stocking all the proof code into one large proof block. We denoted these approaches as plain provers since they generate the whole proof directly. Despite their promising results, plain provers still have several shortcomings. On one hand, plain provers attempt to prove theorems using static LLMs independently, while different problems can usually provide some insights into others. In other words, different problems may share the same lemmas while plain provers cannot utilize the proved lemmas once again even though it has been proved. On the other hand, even though plain provers can generate short-chain proofs with the help of advanced large language models like ChatGPT or GPT-4 (OpenAI, 2023) , it usually fails when it comes to long-chain proofs due to the reasoning difficulty.

To overcome the shortcomings of plain provers and inspired by the modularity of LEGO building blocks, we present LEGO-Prover, a novel approach designed to prove theorems in a block-by-block manner backed by a growing skill library. As shown in Fig. 1(a) right, LEGO-Prover tackles the problem of proving a theorem by first proving the sub-goal lemmas and then finalizing the problem using these lemmas. These lemmas can be retrieved from the skill library or newly constructed during the proving process. Specifically, Fig. 1(b) shows the overall process of LEGO-Prover, containing a prover and an evolver, which are bridged by the growing skill library. The prover takes the problem’s formal statement as input and retrieves skills to prompt the LLM in generating the modular proof, with the generated lemmas accumulated into the skill library. However, lemmas created by the prover are often problem-specific with low reusability. Thus, LEGO-Prover incorporates an evolver that transforms the skills in the library for better generality, reusability, and complexity of the skills. The evolved new skills will also be verified and added back to the skill library.

We conduct extensive experiments on the popular theorem-proving dataset miniF2F (Zheng et al., 2021) to validate the effectiveness of our proposed approach. LEGO-Prover significantly outperforms previous approaches, achieving a pass rate of 57.0% and 50.0% on the miniF2F valid and test datasets, respectively. With a 6.75% absolute improvement on average over the previous state-of-the-art methods. In addition, our case study reveals that LLMs prove theorems modularly akin to LEGO block assembly, utilizing the retrieved skill by directly copying or using as a referee to construct the proof. Moreover, the learned skill library contains 22532 skills encompassing many useful high-level lemmas broadly applicable to various problems, as is shown in our case study and ablation study.

Related works

Machine learning for formal mathematics. Modern formal mathematics environments often center around Interactive Theorem Provers (ITPs) like Lean (de Moura et al., 2015), Isabelle (Paulson, 1994), Metamath (Megill & Wheeler, 2019) and Coq (Barras et al., 1997). These ITPs often include specific formal languages, accompanied formal verifiers, and automated provers like Sledgehammer. ITPs provide machine-human interactive interfaces, which gives verification results during formal proof construction for specific theorems and human coder can correct errors or continue to fill gaps in proofs under the guidance of error messages and local proof states, respectively.

Research leveraging machine learning techniques atop these formal mathematics environments generally falls into two predominant paradigms. The first focuses on proof search strategies and premise selection, epitomized by GPT-f (Polu & Sutskever, 2020a), where a language model advises single-step actions based on the current proving state, and the tree search finds a sequence of correct steps using actions given by the language model. The follow-up works PACT (Han et al., 2022) and Expert Iteration (Polu et al., 2022) incorporate supplemental pre-training tasks like theorem naming to enhance the policy model’s reasoning ability. HTPS (Lample et al., 2022) applies Monte-Carlo tree search coupled with online training to optimize the exploration of the proof space. DT-Solver (Wang et al., 2023b) enhances search efficiency by dynamically adjusting search budgets to accommodate varying levels of state complexity. Thor (Jiang et al., 2022a) blends traditional Automated Theorem Provers (ATPs) with neural policy models to prove theorems in a neural-symbolic manner. Magnushammer (Mikuła et al., 2023) augments Thor’s performance by integrating premise selection, thereby boosting the performance of rule-based ATPs.

Autoformalization. Our LEGO-Prover aligns closely with the second paradigm in machine learning for formal mathematics, which leverages the capabilities of large language models (LLMs) for the formalization of mathematical proofs. Several notable works have paved the way in this domain. For instance, Wang et al. (2018) delved into both supervised and unsupervised translation techniques for auto-formalization tasks. Wu et al. (2022) makes its first attempt at employing a large language model to translate natural language mathematical problems into formal theorem statements. Building on this, Draft, sketch, and proof Jiang et al. (2022b) develops a three-step approach that aims to fully formalize proofs, using natural language as guidance. First et al. (2023) goes a step further by generating complete proofs in a single pass and introducing a proof repair model to enhance the theorem-proving capabilities. Zhao et al. (2023) advances Jiang et al. (2022b) by incorporating cross-verified informal proofs to better inform the generation of formal proof sketches. Despite their contributions, none of the aforementioned methods have succeeded in establishing a learning paradigm that incrementally formalizes increasingly complex problems via a growing skill library, a gap that our work seeks to fill.

Skill-based agents. LEGO-Prover is also related to trending AI agents powered by large language models like GPT-3.5 and GPT-4 (Shen et al., 2023; Park et al., 2023; Wang et al., 2023c; Zahedi & Kambhampati, 2021). These AI agents are characterized by their ability to perform complex tasks through a combination of task planning, logical reasoning, and skill accumulation. For example, Voyager (Wang et al., 2023a) creates an AI agent capable of autonomously playing Minecraft. It has a dynamic growing skill library that empowers the in-game character to tackle increasingly intricate tasks. Similarly, (Cai et al., 2023) showcases the ability to generate reusable Python tools and documentation, which can then be leveraged by weaker GPT models, increasing the ability of the model.

Method

In this section, we introduce the detailed implementations of our proposed LEGO-Prover. Following the setting of Jiang et al. (2022b), we assume that each theorem is equipped with an informal statement, a human-written informal proof, and a formal statement defining the problem. As illustrated in Fig. 2, LEGO-Prover consists of two main components: the prover and the evolver. The prover decomposes the problem into possible subgoal lemmas and proves the problem in a block-by-block style, aided by the skill library. The evolver refines skills in the skill library for enhanced diversity, generality, and reusability, and also resolves decomposed sub-goals from the prover to create new skills. These components are linked via a skill library housing lemmas and requests. In the following sections, we will detail introduce the skill library, the prover, and the evolver.

The skill library contains various vector stores that are optimized for retrieval. Every vector store maintains its data in pairs consisting of documents and their corresponding embeddings, encoded with an embedding language model Practically, ChromaDB serves as our vector store, coupled with the OpenAI’s text-davinci-ada embedding model.. Upon the receipt of a query, the vector store employs the embedding model to encode the query and leverages the k-NN algorithm to retrieve relevant documents stored within. The skill library used in LEGO-Prover is comprised of three distinct vector stores. 1) The lemma vector store contains the Isabelle verified lemmas, encompassing both the lemma’s statement and its proof. This is the core of the skill library and it facilitates the perpetual enhancement of LLMs’ capabilities in constructing increasingly intricate theorems. For representation simplicity, the notion of lemmas in the lemma vector store and skills in the skill library are use interchangeably in this paper. 2) The request vector stores preserve the lemma statements proposed by the decomposer. These requests are crucial to the success of LEGO-Prover, their works as an in-depth reasoned query for retrieving the useful skill for the prover, as well as possible complete lemmas when they are solved by the evolver. 3) The problem vector store houses the formal statements in the miniF2F dataset. The evolver utilizes these problem statements as heuristics to guide the LLMs in generating more beneficial new lemmas.

2 Prover

As illustrated in Fig. 2 (a), the prover employs a three-step process to construct the proof. Initially, an informal solver is deployed to draft a solution in natural language corresponding to the informal statement. Akin to (Jiang et al., 2022b), LEGO-Prover experiments the use of ground truth human-written proofs as alternatives to model-generated proofs. After obtaining the informal proof, LEGO-Prover constructs the formal proof using the decomposer and the formalizer sequentially, which we detailed in the following.

Decomposer. The decomposer aims to decompose the formalization tasks, which transform the informal proof into the decomposed step-by-step informal proof as well as decompose the problem into formal goals. A concrete example of the decomposer is shown in Fig. 6 in Appendix. A.1. Specifically, the decomposer prompts the LLM to refine informal proofs, producing step-by-step informal proof that more closely aligns with the structure of the actual Isabelle proof code. We posit that this alignment is crucial as it considerably reduces the complexity encountered during the formalization process. Concurrently, the decomposer tasks the LLM with generating requests: some potential lemma or theorem statements that could be useful in addressing the given problem. Each request is composed of a chain-of-thought reasoning on what kind of lemma is required for solving the problem followed by the formal statement of the lemma. Subsequently, LEGO-Prover put these requests into the request vector store.

Formalizer. The process of formalization involves translating an informal proof into Isabelle’s proof sketches, as depicted in Fig. 7 (refer to Appendix. A.1). In addition to the problem statement, the refined informal proof, and the formal statement, the formalizer is designed to incorporate useful lemmas retrieved from the lemma vector stores as part of the input. The formalizer employs the proposed request originating from the decomposer and the formal statement of the problem as query texts and, in total, retrieves $n_{f}$ skills. Upon collecting all the necessary input, the LLM is tasked to provide the proof code. Unlike the setting in Jiang et al. (2022b) and Zhao et al. (2023), we prompt the LLM to construct the complete content of the source file in Isabelle. This may encompass the requisite imports, definitions, or lemmas before the elucidation of the main problem to be proven. Consequently, the LLM possesses the capability to generate or apply useful lemmas before embarking on the resolution of the problem. Empirical evaluations demonstrate that our model exhibits a more modular problem-solving approach compared to established baseline methods. This modularity facilitates recycling smaller lemma components, thereby enhancing the LLM’s capability to tackle progressively intricate problems.

After obtaining the formalized proof code, LEGO-Prover employs the Isabelle theorem prover to verify the correctness of the provided proof code. In instances where a particular proof tactic (such as ”by …”) falls short of proving the given conjecture, we resort to 11 heuristic tactics alongside the sledgehammer method to facilitate an auto-correction. The heuristic selection we employ is consistent with those presented in Jiang et al. (2022b). After verifying the code, all validated lemmas or theorems are added to the skill vector store, while any failed lemmas’ statement is added to the request vector store. We consider a formalized proof valid if and only if (a) the proof does not contain ”cheating” keywords (sorry or oops) that exit a proof without completing it. (b) Isabelle can verify the proof code containing the corresponding formal statement.

3 Evolver

The lemmas extracted from the prover are mostly problem-specific, rendering them non-reusable with limited applicability. And the number of these lemmas is also very limited. The objective of the evolver is to create or refine these skills, enhancing their reusability and expanding their functional coverage. As shown in Fig. 2 (b), the evolver contains two functionalities: the directional transformer transforms the current skill and the request solver directly solves the request proposed by the prover to create new lemmas. We detail each in the following.

Directional transformer. The objective of the directional transformer is to facilitate the evolution of a skill along various predefined trajectories, thereby augmenting the reusability and usefulness of the skill. It is composed of four distinct trajectories: extension of dimensions, identification of key concepts, parameterization, and enhancement of complexity. Table. A.1 shows the detailed functionality of each evolving direction. Each instance of the directional transformer adheres to a unified prompt template depicted in Fig. 9. The adaptation involves substituting the core description and its in-context examples for the corresponding evolving directions. Specifically, the directional transformer begins with randomly selecting the least evolved skill (with the least amount of time being selected to evolve). Subsequently, the transformer employs this skill to retrieve $n_{d}$ relevant pending problem’s formal statement from the problem vector store and the relevant request’s formal statement from the request vector store. Upon assembling the inputs for the LLM, the transformer arbitrarily selects one direction of evolution and prompts the LLM to generate a novel skill.

Request solver. The request solver is designed to facilitate the development of new skills by directly addressing the sub-goals proposed by the prover. As depicted in Fig. 8, the process initiated by the request solver involves the random selection of a minimally solved request (with least amount of time being selected to solve the request). After this selection, this request is employed to query the lemma vector store to retrieve pertinent skills that can serve as references. Finally, the request solver prompts the LLM to generate the proof for the request.

After obtaining the new skill (evolved lemma or solved request) generated by the LLM, the evolver uses Isabelle to verify the generated code. To mitigate the risk of redundancy within the skill library, a comparative strategy is conducted between the newly acquired skills and existing ones. This is accomplished by employing the SequenceMatcher method from the difflib Python library, which quantifies the level of difference between the new and existing skills. Only skills that have been verified and exhibit a difference bellowing the predetermined threshold of $0.85$ are incorporated into the skill library.

Experiments

Implementation details. To expedite the experimental procedure, both the prover and the evolver are executed in a multi-processing manner, maintaining a process number ratio of $3:8$ respectively. Consistent with the (Jiang et al., 2022b; Zhao et al., 2023), each problem undergoes 100 attempts of proving. To maximally leverage the expanding skill library, problems are formalized through successive rounds, with each round addressing each valid/test set problem once.

For the execution of the prover and the evolver, ChatGPT is utilized as the LLM. A combination of gpt-3.5-turbo, gpt-3.5-turbo-0301, gpt-3.5-turbo-0613, gpt-3.5-turbo-16k, and gpt-3.5-turbo-16k-0613 is employed, with a model being selected randomly during calls to the OpenAI API. The temperature is consistently set at $T=0.7$ across all procedures. Within the prover, 3-shot examples are leveraged for the decomposer. Regarding the formalizer, the quantity of reference skills $n_{f}$ is set to $6$ for the valid set and $4$ for the test set, and paired with 2 formalization in-context examples. For the directional transformer, the number of reference problem statements $n_{d}$ is set to 4, supplemented by two directional transformation in-context examples. For the request solver, 3 skills are retrieved for reference.

Dataset and evaluation. For a more accurate comparison, we follow (Jiang et al., 2022b; Zhao et al., 2023) and adopt the miniF2F dataset (Zheng et al., 2021). This dataset includes 488 problems sourced from high-school mathematical competitions. These problems vary in difficulty, ranging from basic algebra and number theory, originating from the MATH dataset Hendrycks et al. (2021), to more challenging problems found in the American Invitational Mathematics Examination (AIME) and International Mathematical Olympiad (IMO). The problems are divided into valid and test sets, with 244 problems each. In this paper, we utilize the updated version of the miniF2F dataset from Jiang et al. (2022b). Each question in this updated dataset contains a formal statement in Isabelle language, an informal statement, and a human-written informal proof. For interacting with the Isabelle theorem prover, we employ the PISA environment (Jiang et al., 2021). PISA is a flexible Python REPL wrapper for Isabelle, capable of verifying Isabelle’s code and providing information such as proof states or error messages from Isabelle.

We have included baselines that represent state-of-the-art neural theorem proving in Isabelle. Thor(Jiang et al., 2022a) and Thor with expert iteration on auto-formalized data (Wu et al., 2022) are works focused on proof search paradigms, which use a fine-tuned 700m language model to prove theorems. Draft, Sketch, and Prove (Jiang et al., 2022b) and Subgoal-Learning Zhao et al. (2023) are works that use Codex or ChatGPT to prove theorems directly.

Following the setting from Jiang et al. (2022b), we test the LEGO-Prover with model-generated and human-written informal proofs. The model-generated informal proofs are pre-generated using GPT-4, with up to 20 informal proofs per problem. For each proving attempt, we randomly select one proof as the informal proof to feed into the decomposer procedure. For ablation, we remove the growing skill library to validate the effectiveness of the LEGO-Prover. Due to limited resources and the expense of OpenAI API calls Estimated to be around 300 dollars for one experiment with 100 proof attempts, we perform ablation only under 50 proving attempts per problem on the miniF2F validation set.

2 Main result

In Table. 1, we illustrate the proportion of successful formal proofs found on the miniF2F dataset. Thor and Thor + expert iteration displays the performance of the fine-tuned search-based proving method. The results indicate that all LLM-based methods significantly outperform the search-based methods by around 4.7%. The efficacy of search-based proving methods is limited by the short proof steps that the policy language model generates, drastically increasing the search space and, therefore, hindering the prover from finding long proofs.

Our proposed LEGO-Prover significantly outperforms both search-based and LLM-based methods. With proofs written by humans, the LEGO-Prover improves by 7.3% and 4.5% over the Subgoal-Learning method on the miniF2F-valid and miniF2F-test datasets, respectively. A total of 257 out of 488 problems were solved by the LEGO-Prover with human-written proof. When replacing human-written informal proofs with model-generated informal proofs, the LEGO-Prover still achieves 52.4% and 45.5% pass rates on the valid set and test set, respectively, close to the results with human-written informal proofs.

Effects of the growing skill library. The growing skill library greatly enhances the proving ability of static LLMs like chatGPT or GPT-4. As the major contribution of LEGO-Prover, we are interested in how well it contributes to solving more problems and improving the LLMs’ ability. Specifically, we remove the growing skill library (including the evolver). As shown in the Table. 1, in 50 attempts, LEGO-Prover achieves 50.4% on the validation set, whereas the LEGO-Prover without a skill library achieves 47.1%. For a more intuitive representation, we further plot the trends of the number of problems solved against the number of proving attempts for both settings, shown in Fig. LABEL:fig:results(a). Compared to the problem solved without a growing skill library, the advantage of adding the skill library is initially minimal, as the libraries are still underdeveloped and lack useful skills. However, as the skill library expands, the gap between LEGO-Prover and the ablation method widens consistently. This outcome supports our hypothesis that the prover becomes increasingly adept at formalizing theorems as more skills are added to the skill library.

3 Analysis

Figure. LABEL:fig:results(c) illustrates an example of a skill-evolving tree in the skill library. The grown skill library is a massive forest containing numerous evolved trees like this one. The lemmas, originating from either the prover or the evolver’s request solver sub-task (as the example shown in the figure), become the root nodes of these skill-evolving trees. The evolver’s directional transformation generalizes these lemmas and creates child nodes. In terms of statistics, there are 22532 skills in the skill library in total, with 10.8% of the skills originating from the prover, 38.2% originating from the evolver’s solve request sub-task, and 51.1% originating from the evolver’s directional transformation sub-tasks. Although some lemmas are trivially true or already exist in Isabelle’s theorem library, LEGO-Prover generates more unique, interesting, and useful lemmas. The gap between natural and formal language is the greatest challenge in formalizing natural language mathematical proofs. A simple proving step described in natural language can result in numerous lines of code written in the formal language. However, this gap can gradually diminish as we accumulate more lemmas and theorems. To conclude, the grown skill library generated by LEGO-Prover significantly enlarges this library and further bridges the gap between informal and formal mathematical languages.

3.2 How does the skill boost the ability of LLMs?

To investigate closely how these learned skills can better help and boost the performance of LLM, we manually inspect the successfully proven problems in the miniF2F valid set. The conclusions are as follows:

Skill as directly reusable blocks. This is the most straightforward way of utilizing the generated skills. Since every skill in the skill library is verified by the Isabelle prover, LLM can directly copy the lemma code from the input prompt without fear of causing an error. As shown in Fig. 5 left, the final proof of the problem algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x directly copies the retrieved skill am_gm’s code as part of the proof and uses this lemma to help prove the problem.

Skill as reference for solving the problem. Many skills cannot be directly reused but are very helpful as reference examples for formalizing the main problem. As shown in Fig. 5 right, the retrieved skill examples prod_1n_4n provide great clues for solving the conjecture prod_frac_common_factor. Since the provided skills are lemmas with verified steps, these steps drastically increase the accuracy of the LLM to generate the correct proof steps.

Fig. LABEL:fig:results(b) first compares two scenarios: directly applying retrieved skills to the proofs and constructing new lemmas by imitating retrieved skills to assist in theorem proving (represented by the light blue and light green lines). It then examines the skill evolution pattern of the lemmas used in the proofs (corresponding to Fig. 2 (b) and Table. 2). Out of 135 problems of the miniF2F-valid dataset passing the validation of the Isabelle verifier, 24% is completed with the aid of retrieved skills. Within this subset, 51% of the problems directly incorporate the retrieved skills into their proofs, while the remaining 49% formulate new lemmas that are specifically tailored to address the distinct problems at hand. Regarding the skills directly applied in the proofs, 71% are procured by the ”do requests” procedure. The skills derived through the evolution techniques of ”identifying key concepts” and ”scaling complexity” each contributes to 12%, while those acquired through ”parameterization” constitute 6%. Although skill as directly reusable blocks is the most ideal usage of skills in the library, the problems solved by directly reusing the skill are not substantial. That is because many trivial problems in the dataset miniF2F can be solved trivially without requiring any skill as a reference.

Conclusions

In this work, we introduced a new theorem-proving method, LEGO-Prover, which uses a growing skill library to continuously boost the capability of LLM for formalization. The prover utilizes refined structural informal proof and retrieved lemma to correctly formalize the proof. The evolver solves the request proposed by the prover or evolves existing skills into new skills. LEGO-Prover introduces a fundamentally different theorem proving paradigms for the community. With the previous approaches all struggling to complete the proof at once, LEGO-Prover tries to prove the theorem in a block-by-block manner, akin to divide and concur approaches. Extensive tests show that our method can indeed improve pass rates on the miniF2F dataset. Our ablation studies and detailed analysis showcase the effectiveness of each component we proposed in LEGO-Prover.

References

Appendix A Appendix

In this section, we illustrate the prompts used in the LEGO-Prover. For prover, the prompt used is the decomposer (Fig. 6), and the formalizer (Fig. 7). For the evolver, the prompt used is the directional evolver (Fig. 9) and request solver (Fig. 8). The blue line separates the LLMs’ input and outputs.

For directional evolve, we list all the core statement to be replaced in the Table. 2