InternLM-Math
commited on
Commit
•
9e24972
1
Parent(s):
4e4cfb0
Update README.md
Browse files
README.md
CHANGED
@@ -25,7 +25,7 @@ tags:
|
|
25 |
|
26 |
A state-of-the-art LEAN4 step prover.
|
27 |
|
28 |
-
[💻 Github](https://github.com/InternLM/InternLM-Math) [📊Dataset](https://huggingface.co/datasets/internlm/Lean-Github)
|
29 |
</div>
|
30 |
|
31 |
InternLM-Step-Prover is a 7B language model trained on Lean-Github and multiple sythesis datasets. InternLM-Step-Prover achieves state-of-the-art performances on MiniF2F, ProofNet, and Putnam math benchmarks, showing its formal math proving ability in multiple domains.
|
@@ -88,4 +88,15 @@ PROOFSTEP induction n with t Ht
|
|
88 |
| ReProver | 229M | 1 | 0/640 |
|
89 |
| InternLM2-Step-Prover | 7B | 1 | **5/640** |
|
90 |
|
91 |
-
# Citation and Tech Report
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
25 |
|
26 |
A state-of-the-art LEAN4 step prover.
|
27 |
|
28 |
+
[💻 Github](https://github.com/InternLM/InternLM-Math) [📊Dataset](https://huggingface.co/datasets/internlm/Lean-Github) [📖 Paper](https://arxiv.org/abs/2407.17227)
|
29 |
</div>
|
30 |
|
31 |
InternLM-Step-Prover is a 7B language model trained on Lean-Github and multiple sythesis datasets. InternLM-Step-Prover achieves state-of-the-art performances on MiniF2F, ProofNet, and Putnam math benchmarks, showing its formal math proving ability in multiple domains.
|
|
|
88 |
| ReProver | 229M | 1 | 0/640 |
|
89 |
| InternLM2-Step-Prover | 7B | 1 | **5/640** |
|
90 |
|
91 |
+
# Citation and Tech Report
|
92 |
+
```
|
93 |
+
@misc{wu2024leangithubcompilinggithublean,
|
94 |
+
title={LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover},
|
95 |
+
author={Zijian Wu and Jiayu Wang and Dahua Lin and Kai Chen},
|
96 |
+
year={2024},
|
97 |
+
eprint={2407.17227},
|
98 |
+
archivePrefix={arXiv},
|
99 |
+
primaryClass={cs.AI},
|
100 |
+
url={https://arxiv.org/abs/2407.17227},
|
101 |
+
}
|
102 |
+
```
|