LEGO-Prover: Neural Theorem Proving with Growing Libraries
Authors: Haiming Wang
Huajian Xin
Chuanyang Zheng
Zhengying Liu
Qingxing Cao
Yinya Huang
Jing Xiong
Han Shi
Enze Xie
Jian Yin
Zhenguo Li
Xiaodan Liang
Venue: ICLR 2024 oral (2024)
Keywords: Theorem proving
Large language model
Autoformalization
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: Despite the success of large language models (LLMs), the task of theorem proving still remains one of the hardest reasoning tasks that is far from being fully solved. Prior methods using language models have demonstrated promising results, but they still struggle to prove even middle school level theorems. One common limitation of these methods is that they assume a fixed theorem library during the whole theorem proving process. However, as we all know, creating new useful theorems or even new theories is not only helpful but crucial and necessary for advancing mathematics and proving harder and deeper results. In this work, we present LEGO-Prover, which employs a growing skill library containing verified lemmas as skills to augment the capability of LLMs used in theorem proving. By constructing the proof modularly, LEGO-Prover enables LLMs to utilize existing skills retrieved from the library and to create new skills during the proving process. These skills are further evolved (by prompting an LLM) to enrich the library on another scale. Modular and reusable skills are constantly added to the library to enable tackling increasingly intricate mathematical problems. Moreover, the learned library further bridges the gap between human proofs and formal proofs by making it easier to impute missing steps. LEGO-Prover advances the state-of-the-art pass rate on miniF2F-valid (48.0\% to 57.0\%) and miniF2F-test (45.5\% to 50.0\%). During the proving process, LEGO-Prover also generates over 20,000 skills (theorems/lemmas) and adds them to the growing library. Our ablation study indicates that these newly added skills are indeed helpful for proving theorems, resulting in a 4.9\% improvement in success rate

Published as a conference paper at ICLR 2024
LEGO-PROVER: NEURAL THEOREM PROVING WITH GROWING LIBRARIES
Haiming Wang
Huajian Xin
Chuanyang Zheng' Zhengying Liu
Qingxing Cao Yinya Huang Jing Xiong'
Han Shi?
Enze Xie² Jian Yin
Zhenguo Li
Xiaodan Liang 15.6t
The Chinese University of Hong Kong *City University of Hong Kong 'MBZUAI "DarkMatter AI Research
'um Yat-sen University Huaawii Noah's Ark Lab
[wanghm39, xinhj, caoqx, xiongj69, issjyin) @ wea.lissss..edu.co cyzheng21 @ ese.cuhk. www...u.....kkkk.....o.
(liuzhnggying,, xie.enze, shi.han, Li.Zhenguo) @huawei.com, yinya.huang @ hotmail.com, xdliang328e @ gmail.com
ABSTRACT
Despite success of large language models (LLMs), the task of theorem proving still remains one of the hardest reasoning tasks that is far from being fully solved. Prior methods using language models have demonstrated promising results, but they still struggle to prove even middle school level theorems. One common limitation of these methods is that they assume a fixed theorem library during the whole theorem proving process. However, theorems or even new theories is not only helpful but crucial and necessary for advancing mathematics and proving harder and deeper results. In this work, we present LEGO-Prover, which employs growing skill library containing verified lemmas as skills augment the capability of LLMs used in theorem proving. By constructing the proof modularly, skills retrieved from the library and to create new skills during the proving process. These skills are further evolved (by prompting an LLM) to enrich the library on another scale. Modular and reusable skills are constantly added to the library to enable tackling increasingly intricate mathematical problems. Moreover, the learned library further bridges the gap between human proofs and formal proofs by making it easier to impute missing steps. LEGO- Prover advances the state-of- the-art pass rate on miniF2F-vali (48.0% to 57.0%) and miniF2F-test (45.5% to 50.0%). During the proving process, LEGO-Prover also generates over 20,000 skills (cheorens/lemmas) and adds them to the growing library. Our ablation study indicates that these newly added skills are indeed helpful for proving theorems, resulting in a 4.9% improvement in success rate
we all know, creating new useful
enables LLMs to utilize existing
INTRODUCTION
The automation of formal reasoning tasks, such as theorem proving and mathematical proof for- malization, 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; Xiong et al., 2023; 2024; Huang et al., 2024). 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 high level of expertise.
In the past few years, large language models (LLMs) have emerged as a promising avenue, with their capacity process and produce human-like text, opening doors to the idea of L.M--based neural theorem proving. Specifically, two predominant paradigms have been extensively explored in neural
These authors contributed equally. Corresponding authors
Code available https: tig.t.b....... com/wo/////ooooooo o 2/1.800- Prover.

---

