DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909288037875712 |
|---|---|
| author | Xin, Huajian Ren, Z. Z. Song, Junxiao Shao, Zhihong Zhao, Wanjia Wang, Haocheng Liu, Bo Zhang, Liyue Lu, Xuan Du, Qiushi Gao, Wenjun Zhu, Qihao Yang, Dejian Gou, Zhibin Wu, Z. F. Luo, Fuli Ruan, Chong |
| author_facet | Xin, Huajian Ren, Z. Z. Song, Junxiao Shao, Zhihong Zhao, Wanjia Wang, Haocheng Liu, Bo Zhang, Liyue Lu, Xuan Du, Qiushi Gao, Wenjun Zhu, Qihao Yang, Dejian Gou, Zhibin Wu, Z. F. Luo, Fuli Ruan, Chong |
| contents | We introduce DeepSeek-Prover-V1.5, an open-source language model designed for theorem proving in Lean 4, which enhances DeepSeek-Prover-V1 by optimizing both training and inference processes. Pre-trained on DeepSeekMath-Base with specialization in formal mathematical languages, the model undergoes supervised fine-tuning using an enhanced formal theorem proving dataset derived from DeepSeek-Prover-V1. Further refinement is achieved through reinforcement learning from proof assistant feedback (RLPAF). Beyond the single-pass whole-proof generation approach of DeepSeek-Prover-V1, we propose RMaxTS, a variant of Monte-Carlo tree search that employs an intrinsic-reward-driven exploration strategy to generate diverse proof paths. DeepSeek-Prover-V1.5 demonstrates significant improvements over DeepSeek-Prover-V1, achieving new state-of-the-art results on the test set of the high school level miniF2F benchmark ($63.5\%$) and the undergraduate level ProofNet benchmark ($25.3\%$). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_08152 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search Xin, Huajian Ren, Z. Z. Song, Junxiao Shao, Zhihong Zhao, Wanjia Wang, Haocheng Liu, Bo Zhang, Liyue Lu, Xuan Du, Qiushi Gao, Wenjun Zhu, Qihao Yang, Dejian Gou, Zhibin Wu, Z. F. Luo, Fuli Ruan, Chong Computation and Language Artificial Intelligence Machine Learning Logic in Computer Science We introduce DeepSeek-Prover-V1.5, an open-source language model designed for theorem proving in Lean 4, which enhances DeepSeek-Prover-V1 by optimizing both training and inference processes. Pre-trained on DeepSeekMath-Base with specialization in formal mathematical languages, the model undergoes supervised fine-tuning using an enhanced formal theorem proving dataset derived from DeepSeek-Prover-V1. Further refinement is achieved through reinforcement learning from proof assistant feedback (RLPAF). Beyond the single-pass whole-proof generation approach of DeepSeek-Prover-V1, we propose RMaxTS, a variant of Monte-Carlo tree search that employs an intrinsic-reward-driven exploration strategy to generate diverse proof paths. DeepSeek-Prover-V1.5 demonstrates significant improvements over DeepSeek-Prover-V1, achieving new state-of-the-art results on the test set of the high school level miniF2F benchmark ($63.5\%$) and the undergraduate level ProofNet benchmark ($25.3\%$). |
| title | DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search |
| topic | Computation and Language Artificial Intelligence Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2408.08152 |