REVIEW 9 cited by
Leanabell-Prover: Posttraining Scaling in Formal Reasoning
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
Recent advances in automated theorem proving (ATP) through LLMs have highlighted the potential of formal reasoning with Lean 4 codes. However, ATP has not yet be revolutionized by the recent posttraining scaling as demonstrated by Open AI O1/O3 and Deepseek R1. In this work, we investigate the entire posttraining of ATP, aiming to align it with breakthroughs in reasoning models in natural languages. To begin, we continual train current ATP models with a hybrid dataset, which consists of numerous statement-proof pairs, and additional data aimed at incorporating cognitive behaviors that emulate human reasoning and hypothesis refinement. Next, we explore reinforcement learning with the use of outcome reward returned by Lean 4 compiler. Through our designed continual training and reinforcement learning processes, we have successfully improved existing formal provers, including both DeepSeek-Prover-v1.5 and Goedel-Prover, achieving state-of-the-art performance in the field of whole-proof generation. For example, we achieve a 59.8% pass rate (pass@32) on MiniF2F. This is an on-going project and we will progressively update our findings, release our data and training details.
Forward citations
Cited by 9 Pith papers
-
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.
-
SCOPE: Leveraging Subgoal Critiques for Code Generation
A Lean-oriented prover model, fine-tuned with dense and sparse RL rewards, generates structured semantic critiques that improve LLM code generation accuracy over Reflexion and Self-Refine on LiveCodeBench V6 and BigCodeBench.
-
A Task-Centric Theory for Iterative Self-Improvement with Easy-to-Hard Curricula
Iterative self-improvement provably keeps improving only when initial performance lies in a moderate difficulty interval, and easy-to-hard curricula beat fixed mixtures under moderate difficulty separation and suffici...
-
Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure
A pipeline combining template-guided LLM informalization, a premise library, and structure-aware recursive summarization translates Lean proofs into natural language, scoring 0.857 key-point recall in a small author-c...
-
Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
An inference-only neuro-symbolic pipeline, DSP+, solves 80.7% of miniF2F and the previously unsolved imo_2019_p1, matching heavily RL-trained theorem provers without fine-tuning.
-
LogicPuzzleRL: Cultivating Robust Mathematical Reasoning in LLMs via Reinforcement Learning
Reinforcement learning on seven verifiable logic puzzles improves LLM accuracy on out-of-distribution math benchmarks, especially mid-difficulty problems.
-
Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening
GRPO's rank bias reinforces likely answers and neglects rare correct proofs; an unlikeliness reward that down-weights likely correct samples improves pass@N in formal theorem proving.
-
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.
-
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.
Discussion (0). Continue with ORCID to comment.