DeepSeek-Prover-V1.5：証明アシスタントのフィードバックを活用した強化学習とモンテカルロ木探索

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

August 15, 2024

著者: Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, Chong Ruan

cs.AI

要旨

DeepSeek-Prover-V1.5を紹介します。これはLean 4における定理証明のために設計されたオープンソースの言語モデルで、DeepSeek-Prover-V1を改良し、学習と推論の両プロセスを最適化しています。このモデルは、形式的数学言語に特化したDeepSeekMath-Baseで事前学習され、DeepSeek-Prover-V1から派生した強化された形式的定理証明データセットを用いて教師ありファインチューニングが行われます。さらに、証明アシスタントからのフィードバックを用いた強化学習（RLPAF）を通じて洗練されています。DeepSeek-Prover-V1の単一パスでの証明全体生成アプローチを超えて、我々はRMaxTSを提案します。これは、多様な証明パスを生成するために、内発的報酬に基づく探索戦略を採用したモンテカルロ木探索の変種です。DeepSeek-Prover-V1.5は、DeepSeek-Prover-V1を大幅に上回る性能を示し、高校レベルのminiF2Fベンチマーク（63.5%）および大学レベルのProofNetベンチマーク（25.3%）において、新たな最先端の結果を達成しました。

English

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%).