REVIEW 14 cited by
LEGO-Prover: Neural Theorem Proving with Growing Libraries
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original 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 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.
Forward citations
Cited by 14 Pith papers
-
Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language
Introduces Relaxed NFL intermediate language for LLM-based auto-formalization, with rule-plus-LLM elaboration to Core NFL and tactic-language discharge of verification conditions.
-
Formalizing Mathematics at Scale
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable for...
-
Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
Proof-state snapshotting in Lean 4 delivers 5.6-50x wall-time speedups (average 14x) on 48 miniF2F-v2 problems by reusing elaborated states and avoiding repeated import loading and theorem-body elaboration.
-
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
An RL-guided MCTS proof search for Tamarin finds more and shorter proofs than standard search across 16 protocol models.
-
LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation
LiveFMBench shows that direct LLM prompting for C program formal specs overestimates accuracy by ~20% due to unfaithful behaviors like deceiving provers, while agentic workflows help under low sampling but overall per...
-
StepFun-Prover Preview: Let's Think and Verify Step by Step
A reinforcement learning pipeline with Lean verifier feedback trains a 32B model that scores 70.0% pass@1 on miniF2F-test, a new state of the art.
-
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
Kimina-Prover achieves 80.7% pass@8192 on miniF2F for Lean 4 theorem proving via RL training and a formal reasoning pattern that emulates iterative human-style proof refinement.
-
Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
Autoformalization should target complete theories—axioms, definitions, lemmas, proofs—as unified formal libraries, not isolated statements.
-
Solving Formal Math Problems by Decomposition and Iterative Reflection
An agent that decomposes Lean 4 goals into subproblems and iteratively repairs proofs achieves a 95.9% pass rate on miniF2F-test using a stock Gemini model.
-
A Compute-Matched Re-Evaluation of TroVE on MATH
After matching computational budget, TroVE's toolbox mechanism yields only a marginal, statistically non-significant 1% accuracy gain over a plain sampling baseline on MATH.
-
Clarifying Before Reasoning: A Coq Prover with Structural Context
Enriching LLM theorem-proving prompts with Coq's internal type representations and natural-language explanations raises proof success from 21.8% to 45.8%, surpassing Graph2Tac's 33.2%.
-
IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus
Improved IsabeLLM adds RAG, error tracing, and Isabelle compatibility updates and is tested on verifying Bitcoin Proof of Work consensus.
-
Rethinking Wireless Communications through Formal Mathematical AI Reasoning
Proposes a three-layer framework using formal AI reasoning for verification, derivation, and discovery in wireless communications theory.
-
A Survey of Self-Evolving Agents: What, When, How, and Where to Evolve on the Path to Artificial Super Intelligence
The paper delivers the first systematic review of self-evolving agents, structured around what components evolve, when adaptation occurs, and how it is implemented.
Discussion (0). Sign in to comment.