Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , , , , , , , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909970762563584 |
|---|---|
| author | Chen, Jiangjie Chen, Wenxiang Du, Jiacheng Hu, Jinyi Jiang, Zhicheng Jie, Allan Jin, Xiaoran Jin, Xing Li, Chenggang Shi, Wenlei Wang, Zhihong Wang, Mingxuan Wei, Chenrui Wei, Shufa Xin, Huajian Yang, Fan Gao, Weihao Yuan, Zheng Zhan, Tianyang Zheng, Zeyu Zhou, Tianxi Zhu, Thomas Hanwen |
| author_facet | Chen, Jiangjie Chen, Wenxiang Du, Jiacheng Hu, Jinyi Jiang, Zhicheng Jie, Allan Jin, Xiaoran Jin, Xing Li, Chenggang Shi, Wenlei Wang, Zhihong Wang, Mingxuan Wei, Chenrui Wei, Shufa Xin, Huajian Yang, Fan Gao, Weihao Yuan, Zheng Zhan, Tianyang Zheng, Zeyu Zhou, Tianxi Zhu, Thomas Hanwen |
| contents | Large language models have recently made significant progress to generate rigorous mathematical proofs. In contrast, utilizing LLMs for theorem proving in formal languages (such as Lean) remains challenging and computationally expensive, particularly when addressing problems at the undergraduate level and beyond. In this work, we present \textbf{Seed-Prover 1.5}, a formal theorem-proving model trained via large-scale agentic reinforcement learning, alongside an efficient test-time scaling (TTS) workflow. Through extensive interactions with Lean and other tools, the model continuously accumulates experience during the RL process, substantially enhancing the capability and efficiency of formal theorem proving. Furthermore, leveraging recent advancements in natural language proving, our TTS workflow efficiently bridges the gap between natural and formal languages. Compared to state-of-the-art methods, Seed-Prover 1.5 achieves superior performance with a smaller compute budget. It solves \textbf{88\% of PutnamBench} (undergraduate-level), \textbf{80\% of Fate-H} (graduate-level), and \textbf{33\% of Fate-X} (PhD-level) problems. Notably, using our system, we solved \textbf{11 out of 12 problems} from Putnam 2025 within 9 hours. Our findings suggest that scaling learning from experience, driven by high-quality formal feedback, holds immense potential for the future of formal mathematical reasoning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_17260 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience Chen, Jiangjie Chen, Wenxiang Du, Jiacheng Hu, Jinyi Jiang, Zhicheng Jie, Allan Jin, Xiaoran Jin, Xing Li, Chenggang Shi, Wenlei Wang, Zhihong Wang, Mingxuan Wei, Chenrui Wei, Shufa Xin, Huajian Yang, Fan Gao, Weihao Yuan, Zheng Zhan, Tianyang Zheng, Zeyu Zhou, Tianxi Zhu, Thomas Hanwen Computation and Language Large language models have recently made significant progress to generate rigorous mathematical proofs. In contrast, utilizing LLMs for theorem proving in formal languages (such as Lean) remains challenging and computationally expensive, particularly when addressing problems at the undergraduate level and beyond. In this work, we present \textbf{Seed-Prover 1.5}, a formal theorem-proving model trained via large-scale agentic reinforcement learning, alongside an efficient test-time scaling (TTS) workflow. Through extensive interactions with Lean and other tools, the model continuously accumulates experience during the RL process, substantially enhancing the capability and efficiency of formal theorem proving. Furthermore, leveraging recent advancements in natural language proving, our TTS workflow efficiently bridges the gap between natural and formal languages. Compared to state-of-the-art methods, Seed-Prover 1.5 achieves superior performance with a smaller compute budget. It solves \textbf{88\% of PutnamBench} (undergraduate-level), \textbf{80\% of Fate-H} (graduate-level), and \textbf{33\% of Fate-X} (PhD-level) problems. Notably, using our system, we solved \textbf{11 out of 12 problems} from Putnam 2025 within 9 hours. Our findings suggest that scaling learning from experience, driven by high-quality formal feedback, holds immense potential for the future of formal mathematical reasoning. |
| title | Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience |
| topic | Computation and Language |
| url | https://arxiv.org/abs/2512.17260 |