REVIEW 9 cited by
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
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
Signed reviews
read the original abstract
Proving mathematical theorems using computer-verifiable formal languages like Lean significantly impacts mathematical reasoning. One approach to formal theorem proving involves generating complete proofs using Large Language Models (LLMs) based on Natural Language (NL) proofs. However, due to the scarcity of aligned NL and Formal Language (FL) theorem-proving data most modern LLMs exhibit suboptimal performance.This scarcity results in a paucity of methodologies for training LLMs and techniques to fully utilize their capabilities in composing formal proofs. To address these challenges, this paper proposes TheoremLlama, an end-to-end framework that trains a general-purpose LLM to be a Lean4 expert. TheoremLlama includes NL-FL dataset generation and bootstrapping method to obtain aligned dataset, curriculum learning and block training techniques to train the model, and iterative proof writing method to write Lean4 proofs that work together synergistically. Using the dataset generation method in TheoremLlama, we provide Open Bootstrapped Theorems (OBT), an NL-FL aligned and bootstrapped dataset. Our novel NL-FL bootstrapping method, where NL proofs are integrated into Lean4 code for training datasets, leverages the NL reasoning ability of LLMs for formal reasoning. The TheoremLlama framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets respectively, surpassing the GPT-4 baseline of 22.95% and 25.41%. Our code, model checkpoints, and the generated dataset is published in GitHub
Forward citations
Cited by 9 Pith papers
-
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
A dual-model framework that extracts proof sketches from whole-proof candidates and refines them with a tactic model and Sledgehammer, reaching 59.4 percent on miniF2F in Isabelle.
-
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
Formulates problem-solving as a sound Markov decision process, implements it in Lean as FPS and D-FPS, and introduces three formal problem-solving benchmarks plus the RPE answer-equivalence checker.
-
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
-
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
MATP-BENCH pairs 1,056 multimodal math problems with formal theorem statements in Lean 4, Coq, and Isabelle; the strongest tested model solves only 5.68% of Lean 4 end-to-end proving tasks at pass@10.
-
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
An open-source theorem-proving model reaches state-of-the-art scores on miniF2F (57.6% Pass@32) and PutnamBench by training on 800K formal proofs synthesized through autoformalization and expert iteration.
-
Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
Verifier-integrated reinforcement learning with multi-turn reflection improves 7B-scale Lean 4 theorem proving by 2 to 3 points on MiniF2F at pass@128.
-
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%.
-
Psychometric-Based Evaluation for Theorem Proving with Large Language Models
The authors annotate miniF2F theorems with LLM-computed difficulty and discrimination scores, then use adaptive testing to rank 10 theorem-proving LLMs using only about 23% of the theorems.
-
CoRT: Code-integrated Reasoning within Thinking
Inserting targeted hints into a few training examples teaches reasoning models to compute with Python instead of text, improving accuracy and cutting token use by 30 to 50 percent.
Discussion (0). Continue with ORCID to comment.