Published as a conference paper at ICLR 2024
Plain Prover
LEGO Prover
theores amc12a, 21126_2883_04:
fixes betreal
incquality arithretic gesnetric weans)
assumes "esa" "I=b"
Lemma @
(a/a)
rikes y.11 real
statennet
proof
ae" (Is proof
assumes "xx se g" "y sc shous *x"2 y 20xey" using asons by <ATP>
I- Prove special fore of the AN-CM in-
to tema 2. Synthesizzed by " proves a special form of the AM-D4 inequality required in the proof of the target theores. +)
prover
request
equalsty as an internedate resutt that is equivalert to the leara on the right e] also have "... 8" proof
retrieved
define at where (xtrs
rixes real
Lorna
Leana
">"ugrt(y(a!"
assures "x > "y shous *x/y y/x 50
have "al legez or using cl
al_a2 by <ATP>
proof
Veges 8" using c1
by <ATPs
"x/y v/x sartiwyy sgrt(y/e1"
then have "at"2 a2*2
a2*
using (of "sarttudy?" "sartty/o"1
growing skitl Library
using c2 c3 by -ATP-
by <ATPs
then have "sertixry122 sartly/kin2
(krt(k/y) vegrt ly/a1"
qed
using dlf by force
then have "x/y + y/k 2.2 sqrtix/y
theores amc12a 2863_p24:
yxx"
assumes "bsa" "Ieb"
fixes be:rmal
Temta
directionat
evolved
have "x/y y/X using at c1
shows "ta [a/b] In (b/a) In a
by show ?thesis by
CVO Lver
ged
tinally show 7the51s
using x: .8 by <ATP>
qod
qud Finally khow 2thes
notwed
SOlver
reqest
(a)
(b)
Figure 1: (a) Comparison between plain provers and LEGO- Unlike plain provers that prove the theorem sequentially. LEGO-Prove constructs the proof in modular paradigm. Useful lemmas be directly retrieved from the skill library and used as part of the proof. A newly constructed lemma can also be added to the skill library to help the proof of other theorems. (b) Overall framework of our proposed LEGO-Prover. The L.GOO-Prover comprises two main components: the prover and the evolver. The prover modularly proves theorems using retrieved lemmas and, in the process, generates new lemmas and lemma requests as hy-products. Meanwhile, the evolver either transforms lemmas for enhanced reusability and generalizability directly addresses the requests. These components are interconnected through a growing library, which archives both verified lemmas and unsolved requests.
theorem proving. One stream of work involves step-by-ster 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 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 al., 2023; First et al., 2023). As shown in Fig. ((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 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 LLMs like ChatGPT or GPT-4 (OpenAI, 2023). it usually fails when it comes to long-chain proofs due to the reasoning difficulty.
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. ((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 prover and an evolver that share an expanding skill library. The prover takes the problem's '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-specifie 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. LEGO-Prover runs the prover and evolver in parallel (Algorithm 1). For each problem in the dataset, the prover makes 100 attempts, while the evolver continuously works to evolve new skills or solve requests, providing more lemmas for the prover.
2

---

Published as a conference paper at ICLR 2024
We conduct extensive experiments the popular theorem- prooinn dataset miniF2F (Zheng et al., 2021). 1). LEGO -rover significantly outperforms previous approaches, achieving pass rate of 57.0% and 50.0% the miniF2F valid and test datasets, respectively. With 6.75% absolute improvement on average over the previous state-of-the-ard methods. 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 more than 20,000 skills encompassing many useful lemmas, as 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), and Coq (Barras al., 1997). These ITPs often include specific formal languages, accompanied formal verifiers, and automated provers like Sledgehammer. ITPs provide machine- humaan interactive interfaces, which give verification results during formal proof construction for specific theorems, and human coders can correct errors or continue to fill gaps in proofs under the guidance of error messages and local proof states, respectively.
Proof search and premise selection. 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 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 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 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 (Mikula et al., 2023) augments Thor's performance by integrating premise selection, thereby boosting the performance of rule-based ATPs.
Autoformalization. The second paradigm in machine learning for formal mathematics leverages the capabilities of LLMs for the formalization of mathematical proofs. (Wu et al., 2022) makes its first attempt at employing an LLM to translate natural language mathematical problems into formal theorem statements. Building on this, DSP (Jiang et al., 2022b) uses natural language as guidance to fully formalize proofs. (First et al., 2023) goes step further by generating complete proofs in single pass and introducing a proof repair model to enhance the theorem- prrvving capabilities. (Zhao et al., 2023) advances DSP by incorporating vross-verified informal proofs 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 LLMs (Shen et al., 2023; Park et al., 2023). 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. DreamCoder (Ellis et al., 2020) develops problem-solve expertise by creating and expanding programming languages, guided by a neural network and a 'wake- sleep' learning algorithm. Lastly, template-basee based conjecturing (Nagashima et al., 2023) introduces a novel approach to generate auxiliary lemmas and use them to prove final goals.
3 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, hrman-written informal proof, and formal statement defining the problem. In the subsequent sections, we will provide detailed introductions to the skill library, the prover, and the evolver. A detailed algorithm description is provided in Appendix A.2.
3

---

Published as a conference paper at ICLR 2024
informel
Informal proof excien ard than thang An us that Ind torn an ot least 2, ss the valles do 2-208...
decorposed
Tornal proof
2f b >-1,, west Esble vatua of Stew that 18 1. 7,
@
5. Zetroduce vart-
cocomes Ty on
2. Saven that
using usaia by AATP
G. Lee the IM--!
Teams
that the tere /
fixms real
shows
proof
heve "kty ugt Karry) serthyod"
"rgrixoy"" "sprttyos"))
skitl Library
and
decomposed formal geals
Lonna secter store
Tarns
Flane V 15 rea! shout Jeasn
stallar Lomna
theones ant 2000
nesumet "bas" "Id"
"ia (9/2) In (2/9)
farml stateeent
y22 Soany"
probten vector store
by uid:
allo have
using ax yo by HATS
sccened 2 4"
foond
finully 5tov Noti
Teass
Aeporon ank 2044
axanneg "Lau"" "aagg
clactar pratic
Fixes real "x shove sgrt
eastand
lives 12 real aloess "x"2 7 Deway"
store
(brul
antng ascms
Lemms t1
add: Leal_cort.aatt
istmp wdd:
store
Lenno
slacler
la 11 have
roal
cossmes Ta 6"
Le U using.
store
[slip addi 1og Ief)
7thooda
Figure 2: Overview LEGO-Prover. (a) The prover follows three steps to solve a problem: first, the informal solver generates a solution to the problem statement. This solution is then broken down by the decomposer into a step-by-step proof, and suggesting useful sub-goals as lemma statements. We use these statements to retrieve useful lemma from the skill library. Finally, the formalizer generates the final proof using the decomposed informal proof and the retrieved lemmas in block-by-block fashion. LEGO-Prover subsequently adds the proposed requests and newly constructed lemmas to the request store and lemma store, respectively. evolver contains two evolution approaches, the directional transformer transforms the existing skill into a more general and reusable form in four predefined directions. The request solver directly solves the requested subgoal proposed by the prover. Formally verified lemmas from the evolver are added to the lemma vector store.
(b) The
3.1 SKILL LIBRARY
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?. Upon the receipt of a query, the vector store employs the embedding model 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 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.
3.2 PROVER
As illustrated in Fig. 2 (a) and Algorithm 2, the prover employs a three-step process to construct the proof. Initially, LLM is deployed as an informal problem solver, drafting solutions in natural language that correspond to the informal statements presented. Similar to the approach discussed in
Practically, ChromaDB serves as our vector store, coupled with the OpenAl's Al's text-davinci-ada embedding
model.
4

---

Published as a conference paper at ICLR 2024
Table 1: Prompt outine for four components in LEGO-Prover.
Decomposer
Formalizer
Directional transformer
Request solver
Ippi::
Inpur:
Inpor:
Iipu::
pusiide a better structured step-lty- step proof that cleser to Isabelle. and request relevani lemmus, and orems that might help proving this problem.
provde formal proof in response
.your task is to modiffy the given lemma. theorem. function, def- inition given
provide formal proof in resgomse to given formal statemnn....
problem statement...
Useful skills [Jemma code)
to sulving one or more the problems provided. You should accompplish this {irmsdumm direction describ- tion) j...
(rerived ple l...
comteci eham-
Usdul skills 2: { lemmm code) }
Formal statement: (problem state ment)
(in comeet example)
(in-ooneext esample) }...
Statoment: (informal statement Informal proof: (informal pruof)
Statement: (informal statement)
Oupur: Formal proof (sew lemma vode)
Informal proof: (stractual informal proof)
Problem I: {prublem/cquees)
Formal statement: { (formal state-
Problem 2: problem/cquess)
ment)
Formal statement: (formal
Ouput:
men]
{in cuntest example) )... Skill ecolve: (Jemma cude)
Structural pruof: step I...
Ouper:
Required skills:
Foraml proof: complete formal
Outpuc:
Thought 1: (CoT for request
proof code
Evulved skill: (new Jemma code
Code (lemmu siatementt)
(Jiang et al., 2022b), LEGO-Prove explores the use of both ground truth, which are human- proofs, and model -enerrted proof's as viable alternatives. After obtaining the informal proof, LEGO- Prover methodically builds the formal proof. This process involves two sequential stages: first, the decomposer breaks down the proof into manageable components; second, the formalizer rigorously structures these components into a formal proof.
The decomposer aims to decompose the formalization tasks, which transform the informal proof into the decomposed step-by-step informal proof well decompose the problem into formal goals. As shown in Table. 1 column (and Fig. 6 for complete example), 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 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.
Decomposer.
Formalizer. As depicted in Table. 1 column 2 (full example shown in Fig. 7), the process of formalization involves translating an informal proof into Isabelle's 's proof sketches. The formalizer employs the proposed request originating from the decomposer and the formal statement of the problem as query texts and, in total, retrieves ny skills. Upon collecting all the necessary input, the LLM is tasked 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 needs 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 more modular problem- wroblem-solvingg 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 tacties alongside the sledgehammer method to facilitate an auto-correction. The heuristic selection 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.
3.3 EVOLVER
The lemmas extracted from the prover are mostly problem-specific, rendering them non neu-reus 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. Algorithm 3 also illustrates the overall process for the evolver.
5

---

Published as a conference paper at ICLR 2024
Directional transformer. As shown in Table 1 column 3 (full example in Fig. 9). 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 trajec- tories: extension of dimensions, identification of key concepts, parameterization, and enhancement of complexity. Table. B shows the detailed functionality of each evolving direction. Each instance of the directional transformer adheres to unified prompt template depicted in Fig. 9. The adap- tation 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 directional transformer employs this skill to retrieve na relevant pending problem's formal statement from the problem vector store and the relevant request's 's formal statement from the request vector store. Upon assembling the inputs for the LLM,, the directional transformer arbitrarily selects one direction of cvolution and prompts the LLM to generate a novel skill.
The request solver is designed to facilitate the development of new skills by directly addressing the sub-goals proposed by the prover. As shown in Table. column 4 (full example in Fig. 8, the process initiated by the request solver involves the random selection of 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 retrieve pertinent skills that serve as in-context demonstration examples. Finally, the request solver prompts the L.LM to generate the proof for the request. should be noted that these requests, which are conjectures proposed by LLMs without verified proof, could potentially be incorrect. Only those conjectures that can be substantiated with valid proof are accepted by formal verifier. The challenge lies in the fact that determining the satisfiability of a conjecture, especially within complex mathematical theories, is an undecidable problem. Consequently, no purely symbolic method can guarantee the rejection of these incorrect conjectures. While conjectures with illegal syntax are straightforwardly rejected by the verifier, those that are semantically incorrect can only be incrementally dismissed after multiple unsuccessful attempts to prove them using LLMs.
Request solver.
After obtaining the new skill (evolved lemma or solved request) generated by the LLM, the evolver uses Isabelle to verify the generated code. To reduce redundancy in the skill library, we compare new skills against existing ones using the SequenceMa t cher method from Python's 's di f ll... Only skills that are verified and show difference below the threshold of 0.85 are added to the library.
4 EXPERIMENTS
4.1 EXPERIMENTAL SETUP
In this section, we introduce the experiment setup for LEGO-Prover. Consistent with the (Jiang al., 2022b; Zhao et al., 2023), each problem undergoes 100 attempts of proving using ChatGPT (GPT-3.5). More implementation details are provided in Appendix A.I.
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 that 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 AIME and IMO. The problems are divided into valid and test sets, with 244 problems each². LEGO-Prove employs the updated miniF2F dataset from (Jiang et al., 2022b), featuring questions with formal and informal statements, along with numan-written informal proofs.
Baseline methods. We have included basclines that represent state-of-the-ar neural theorem proving in Isabelle. Thor(Jiang et al., 2022a) and Thor with expert iteration on auto-formalizer data (Wu et al., 2022) are works focused on proof search paradigms, which use fine-tuned 700m language model to prove theorems. Draft, Sketch, and Prove (Jiang et al., 2022b) and Labgoal--earning (Zhao et al., 2023) are works that use Codex ChatGPT to prove theorems directly.
Following the setting from (Jiang et al., 2022b), we test the BEGO-Prover with model- -eder-ee and human-written informal proofs. The model-generated informal proofs are pre-generated using
$I TT.EGOPPron Prover does not require training, thus these two splits are treated identically, displaying separate results only for detailed comparisons with prior methods.

---

Published as a conference paper at ICLR 2024
Table 2: Proving success rates on the miniF2F dataset with Isabelle. The table displays the success rates of previous works and the LEGO-Prover, The highest success rates for each set are highlighted in bold. LEGO- Prover* denotes the cumulative pass rate the miniF2F datasct, considering the total number of problems solved using model-generated and human-wrilten informal proofs.
Success rate
LLM
miniF2F-valid
miniF2F-test
Baselines
Thor (Jiang et al., 2022a)
28.3%
29.9%
Thor expert iteration (Wu al., 2022)
Codex
37.3%
35.2%
Draft, sketch, and Prove (Jiang et al., 2022b)
Codex
42.6%
39.3%
Subgoal-Learingg (Zhao et al., 2023)
ChatGPT
48.0%
45.5%
Ours (100 attempts)
LEGO-Prower (model informal proof) ESGO-Prover (human informal proof) LEGO-Prover*
ChatGPT
52.0%
45.5%
ChatGPT
55.3%
50.0%
ChatGPT
57.0%
50.0%
Ablations (100 attempts)
Skill Library (human informal proof)
ChatGPT
50.4% (-..9%)
GPT-4, with up to 20 informal proofs per problem (12.13 on average). For each proving attempt, we randomly select one proof as the informal proof to feed into the decomposer procedure. For the ablation study, we remove the growing skill library to validate the effectiveness of the LEGO-Prover using numan-writter informal proofs, In this setup, the prover operates as usual, but we ignore the requests provided by the decomposer and supply an empty list of reference skills to the formalizer. As a result, the evolver is not utilized. Due to limited resources and the expense of OpenAl API calls", we perform ablation only on the miniF2F validation set.
4.2 MAIN RESULT
In Table. 2. we illustrate the proportion of successful formal proofs found on the miniF2F dataset. Our proposed LEGOOProver 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 numan-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- we are interested in how well it contributes solving more problems and improving the LLMs' ability. Specifically, we remove the growing skill library (including the evolver). As shown in the Table. 2, LEGO- achieves 55.3% on the validation set, whereas the LEGO-Prover without skill library achieves 50.4%. 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. 3(a). Compared to the problem solved without a growing skill library, the advantage of adding the skill library is initially minimal, the libraries library expands, the gap between LEGO-Prove and the ablation method widens consistently (the performance gap in 50 attempts is 3.3% which increases to 4.9% in 100 attempts). This outcome supports our hypothesis that the prover becomes increasingly adept at formalizing theorems as more skills are added the skill library.
still underdeveloped and lack useful skills. However, as the skill
4.3 ANALYSIS
4.3.1
WHAT DOES THE GROWING SKILL LIBRARY LOOK LIKE?
Figure. 3(c) illustrates an example of svill-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 's request solver sub-task (as the example shown in the figure), become
Estimated to be around 600 dollars for experiment with 100 proof attempts
7

---

Published as a conference paper at ICLR 2024
miniF2F-valid (human informal proof)
cumulaatus frequency ovalution pattarss
miniF2F-valid (human informal proof)
20
50
122-
#successful proofs
-44
aaatus in 10.0 12
200
10.0
10
of ummas by tation scalee complecty
direct use of ever stilss
82-
ootend dimorsions
isentityy
2b wilon ski ibrary LEGO Prover
number
0
20
80
100
20
80
100
tttttll prover attempts
ittotal prover attemppss
(a)
Forral statement
Thooren diaicion WARr
skill
you par "Caheel O1w (2
stous
and 1yn
tratt. 116221
the
proot
(astesl) luee 1272 1r Costact
flass 12 10
request
ced
old skill with
Hhee laee 1Ch,
Ortvents die
and 12 ogr 4 katurtitee
(a
Floes
12
bats for dis setre bau HE Tane, ramoraluee
thas lewade anta
cod
(hooren 1ns 190 in sotgerr
and
assano 1o "Bea Lourds Beg"
4 not Inteni
new SKil1
sheus *ra, 3, E.
(ar2arr: car (2oo221"
vasd-
craut
lak 1Jy be
sides (sie lee leas
tetgs Ib
altiaaiity here teroidi1" the towess by aa
the ihos lemads Jootia Dut Listen Liyk-
by lortic Menne)) rafrelation
Tess
by lectis mams end moweett
(ot toro
Jers
ex?
(c)
Figure 3: (a) A comparison of proof success rate between LEGO-Prote with and without the growing skill library. (b) Distribution of skill origins in successful proofs, shown against prover attempts and their percentage contributions to total successes. Solid lines represent the distribution of skill usage methods, while dotted lines detail the specific skill origins. (c) A skill-evolving tree gradually generated through multiple steps for imo 1988 p6 conceals how a relatively large-scale skill library is produced from a few seed theorems.
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 s solve request sub-task, and 51.1% % originating from the evolver's directional transformation sub-taske Although some lemmas generated by LEGO-Proves are trivial or already in Isabelle's 's theorem library, most are unique, interesting, and useful. The main challenge in futo-formalization lies in bridging the gap between natural and formal mathematical languages; simple step in natural language often translates to numerous lines in formal language. However, as more lemmas and theorems are accumulated, this gap narrows. Ultimately, IEGO-Prover's 's expanded skill library significantly contributes to bridging this divide
4.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. 4 left, wwgeerraaagg_aaaaaaee www.mffaiiirnmmsmomm 2eeq2mmm div2x directly
the final proof of the problem copies the retrieved skill am gm's 's code as part of the proof and uses this lemma to help prove the problem.
8

---

Published as a conference paper at ICLR 2024
retrieved skill
retrieved skill
Teams real
Leama Band
ki3 fact
shout "1a + 1//Cpx) > sart 2"
preoft tndure nf cuse
srout
"Iaert sart (2/12 2" simp
shov Tease by sims
thes base 1/CPes)
sgen sir (171Paa))
next
dividi reniesrran lesa_ss
real tef real sort rewd sie couares haund)
thas show Pease by (step atts al glgebia stepsi qrd
imstis statta
docbeut divase riggt si-
side self less niteral extrac31 extt one aot real die strt re-
ret "ealuggrtoss times_di-
synthesized proof
vide right zero (uteral)
ged
then 7ehanis
17C2ex sirt sieo
tiees and ascrenl
cosanso "a
ia KI)
preoffindzzt nn
synthesized proof
cosd
by step
next
assumes 8*
have *Ilk LoeSac n. Co k (a.a 1I1 ila Sac n of la Sic 103"
shous 3/12cs1 sqrt
n3) (Ik L.ch.
have "[sort cort (1/C2e0))32 9" by sipp
slss have (<o Suc e (a Soc all in 11"
(3/12sa1)
using by sing
1sat (verit) ol1, le diff assas divide norreg romnyy less_ot."
also have
1
roa rorl pon2 Sanusgarce 6 (ound)
usiing esama (xes (swrst) comuut add divsse dixteia divitors
then have
diw.rrooat.iiiiiie.... carccl o7. __t_ttt__ and ot,net _ee J plus, 1. right_ inver_e to time divide an, left)
by rottis add aiviie_diisraa ssors dic 1 divide ouiiit di-
Finally qud
oL sivide real L _art__ca
Le reaLart,or ti
vid. oaccourre ight zere sueorall
1/(Pks)
anc12o, -Ipeceeettl.. 180, (ffcoreat) a 4) (E 431 te0" preof
then show tihesss by slms
(a Stop 2: Revelts the piver protuct is syfrae (at cocttfoor (127687k deritrer (16)412) Veveetsytr
thesren aroctra faxiarrraaarrreerrrrro t2peopraattiii 1/
(Jeereeters LaM8)) 4]
[c00] prost
(14soreal) 14 331 kil
fixes 2:
Sioplify the prosuct by cancelang out conmon factors, Notice that each term in nuterator cancels with the corresgoneing tem the
(ndoes 1: Vo want to shov that 5x Vfraef3itze tees vagretals is er
sttraetl pet
slso here t... m 1f (iCciaane....00 it 17 (2005)14)s.
(frac 1964 2 (133 of
in Step simplaty (hserstttrecal (fract1322d)
suartt22ss true.
eva"
use Lanms
simplaty the product
have ett (200 (6/511 seb 18/5)*
blse have "axs a 581
ma sfract2adds cautvatent to
using Eooollie conel factorket rest by cutuuaaee
[- Step 51 Since "sarrE22 lges
(+
of sutrec (2003) fand that
(traell)i2s loes (2),
conctude that (agre(2) 1p93
exual $1825.
have
582"
tken show sert 2 12 + xl" by simp
by simp finalily 7therts
Conclude that the gliven product is equll to 55025, +]
and
(a) Directly Use
Propose Lemma by Imitation
Figure 4: Two primary forms of utilizing the skills: directly use or propose lemma by imitation
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. right, the retrieved skill examples prod 1n 4n provide great clues for solving the conjecture prod_ crro__fracccommc hommmon_factor..oomm 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. 3(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 (shown in the solid line). We examine manually to determine the skill evolution pattern of the lemmas used in the proofs (shown in the dotted line). 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 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.
5 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 L.M 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.
9

---

Published as a conference paper at ICLR 2024
ACKNOWLEDGEMENTS
This work was supported in part by the National Key R&D Program of China under Grant No. 2020AAA0109700, Guangdong Outstanding Youth Fund (Grant No. 2021B1515020061) National Natural Science Foundation of China (NSFC) under Grant No.61976233, Mobility Grant Award under Grant No. M-0461, Shenzhen Science and Technology Program (Grant No. Nansha Key RD Program under Grant No.2022ZD014, National Nat- ural Science Foundation of China (U2001211. U22B2060), Research Foundation of Science and Technology Plan Project of Guangzhou City (2023B01J0001, 2024BOI W0004), and National Natural Science Foundation of China under Grant No.62006255. We thank MindSpore for the partial support of this work, which is a new deep learning computing framework.
01120220091142200000
Xiaodan Liang is with the School of Intelligent Systems Engineering, Sun Yat-sen University at Shenzhen, Shenzhen 518107, China, and also with DarkMatter AI Research Guangzhou 51 1458, China.
REFERENCES
Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, and Josef Urban. Licensing the mizar mathematical library. In James H. Davenport, William M. Farmer, Josef Urban, and Florian Rabe (eds.), Intelligent Computer Mathematics 18th Symposium, Calculemus 201 I, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011 I. Proceedings, volume 6824 of Lecture Notes in Computer Science, pp. 163. Springer, 2011. doi: 10.1007/ 978-3-642-2288 11-11. URL https: /ww./iiioo////// org / 10. 1007/ 976 11.
642 22673-1
Alexander A. Alemi, François Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban. DeepMath deep sequence models for premise selection. In Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS' 16, pp. 2251-2251, Red Hook, NY, USA. December 2016. Curran Associates Inc. ISBN 978- 1-1108-3881-9
Jeremy Avigad. Mathematics and the formal turn. 2023. URL https: www. andrew. cmu. aet//user//avigad/aaaapa
pdf.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wileox. Holist: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of PMLR, 2019. URL http: http::tt/////et htttt::ppppocceeednieee mlr.
Machine Learning Research, pp. press/ v /bannaalllll 9a html.
Kshitij Bansal, Christian Szegedy, Markus Norman Rabe, Sarah M. Loos, and Viktor Toman. Learning to Reason in Large Theories without Imitation. September 2020. URL htttp:://opeeeeeeeeeee
net/ forum? wttp:uummidioooldeeeoemmm k2AHH.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Ed- uardo Giménez, Hugo Herbelin, Gérard Huet, César Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq Proof Assistant Reference Manual Version 1. report, INRIA, May 1997. URL https: happs///hale //hhhhaaaa. inria. fr/ Anria-0006990 Pages: 214. 3
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovié, Tim King, Andrew Reynolds, and Cesare Tinelli. Cvc4. In Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 201 Proceedings 23, pp. 171-177.
Springer, 2011.
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović. Superposition for Full Higher-order Logic. In André Platzer and Geoff Sutcliffe (eds.), Automated Deduction CADE 28, Lecture Notes in Computer Science, pp. 396-412, Cham, 2021. Springer International Publishing. ISBN 978-3-030--78876655 doi: 10. 10.11077978833-00777777----5-
"hnp://wwww.inddpor..nl
10

---

Published as a conference paper at ICLR 2024
Garrett Birkhoff. Rings of sets. Duke Mathematical Journal, (3):443 454,, 1937.
Rishi Bommasani, Drew A. Hudson, Ehsan Adeli, Russ Altman, Simran Arora, Sydney von Arx, and et al. Bernstein, Michael S. On the Opportunities and Risks of Foundation Models. Technical Re- port TrtXivv2108.07255 arXiv, August 2021. URL http: aawairivvvv...m.a .rgg wttp://///ab//1..00255553535 07258. arXiv:2108.0728 07.25
[es] type: article.
Tom Brown, Benjamin Mann, Nick Ryder, Melanic Subbiah, Jared D Kaplan, and Prafulla al. Dhariwal. Language Models are Few-Shot Learners. In H. Larochelle, M. Ranzato, R. Hadsell, M. Balcan, and H. Lin (eds.), Advances Neural Information Processing Systems, volume 33, pp. 1877-1901. Curran Associates, Inc., 2020. URL https: http://pooeeediggg.e.eee neurips. pdf.
96741 Bbfbbac1442664-222000
Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, Harsha Nori, Hamid Palangi, Marco Tulio Ribeiro, and Yi Zhang. Sparks of artificial general intelligence: Early experiments with gpt-4, 2023.
Aydar Bulatov, Yuri Kuratov, and Mikhail S. Burtsev. Recurrent memory transformer, 2022.
Aydar Bulatov, Yuri Kuratov, and Mikhail S. Burtsev. Scaling transformer 1m tokens and beyond with rmt, 2023.
Kevin Buzzard. Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. CoRR, 0bs//910.12330 2019, URL http: /ttttp:/aaxiie //tpxaaaivvvv//a///aa/eaeeaawava org/ abs/1910. 12320.
Tianle Cai, Xuezhi Wang, Tengyu Ma, Xinyun Chen, and Denny Zhou. Large language models as tool makers. arXiv preprint arXiv:2305. 17126, 2023. 3
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé Oliveira Pinto, Jared Kaplan, and et al. Harrison Edwards. Evaluating large language models trained code. CoRR, abs/2107.03374 033374, 2021. URL https: //axxaaivv./..///////.aa/.aaaav/ org/ abs/ 221/21117..333
Noam Chomsky. Three models for the description of language. IRE Transactions on information theory, 2(3):113-122 1956.
Thierry Coquand and Gérard Huet. The calculus of constructions. PhD thesis, INRIA, 1986.
Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76
(2):95-122) February 1988. ISSN 0890-5401. doi: 101101660590-5440083390000000000 URL https: //www www.ssciiiieeeccccmm com http:///ee//.rrraaaaa///////////
Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints (eds.), COLOG-88, Lecture Notes in Computer Science, pp. 50-66, Berlin, Heidelberg, 1990. Springer. ISBN 978-3-540-46963-6. doi: 10.100770-540-5233--9111
Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the solution the cap set problem. In John Harrison, John O'Leary, and Andrew Tolmach (eds.). 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPlcs, pp. 15:1-15:18 Schloss Dagstuhl- Leibniz-Zentrum für Informatik, URL https://///// /wwi www.ooogo/.......... 4030/41100IIISS ITP.
2019, doi: 00.42300LPP(cs.ITP.00199 2019.15
Giannis Daras and Alexandros G. Dimakis. Discovering the Hidden Vocabulary of DALLE-2. Technical Report arXiv:2206.00166 arXiv, May 2022. URL http::/arxiv..tt wrg.:/ooorrrroooo abs// 2206. 00169. arXiv:2206.00166
[cs] type: article.
Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving.
Communications of the ACM, 5(7):394-397, 1962. ISSN 0001-0782. doi: 10. 10.11457362233366555.
URL htt.:::://ool.oooo100111////////
368557.
Leonardo De Moura and Nikolaj Bjøreer. Z3: An efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference Tools and Algorithms for the Construction and Analysis of Systems, 0S/ETAPSS 08, pp. 337-340, Berlin, Heidelberg. 2008. Spring.r-Verlag. ISBN 3540787992.
11

---

Published as a conference paper at ICLR 2024
Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In C. R. Ramakrishnan and Jakob Rehof (eds.), Tools and Algorithmss for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pp. 337-340, Berlin, Heidelberg, 2008. Springer. ISBN 978-3-540-78800-3. doi: 10. 10.107778--3-4000 500---000---------33 24.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction CADE-25, Lecture Notes in Computer Science, pp. 378-388, Cham, 2015. Springer International Publishing. ISBN 978-3--19-211401-6 doi: 10. 111100/9778-3331-21140011 1,3
Jacob Devlin, Ming- Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: pre-training of deep bidirectional transformers for language understanding. In Jill Burstein, Christy Doran, and Thamar Solorio (eds.), Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT 2019, Minneapolis, MN, USA, June 2-7, 2019, Volume (Long and Short Papers), pp. 4171- doi: 10.18653/v1/n19-111 1423. URL
4186. Association for Computational Linguistics, 2019.
https: /doi /tw//o.g..oo..oo. 1e.....663///11nln
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metapro- gramming framework for formal verification. Proc. ACM Program. Lang., 1(CFP)), aug 2017. doi: 10.1145/3110278 URL https: http//ii.oogg//////////o 1tt..//////111//111101011111
Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sable-Meyer, Luc Cary, Lucas Morales, Luke Hewitt, Armando Solar-Lezama, and Joshua B. Tenenbaum. Dreamcoder: Growing generalizable, interpretable knowledge with wake-sleep bayesian program learning, 2020.
Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. CoRR, abs/2303.04910, 2023. doi: 14485500/rxx1.22333.099900 URL https: / doi. org/o//g//oooo. /10. 485544555//// art.vv 2303. 1, 2,
Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy. The Pile: An 800gb dataset of diverse text for language modeling. arXiv preprint arXiv:2101.00022 2020.
Vijay K. Garg. Introduction Lattice Theory with Computer Science Applications. Wiley Publishing, 1st edition, 2015. ISBN 1118914376.
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning reason with HOL4 tactics. In Thomas Eiter and David Sands (eds.), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Maun, Botswana, May 7-12, 2017, volume 46 of EPiC Series in Computing, pp. 143. EasyChair, 2017. doi: 10.29007/ntlb. URL https: //wii./.../////////.../ orggiorgg/aa. 290002900010 /t..b.
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, and Matías Steinberg. The independence of the continuum hypothesis in isabelle/zf. Arch. Formal Proofs, 2022, 2022. URL https:
//www. iss- www.:a.p................a......a httpp/.rggeetteree/eeeeee/ htt.rriieesenddeeeeeennneeeeeee
html.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof Artifact Co-training for Theorem Proving with Language Models. ICLR 2022, February 2021. URL pttt:://arxia org/ /ag/abb////aaa / 22222.002.22 0 06203. arXiv: 2102.06203.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL https:////// wwtp///pweeeeeeoe/ooppp/p. net forum? id=rppdc JU4 1, 2,
John Harrison. HOL light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (eds.), Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pp. 60-66. 66. Springer, 2009. doi: 10.10077998-33642-0583 https: http:://ooioooo .org/10 /0. 1007 000000077777000 642- 0222203399--2
9 4. URL
12

---

Published as a conference paper at ICLR 2024
John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Jörg H. Siekmann (ed.), Computational Logic, volume 9 Handbook of the History of Logic, pp. 135-214. Elsevier, 2014a. doi: 112-111668897804444--1100 4.500404 URL httpt:://ci..oooet
101 6//6///9720 78 0- 44 51 624 4 - 50004-6.
John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Computa- tional Logic, volume 9, pp. 135-214, 2014b.
John Harrison, Josef Urban, and Freek Wiedijk. History of Interactive Theorem Proving. In Handbook of the History of Logic, volume 9, pp. 135-214. Elsevier, 2014c. ISBN 978-0-444-51624 URL https: //1 /tts:://nnniiiiii wwwiiiinnnhhhh el elsevier.
4. doi: 10. 0.1006/99766-0444-1104444440 hatmm//etrrieeeee//////3664--611
Chadi Helwe, Chloe Clavel, and Fabian Suchanek. Reasoning with Transformer- -aasdd Models: Deep Learning, but Shallow Reasoning. Deep Learning, pp. 28.
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt, Measuring mathematical problem solving with the math dataset, 2021."
William Alvin Howard. The Formulac-ass Types Notion of Construction. In Haskell Curry, Hindley B, Seldin J. Roger, and P. Jonathan (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.
Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Lingi Song, and Xiaodan Liang. Mustard: Mastering uniform synthesis of theorem and proof data, 2024.
Geoffrey Jefferson. The mind of mechanical man. British Medical Journal, 1(4616): 1949.
Ziwei Ji, Nayeon Lee, Rita Frieske, Tiezheng Yu, Dan Su, Yan Xu, Etsuko Ishii, Yejin Bang, Andrea Madotto, and Pascale Fung. Survey of hallucination in natural language generation. CoRR, abs/2202.03629, 2022. URL https:://////
attpp:://axxv... /ttp//aaxvvv..///////////...a org/ haagg//bs// aba//2b22/22// 03629.
Albert Q Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóádš, Piotr Mitoš, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. arXiv preprint 22X.::2205.1892 2022a. 1, 3, 6,
Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothéc Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. CoRR, abs/2210. 12283, 2022b. doi: 10.48550k/rXiv.221100 12283. URL httph:tpp/// http://ooooooroooo orgg10 48550/ /wt.vvarivvvv...v 2210 12283. 1, 2, 3, 6, 7, 20, 21, 22
Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of
isabelle proofs. 2021. 1, 18
Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large Language Models are Zero-Shot Reasoners. Technical Report arXiv:2205. 11916, arXiv, May 2022. URL http: /tw.ivaiiviv/v.////vv//.../aaaaa org/ abs 11916. arXiv:2205. 11916 [cs] type: article.
Laura Kovács and Andrei Voronkov. First-Order Theorem Proving and Vampire. In Natasha Sharygina and Helmut Veith (eds.), Computer Aided Verification, Lecture Notes in Computer Science, pp. 1-35, Berlin, Heidelberg, 2013. Springer. ISBN 978-3-642-39799988 doi: 10.1007/ 978-3-642-39799-88
Guillaume Lample and François Charton. Deep Learning for Symbolic Mathematics. wwtpw/wwwwwww./////....//
arXiv:1912.01411 [cs], December 2019. URL
arXiv: 1912.01412.
Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. HyperTree Proof Search for Neural Theorem Proving. Technical Report arXiv:2205.11 1491, arXiv, May 2022. URL http: / wawpi..xooooo/..... [es] type: article. 1,
11491, arXiv:2205.1 11491
13

---

Published as a conference paper at ICLR 2024
Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. Deep learning. Nature, 521(7553):436 444, May 2015. ISSN 1476-4687. doi: 10.1038/nature 14539. URL https: /www.... nature com/ Number: 7553 Publisher: Nature Publishing Group.
Mike Lewis, Yinhan Liu, Naman Goyal, Marjan Ghazvininejad, Abdelrahman Mohamed, Omer Levy, Ves Stoyanov, and Luke Zettlemoyer. Bart: Denoising sequence-to sowuennceto-sqqueeee -o-seuennce pre-training for natural language generation, translation, and comprehension, 2019.
Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Soke Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. In NeurlPS, 2022. URL http: / nips ec wppppperpppppppeeeeepeeeeeee.eee files/ /paprr/ 2022 httt://aaa//abbeeeeeeeeeeeeeeeee html.
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. IsarStep: a Benchmark for High-level Mathematical Reasoning. In ICLR 2021, September 2020. URL https: /ttp//eeeeeeeeeeee////e/e/ net/
Corum?id=Pan 6622266k26
Yujia Li, David Choi, Junyoung Chung, Nate Kushman, and et al. Schrittwieser. Competition-
Level Code Generation with AlphaCode. arXiv:2203.07814 [cs], February 2022. htth:
//arxiv. org/ aba /203 07814. arXiv: 2203.07814.
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:23309.44200 2023.
Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zeutlemoyer and Veselin Stoyanov. Roberta: A robustly optimized BERT pretraining approach. CoRR, abs/1907. 1692, 2019, URL http:
abs / 1907. 11 19692.
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In Thomas Eiter and David Sands (eds.), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPiC Series in Computing, pp. 85-105. EasyChair, 2017. doi: 10,29007/8mwc. URL https: / //w.i .rrg/ 100. 29007/ 8mwc.
Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, and Dongmei Zhang. WazardMath: Empowering Mathematical Reasoning for Large Language Models via Reinforced Evol-Instruct, August 2023. URL http:
//axxiv.org/able. /230 09583. trXiv:2308.09588 [cs].
Carlin MacKenzie, Jacquee D. Fleuriot, and James Vaughan. An evaluation of the archive of formal proofs. CoRR, abs/2104.01052, 2021. URL https: http::///axxvv.oooo/e
21 04. 01052.
The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp- 367-381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 978- 978-1-4503-709744 doi: 1141/
3372885.3373824 URL https: : /oii. wot.orgg///oo /10 1ee.1111533238 /tt.//333728888333222 3373824.
John McCarthy, Marvin L Minsky, Nathaniel Rochester, and Claude E Shannon. A proposal for the dartmouth summer research project artificial intelligence, august 31, 1955. Al magazine, 27(4): 12-12, 2006.
Norman Megill and David A Wheeler, Metamath: computer language for mathematical proofs. Lulu Press, 2019, ISBN 978-0-359-70223-7, OCLC: 1105224041.
Maciej
Mikula, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Fukasz Kuciński, Piotr Mitos, and Yuhuai Wu. Magnushammer: A transformer- based approach to premise selection. arXiv preprint arXiv:2303.04488, 2023.
Yutaka Nagashima, Zijin Xu, Ningli Wang, Daniel Sebastian Goc, and James Bang. Template-basel conjecturing for automated induction in isabelle/hol, 2023. 3
14

---

Published as a conference paper at ICLR 2024
OpenAL. GPT-4 technical report. CoRR, abs/2303.08877, 2023. doi: 10.48550a2X1..2200.87774 URL httph:://///. / doii http///....0////.............o.. wwt./////.............
Joon Sung Park, Joseph C. O'Brien, Carrie J. Cai, Meredith Ringel Morris, Percy Liang, and Michael S. Bernstein. Generative agents: Interactive simulacra of human behavior, 2023.
Lawrence C. Paulson. Isabelle Generic Theorem Prover. Springer Verlag, 1994. 1,3
Stanislas Polu and Lya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.0333 003933, 2020a. URL www.h:tpp//// http://axvvvvvoo org/ aat//bb////00 03393. 2,3
Stanislas Polu and lya Sutskever. Generative Language Modeling for Automated Theorem Prov- ing. arXiv:2009.00 00339 [cs, stat], September 2020b. URL http::://wwww..o////////////////
03393. arxiv: 2009.03393.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever, Formal Mathematics Statement Curriculum Learning. (arXiv:2202.013444) Februaa 2022. doi: 10.48550/arX1v22222.00 arXiv:2202.01344 [cs]
URL http::/arxiv..rrgg/// 22000///0/////////aa/o/////////0 01344.
type: article. 2,
Jianing Qiu, Lin Li, Jiankai Sun, Jiachuan Peng, Peilun Shi, Ruiyang Zhang, Yinzhao Dong. Kyle Lam, Frank P-W Lo, Bo Xiao, et. Large ai models health informatics: Applications, challenges,,, and the future. arXiv preprint arXiv:2303. 11568, 2023.
Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy, Mathematical Reasoning via Self-supervised Skip-tree tree Training. September 2020. URL https: / openreview net/ forum? Ya
Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https:// openreview net/ forum iid-imgnnooCMEE
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and llya Sutskever. Language Models are Unsupervised Multitask Learners, pp. 24.
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Πlya Sutskever. Lan- guage models unsupervised multitask learners. 8018a. URL https: : / //d./mmmmcsyyyw
moc.eeeeeooeeeeee ls/ htter/eemmmeea//aaaaaeeeeeeeee - .ddf.
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Lan-
guage models are unsupervised multitask leamners. 2018b. URL https: /ttptttp::///mmeeppppe fpksyww...
htw.ffooontnee//eteeerr... -anguage - lagggggaaggaooeeaaagaaaaggggg-ee moddelll...ooooo pdf.
Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J. Liu. Exploring the limits of transfer learning with a unified text-to-text transformer, 2020.
Scott Reed, Konrad Zolna, Emilio Parisotto, Sergio Gomez Colmenarejo, and et al. Novikov, Alexander. Generalist Agent. Technical Report arXiv:2205.0611 .0615,, arXiv, May 2022. URL httt:///rxxie org/ abs
abs 2205 06175. arXiv:2205.06117 [es] type: article.
Alexandre Riazanov and Andrei Voronkov. The design and implementation of vampire. Al communi- cations, (1123))91-1100 2002.
J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1):23 41, 1965. ISSN 0004-5411. doi: 10.1145/321250.321225 URL htRLhtsss///o..ooo 10. /2224////2200 321212.....122......
Stephan Schulz. E brainiac theorem prover. Al Communications, 15(2.3):111-126 August 2002. ISSN 0921-7126.
Yongliang Shen, Kaitao Song, Xu Tan, Dongsheng Li, Weiming Lu, and Yueting Zhuang. Hugginggpt: Solving ai tasks with chatgpt and its friends in hugging face, 2023.
15

---

Published as a conference paper at ICLR 2024
David Silver, Aja Huang, Chris J. Maddison, and et al. Guez. Mastering the game of Go with deep neural networks and tree search. Nature, 529(7587):484 489, January 2016. ISSN 1476-4687. doi: (tt1038//attre169990 URL https: //www/wwwww nature com/ Publisher: Nature Publishing Group.
Number: 7587
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanetot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, Timothy Lillicrap, Karen Simonyan, and Demis Hassabis. Mastering Chess and Shogi by Self-Play with General Reinforcement Learning Algorithm. arXiv:1712.01815 [cs], December 2017. URL http:://axk: org/ abs//ss/...... 1712 01815.
arXiv: 1712.01815.
Hugo Touvron, Thibaut Lavril, Gautier Izacard. Xavier Martinet, Marie-Anne Lachaux, Timothée Lacroix, Baptiste Rozière, Naman Goyal, Eric Hambro, Faisal Azhar, Aurelien Rodriguez, Armand Joulin, Edouard Grave, and Guillaume Lample. LLaMA: Open and Efficient Foundation Language Models, February 2023a. BRLLttp:/// http://axxxxxi..g.. [cs].
13971. arXiv:2302.13977
Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, and et al. Babaci, Yasmine. Llama 2: Open Foundation and Fine-Tuned Chat Models, July 2023b. URL http:
//arxiv. org/ abs 20los/2300 2307. 09288. arXiv:2307.0928, [cs].
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (eds.), Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp. 5998-6008, 2017. URL https: http::/://////ceeeeeeee mew.eediiiinnnnnnner..eee neurips. cc htpppaape//////ee//// 2017 /hash/ 3f5ee2435 dee www.ddddddlcccccco 10d00 Abstract. html.
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: Arxiv-2305. 16.-991,...,,,,, 2023a.
Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et al. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the 61st Anmual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). pp. 12646, 2023b. 1, 2,
Mingzhe Wang and Jia Deng. Learning to Prove Theorems by Learning to Generate Theorems. In Advances in Neural Information Processing Systems, volume 33, pp. 18146-18157. Curran As- sociates, Inc., 2020. URL hwwpt:tt///cc /tppttpe:/pprooeeeeeee ngs neurips. pctpppaper///////aaaaaaaa h2sh//ash0////////// d2a27e83d40 9 F0wcae669377c.444ee0coo -bbtt4aarabbbbaaaaa...bb. html.
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11, pp. 255-270. Springer, 2018
Zhenhailong Wang, Shaoguang Mao, Wenshan Wu, Tao Ge, Furu Wei, and Heng Ji. Unleashing cognitive synergy in large language models: A task-solving agent through multi-persona self- collaboration, 2023c.
Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. Spass version 3.5. Renate A. Schmidt (ed.), Automated Deduction CADE-22, pp. 140-145, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. ISBN 978 978-3-642-02959-2.
Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR. 2016a. 2016, URL http:// / ///////aa /aaxiviiiiv//////i///aaa////aaiv o abs / 1608 02644.
Daniel Whalen. Holophrasm: neural Automated Theorem Prover for higher-order logic. Technical Report arXiv:1608. 02644,, arXiv, August 2016b. URL http: aawai.iii.v.//../ org/ wwg/abs/////eoooooooo/......aaaa 1608. 02.44, 4. arXiv: 12640044000264 [cs] type: article.
16

---

Published as a conference paper at ICLR 2024
Wikipedia contributors. Recursion (computer science) Wikipedia, the free encyclope- dia, 2023. URL https: //e..///nnnn www.wewia..iaoo..............a.. org/ w/ innex. Sawpptttteeeeesssiiii coomuteer_scienee (ol.:/enieeoooodl1111111d1dd0 6oldid=114343133 [Online; accessed 14-May-2023J.
Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, and Roger Grosse. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. ICLR 2021, April 2021. URL http: //axxiv. arXiv: 2007.02922
org/abs/ 2007. 02924.
Yuhuai Wu, Albert Qiaochu Jiang. Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353-32368, 2022. 3, 6,
Jing Xiong, Chengming Li, Min Yang, Xiping Hu, and Bin Hu. Expression syntax information bottleneck for math word problems. In Enrique Amigó, Pablo Castells, Julio Gonzalo, Ben Carterette, J. Shane Culpepper, and Gabriella Kazai (eds.), SIGIR '22: The 45th International ACM SIGIR Conference on Research and Development Information Retrieval, Madrid, Spain, July 11 15, 2022, pp. 2166 2171. ACM, 2022. doi: 10.1 00.114//7777495333188888 URL https: //doi. owg/ 10. 1145 /4445//4479995 3531824.
Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, and Qun Liu. Trigo: Benchmarking formal mathematical proof reduction for generative language models, 2023.
Jing Xiong, Zixuan Li, Chuanyang Zheng, Zhijiang Guo, Yichun Yin, Enze Xie, Zhicheng Yang, Qingxing Cao, Haiming Wang, Xiongwei Han, Jing Tang, Chengming Li, and Xiaodan Liang. Dq-lore: Dual queries with low rank upproximation re-ranking for in-context learning, 2024. 1
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp. 6984 6994. PMLR, 2019. URL http::/ppa httt:://prceeeding mlr. press/ v97 //a//yangggll 9a. html.
Kaiyu Yang, Aidan M Swope. Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with -aggeeel- language models. arXiv preprint arXiv:2306. 15626, 2023. 1,2
Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T. Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models, 2023.
Zahra Zahedi and Subbarao Kambhampati. Human-ai symbiosis: A survey of current approaches, 2021.
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demon- stration learning for formal theorem proving. arXiv preprint TrXiv:2305.16366 2023. 1, 2, 3, 5, 7, 20, 22
Chuanyang Zheng. Zhengying Liu, Enze Xie, Zhenguo Li, and Yu Progressive-hing prompting improves reasoning in large language models. arXiv preprint arXiv:2304.09797, 2023a.
Chuanyang Zheng, 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, 2023b. 21, 22
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: cross-system benchmark for formal Olympiad-leve mathematics. September 2021. URL https: http///eee/eeeeeee//e/ee/ / forum? id--dd9-0 wedddgg9Ppgpaae FereeeFFFFT IFV.. 3,
17

---

Published as a conference paper at ICLR 2024
A MORE DETAILS ON LEGO-PROVER
A. IMPLEMENTATION DETAILS
To expedite the experimental procedure, both the prover and the evolver are executed in multi- processing manner, maintaining process number ratio of 3 8 respectively. In order 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. 6 The temperature 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 ny is set to for the valid set and 4 for the test and paired with 2 formalization in-context examples. For the directional transformer, the number of reference problem statements nd is set to 4, supplemented by two directional transformation in-context examples. For the request solver, skills retrieved for forming the in-context demonstration examples.
For interacting with the Isabelle theorem prover, employ the PISA environment (Jiang al., 2021). PISA is a flexible Python REPI. wrapper for Isabelle, capable of verifying Isabelle's code and providing information such as proof states or error messages from Isabelle. We consider formalized proof valid if and only if (a) the proof does not contain "cheating" keywords (sorry or oops) that exit proof without completing it. (b) Isabelle can verify the proof code containing the corresponding formal statement.
A.2 ALGORITHM DESCRIPTION
In this section, the pscudo-code for our proposed LEGO-Prover presented. Initially, the main process of LEGOO-rovee is introduced in Algorithm I, followed by detailed descriptions of the prover process in Algorithm 2, and the evolver process in Algorithm 3.
LEGO Prover main process. Algorithm details the parallel execution of provers and evolvers in the main process. The algorithm begins by taking the miniF2F dataset as imput, which comprises 244 problems per split, each featuring an informal statement, informal proof, and formal statement. Lines 2-5 initialize three vector stores using ChromaDR, a vector database. The mp Queue intro- duced in line 6 is Python multiprocessing queue, facilitating synchronization of queue elements across different processes. Each problem is replicated n.at n.attempts s __errr__________ per.problen times and added the miniF22 Quuuee. Lines 8- 13 launch n.prover prover processes and n_evolver evolver processes.
Algorithm LEGO-Prover main process
1: Input: miniF2FData (containing 244 problems, each with informal statement, informal proof, and formal statement)
2: Initialize:
3: LemmaS <- ChromaDBO) //1emma vector stere, initially empty
4: RequestS ChromaDBO //request vector store, initially empty
5: ProblemS + ChromaDB(minif2FDDa)
/ //problen. vector store, initialized with miniF2F problem formal statements.
6: miniF2FQueue t- QupuuuuueemmiiFFFaaaa x settempts.pe..pooleen //share queue
7: Begin Parallel Execution
8: For i = to n.pprover
9: Start Process: prover(Lemmaa, RequestS, miniF2FQueue)
10:
End For
11: For j = 1 to n_evolver
12: Start Process: evolver(LemmaS, RequestS, ProblemS)
13: End For
14:
End Parallel Execution
A combination of gpt-3.5-turbo, gpt-3.5-turho-0300 apt-3.5-turbo-0611, gpt-3.5-turbo- 16llb and gpt-3.5- turbo-16k 16k-0613 is employed, with model being selected randomly during calls to the OpenAl API.
18

---

Published as a conference paper at ICLR 2024
Algorithm 2 Prover process
1: Function prover(Lemmas, RequestS, miniF2FQueue)
2: while minir22Queue not empty do
3: //infstmt, infProof, formštmt are abbreviations for informal statement, informal proot, and formal statement
4: infStmt, infProof, formStmt miniF2FQueue.popp
5: / //Use informal solver to preduce model informal proof
6: if model informal proof required then
7: infProof + InformalSolver(nnSSmm))
8: end if
9: / //cecomposer generate strucal step-by-step informal proof and 1enma statements as requests.
10: strucIn/Proof, lemmaRequests +- Decomposer(infSmt, infProof, formStmt) / //add request to request vector store and retrieve relevant 1eria from 1mmma vect.or store
12:
SqquessS.adds(mmmRRqquusss. ini_updatte.contt-)) retrievedLemmas +
13:
14:
/ /fooraalizz generate complete proof code
15:
proofCode t- FormalizerinnSStmt, strucInfProof, formStmt, retrievedLeemmas)
16:
//Isabelle theorem prover verify the proof code and return
proofResult (true/false), correct lemmas and failed lemma's statement as new request
proofResult, correctLemmas, newRequests + Iaablllfaav.eeriyypooooCooe)) RequestS RequestS.addssneewReee adds(new init update count=0) LemmaS. addec init update count=0) end while
18:
20:
21:
End Function
Prover process. Algorithm outlines the prover process. The prover employs the functions Decomposer (line 10) and Formal izer (line 15), which are LLM wrapper functions. These functions sequentially build the prompt text by filling the placeholders, query the LLM, and parse its output. Back to the algorithm, each instance of the prover process continually retrieves unsolved miniF2F problems from miniF22 FfFF2Fuuuue Queue (line 2). Specifically, the prover extracts the informal statement, the human-written informal proof, and the formal statement from the problem data. In lines 6-8, the InformalSolver generates the informal proof if required". In lines 10-13, the Decomposer used to create step-by-step structural informal proof and to generate lemma requests. These requests are first added to the request vector store and later utilized to retrieve corresponding lemmas from the lemma vector store. In lines 15-19, the Formal zer produces the proof code, which is then verified by the Isabelle theorem prover. Correct lemmas are added the lemma vector store with their initial update counts set to zero. For lemmas that fail verification, their proof code is removed, and their statements are added to the request vector store.
Evolver process. Algorithm describes the evolver process. The evolver runs parallelly with the prover and runs continuously until the prover completes all proving tasks. Similar to the Decomposer and Formalis zer, both DirectionalTrans former and Request LLM wrappers. Back to the algorithm, in each iteration, the evolver initially randomly selects an evolving type between Di rxreciiinnll
Trans former and Request. Solver (line 3). Lines 4-14 describe the overall pipeline of directional transformer. Specifically, when Directi on Transformes is chosen, the evolver randomly picks one of four transformation types. In lines 7-12, lemma with the lowest update count is selected from the lemma vector store, and its update count is then incremented. The evolver uses this lemma to query the request and problem vector stores for relevant problems. In line 14, the Direct Lon.lTransssss.ooooo former queries the LLM to transform the selected lemma into new one. Lines 16-22 showease the pipeline for the request solver. In lines 17-20, if the Request Solver ver selected, the process begins by choosing the least updated request from the request vector store and incrementing its update count. This request is then used to query for relevant lemmas. The RequestSolvee prompts the LLM to address the
As descrihed in Sec. 4.1, Baseline method, in practice, the pre-generated model informal proof used.
19

---

Published as a conference paper at ICLR 2024
request. In lines 25-27, the Isabelle theorem prover verifies the generated lemma code, and if correct, is added to the lemma vector store.
Algorithm 3 Evolver process
1: Function evolver(LemmaS, RequestS, ProblemS)
2: while TRUE do
3: evolving' yppe <- caaaloom.choiceeeDDeeeeee
Transformer', 'Request Solver'))
4: if evolvingType == 'Directional Transformer' then
5:
transType <- Random chonnnccccoiie(ddeiiffff Identify key concepts', 'Parameterize', 'Scale complexity', "Extend dimensions")
6:
//get lemma in emmma vector store with least update counts. selectedLemma <- L gettccsttpdaaee()
7:
8:
the update count of the selected Lemma LemmaS. wwt.saaaCoooomseeeeeelllc.cccmm //retrieve relevant requests and problens from RequestS and ProblemS that the lemma may help to solve
//add
9:
10:
relRequest ReequssS.retiieeeKWWWeeeeee.
12:
relProblems + //ask Directional Fransformes to transform the 1emma Type, relRequest, relProblems, select-
14:
newLemma +-
edI.emma)
15:
else
16:
//get a request in request vector store with least update counts. selectedRequest (
17:
18:
//add one to the update count of the seiected request Requesss..dattCCnnsssleeellllll relLemmas t CenmmmSSSrriiie&&KWeeeeeeeeRRee //ask request solver solve the lemma
19:
20:
21:
22:
newLemma +- RequestSolver(elleemmaaa selectedRequest)
end if
24:
/ //errity the newLemma code with isabelle
proofResult <- waabeellEEww.eefffyypoooCCCc
26: if esoofResult = TRUE then
27:
LemmaS adds(nwwLemma, init.update.count-)) end if
28:
29:
end while
30:
End Function
A.3 COMPUTATIONAL. COST
In this section, we examine the computational costs associated with our proposed LEGO-Prover. Unlike previous methods such Draft, Sketch, Prove (Jiang al., 2022b) and Subgoal-based Learning (Zhao et al., 2023), LEGO-Prover employs an additional skill library and an accompanying evolver to facilitate theorem proving. pertinent question arises regarding the extra computational resources required to construct, maintain, and update this skill library through the evolver. Rather than measuring computational cost based on the number of LLM calls, assess it by evaluating the number of tokens consumed in LEGO-Prove for more precise estimate. This is done by empirically calculating the average tokens used by both the prover and the evolver across all four experiments, which include the test and validation sets for LEGO-Prover with both model-generated and human-written informal proofs.
On average, for a single experiment on the miniF2F test/valid set, the prover consumes 131 million tokens and the evolver consumes 117 million tokens. This results a token consumption ratio of 1 : 0.89 for the prover to the evolver. As shown in Table 2, LEGO-Prove outperforms the version without the library by 4.9%. This leads to a question: how well would the prover perform the additional computational resources allocated to the evolver proving with the prover only? Given that the token consumption of the prover and the evolver is approximately 1:1, allowed the ablation setup continue proving for an additional 100 attempts.
instead used to continue theorem
20

---

Published as a conference paper at ICLR 2024
min mn-vaai- (human informal proof)
55
20
10
53.2%
120
16
#succescful proets
42:156
14
#Skils library [x]07
100
80
60
ablation: skill library number of skilb
40
25
50
75
100
125
150
175
200
#tocal prover atsempts
Figure 5: Ablation performance on balanced computational cost. We extended our ablation setup to include additional 100 proof attempts. Despite this limitation, our proposed LEGO-Prover continued outperform the ablation setup, achieving 2.1 higher success rate within the same computational budget constraints. The rightmost vertical line indicates the balanced computational cost between the LEGO-Prrved and the ablation setup (189 proving attempts).
This approach balances the computational costs between LEGO-Provee and LEGO-Prover without the skill library. As illustrated in Fig. 5, LEGO-Prover without skill library achieves 53.2% pass rate after 189 prove attempts, which is 2.1% lower than that EGG-Prover with the skill library in just 100 prove attempts. This highlights the efficiency of our proposed method, even with balanced computational budget. The ablation setup achieves 53.6% at 200 proving attempts in the end.
Although LEGO-Prover outperforms its variant without the skill library when computation costs balanced, the extra tokens consumed by the evolver still constitute a significant portion of the total computation. This cost accumulates due to several factors: 1) Limitations of the LLM's capabilities. The LLM struggles to produce correct proofs, with the evolver's average proof success rate being only 24.1% 1%. Moreover, the evolver might generate proofs that are either trivial or too similar to existing lemmas in the library. After filtering, average of only 9.1 % of the generated proofs are added the lemma vector store. 2) The task extracting useful lemmas applicable to other problems is challenging. Identifying useful and non-trivial common lemmas for specific problem set is difficult, even for humans. The LLM often yields lemmas that are either overly trivial or too specific, lacking generality. 3) Characteristics of the dataset. The miniF2F dataset, comprising only 488 problems, includes many that are simple enough to solve without additional lemmas. Others may require unique solving techniques, not sharing common intermediate lemmas. Future work focusing on improving the performance of the directional transformer, the accuracy of the request solver, and retrieval efficiency presents promising avenues reduce these additional computational costs
A.4 MORE BASELINE COMPARISON
Lyra (Zheng et al., 2023b) extends DSP (Jiang al., 2022b) with GPT-4's auto-correction ability, prompting GPT-4 to revise the formal proof based on eгror messages produced by Isabelle. To evaluate how well our method performs human-infoon -omarninformml proof, we compared LEGO-Proves with Lyra, and the results are shown in Table 3. By comparing DSP using GPT-4 with those using Codex and ChatGPT, we can see that GPT-4's formal mathematics capability has substantially improved (51.2% vs 42.6% and 43.0% vs 39.3%). Meanwhile, LEGO-Prover, using ChatGPT, achieves better performance (+4.1% and +7.0%) compared to DSP using GPT-4. Moreover, LEGO-Prover also outperforms Lyra using GPT-4 (+3.3% and +2.9%) and even achieves comparable results when Lyra extended to 200 proving attempts with GPT-4. This result is remarkable since the performance of GPT-4 in formal mathematics is substantially better than that of Codex and ChatGPT.
21

---

Published as a conference paper at ICLR 2024
Table 3: Comparison of proving success rates with GPT-4. All methods listed, except for Lyra (200 attempts), involve 100 proving attempts. The cited paper presented after the method indicates the origin of the results discussed here.
Success rate
LLM
informal-proof
minil2FFvalid
miniF22Fttest
Baselines
Draft, sketch, and Prove (Jiang et al., 2022b)
Codex
human
42.6%
39.3%
Draft, sketch, and Prove (Zhao al., 2023)
ChatGPT
model
41.8%
38.5%
Draft, sketch, and Prove (Zheng et al., 2023h)
GPT-4
model
51.2%
43.0%
Lyra (Zheng ct al., 2023b) Lyra (200 attempts) (Zheng et al., 2023b)
GPT-4
model
52.0%
47.1%
GPT-4
model
55.3%
51.2%
Ours
LEGO-Prover
ChatGPT
human
55.3 %
50.0%
B PROMPT EXAMPLES
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 the directional transformer,
list all the core statements be replaced in the Table.
Table 4: The core description of individual directional evolve. The description will be replaced with the directional evolve prompt template.
Evolve type
Description
Determine essential ideas, methods, or
Identify key concepts
theorems that crucial solving the initial problem. If the problem involves specific numbers, generalize it by replacing these with variables.
Parameterize
Try both simpler and more complicated versions of the problem
Scale complexity
how the approach adapts.
If the problem is defined in specific number of dimensions, consider it holds in more or fewer dimensions.
Extend dimensions
22

---

Published as a conference paper at ICLR 2024
Input:
System message: As a mathemutiiian and expert in Isabelle chourem prover, your task to unalyze the given theorem (including the prob- len's informal ststement humsn writsen informal proof, and formal statement). Provide better stractoned stop-hy-step proof that closer Tachelle and request lemmas,
might help proving Statement: If 2 6 1, what is the lagest possible value log, (0//5) + Loggy (b/a)T Show it loga logs
Informal Using legaritimic miles,
(logie b using [IAM GMII that parentheses must least the largest possible values
Toga T
Since both
that
occurs when
Formal statement:
theccwes
fixess 21 treal
assames "lotcl l00e"
and "1x00"
Structure proof: Step Introdicc vartibles and to reprosent the noturn logirithms respoctivelly
Step 2: Given thet 1. conclude that the natural logarifumm of y, grester than dI. This implies
Siep 3: Using the noumptions, establish thit
Step Express
main inqqullty Step St Simplify the expression derived in Step
Seep 6: Demonstrtte that the above expression is less than or equal to The Arithmetic Meun-Gevmeric Meun Inoqualiiy (AM-GM) used here to anguee that the tonn /t + m/y) least 2, hence expression most
Required
Thoughts I: A base lemma proving amagm incquiliy that useful for step
Cisle 1:
Lemm arLge:
Elsea
seal
ty
above y22 2
Thoughts 2: According the step we derived special form of am, am.gm inequality, which proofss the conjecture 1t u/ar >== required in slep
Cisle 2:
Lemm mn.gr.tiividle. Forms
shows "s/y y/x 2w
[ww more etamples Like above...
Statenent: lesst possible value (xty 1)2 (sr y)² for real y/? Show Informnal proof:
Espandingg that expression a + 2ry + n² 2² 2xry or + 2/ u By the Trivial Inoquality (ill
nonnegarive)
value
which achieved
theceess and 2021, 177
2steall
showe Ville 2) 11"2 y1"2*
apply (auto eimponl www.a strpo povcr__o__ogarr
Output:
Structure proof:
Step Expand the expression (xy
u) to 22y Siep 2: Simplify the expression derived in Step oheain =² + 2²²²
22
Step Apply the Trivial Inoguility can squerss nonnggative, argue minimam value expression
Required skills:
Thoughts 1: The Trivial Incquiity a key concept in this proof. Undesstandnng and applying this inequality is enicial show that the misiaum value of expression
Leama trivist incquality:
Eiseen 11 small
showa "0 \<la a"2"
Thoughts 2: The ability expand and simplify algehruic important in proof.
expand exprrsssion:
fixes v 1: roal
shows "Ix 37"2 21 x
y"2 x
Thoughts The
subsiitte values expression evalunte necessory the value achieved
Code
Leama nutotiturr.vvvlees.
disene x 11 real
"x 12"2
Figure 6: Prompt example for decomposer.
23

---

Published as a conference paper at ICLR 2024
Input:
System messuge: As mabeemaiciinn familiar with Isabelle, your takk is to provide formal proof response to given problem statement. Your proff should be structured and clearyy wrillen, morting the following criteriat
verified
Each step of proo should explained detail using comments encloeed
and "ey".
The explanation for each step should be clear and concise. awoiding any unnceessary or apologetic langiage
useful and reuaall lemmas sulve the problem. large step proofs (non-trivial, well organized and easy to follow, with each step building upon the previcus one.
You strondl encouraged
should
(gmeralizabble).
your
Here are some useful skills for reference:
Usedul skills 1:
Lemma square ditr idesmity
Elsenn
ceal
proof
have ti yt"2 by 23 2012 1872 by taimp add: power?
2
0472
x'21"
y'2
by tairp aissscaaaiigss)
finally show ithosis by auzo
ged
useful skills...]
Statement: Show positive inleger n. divides 4
Informal Proof:
Step Since positive. find natural number where
Then show that divides 4
thecees mumbertt heory. 2chrokeeggin
Vasoteap
ahowa (2:met)) ded 4'off
Formaal proof:
theory Scratich
imports Complex_ Vain
2chroleegggn
fixess tt 11 rat
assames h0 "n Vehoterg (*
" ded 1"="
proot
obtain mi ieet whene c0: "m-1-p" ciodgshammer
have ged
eledgeharmer
unfoldiing electgehomer
and
formalization example...
Statement: What the leust pussible value (zy 1)2 (or + 2 for roal numbers und y/? Show that it Informal proot:
Step Expand the expressio
1)a
v)? obsainn x 22y =2y² 2xy
Siep 2: Simplify the expression derived Step cheain =² + + =
Step 3: Apply the Trivial Inqquaity, which stotes that all squires are noonegative,
that the minimum value the expression is
Step
minimun
achieved
Formal statement:
theoren anc12e_2021 2021__tt
asseal
shows
V4lc (0x
21"2
DE 72"2*
Output:
Formall proof:
Liwocy Scratih
imports Maip
begin
atLgge
ahowa *x"2 y22 Vogeo 2
proof
have
by sirp
Lhen have *x
y"2 Vogu df
Isinp aektt gebrr power? di Ff)
*x"2 y Viggoo
by sizp
then show Itheeis
theccers and 2021 p7
Eiseen s2seal
showe "1 Veles
y1
egply simpota igeenn scirgss power? sugaree
by iralis eniigg cod.commte add.i.n adkio Linnmkee poiippon_ be
power2, mum power. mono nerro le povert))
erd
Figure 7: Prompt example for formalization. 24

---

Published as a conference paper at ICLR 2024
Input:
System message: As muthemalician familiar with Isabelle, your task to provide furmal proof in response to given formal statement.
Your proff should be structured and clearly written, morting the following criteriat
verified
Please ensuee that your proof is cell-organieed sasy to follow, with each step building upon the previous one.
Formal statement:
Leama power sag lequ
Eisees at :roml
assunes "3-0" "alototoge"" *a"tn 4ho"
Liwory Sozalich
Imports Complex
begin
Lerm power _ower__e__igpp..
fixes areel
"poOf "al/rrttep"" a'""
abova
proof
have *a" (nint
using asmne(3) acono(2) metis asmssll ditt in 0_og ditt_relit_og. ieunemees cocmrnt) Jess popp_itp_tttt__eee liner not lit conparison (2) le one. le power order. lees order rece frowt) order_refl
inorrder
power_ 0 power luftt power wwwrresiinggg iff Cu inwer_.inedd Intee real ge....ge_...f unigue real roon, power
powest
"n-rec"
by jent (verit)) woore:)) asera asenst3) concel_omm Low.rrensdd aett olesodd ff diteeellddddd.... diff_ix Duef powe pooerdeeressinng nower_inject. verit comp verit_ocmp_. (omppiimpitty
thus "o by worit) ascno(l) acens 12) acomst3) Loss extrra33) net_noguice power_injstt.oo power power_porict scrict, decreasingg.ttt.. litt zero_Jess ditt)
ged
roguest solving examplex..]
Furmal statement:
Lerm sopparee pwwppccoeccc............ooooo Linss:
#izone
to 'cand: (a"a) o]*
Output:
Formal proof:
theory
imports Corplexx/aain
begin
Lema aupanett_pcpprrttti real
assumes *0 Vvandd 0
shows *a"n 2't a"
Yeands (atn) to to m)*
proof
by tsimp add: (1ono(1) poweecaadd)
next
taimp asono(1) mowe
god
and
Figure 8: Prompt example for solving request.
25

---

Published as a conference paper at ICLR 2024
Input:
System Message: As expert mathemarician who pruficiens. in Isabelle theorem proving, your tack is to modily the given lemma thee rems finction, definition given in the code to aid solving more the problems provided. You should accompplish this by fevolive description }. Problem
problems:
theoren gotha__llecta__.. seal
and 1: "zeal V-Rightazzow roats
assunes ho "V<tacs.. I
hi
and h3 ta Venotog
showa "1 (ar1) Go-11
reference problems...
Skill evolve:
impare Main
begin
Larma hel nuttrer hww.beet/wwry..0000
11
showe
Vooro n mod Voaro mod
by auta
Evalived
thecry Scratch
imgortss Corgl Main
boggin
Lerma renainderr_oouue moduloo
Eisees 11 nat
"d g*
(0.,"=1)"
proof
have *r. mod. df by (eale mod lose givisortor acenetl:))
have "n Veges by simp ultimataly
ged end
(2 more directional evolnv examples]
evolve:
Scratch
imports Compl
locgin
Lemra civide wwwooorooouul mul: roal Venotoop and Venoterp and *a b e dt shows
using by simps steld_stmpe) and
Output:
Exolved skill:
thocry
imports Maip
bogiin
divik assunes "t Vemotoop
and *d (youutupp of
and
shows *N: d
using by: wings sield)
Figure 9: Prompt examples for directional evolve
26

