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\%$)。

要約(オリジナル)

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

arxiv情報

提供元, 利用サービス

arxiv.jp, Google