internlm/internlm2_5-step-prover
5157
InternLM2.5-Step-Prover
<div align="center">
<img src="https://raw.githubusercontent.com/InternLM/InternLM/main/assets/logo.svg" width="200"/> <div> </div> <div align="center"> <b><font size="5">InternLM-Math</font></b> <sup> <a href="https://internlm.intern-ai.org.cn/"> <i><font size="4">HOT</font></i> </a> </sup> <div> </div> </div>
A state-of-the-art LEAN4 step prover.
💻 Github 📊Dataset 📖 Paper </div>
InternLM2.5-Step-Prover is a 7B language model which achieves state-of-the-art performances on MiniF2F, ProofNet, and Putnam math benchmarks, showing its formal math proving ability in multiple domains.
Dialogue Example
### Input template
f"---\nNAME: {theorem.full_name}\n\n"
f"---\nPROOF_BEFORE: {proof_before}\n\n"
f"---\nSTATE_BEFORE: {state}\n\n"
f"---\nTACTIC: "
### Input example
---
NAME: square_sub_one_divisible_eight
---
PROOF_BEFORE: rw [h, pow_two]
---
STATE_BEFORE: m n : N
h : n = 2 * m + 1
⊢ 8 | (2 * m + 1) * (2 * m + 1) - 1
---
TACTIC:
### Output example
rw [← Nat.mod_add_div (2 * m + 1) 8]If you want to use critic model, please refer critic's model page.
Performance
MiniF2F
Proofnet & Putnam
Citation and Tech Report
@misc{wu2024internlm25stepproveradvancingautomatedtheorem,
title={InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems},
author={Zijian Wu and Suozhi Huang and Zhejian Zhou and Huaiyuan Ying and Jiayu Wang and Dahua Lin and Kai Chen},
year={2024},
eprint={2410.15700},
archivePrefix={arXiv},
primaryClass={cs.AI},
url={https://arxiv.org/abs/2410.15700},
}