DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908455228407808 |
|---|---|
| author | Ren, Z. Z. Shao, Zhihong Song, Junxiao Xin, Huajian Wang, Haocheng Zhao, Wanjia Zhang, Liyue Fu, Zhe Zhu, Qihao Yang, Dejian Wu, Z. F. Gou, Zhibin Ma, Shirong Tang, Hongxuan Liu, Yuxuan Gao, Wenjun Guo, Daya Ruan, Chong |
| author_facet | Ren, Z. Z. Shao, Zhihong Song, Junxiao Xin, Huajian Wang, Haocheng Zhao, Wanjia Zhang, Liyue Fu, Zhe Zhu, Qihao Yang, Dejian Wu, Z. F. Gou, Zhibin Ma, Shirong Tang, Hongxuan Liu, Yuxuan Gao, Wenjun Guo, Daya Ruan, Chong |
| contents | We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3's step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model. The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. In addition to standard benchmarks, we introduce ProverBench, a collection of 325 formalized problems, to enrich our evaluation, including 15 selected problems from the recent AIME competitions (years 24-25). Further evaluation on these 15 AIME problems shows that the model successfully solves 6 of them. In comparison, DeepSeek-V3 solves 8 of these problems using majority voting, highlighting that the gap between formal and informal mathematical reasoning in large language models is substantially narrowing. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_21801 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition Ren, Z. Z. Shao, Zhihong Song, Junxiao Xin, Huajian Wang, Haocheng Zhao, Wanjia Zhang, Liyue Fu, Zhe Zhu, Qihao Yang, Dejian Wu, Z. F. Gou, Zhibin Ma, Shirong Tang, Hongxuan Liu, Yuxuan Gao, Wenjun Guo, Daya Ruan, Chong Computation and Language Artificial Intelligence We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3's step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model. The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. In addition to standard benchmarks, we introduce ProverBench, a collection of 325 formalized problems, to enrich our evaluation, including 15 selected problems from the recent AIME competitions (years 24-25). Further evaluation on these 15 AIME problems shows that the model successfully solves 6 of them. In comparison, DeepSeek-V3 solves 8 of these problems using majority voting, highlighting that the gap between formal and informal mathematical reasoning in large language models is substantially narrowing. |
| title | DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition |
| topic | Computation and Language Artificial Intelligence |
| url | https://arxiv.org/abs/2504.21801 |