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

Paper · 2024 · Zijian Wu, Suozhi Huang, Zhejian Zhou et al.

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 LaboratoryShanghai ·

China152 works · 13,164 citations

Fields, topics and concepts

📚 Shelves 3Computer Science · 18,614 works Artificial Intelligence · 17,965 works Computational Theory and Mathematics · 321 works

🧭 Topics 1Reasoning · 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. DOI 10.48550/arxiv.2410.15700 · arXiv 2410.15700

@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}
}

References

1 references, 1 of them with a card of ours. ↗ leads to the work.

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. In Guyon, I., Luxburg, U. V., Bengio, S., Wallach, H., Fergus, R., Vishwanathan,…

Updated 2 November 2026

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wu-2024-internlm2-5-stepprover-advancing-automated/