Source-linked AI summary
LEGO-Prover: Neural Theorem Proving with Growing Libraries
Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, Xiaodan Liang
TL;DR
The paper addresses the difficulty of formal theorem proving when language-model provers struggle with long proofs and rely on fixed theorem libraries. LEGO-Prover grows a verified skill library through modular proof construction and skill evolution, improving miniF2F results while accumulating reusable lemmas.
Problem
Language-model theorem provers struggle with difficult proofs, while prior methods commonly assume a fixed theorem library during proving.
Method
LEGO-Prover decomposes proofs into blocks, retrieves verified lemmas, creates new skills, and evolves them for greater reusability.
Results
LEGO-Prover improves over prior search-based and LLM-based methods, achieving 52.4% and 45.5% pass rates with model-generated informal proofs on miniF2F-valid and test.
Takeaways & Limitations
The growing library reaches 22,532 skills, and ablations show that newly added skills help prove theorems.
Takeaways & Limitations
Directly reusable skills solve few substantial problems because many miniF2F problems are trivial without a skill reference.
Abstract
from arXiv · showhide
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 47.1%). During the proving process, LEGO-Prover also manages to generate 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 an improvement from a success rate of 47.1% to 50.4%. We also release our code and all the generated skills.
1 INTRODUCTION
LEGO-Prover addresses the difficulty of long-chain theorem proving by constructing proofs modularly with a growing library of verified skills. It improves miniF2F performance while generating thousands of reusable lemmas.
- 1 INTRODUCTION: Neural theorem proving primarily uses either step-by-step proof generation with search or single-decoding construction of entire proofs.
- 1 INTRODUCTION: LEGO-Prover constructs proofs modularly by retrieving useful lemmas, adding newly constructed lemmas, and evolving skills for reusability.Its prover and evolver are bridged by a growing skill library.
- 1 INTRODUCTION: 57.0% and 50.0% pass rates were achieved on miniF2F-valid and miniF2F-test, with a 6.75% average absolute improvement over prior state of the art.
- 1 INTRODUCTION: 22,532 verified skills were accumulated, including broadly applicable high-level lemmas examined through case studies and ablations.
2 RELATED WORKS
Machine-learning research in formal mathematics combines interactive theorem provers with language-model-based proof search and formalization. Related work also includes autoformalization and skill-accumulating language-model agents.
- 2 RELATED WORKS: Interactive theorem provers provide formal languages, verification, and automated proving tools for machine-assisted mathematical proof construction.
- 2 RELATED WORKS: Proof-search systems use language models for single-step actions while tree search finds sequences of correct proof steps.
- 2 RELATED WORKS: Autoformalization methods translate natural-language mathematics into formal theorem statements or proofs using supervised, unsupervised, and language-model techniques.
- 2 RELATED WORKS: Skill-based language-model agents combine task planning, logical reasoning, and skill accumulation to perform complex tasks.
3 METHOD
LEGO-Prover combines a retrievable verified-lemma library with a prover that decomposes and formalizes proofs and an evolver that expands skill reusability. Isabelle verifies generated code and filters the evolving library.
- 3 METHOD: The method has a prover for block-by-block proof construction and an evolver that refines or solves skills, linked through a growing skill library.
- 3.1 SKILL LIBRARY: The skill library uses vector stores for verified lemmas, decomposer requests, and related retrieval documents encoded with embeddings.
- 3.2 PROVER: The prover drafts an informal solution, decomposes it into structured steps and formal subgoals, retrieves lemmas, and formalizes the proof.
- 3.2 PROVER: The formalizer retrieves nf skills using decomposer requests and the formal problem statement, then prompts an LLM to generate a complete Isabelle source file.
- 3 METHOD: Generated proof code and evolved skills are verified with Isabelle, while heuristic tactics and Sledgehammer support correction when tactics fail.
- 3 METHOD: The evolver generalizes skills through four directions and directly solves prover requests to create new lemmas.
4 EXPERIMENTS
LEGO-Prover is evaluated on miniF2F with Isabelle against prior neural and search-based theorem provers, including ablations of its growing skill library. The experiments also examine how generated skills are used and evolved.
- 4.1 EXPERIMENTAL SETUP: The evaluation uses 488 miniF2F problems split evenly into valid and test sets, with Isabelle formal statements, informal statements, and human-written proofs.PISA provides the interface for verifying Isabelle code and returning proof states or error messages.
- 4.2 MAIN RESULT: LLM-based methods outperform search-based methods by around 4.7%, whose short generated proof steps expand the search space and hinder long-proof discovery.The baselines include Thor variants, Draft, Sketch, and Prove, and Subgoal-Learning.
- 4.2 MAIN RESULT: 257 of 488 problems were solved with human-written informal proofs, improving over Subgoal-Learning by 7.3% on miniF2F-valid and 4.5% on miniF2F-test.With model-generated informal proofs, pass rates were 52.4% and 45.5% on valid and test, respectively.
- 4.2 MAIN RESULT: LEGO-Prover achieves 50.4% on the validation set with a growing skill library, compared with 47.1% without it after 50 attempts.The ablation removes the evolver and growing library to measure their contribution.
- 4.3.2 HOW DOES THE SKILL BOOST THE ABILITY OF LLMS?: Skills support proof construction either as directly copied verified lemmas or as reference examples for synthesizing new lemmas and formal proof steps.The directly reusable-block mode is reliable because Isabelle verifies every skill, while reference skills provide clues for formalization.
- 4.3.2 HOW DOES THE SKILL BOOST THE ABILITY OF LLMS?: Directly reused skills are not substantial across solved problems because many miniF2F problems can be solved without any skill reference.This limits the share of problems attributable to the most direct form of skill reuse.
5 CONCLUSIONS
LEGO-Prover uses a growing skill library to formalize proofs block by block, while its prover and evolver retrieve, solve, refine, and create lemmas. Experiments and ablations support the effectiveness of this design.
- 5 CONCLUSIONS: LEGO-Prover proves theorems block by block with a growing library, rather than attempting to complete each proof at once.The prover decomposes problems into subgoal lemmas, while the evolver resolves requests and evolves existing skills.
- 5 CONCLUSIONS: The prover uses refined structural informal proofs and retrieved lemmas, while the evolver creates new skills or refines existing ones.The two components are coordinated through the growing skill library.
- 5 CONCLUSIONS: Extensive tests, ablations, and detailed analyses report improved miniF2F pass rates and effectiveness for the proposed components.
J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM,
This material consists of references to prior work spanning automated reasoning, language models, theorem proving, formal mathematics, and related AI systems.
- RELATED WORK: The cited literature covers theorem provers, proof search, autoformalization, and neural methods for formal mathematics.
- RELATED WORK: The references also include large language models, attention architectures, embodied agents, and self-play systems related to neural reasoning and skill accumulation.
A.1 PROMPT EXAMPLES
This section presents prompt examples for LEGO-Prover’s decomposer, formalizer, and evolver, including directional skill evolution and theorem-solving requests.
- Prompt overview: The prompts cover decomposition, formalization, solving requests, and directional evolution within LEGO-Prover.The decomposer and formalizer serve the prover, while the directional evolver and request solver serve the evolver.
- Directional evolve: Directional-evolution prompts replace a core description with direction-specific instructions for generating evolved skills.The described directions include extending dimensions, identifying key concepts, parameterizing, and increasing complexity.
- Decomposer: The decomposer prompt uses theorem statements and informal proofs to produce structured proof steps and formal goals.Its intended alignment with Isabelle proof code is illustrated through a logarithm example using AM-GM.
- Request solver: The examples also include prompts that modify existing lemmas or definitions to aid solving related Isabelle problems.The request-solving prompt frames this modification task around reference problems and an evolution description.