# InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search

arXiv: https://arxiv.org/abs/2410.15700 · HTML: https://mlsanity.com/paper/2410.15700/

## Key facts

- Cited by 34 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 24 references that are in the map.
- First posted on arXiv 21 Oct 2024.

## Builds on (most cited first, 20 of 20)

- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Math-Shepherd: Verify and Reinforce LLMs Step-by-step without Human Annotations](https://mlsanity.com/paper/2312.08935/) (2023)
- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [Improve Mathematical Reasoning in Language Models by Automated Process Supervision](https://mlsanity.com/paper/2406.06592/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Thinking Fast and Slow with Deep Learning and Tree Search](https://mlsanity.com/paper/1705.08439/) (2017)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [ChatGLM-Math: Improving Math Problem-Solving in Large Language Models with a Self-Critique Pipeline](https://mlsanity.com/paper/2404.02893/) (2024)

## Built on by (most cited first, 30 of 34)

- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [A Survey of Frontiers in LLM Reasoning: Inference Scaling, Learning to Reason, and Agentic Systems](https://mlsanity.com/paper/2504.09037/) (2025)
- [Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening](https://mlsanity.com/paper/2506.02355/) (2025)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning](https://mlsanity.com/paper/2505.23754/) (2025)
- [Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skills](https://mlsanity.com/paper/2512.16301/) (2025)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://mlsanity.com/paper/2506.11487/) (2025)
- [StepFun-Prover Preview: Let's Think and Verify Step by Step](https://mlsanity.com/paper/2507.20199/) (2025)
- [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026)
- [Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability](https://mlsanity.com/paper/2505.23703/) (2025)
- [Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities](https://mlsanity.com/paper/2505.12680/) (2025)
- [Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving](https://mlsanity.com/paper/2506.17104/) (2025)
- [OProver: A Unified Framework for Agentic Formal Theorem Proving](https://mlsanity.com/paper/2605.17283/) (2026)
- [Diverse Inference and Verification for Advanced Reasoning](https://mlsanity.com/paper/2502.09955/) (2025)
- [FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4](https://mlsanity.com/paper/2503.03238/) (2025)
- [DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent](https://mlsanity.com/paper/2604.26311/) (2026)
- [RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation](https://mlsanity.com/paper/2505.22846/) (2025)
- [Whatever Remains Must Be True: Filtering Drives Reasoning in LLMs, Shaping Diversity](https://mlsanity.com/paper/2512.05962/) (2025)
- [Clarifying Before Reasoning: A Coq Prover with Structural Context](https://mlsanity.com/paper/2507.02541/) (2025)
- [InMind: Evaluating LLMs in Capturing and Applying Individual Human Reasoning Styles](https://mlsanity.com/paper/2508.16072/) (2025)
- [Discovering New Theorems via LLMs with In-Context Proof Learning in Lean](https://mlsanity.com/paper/2509.14274/) (2025)
- [EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving](https://mlsanity.com/paper/2509.12603/) (2025)
- [Neuro-Symbolic Proof Generation for Scaling Systems Software Verification](https://mlsanity.com/paper/2603.19715/) (2026)
- [A Theoretical Framework for Self-Play Theorem Proving Algorithms](https://mlsanity.com/paper/2606.01861/) (2026)
- [MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis](https://mlsanity.com/paper/2606.13782/) (2026)
- [LAMP: Lean-based Agentic framework with MCP and Proof Repair](https://mlsanity.com/paper/2606.28841/) (2026)
- [Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing](https://mlsanity.com/paper/2608.28639/) (2026)

## Abstract (arXiv)

Large Language Models (LLMs) have emerged as powerful tools in mathematical theorem proving, particularly when utilizing formal languages such as LEAN. A prevalent proof method involves the LLM prover iteratively constructing the proof tactic by tactic, typically following a best-first search scheme. However, this method often ignores the critical preference information inside the existing tactic trajectories, hindering the search for deeper proofs. We propose an intuitive yet effective method, which utilizes a critic model to capture the preference information and to guide the search of the prover model at runtime. Given the prover-critic framework, a large-scale expert iteration with more than 20,000 CPU days is then applied to further fine-tune the prover and the critic. The trained InternLM2.5-StepProver critic significantly boosts the performance of the prover model (59.4% to 65.9%). We also analyze the impact of the critic on various aspects of the theorem proving process during expert iteration, providing insights into its effectiveness. We open-source our models and searched proofs at https://github.com/InternLM/InternLM-Math and https://huggingface.co/datasets/internlm/Lean-Workbook.