DeepSeek-Prover-V1.5:証明アシスタントのフィードバックを活用した強化学習とモンテカルロ木探索DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for
Reinforcement Learning and Monte-Carlo Tree Search
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%)において、新たな最先端の結果を達成しました。