---

Published as a conference paper at ICLR 2024
C EXAMPLES OF GENERATED SKILLS
Lerma Floor..gqre
"n g*
ahowa
*Eloor laggtt of Voleo n. Yoand (Floor laget of 1372*
proof
leggtt
prooÉ
have "Cloas bagel Veloo west at by sinp
hence
b(fleorbegrt n)) Vcleo legrt n1 iretle floor of Fleon Tinorder le of int of_int__leeer_le oi_iit_le_ if of inuuer J_e_iff arder, Layruazew =eal_aqus_to_it ceal_aoot poud powt Ie aero powerr) Einally abow Pthmeeia asith
also have "... ont sirp
qed
have (Floontagrt 1) 13"2*
proof
have tloor 1" Linarith
(floor
by (verit)
Int power I.le_iff pover, prrer.ttriot.re
also have "... ttlooriagrt 201"2 2 + Eloorieget nf + 1" by (stmp sodt power2 som Einally have "bgrr 12 (floor nii 4 2 Floordegt n) 1. noreover "ogre
by stmp
ultimbblly show Ithests by inttis Voggero loget trest hupuup rest fne (C looperrt trea verflooo
ve" supo2] Vocllcse doubl e eeg... A Tiverssiiim Flonor mero tsunnn (nmel)ee()) le Floor_eeti beox rup Jo it_tt__jee Jera ot_int_ot_um power power mono power one right Legrt, pos? sqarre eq
ot_int_
power_ conooooooooee pios_int_cooe
qed
ultimately sbow Tcheeic simp
ged
Log_ Floos_oo0! fixes b 11 nat
assunes "a Df tb
"b"x \<le> Yeand>
Miaggsttesseaarere Veldiscroiog tscal Vertooo
proof
have 1o'x k<ie> Yaand a < <'" (el) Iclongshhriimmarre log (seal (b'A) Veie 1oo is treal al Yeand loc i treal at log la tocal (o" [e+1))*
(verll) padis striet in bess_.nnrai_eetrall jor cancel Lirr o
stuntt denetllaid of lasa also have *... Vccegicttsiaaaroo x kite log tresl a) vand log troal < x-1
ecunetunno 20ra jess__oossp__e_e powast
by tast (vurit) ooiinntttt_ae_eeee iff cormtre antiajnooov assra oraloord ifcure oodas. striet_trasst dai_pcckr.srrion strrsstttttttraeeeeeeee trans2 orrds crans to Leso_addoon Lose_imoo___s paa_t_attt__tteeeoe_oe____ Jess poc
res af lew aلاانك af of of power carcel lif ofjaa_pooer power power_eoototto jat pooel power Dee ju Jese clase zcre cae zoro_ Locs_oossppoo
Linerder Jasss La
using by (ant. (veria) sacueqpluss in left flser_at Jeyat floer _ Lesa_uuerni__otee rot_power_ Jess_ing less less not one ie__i___o pero aot Jos_ et Lesa ofunet_ of uf soweooteio wtt.etoooo..osssiiii akcowaiing will www.uappppllyyyygg.... wei wwil__ varit_ennsinpii te Jo concolll Einally show Whesss by sing
ged
27

---

Published as a conference paper at ICLR 2024
Lema
pái
shows "2 cos Vileo aba l9ost [2 san (2 xI) sqet sic. (2 X011
proof
have (co5
taime cos_
also have .... loggt 11 - (oin ix 221)"2)
by last. (buzit) ad.
"oquelldee acosin accaing arosing arsingpi azosingain asmua()) amartt))
dif coup oo dift ditr sice_divididdiiee
oun_s_ halves int_oport: pnt_ ie nuneraal coaaa mimes divide lett milt right totscullittto aureral_orw plus Leg_a powerninu Blcd seal por re sirgpuninn Jegom also have sinpporiodic_st sinupi iin sin_twepp)
2)1*
using airullff
p4] aato
also have *... laggt 12 (oin 10 "211
by taipp stklt sinuaguneeLs)
"2)"" aqez (1 taic x p4t (appl Vellese> Vepoar-- sgrt 0 supp >2] sigt 11 (sin a/\s"supp)))))) (asspp) (oppe x. cas b. på] Vauliss (اااا hance "2 cos - (2
finally have *coa
(igzt
tratis Vstper-- coa
(sin 2)1"
have .... vollo abs laget
x11 agpt san x13)"
using ako_sunninnn.om (or "aqez (1 sin (2 203 egst [1 sin [2 x]1
by jent (verit)
(sin Ix pe))
11 6ein (e'ogod) voclows Vooperoena
Velcss difr_ge_ oe ninuste ault_2 nag O post_oort ain toubla airoouninnee senca sin.plouxiin sinutero aquare_)e..) (n.3)
stp- lain hetaupp21 add aaliineraaaatt dice ail.
Finally ahow iLheaia by
ged
fixes a. b. 11 nat
ansmes "prine 5f "p 2" "p dod 1e12 b122" "p divil at "Vonott ded by avd. bt \<and-
shows "Veaiists
proot
obtain vbere dedt "a"2 2522 l using acane by auto
obtaain wbere dooez "a 1 using acome by auto
have
(a"2 b02)* using seeee pow
"ta"2 5"21 p*) tent (verit) aseno(3)
(3) sii_sst_iiggtt__t
poo2 ardns_ard__oowee
then have *p cvd 1172 2"2 + E221" using Lost by touto simp: strpp)
then have didiit "p atd (172 = + b22 172 1a"2 + b"213" using k. det by cimp
have
1"2 102))
(eritt) asses(1)
acanc()) assrs13) dot_catsiionniirt
prime powcr__nor_tt1
than have dvd3: fp avd 62"2
172)1* by (ant (varit) Vooparpp did suppu a plc"supe2 "ec""uupoVvioooo assrs ett.ttttttiitt pos2 prime itt prtn__or__ooee__asr
(2) 35cma13) dot_
have "Venct-
have "Veeoor> using
using Ant poptttooouaaee p asana()) by
povert (qpqars))
then have *iyzoc>> p and (1 1"2)* using dvill by lant (eeitt Voopero and 11e Soppp = plc"pup bix "uppieeloss aceno()) ard_odd__ right nod stt pos2 peime mot int prime and powertnet itti
have prime_ovs_muitD)
172)
(vesit) Veeperr-venoe dvd liv aae"uuuealoe asmat))
then have *Vetoc> lvvexitt x. ard (1 172) x²2)" by simp
than have "iooor> (vsaxiste> dvd (1 172) 222 by betis kaperp/onddstex. and (1 Ik<"upe)) xix powce2_ squarc)
avd_malc
mult. wwutt.lstt_ommmee
have "Vctorall Veoot>
172)
by almp
than have *(<dorall> x. x*2 + Ve00 of by spotis Veopar verocsss.s ded It 1se'sup21 xivelose arittrivrrett. powcr2_pq [quare]]
15 dud
for
proot
have "p drd (1 + x0 using Lost by simp then have "p dud (a. ictt_sice_dione disteddio
211" using that by botta dift po dutgg Aaair
Lhec have ded (a then have "p dud bs
p. s0" by siag
1 pi)" by taipp add: atoddaasinps)
then have "p dudl using asms prine awt.mttt wow__uttttottttttttooooo oqunat
s1*] by goets cogemmonnsssex.... did cCSupp21 stoiluse avdunll Lade nols Jeas
show Ithasia by (sacia adi.comata asama[]] asans(4) asara(5) avLaadioonnis prinn that)
qed
obtain wbeae "p ded La bit and Yx72 >iseeiltte.. ded (ic"aup2) aiveloose and_rryyyiihtt powera___ooooo)
using Vooporo Wourlll x Vogio piselese by (neLia
show hhells by autio
ged
28

---

Published as a conference paper at ICLR 2024
Lema
asounes *0 <. 'vandd 12
and "k \<lo> at
shows
Itact ract In (tact 231 (teet tact
103"
proof
have "/n kt (Cact. in - 113 / [Cact x fast to X11 (Tact to 131 (Cact. k. Cacs (n 103 (Sact
by tauto cimp: ticis_stmpo)
also have *... in (Cact in 11) > (Eact, In 11) 1 x (fact tn 2211 / (Tacs k fact to KO3* by tratis adtiocmmzz dir. distri distrib_zight sult.comeza
(toct 113) by htatis addiommece asans12) som. dlssiid Le Stt cult.commattt also have *... (Eact a) / (Cact & foct in X0)" by lant, (owrit)) Voppecored (Gr 1) Fact to (Cact
R]1"
fasl in 10 (Gars k fact ki real to Gas 10) veclosi Vosparpeedd
fact to 132 (fact fast X)) roal fact 131 (cact MeVelloso asase()) perailleesssllggggg GesunAu oe leo_leoo_ee of of.nel_mnl)) Finally show ithosis
Lema wtwp:ooootooooor..ooo
assunes "n D* Tr.
shows "prine_tacttee factors (Lem m0 prime ractors Vountor: prime factoss att
"ccinettcctess 11am Veoubsotop pcine_Factoes proot
peine_tactors
fax assune "p Velop print_factors (eon ni have "p dvd. ien
have to Vour p dud using asans by (ant (verit] Vesperop Velio peino. factocisation (Las (sclose antioys_oonva dual order..rrrtt.. strict Afc_ inipeine Latt prime factors Laii
then show "p Veine grine factots Vemiom peine factors n" by goocis Voopomp Velied primee factorisation (lan m) strict
factors Jam sup.
comutt)
qed
next
Frstecs Vemiom prine_factors Vaubactec prine_tactors (1an proof
fux p assune No Veloo paine factors Vauiio scine_facooss nt
then have "p did Veage p did ot by zuzo using arineffacted
have "p
by
show
ni by jutis Veparpp scine_factee Veuiion orine_facton aiselosee Viopepp aod i voor and mivelose asers asmsi12) ded andiaail did Jon did_mitt_caaeee Iar. bon Ligh__ittttt lemoordd Lan tal Duif 1 len Jdin tonproanne torupe 11 Cariut ii pot rasturatttaaoo Jon LndE_
qud
ged
29

---

Published as a conference paper at ICLR 2024
Lema Los_larrpppprrtto
shows Maod Jan and "a ded scooclettclancaroe
and "b #Congletteignaanee
proof
show "ged lan to 1n" by auto
peooÉ
assune "a and ln
"lem ded
moreover have
by auto
ultimeblly show tion b 2n" by taimp add: dri_antismm
next.
"La
moreovee have fllas a to dad 1nt by Stelis Veaperolcan a la blodous (ee)) ulrinately show ta dud br (slmp add: dxLanniayet
next.
show to dud proof
1am at
"lo
morrovee have th aldd lar a bnt by auto
ultimately show fIem la by (einp stklt chelaant Lnya))
bence "h doal lan a 1!! by sizp
norrover have hiee ched by inetiis Viepero atyoolose did refl) ultimabaly dod (sirg aayi
qud
next
alhow to ded Viland b ded i Sellenggeenrighhteeree lon b ded ot
Viandd is eied
banow the thell loa a b. 'oands is ded len 1f by auto
thes "Ian ded of fratts (sppecia dud Ysand- b dud etsclosee len_lessc)
hence "a avd Icm 'vannd is dhd Iem bit my nuto
thess "A chrd Vyland b chell by (netiis Vitpeerl b dud ctvce cowo net.irantt
ged
30

---

Published as a conference paper at ICLR 2024
Lema ros_eycllcity:
shows "(2"a) and (Tesnat) = (42 a and then elso i mod than alse 41
proodd (induction
by simp
next
BBuc a)
and
Lhan slow Nasse
peoož casas
have 1(22 mas) [mm]]
(2eenat] to mnd
by (aimp add: Pac22_
also have "...
(2senal)" nounod 3) and (vezit) 12" nesiinttttiiiial oowe wult.comnrettan dulr.dilta iigh power_ power_yilt distrri)
also have "... (2ccmal)) tn mad 1) and
by (aimp add: powas_Bac2)
also *... (2:inat)
mod
by wing
firally ahow Pthesls
using by
then have cneni" In nod (Poonet) "n mod
by (aing athlt (oale__Faal)
and Te using Sta by jast: (owrit] cellaal at mod_mallt_ Jeft power nero__eee_ooe
have *...
also have "... (2semat)" in mod and
by (sing wdlt by sing
dinally abow tthwell
using by Veetiix Greurettude Sun Bacu Batteg.plod Veopero22
red 31 aed 7yaslooso Vogpen mod Tyealese adL adL_2_ne_
mad
wid Shi shifft cancel right right evell mimerally (3) red Sue mod 9ho eg mod trivial molt right
fuati net diti and (3) mureral A. mawral,Bitd RiLD rumecal mumecall_pleec plaecuureral pawet_one lift. semiirine_romm100) senising_/omn(3)) saniringream1) sero_rac__ne)
then have "(2rrneti" maai In-13 mon i (2::nat] 'n mod
by (sing wiitt
using Soo. IH by tent. iverit) add cancel right. left mod noc trivial noc mong oong malt. corm nectral nat add not leox, le muneral, 1it0 ore power? pes? wawe pemo.reg.one) also have "... (2stnal) mad 3 and 7e
by (sing power
have "... (Pssnet]" (Sue nod 31) mod
by simp
dinally show Ptheets
by O_no_
Socueng Vopperd2 in mod 31 mod oiveloods Veepert2 1) mod
mod
Voogero2 2 mod
mod Vyvclood
Vogprro2 mod. mod 1 w Sue nod 31 medl TVvel bees add. 2 egg Stxt add Sao right and Sae ahi ft
wwwl_ret_nuneral (3) wed__ modLae mult. mult. 2_iight manuskoble rureral Lung Aug_ nuneral Lawerl_Bitt Bito manero__.Dee
mumeral powert2 pover2_oo_rrome regaae po
ged
god
31

