--- title: "InternLM2.5-StepProver — paper by Wu et al. (2024)" description: "The authors also release a large set of new machine-checked solutions. 1 reference, cited by 58 papers here." authors: ["Zijian Wu", "Suozhi Huang", "Zhejian Zhou", "Huaiyuan Ying", "Zheng Yuan", "Wenwei Zhang", "Dahua Lin", "Kai Chen"] year: 2024 venue: "arXiv:2410.15700" source: "https://arxiv.org/abs/2410.15700" doi: "10.48550/arxiv.2410.15700" arxiv: "2410.15700" licence: "CC BY 4.0 (arXiv)" licence_url: "https://creativecommons.org/licenses/by/4.0/" summary_licence: "Elamur Cosmic License" canonical: "https://research.elamur.ai/free/en/papers/wu-2024-internlm2-5-stepprover-advancing-automated/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/wu-2024-internlm2-5-stepprover-advancing-automated/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/7/) / InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search # InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search **Authors:** [Zijian Wu](https://md.research.elamur.ai/free/en/authors/zijian-wu/), Suozhi Huang, [Zhejian Zhou](https://md.research.elamur.ai/free/en/authors/zhejian-zhou/), [Huaiyuan Ying](https://md.research.elamur.ai/free/en/authors/huaiyuan-ying/), [Zheng Yuan](https://md.research.elamur.ai/free/en/authors/zheng-yuan/), [Wenwei Zhang](https://md.research.elamur.ai/free/en/authors/wenwei-zhang/), [Dahua Lin](https://md.research.elamur.ai/free/en/authors/dahua-lin/) and [Kai Chen](https://md.research.elamur.ai/free/en/authors/kai-chen/) · **Year:** 2024 · **Venue:** arXiv:2410.15700 · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/) **Links:** [Publisher's page](https://arxiv.org/abs/2410.15700) · [PDF](https://arxiv.org/pdf/2410.15700v2) · [DOI 10.48550/arxiv.2410.15700](https://doi.org/10.48550/arxiv.2410.15700) · [arXiv 2410.15700](https://arxiv.org/abs/2410.15700) · [OpenAlex](https://openalex.org/W4404088889) **Citations:** 1 citations (OpenAlex, 2026-10-14) · [58](https://md.research.elamur.ai/free/en/papers/wu-2024-internlm2-5-stepprover-advancing-automated/cited-by/) in our library, of the 149,439 papers whose bibliographies we read ## Summary Most LLM theorem provers for LEAN build a proof one tactic at a time. They pick which proof state to expand next using the prover's own log-probabilities. That signal gets unreliable as proofs get longer, so these systems rarely find deep proofs. The authors add a separate critic model that scores each proof state. They train it on preference pairs taken from earlier search trees: states nearer to a finished proof beat their parents, and states on a successful path beat sibling branches that went nowhere. The critic then decides which states the prover explores. Starting from InternLM2-StepProver, they ran a large expert-iteration campaign on Lean-workbook-plus, using more than 20,000 CPU days, and retrained both the prover and the critic as new proofs came in. With critic guidance, the prover's miniF2F score rose from 59.4% to 65.9%, and it found much longer proofs. The work shows that structured value guidance helps formal proof search go deeper. The authors also release a large set of new machine-checked solutions. ## Key points - **Critic-guided search (CG):** the critic is trained in a ranking style similar to RLHF reward models, using "path pairs" and "sibling pairs" rather than binary provable/unprovable labels. The first critic was trained on about 8,000 pairs. - **miniF2F results:** best-first search alone scores 59.4%. CG alone reaches 65.6%, and combining BF+CG reaches 65.9%. On ProofNet, BF solves 22.3%, CG 23.9% and the hybrid 27.0%. - **Lean-workbook-plus:** 17.0% of the problems were resolved in total (10,880 proved and 3,195 disproved), up from 9.5% for InternLM2-StepProver. The solutions are released openly. - **Deeper proofs:** shortest proofs average 1.66 tactics with BF and 4.44 with CG. With large budgets BF behaves almost like brute force, while CG goes beyond the log-linear trend in solved problems versus compute. - **Limitations:** the work focuses on competition-style math, and there is no stable metric yet for evaluating critic models. About 98.5% of the CPU time went to problems that were never solved. *Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.* ## Institutions - [Shanghai Artificial Intelligence Laboratory](https://md.research.elamur.ai/free/en/labs/shanghai-artificial-intelligence-laboratory/) — Research institute, Shanghai, China · 152 works · 13,166 citations 📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works 🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works ## Cite Cite as: Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Zheng Yuan, Wenwei Zhang, Dahua Lin and Kai Chen. 2024. InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search. arXiv:2410.15700. The paper itself, not this page. BibTeX from the library's record of the work. ```bibtex @misc{wu2024internlm2, title = {{InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search}}, author = {Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Zheng Yuan, Wenwei Zhang, Dahua Lin and Kai Chen}, year = {2024}, doi = {10.48550/arxiv.2410.15700}, eprint = {2410.15700}, archivePrefix = {arXiv}, url = {https://doi.org/10.48550/arxiv.2410.15700} } ``` - [← previous Instruction Pre-Training: Language Models are Supervised Multitask Learners](https://md.research.elamur.ai/free/en/papers/cheng-2024-instruction-pre-training-language-models/) - [next → Language Models are Homer Simpson! Safety Re-Alignment of Fine-tuned Language Models through Task Arithmetic](https://md.research.elamur.ai/free/en/papers/bhardwaj-2024-language-models-are-homer-simpson/) - [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/7/) ## References 1 references, 1 of them with a card of ours. ↗ leads to the work. 1. nal critic model. The models are trained with a state-tactic paradigm via expert iteration on a large-scale LEAN dataset. Anthony, T., Tian, Z., and Barber, D. [Thinking fast and slow with deep learning and tree search](https://md.research.elamur.ai/free/en/papers/anthony-2017-thinking-fast-slow-deep-learning/). In Guyon, I., Luxburg, U. V., Bengio, S., Wallach, H., Fergus, R., Vishwanathan,… *Updated 2 November 2026*