REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918215579336704 |
|---|---|
| author | Shen, Ziju Huang, Naohao Yang, Fanyi Wang, Yutong Gao, Guoxiong Xu, Tianyi Jiang, Jiedong He, Wanyi Yang, Pu Sun, Mengzhou Ju, Haocheng Wu, Peihao Dai, Bryan Dong, Bin |
| author_facet | Shen, Ziju Huang, Naohao Yang, Fanyi Wang, Yutong Gao, Guoxiong Xu, Tianyi Jiang, Jiedong He, Wanyi Yang, Pu Sun, Mengzhou Ju, Haocheng Wu, Peihao Dai, Bryan Dong, Bin |
| contents | Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this paper, we present REAL-Prover, a new open-source stepwise theorem prover for Lean 4 to push this boundary. This prover, based on our fine-tuned large language model (REAL-Prover-v1) and integrated with a retrieval system (Leansearch-PS), notably boosts performance on solving college-level mathematics problems. To train REAL-Prover-v1, we developed HERALD-AF, a data extraction pipeline that converts natural language math problems into formal statements, and a new open-source Lean 4 interactive environment (Jixia-interactive) to facilitate synthesis data collection. In our experiments, our prover using only supervised fine-tune achieves competitive results with a 23.7% success rate (Pass@64) on the ProofNet dataset-comparable to state-of-the-art (SOTA) models. To further evaluate our approach, we introduce FATE-M, a new benchmark focused on algebraic problems, where our prover achieves a SOTA success rate of 56.7% (Pass@64). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_20613 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning Shen, Ziju Huang, Naohao Yang, Fanyi Wang, Yutong Gao, Guoxiong Xu, Tianyi Jiang, Jiedong He, Wanyi Yang, Pu Sun, Mengzhou Ju, Haocheng Wu, Peihao Dai, Bryan Dong, Bin Computation and Language Artificial Intelligence Machine Learning Logic in Computer Science Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this paper, we present REAL-Prover, a new open-source stepwise theorem prover for Lean 4 to push this boundary. This prover, based on our fine-tuned large language model (REAL-Prover-v1) and integrated with a retrieval system (Leansearch-PS), notably boosts performance on solving college-level mathematics problems. To train REAL-Prover-v1, we developed HERALD-AF, a data extraction pipeline that converts natural language math problems into formal statements, and a new open-source Lean 4 interactive environment (Jixia-interactive) to facilitate synthesis data collection. In our experiments, our prover using only supervised fine-tune achieves competitive results with a 23.7% success rate (Pass@64) on the ProofNet dataset-comparable to state-of-the-art (SOTA) models. To further evaluate our approach, we introduce FATE-M, a new benchmark focused on algebraic problems, where our prover achieves a SOTA success rate of 56.7% (Pass@64). |
| title | REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning |
| topic | Computation and Language Artificial Intelligence Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2505.20613 |