---

Published as a conference paper at ICLR 2024
11
assunes "ood
Veieo X" % 73"
shows "k \<iip 14, proof
using assno have "/: nod 1eim 10, 1, 2, 3, 4 5, 5, 71 by auto
"god
Lhin conaider *A nod 8 = of "K mod 1 and 8 2* % mod 3" nod 8 4"h 1K. 5" mad
5" mod T5
proof [cases)
assune *x mod B have *8 have 1ged Verotasp by aimp
then show 2thosis using asers by slmp next.
have *R. [1, 17, ...)" by (necis (2ons(2) insost aboorbz Lnsart_comrzze insert nod_)
Llec have * Vylio [I, 3, 5, 73 by (aail Vaggartk rad 8 Lysolooee asara(3) - ledd)
then show 2thasia
then have *K: Velio [2, 20, 18, 25, ...)" by fazt (verit) (3) InsectIl aoc_]esa)
then have * Vyiro 12, 61" using
Lines have docreaacai 1e02 add ao oerguonp_ttt_lngee
using
(well) Goeunallasee Voagerkk nad 2youlosse adtaaaaii
exoreexpiffe iit_ppaa dasl oodac.stticc staeetttraaaa gret_ goi_nex__iigtt be leoos Sunieg le, reserall aelli less numeral pede reti mod. modLleos - leonson pl pla Lo Suc wero (om
(secls (1))
next
anaaama 5% saul
then have
*k Voiro 13, 27, ...." tore: cvertti (3soms() Insert mod. less) Vooperoi
2Lhasia by sinp
next
"x rod
by (werlt) (3) Insectil aod_lesa)
then have * Viiio 14, 6)* using asems by euto
Llees have *guzd Veoolagg using woore by last (neilt) Dee Suxt fon.foooonnooooooo Bax Oured nameral (2)
Susunumeral 'soparok nod Avecloase aktreacan akL eoes i cong it
cong ergi singece) cong emp simps(() cong mmp singe(())
get
gudLnoiiiight Light lesl
me_neeerl cxt mxLadd nodeetllll Le Bun and lase mad not less nuneral One plass eg Suo semiring nomior zero, Jess wssms(1))
then show Pthesis
aonnam mod
thenr hurve *
Vycioo 15, 13, 21, 29, ...." by firt (ventt w3ams(3) Ineert mod, less)
Liaee have * Velio 15, 73*h Gene (omril) Voggarok mad 8 Stsclosse asarra]] Ir recll
by strp
next
acsuane "ix mod
then have *k (yiino 16, 14, 22, using by by iette esener3) insert, absorbb insert commute insert. mod leee)
then have "god Venaterg using soons my metis Soe, 0 mod (imeral bite by cong eg itt simpo(2)
cong emg iff singoce)) gest ged betton left botton god Soo, & geat nat right neceral ges red net not_moll2 0_._l_ rumeral lff maneala(()) Lne swnt norm((3) singletor_iff by (ecco asemo(t))
next
assuae "Ix mod
have Viirt 17,
by (verit) assns(3) incest Jessl Vorperbk Pyycl
sing
then show 7thoois by stmp
ged ged
32


Reviews:
[{"review_id": "fUd5j86dMz", "reviewer": "Reviewer_oKSy", "summary": "This paper proposes a new approach to automated theorem proving with LLMs based on building up a library of lemmas useful for proofs. It is instantiated as a system called LEGO-Prover for proofs in Isabelle and is evaluated on the miniF2F dataset. The approach is fairly complex so I've broken down my understanding of it below:\n\nThere are 3 vector stores used:\n- Problem Store: Holds (unsolved) problems from miniF2F. This is where new problems will be drawn from, and is also used at various other points to guide how lemmas are proposed/modified.\n- Request Store: Lemmas that have been proposed but not yet solved.\n- Lemma Store: Lemmas that have been solved.\n\nOuter loop (I'm less clear on this and have also included it in the Questions section):\n- There are 4 LLMs, described below, used in the solving loop.\n- LEGO-Prover makes 100 passes through the miniF2F dataset, and in each pass makes a single attempt at each problem in the dataset – i.e. it runs the Decomposer LLM once on that problem and Formalizer LLM once on that problem (correct me if I'm wrong).\n- Concurrently with each pass through the dataset, for every 3 Problem Store problems attempted it makes 8 Request Store attempts, where an attempt is either a call to the Request Solver LLM or the Directional Evolution LLM, or perhaps both (please help clarify, thanks).\n\nLLMs (all implemented as variants on GPT3.5):\n- The Decomposer LLM takes the formal statement (from Problem Store), informal statement, and informal proof (which is either given or is produced by the Informal Solver LLM) and outputs an informal step-by-step proof in natural language followed by a list of formal statements of lemmas that would be useful. These lemmas are added to the Request Store, where attempts will be made to solve them later, at which point they'll be moved to the Lemma Store.\n- The Formalizer LLM takes the step-by-step informal proof, the informal and formal problem statements, and the result of querying the Lemma Store for relevant lemmas, and attempts to produce a complete formal proof which itself may use the retrieved lemmas by copying them verbatim (from the prompt) or may riff on them or define new lemmas. Any successfully-proven lemmas during the process are added to the Lemma Store, and unsuccessful ones are added to the Request Store. A sledgehammer/heuristic based autocorrect is used on all failed tactic applications.\n- The Request Solver LLM takes the least recently attempted lemma from the Request Store and attempts to prove it (aided by retrieved relevant lemmas from the Lemma Store). If a newly proven lemma is measured as too similar to an existing one via the difflib Python library, it is discarded.\n- The Directional Evolution LLM takes the last recently evolved lemma and queries the Problem Store for unsolved problems related to this lemma and modifies the lemma along one of four axes (identifying key concepts, parameterizing it, making more or less complex versions of it, or extending the dimensionality of it) in order to make a new lemma more relevant to the problem.", "questions": "- Table 1: is it correct that the `LEGO-Prover*` entry effectively has more than 100 attempts since its merging all solutions from 100 human proof attempts and 100 model proof attempts?\n- Table 1: where is the entry for LEGO-Prover (model proof) miniF2F-test?\n- What exactly happens in the ablation: does it call the informal solver, then the decomposer (but without creating helper lemmas, just getting a step-by-step proof), then the formalizer directly (without retrieving helper lemmas)? And is the autocorrect sledgehammer approach used in the ablation as well? Does it get human or model informal proofs?\n    - I could imagine two reasonable ablations, one that includes first generating a step-by-step proof and one that just directly produces the final proof. Both would be quite informative, though I think only the step-by-step one would be essential.\n- Is it right that on each of the 100 passes, LEGO-Prover runs the Decomposer once then the Formalizer once on each problem?\n- I know that for every 3 Problem Store problems attempted it makes 8 Request Store attempts (or \"Evolver\" attempts). Based on the Evolver section that could either mean using Directional Transformer or the Request Solver or both – is one or the other picked in some ratio, or are both used?\n- Presumably sometimes the skills aren't used at all and just happen to be retrieved mistakenly as relevant by the vector store. Are these cases counted as \"used to formulate new lemmas\" in your analysis, since it's hard to disentangle them without some sort of similarity analysis?\n- \"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.\" To prove the point of the library having many broadly applicable lemmas, and to better understand the usefulness of the lemmas in general, it'd be helpful to see an analysis of lemma usage frequency in *correct solutions* to problems – for example how often is the most frequently-used lemma used?\n    - A more detailed analysis, not necessary for this submission in my opinion but which certainly would strengthen it: have a histogram with number of uses on the x-axis so you can see this distribution of usage frequency for all of the lemmas. \n\nvery minor:\n- Fig 3c: I think some labels might be mixed up: The skill resulting form parameterize() doesn't look like it fits the prompt for \"parameterize\" which is \"If the problem involves specific numbers, generalize it by replacing these with variables.\" Instead it just seems like a fairly different skill that no longer involves sums of squares and is now checking for less-than-or-equal-to (assuming this is `\\<le>`) instead of equality. Meanwhile the \"identify key concepts\" example looks closer to parameterization.", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The overall idea here is an exciting one – building up a library of useful lemmas that can help with solving proofs is certainly an appealing and very natural idea; it's quite similar to how humans use automated theorem provers. It also makes sense that having skills that build on one another could lead to solving increasingly complex problems, and I think that this is a promising and exciting direction!\n- I appreciate the analysis of how often the skills are used verbatim versus modified (4.3.2) as well as the analysis of where the various skills came from (evolver vs prover etc).\n- The ablations are clarifying and helpful\n- The version with the human-written step by step proof was helpful to include for understanding how good the pipeline could get if that part were ground truth\n- The legos and other icons used in the paper are very nice\n\nWhile I've given a negative review and spend much of the review giving thoughts on ways to improve, I do want to note that I really do believe that this kind of skill library learning approach could be very powerful and is in the long run an important direction in this field even if I'm not recommending this work for acceptance (at least, as it currently is) for reasons discussed below.", "weaknesses": "**1. Comparison to baseline is not very strong**\n- In my understanding, the best-performing prior work **Subgoal-Learning (Zhao et al., 2023)** does not get the human written informal proof, so the natural comparison is between this baseline and **LEGO-Prover (model proof)**. The improvement on miniF2F-valid is from 48% to 52.4%, which is a 4.4% improvement. This is decent, but not huge given the complexity of the method and amount of additional LLM queries required (which could have been used just running more iterations of the other approach, for example).\n- Additionally, there's no comparison on miniF2F-test for **LEGO-Prover (model proof)** which seems important to include if following the above interpretation as the main result.\n- I also find one of the main results in the abstract misleading: the 48% to 57% improvement is actually between the baseline (which gets 100 attempts) and **LEGO-Prover-Star** which is a combination of **LEGO-Prover (model proof)** and **LEGO-Prover (human proof)** which in my understanding *each* get 100 attempts. This doesn't seem like a fair comparison since there's a combined 200 attempts used in **LEGO-Prover-Star**. (I'm open to revising this if there's an explanation I'm missing or I'm misunderstanding the setup here of course).\n\n**2. Comparison to ablation is not very strong**\n- The ablation of the skill library changes the 50-attempt solution rate of the method on the validation set from 47.1% to 50.4%. This 3.3% solution rate gain is not much for the complexity of the proposed method. I like the idea of the skill library and I do believe that by experimenting with variations on the approach the authors can achieve greater results, but as-is the library doesn't seem to add much.\n- The library version must also involve far more and far larger queries to the LLM, given all of the lemmas included in prompts and the fact that for every 3 problem solving attempts there are 8 evolving attempts. Simply using all those extra tokens for more attempts at solving the original problems would likely provide a lot of benefit and could conceivably close the 3.3% gap (this could of course be disproven through an experiment, and would be a valuable thing to include).\n\n**3. Could use more details at certain points, and overall readability**\n- It took me a very long time to understand the method; in part this is just due to the many moving pieces, but I think the explanation itself could also be improved and I'll do my best to lay out some of my confusions/thoughts which I hope will help the authors.\n    - I think that presenting the top level algorithm loop first would greatly improve this: that LEGO-Prover makes 100 passes through the miniF2F dataset and in each pass makes a single attempt at each problem in the dataset using the Solver (which is composed of two pieces: Decomposer and Formalizer). And that *concurrently*, for every 3 problems attempted it makes 8 attempts at solving any pending Lemmas that are proposed but unsolved (and also it calls the Directional Transformer to evolve them? Though I'm unclear on how much that is called relative to the Request Solver). A very high level schematic and brief description early on could be helpful for this – as is, I found myself trying to understand the 4 pieces (Decomposer, Formalizer, Request Solver, Directional Transformer) somewhat independently only to find later that there's this larger 100 pass cycle split into two concurrent processes, which came as a surprise around page 6 (until then I was just unsure when the lemmas got evolved/proved during this whole process), though perhaps I've missed some earlier discussion.\n    - A bit more clarity could also be used in this top level loop, which I'll leave questions on in the Questions section.\n    - Figure 2 was quite difficult to understand (though I appreciate how nice the visuals are). I left some notes in the \"minor\" section around tweaks that could help with that.\n    - Figure 1b is meant to be an overview but I also struggled to understand it, and it doesnt include a depiction of the Request Solver (which seems important – when are the lemmas solved?). These figures all make sense to me now having read the paper, but they didn't help as much as I would hope for understanding the idea at a glance. This isn't a huge negative, but it would have been nice to get more of a feel for the overall setup from these splash figures.\n\nminor suggestions:\n- In the related work on skill libraries it'd be worth mentioning DreamCoder (Ellis et al 2021)\n- At a glance it's difficult to see that Fig 2 is actually two subfigures – spacing them out more and/or making a thicker/different line between the two would help readability.\n- I'd suggest that Fig 2 should not reuse \"skill library\" in all 3 places, it should separately be lemma store, request store, and problem store. It was quite confusing that things labelled as \"retrieved skill\" and \"formal statement\" and \"request\" and \"similar skill\" (using labels in top right of each box) are all coming out of the skill library in different situations. Alternatively, something like color coding the different parts of the store and using color to show which is used in each place. This would just generally help for readers who glance at the figures before reading through the whole setup.\n- The main text having a table containing just the system messages from the prompt (can abbreviate away the \"expert mathematician\" bit) would be immensely helpful if space permits – looking to the appendix for those was key for my understanding. This would immediately clear up a lot of things, such as how the decomposer is producing two different outputs.\n- Section 3.3 has a \"Table ??\" where the reference must have broken; likewise there is a \"Figure ??\" and a \"Fig. ?? (a)\" near the end of 4.2\n- at the bottom of page 5, the phrase \"As depicted in Fig. 7\" should be moved a few sentences ahead – Fig 7 has the prompt, which is only relevant to the latter sentence \"Finally, the request solver prompts the LLM to generate the proof for the request.\"\n- Missing period at end of first paragraph of section 2", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "P6fNagT9qd", "reviewer": "Reviewer_UPjC", "summary": "This paper presents a framework of using LLMs to build a growable lemma library to solve math problems in the Isabelle proof assistant. The key feature of this framework is that potentially needed lemmas (to solve a target problem) can be conjectured and added to a library, and lemmas in the library can be generalised and deduplicated as the library grows. Impressive performance gain has been shown by maintaining such a skill library.", "questions": "- page 4, skill library, request vector stores: does the request vector store simply keep a list of conjectured statements proposed by the decomposer? What if some of them are wrong? When will the evolver attempt to prove them?\n- page 4, 'generating more beneficial new lemmas': could you elaborate a bit on why the evolver can utilize the problem statements to generate more beneficial new lemmas?\n- page 5, 'a minimally solved request (with least amount of time being selected to solve the request)': I don't quite follow the 'least amount of time' part. More explanation is highly appreciated.\n- page 6, 'serve as references': could you shed some light on why references are needed here? \n- as the pipeline is relatively complex, can we expect to have it open-sourced?\n\n\nminor:\n- page 2, related work: though not LLM-based, there has been some prior work on [template-based lemma conjecturing](https://arxiv.org/pdf/2212.11151.pdf)\n- page 5: 'Table. ?? shows'\n- page 8: 'Figure ??, in', 'Fig. ??'", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 4, "strengths": "- Library learning has been an attractive topic in neuro-symbolic learning, and previous experiments have mainly been carried out on synthetic environments like [DreamCoder](https://arxiv.org/abs/2006.08381). To the best of my knowledge, this is the first time effectiveness of maintaining a library has been shown in a mature proof assistant environment. \n- The paper is relatively well-written with clear explanation of its key component and illustrative examples.", "weaknesses": "I don't see any major weakness in this paper except for that the authors can perhaps write down the pseudo code of their algorithm to make the inter-components interactions more explicit.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "HK88nD5HRB", "reviewer": "Reviewer_SGTy", "summary": "In this paper the authors present the LEGO-Prover, a theorem-prover which employs a growing library containing verified lemmas as building blocks to increase the capability of the LLMs (ChatGPT) used in theorem proving. \nThe LEGO-Prover enables LLMs to utilize existing results retrieved from the library and to create new results during the theorem-proving process.\nThe proposed approach is also favourably evaluated experimentally.\n\n========================= Update after rebuttal =================================================\nI am happy to raise my score in the light of the new information provided by the authors during the rebuttal phase and the discussion.", "questions": "The ablation study seems to point to the usefulness of the skills library in improving the performance of the LEGO-prover. However, what is the computational cost of building and maintaining such a library? This is not discussed in the paper.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1) The modularity of the approach allows for breaking proofs into intermediate steps and for building proofs bottom-to-top from simpler lemmas to complex theorems.\n\n2) The related work is analysed in depth.\n\n3) The ablation study seems to point to the fact that the skill library actually makes a difference, even though the authors might actually be overselling it, as at test time, this is only about 1%.", "weaknesses": "1) The paper refers a lot to the figures, but these are not always explained in detail and they are quite complex to understand, with a lot of different components. Figures can be used as a support for the text, but not as a replacement.\n\n2) The comparison with Thor+expert iteration and Draft, sketch, and Prove might not be completely fair, as these make use of GPT-3 instead of ChatGPT. \n\n3) It would be helpful to have the workings of the LEGO-prover presented in some algorithmic way, in order to have an overview of the whole pipeline.\n\n\nMinor: there is a missing cross-ref on p. 8.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "OGRwWfgmEd", "reviewer": "Reviewer_Nn2P", "summary": "The prior work on theorem proving enhanced by LLMs (or, more generally, machine learning) has a problem that only the fixed library of theorems can be assumed. To solve this drawback, the paper proposes LEGO-Prover, which in parallel grows the library of proven theorems for reuse (called skills in the paper) and proves the theorems of interest. LEGO-Prover utilizes LLMs to retrieve skills from the growing library and decompose overall informal theorems into small snippets in a step-by-step style.\n\n== POST-REBUTTAL ==\nI raised my rating from 6 to 8 because the response addressed my major concerns.", "questions": "- Is miniF2F split just for comparison with the prior works which use miniF2F-valid and miniF2F-test?\n- Is it possible to discuss why the performance of LEGO-Prover on miniF2F-test is not so good as on miniF2F-valid?\n- Where can I find Zhao et al. (2023) employ 100 attempts of proving in their experiment?\n- Why does Table 1 include cells not having numbers? Can they be filled?\n- Figure 3 (a) shows that the difference between LEGO-prover and the version without the growing skill library is stable even when the number of prover attempts changes. Does this mean the use of the growing skill library is effective only in proving of theorems with short proofs? If not, what other reasons can be considered?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 4, "strengths": "- The paper addresses a new problem of how (automation of) theorem proving can be enhanced under a growing library of proven theorems (skills).\n- The paper utilizes LLMs to retrieve skills from a growing library effectively. The problem is that the grown library cannot be accessed during training. The paper addresses the issue by employing LLMs as an oracle telling useful skills in the growing library. Without a very general model like LLMs, the issue would become more challenging to solve.\n- The effectiveness of the proposed method is experimentally shown.", "weaknesses": "- I am unsure why the paper splits the miniF2F dataset into valid and test datasets, although the proposed method does not need training.\n- The proposed method outperforms the previous approaches significantly on miniF2F-valid, but the difference on miniF2F-test is smaller. The paper does not discuss this point.\n- The paper says, \"Consistent with the (Jiang et al. 2022b; Zhao et al., 2023), each problem undergoes 100 attempts of proving,\" but I cannot find such a setting in the paper of Zhao et al. (2023).\n- Table 1 includes cells that have no number (represented by \"-\"), but there is no explanation nor justification for it.\n- (Minor) The presentation can be improved. The figures in the paper include code fragments, but it is difficult to read and understand them due to the small font size and the lack of explanation. Regarding the latter, for instance, I cannot find, in Figure 1(b), where the retrieved and new skills go to and come from, respectively.\n- (Minor) The text can be improved. The paper seems to have several missing citations and incorrect references (e.g., I think \"Figure 3(b)\" on page 9 should correctly be \"Figure 4\"). Another issue is that the paper cites the author names of the prior work even where it cites the paper, and vice versa (e.g., \"Subgoal-Learning Zhao et al. (2023)\" on page 7 should correctly be \"Subgoal-Learning (Zhao et al. 2023)\").", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "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": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (oral)