2ヶ月前
DeepSeek-Prover-V1.5: 証明アシスタントのフィードバックを強化学習とモンテカルロ木探索に活用する
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
要約
私たちは、Lean 4での定理証明を目的としたオープンソースの言語モデルであるDeepSeek-Prover-V1.5を紹介します。このモデルは、DeepSeek-Prover-V1の訓練と推論プロセスの最適化により性能が向上しています。形式的な数学言語に特化したDeepSeekMath-Baseで事前学習された後、DeepSeek-Prover-V1から派生した強化された形式定理証明データセットを使用して監督ファインチューニングが行われます。さらに、証明アシスタントからのフィードバックによる強化学習（RLPAF）を通じて改良が図られています。DeepSeek-Prover-V1の単一パス全体証明生成アプローチを超えて、RMaxTSというモンテカルロ木探索の変種を提案します。RMaxTSは、内在報酬駆動型探査戦略を採用し、多様な証明経路を生成します。DeepSeek-Prover-V1.5は、高校レベルのminiF2Fベンチマーク（63.5%）と大学レベルのProofNetベンチマーク（25.3%）のテストセットにおいて、DeepSeek-Prover-V1に対して大幅な改善を示し、新しい最先端の結果を達成しています。