DeepSeek オープンソースの大規模数学モデル、高校および大学の定理証明用の新しい SOTA

DeepSeek-Prover-V1.5 は、強化学習とモンテカルロ木探索を組み合わせることで、証明生成の効率と精度を大幅に向上させます。

AI テクノロジーの進歩と数学的発見は、これまでにないほど絡み合っています。

少し前、有名な数学者テレサ・タオがオックスフォード数学公開講座で「科学と数学におけるAIの可能性」というテーマで講演しました。同氏は、AIを数学に統合することで、（エラーが発生しやすい）人間の証明よりも速く形式的な証明を書くことが可能になると指摘している。これは重要な転換点となり、形式的証明の使用が既存の証明の検証に限定されず、新しい数学的知識の創造にも使用されることを意味します。これは、人間と AI の数学者間の広範な協力によって達成されます。私たちは「大きな数学」の時代を迎えようとしています。

テレンス・タオが言ったように、AI を形式定理の証明に適用することは、数学者にとって日常的な作業になっています。その一方で、AI 科学者は、DeepSeek によって発表されたばかりの新しいモデル、DeepSeek-Prover-V1.5 など、形式的定理証明における AI のパフォーマンスと効率の向上にも熱心に取り組んでいます。

DeepSeek-Prover-V1.5 は、70 億のパラメーターを備えたオープンソース モデルです。強化学習 (証明アシスタントのフィードバック、RLPAF に基づく強化学習) とモンテカルロ木探索 (特に提案された RMaxTS バリアント) を組み合わせることで、証明生成の効率と精度が大幅に向上します。 DeepSeek-Prover-V1.5 は、リーン 4 の形式定理証明において、すべてのオープンソース モデルよりも優れたパフォーマンスを発揮します。

以下はテクニカルレポートの詳細です。

技術レポートの概要

• レポートのタイトル: DeepSeek-Prover-V1.5: 強化学習とモンテカルロ木探索のための証明アシスタントのフィードバックの利用
• レポートリンク: https://arxiv.org/pdf/2408.08152
• GitHub リンク: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5

近年、大規模な-スケール言語 モデル分野の進歩により、数学的推論と定理証明における人工知能の開発が大きく促進されました。ただし、言語モデルは、形式定理の証明において依然として大きな課題に直面しています。たとえば、Lean や Isabelle のようなシステムを使用した証明では、検証システムの形式仕様を満たすために厳密な導出が必要です。 GPT-4 のような高度なモデルでも、複雑な形式的証明を処理することはできません。これは、形式的証明におけるコーディングと数学的推論の複雑さを浮き彫りにします。効率的な形式定理証明モデルには、Lean Proof Assistant などの形式システムの構文とセマンティクスを理解する必要があるだけでなく、抽象的な数学的推論と正確な形式式を組み合わせる必要もあります。

形式的定理証明では、言語モデルは通常、証明ステップ生成と全体証明生成という 2 つの戦略を採用します。

証明ステップは、各戦略を予測して検証し、形式的検証ツールを使用して現在の戦略の状態に関する最新情報を取得し、効果的な証明を構築するためにツリー検索手法を組み合わせることによって生成されます。完全な証明の生成は計算効率が高く、定理ステートメントに基づいて証明コード全体を一度に生成し、証明モデルと形式的定理検証器の間の調整に必要な通信量を削減します。

DeepSeek-Prover-V1 は完全な証明生成により Lean 4 で SOTA の結果を達成しましたが、このアプローチには特有の課題もあります。中間の政策状態情報を持たない長期的なシーケンス予測が必要であり、将来の政策はこれらの隠れた結果に依存します。リーンの戦略パターンでは、証明の状態を変化させる一連の戦略を通じて証明が構築されます。この順序性によりエラーが蓄積される可能性があり、小さなエラーによって証明が正しいパスから外れる可能性があります。具体的には、自己回帰モデルは、成長の証明を生成するときに、中間の政策状態について誤った認識を持っている可能性があります。

完全な証明生成の単純さと計算効率を犠牲にすることなく中間ポリシー状態をシームレスに統合するために、研究者は DeepSeek-Prover-V1.5 で統合アプローチを開発しました。このアプローチは、プルーフ ステップ生成の利点と、切り捨てと再開のメカニズムによる完全なプルーフ生成の利点を組み合わせています。

プロセスは、標準の完全な証明生成から始まり、言語モデルが定理ステートメントのプレフィックスに基づいて証明コードを完成させ、その後リーン証明者によって検証されます。正しいことが証明された場合、プロセスは終了します。エラーが見つかった場合、最初のエラー メッセージからコードが切り捨てられ、それ以降のコードは破棄されます。次に、正常に生成された証明コードをヒントとして使用して、次の証明セグメントを生成します。

モデルの新しく完成した部分の精度を向上させるために、研究者はリーン 4 証明者の最新のステータスをプロンプトの最後にコメントとして追加しました。このアプローチは、最後に正常に適用された戦略から再開することに限定されないことに注意してください。研究者らは、切り捨てと再開のメカニズムをモンテカルロ木探索 (MCTS) に統合し、木探索戦略により切り捨てポイントを配置しました。さらに、彼らは、証明探索における報酬の希薄性問題を解決するための、新しい報酬のない探索アルゴリズムを提案しました。これらは、樹木検索エージェントに、政策国家空間を広く探索するための本質的な推進力、つまり好奇心を与えます。これらのアルゴリズム モジュールは、完全な証明生成モデルを柔軟でインタラクティブな定理証明ツールに拡張し、証明アシスタントからのフィードバックを効果的に活用して多様な解決策を生成できます。

中心的な貢献

研究者らは、言語モデルに基づいて形式的な数学的証明ツールを開発するための包括的なフレームワークを提案しました。彼らは、大規模な数学的事前トレーニング、形式的な証明の構築と強化といういくつかの重要なコンポーネントを統合しました。数学的コーパス、証明アシスタントのフィードバックに基づくオンライン強化学習、定理証明の長期計画のためのツリー検索方法論。事前トレーニング済みモデル、教師あり微調整モデル、強化学習モデル、モンテカルロ木探索アルゴリズムのコードは、さらなる研究や応用のために公開されています。

1. 事前トレーニング

研究者らは、リーンとIsabelle Metamath や Metamath などの形式言語は、証明アシスタントとして広く使用されています。

2. 監視付き微調整

研究者たちは、2 つのデータ拡張手法を実装することで、リーン 4 コード補完データセットを改善しました。まず、彼らは DeepSeek-Coder V2 236B を使用して、リーン 4 コードと一緒に CoT (思考連鎖) コメントに注釈を付け、形式的定理の証明と自然言語推論を調整しました。次に、中間ポリシー状態情報を Lean 4 証明コードに挿入し、モデルがコンパイラのフィードバックをより効率的に利用できるようにします。次に、このデータセットを使用して、事前トレーニングされたモデルを微調整しました。

3. 強化学習

研究者らは、GRPO アルゴリズムを使用して、教師あり微調整モデルで RLPAF (証明アシスタントのフィードバックからの強化学習、証明アシスタントのフィードバックに基づく強化学習) を実行しました。リーン証明者の検証結果は報酬の監視として機能し、検証システムの正式な仕様とモデルの一貫性を高めます。

4. モンテカルロ木探索

研究者たちは、新しい抽象化と対応する探索アルゴリズムを導入することにより、形式定理証明における木探索手法を進歩させました。それらの切り捨ておよび再起動メカニズムは、ツリー検索プロセスを完全な証明生成フレームワークにシームレスに統合する状態アクションの抽象化として機能します。彼らは、RMax 戦略を活用して、証明検索問題における報酬が少ない探索課題を解決する革新的なモンテカルロ木検索アルゴリズムである RMaxTS を紹介します。このアルゴリズムは、固有の報酬を割り当てることで、証明エージェントが多様な計画パスを生成することを奨励し、それによって証明空間の広範な探索を促進します。

評価とメトリクス

1. 高校レベルのminiF2Fデータセット

シングルパス法の完全証明生成設定では、DeepSeek-Prover-V1.5のテストセット上でminiF2F 60.2% の合格率を達成しました。これは、DeepSeek-Prover-V1 の 50.0% を 10.2 ポイント上回りました。ツリー検索テクノロジーと組み合わせると、合格率はさらに向上し、新しい SOTA 63.5% に達します。

2. 学部レベルの ProofNet データセット

DeepSeek-Prover-V1.5 も、ProofNet の単一チャネルメソッド完全証明生成設定で優れたパフォーマンスを示し、検証セットで 100% の合格率を示しました。 21.6%、テストセットでは 23.7%。ツリー検索手法と組み合わせると、これらの結果はさらに強化され、検証セットで 25.4%、テスト セットで 25.3% という新しい SOTA に達します。

モデルトレーニング

数学言語を通じて形式的な証明と推論を生成する言語モデルの能力を向上させるために、研究者たちは基本モデルをさらに事前トレーニングし、この改良されたモデルを DeepSeek -ProverV1 と名付けました。 5ベース。

次に、この記事では、DeepSeek-Prover-V1.5 の教師あり微調整 (SFT) に含まれる方法とプロセスについて説明します。具体的には、研究者らは、詳細な説明の注釈を追加することで、DeepSeekProver-V1 証明データセットを強化しました。この機能強化は、自然言語記述と Lean 4 コードの間の一貫性を向上させ、それによって形式的数学的推論の向上を促進することを目的としています。さらに、研究者らは、モンテカルロ木探索プロセスで使用される切り捨ておよび再起動メカニズムをサポートする補助予測タスクとして中間ポリシー状態情報を組み込み、結果のモデルを DeepSeek-ProverV1.5-SFT と呼びました。

証明アシスタントのフィードバックに基づく強化学習

DeepSeek-Prover-V1.5-SFT のパフォーマンスをさらに向上させるために、研究では強化学習ステージが導入され、その結果 DeepSeek-Prover-V1 が誕生しました。 .5-RLモデル。このステージでは、強化学習 (RL) を利用して、リーン 4 証明者からの検証フィードバックに基づいてパフォーマンスを向上させます。この RL プロセスの具体的な詳細は次のとおりです。

トレーニングのヒント。強化学習フェーズでは、研究では教師あり微調整データセットからの部分定理ステートメントをトレーニング キューとして使用します。フィルタリング後、約 4,500 個の固有の定理ステートメントが保持されました。各定理には、両方のモードでモデルの証明生成機能を強化するための CoT および非 CoT ガイダンス ヒントが付属しています。

報酬。 RL を介して LLM をトレーニングする場合、トレーニングされた報酬モデルはフィードバック信号を提供することがよくあります。対照的に、形式的定理の証明には、証明アシスタントによる生成された証明の厳密な検証の恩恵があり、大きな利点が得られます。具体的には、生成された各プルーフは、正しく検証された場合には 1 の報酬を受け取り、それ以外の場合には 0 の報酬を受け取ります。このバイナリ報酬信号は正確ですが、特に教師あり微調整モデルにとって困難な定理の場合、疎でもあります。このまばらさを軽減するために、前述したように、困難ではあるがモデルの教師あり微調整が達成可能なトレーニング キューを選択しました。

強化学習アルゴリズム。この研究では、本論文の RL アルゴリズムとして Group Relative Policy Optimization (GRPO) を採用しています。これは、PPO と比較してより高い有効性と効率性を示しています。具体的には、GRPO は各定理ヒントの候補となる証明のセットを抽出し、セット内の出力の相対的な報酬に基づいてモデルを最適化します。

評価。図 3 は、miniF2F と ProofNet データセットの各トレーニング ステージの比較分析を示しています。 CoT モードは、ほとんどの設定で非 CoT モードよりも一貫して優れたパフォーマンスを発揮します。

探索指向のモンテカルロ木探索

全体的な証明生成設定で木探索アプローチを実装するために、この研究ではカスタマイズされた状態とアクション空間を定義する証明ツリーの抽象化を導入し、truncate を活用します。そして再起動機構。研究者らはまず、不完全な証明を各証明ステップに対応する一連のツリー ノードに分解し、次にこれらのツリー ノードに格納されている部分コンテンツを使用して証明生成プロセスを続行します。図 4 は、プルーフ生成全体からプルーフ検索ツリーを構築するプロセスを示しています。

切り捨て: この研究では、ポリシー レベルで証明検索ツリーを構築します。各ツリーのエッジは、ポリシー状態の単一の遷移ステップを表します。まず、研究では、モデルによって生成された証明全体をリーン証明者に送信し、それをポリシーに解析しました。その後、証明は最も早い検証エラーで切り捨てられ、後続のすべての戦略コードが正常に適用されて証明が必要な定理に到達することが保証されます。戦略コードはいくつかのコード スニペットに分割されており、各コード スニペットには有効な戦略コードとそれに関連する思考連鎖の注釈が含まれており、戦略の状態遷移を表す単一のツリー エッジに対応します。この抽象化により、各ポリシー コードは一連のツリー ノードに変換され、ルートから特定のノードまでのパスが形成されます。

やり直し: リーン 4 では、異なる戦略が同じ戦略状態につながる可能性があります。これは、証明ツリー内の各ノードが、同じ結果を達成できる複数の戦略コードに対応する可能性があることを意味します。この問題を解決するために、研究者らはこれらの同等のポリシー コードのセットを各ノードに保存しました。ツリー検索エージェントはノードを展開するときに、言語モデルのヒントとしてポリシーをランダムに選択します。

モンテカルロ木探索の本質的な報酬

次の記事では、本質的な報酬駆動探索アルゴリズム - RMax を木探索に適用し (RMaxTS)、報酬なし探索が証明に組み込まれているものを紹介します。検索の問題。

RMax が MCTS に適用されました。この研究では、古典的な探索メカニズムである RMax を使用して、モンテカルロ木探索の本質的な報酬を構築します。証明が完了するまで外部報酬が提供されない証明検索のコンテキストでは、このアルゴリズム プロセスは、エージェントの探索が本質的な報酬、つまり の設定によってのみ駆動される ZeroRMax に似ています。ツリー拡張ステップの本質的な報酬は、新しいノードが検索ツリーに追加されるかどうかによって決まります

このヒューリスティックにより、冗長な生成が削減され、サンプル効率が向上する可能性があります。

実験結果

このセクションでは、研究者は 2 つのベンチマーク miniF2F と ProofNet を使用して、DeepSeek-Prover-V1.5 の定理証明能力を評価します。前者には高校レベルの演習や競技問題が含まれ、後者には学部レベルの定理が含まれます。

一貫性を確保するために、研究者らは評価時と同じトレーニングモデルと推論構成を使用し、完全証明生成とモンテカルロ木探索法の結果を示しました。

まず、この論文では、DeepSeek-Prover-V1.5 といくつかの以前の SOTA モデルのパフォーマンスと進歩に焦点を当てた比較分析を紹介します。

• 一般モデル
  
  

GPT-3.5 および GPT-4 は、OpenAI によって開発された高度な生成 AI モデルであり、有名なコード生成を含むさまざまなタスクでの有効性が認められています。これらのモデルは定理証明専用に設計されたものではありませんが、その幅広いパラメーター範囲により重要な機能が提供されます。

COPRA は、形式的定理証明におけるこれらのモデルの評価を容易にし、これらの大規模な言語モデルを活用して戦術的アプリケーションを提案する文脈学習エージェントです。

さらに、研究者らは、形式的定理証明の基本モデルとしてよく使用される、広範囲の一般数学コーパスで訓練された言語モデルのファミリーである Llemma についても説明します。

• 形式数学に特化したモデル

GPT-f は、定理証明タスクの証明ステップの生成に Transformers を適用する最初の試みであり、構築する最良優先探索モジュールを利用します。完全な証明。その後の開発には、ReProver、LLMStep、Lean-STaR などがあります。

Hypertree Proof Search は、リーンを使用した形式的定理証明におけるモンテカルロ木探索の応用を検討します。同じ期間に、InternLM2-Math および InternLM2-StepProver も優れたパフォーマンスを示しました。

その後、研究者らはこれらのモデルを DeepSeek-Prover-V1.5 と比較しました。

miniF2F の結果

表 1 は、miniF2F テスト データセットに対するさまざまな定理証明方法の比較分析を示しています。

単一チャネル完全証明生成設定では、DeepSeekProver-V1.5-RL の合格率が最も高く、60.2% に達し、DeepSeek-Prover-V1 の 50.0% よりも 10.2 ポイント高くなりました。 DeepSeek-Prover-V1.5-RL は、サンプリング バジェットを 128 回の試行に制限し、問題の 51.6% を証明します。これは、他の完全証明生成メソッドを大幅に上回り、主要なツリー検索メソッドと同等のパフォーマンスを発揮します。ツリー検索手法のカテゴリでは、DeepSeek-Prover-V1.5-RL + RMaxTS が 62.7% の合格率でトップに立ち、新たな SOTA レベルを確立し、既存の手法との差を広げています。

DeepSeek-Prover-V1.5-RL では 54.9% の合格率を達成するために 3200 個の完全な証明サンプルしか必要とせず、64 回の実行が必要だった InternLM2-StepProver の以前の SOTA レベルを超えていることは注目に値します。 54.5% の合格率を達成するには、3,200 回のツリー検索が必要です。

ProofNet の結果

表 2 は、ProofNet データセットでのさまざまな定理証明手法の比較分析を示しています。 ProofNet データセット全体における DeepSeek-Prover-V1.5-RL の合格率は、それぞれ 22.6% と 25.3% に達しました。이는 기존 SOTA 방식인 ReProver(13.8%)와 InternLM2-StepProver(18.1%)를 능가하는 결과입니다. 완전한 증명 생성 시도 횟수가 3200으로 제한되는 경우 DeepSeek-Prover-V1.5는 정리의 21.7%를 증명하며 이는 이전 최첨단 InternLM2-StepProver에 비해 3.6% 향상된 수치입니다.

대규모 샘플링에서 훈련 전략의 효과 재검토

# 🎜🎜 #

연구원들은 단일 패스 완전 증명 생성 및 몬테카를로 트리 검색에 중점을 두고 대규모 샘플링 환경에서 여러 교육 모듈의 효과를 재검토했습니다.

표 3은 miniF2F 테스트 데이터 세트에서 두 세대 모드, 즉 비CoT와 CoT의 성능을 비교하여 샘플 예산으로 보여줍니다. 증가할수록 비CoT 모드에 비해 CoT의 장점이 확대됩니다.

절제 실험

#🎜🎜 # 연구진은 절제 실험에서 RMaxTS의 알고리즘 설계를 테스트했다. 실험은 miniF2F 테스트 데이터 세트에서 DeepSeek-Prover-V1.5-RL을 사용하여 CoT 모드에서 수행됩니다. 그림 5에서 볼 수 있듯이 왼쪽은 6400개의 생성된 샘플 내에서 Pass@K 정확도 곡선을 보여주고, 오른쪽은 더 큰 샘플 크기의 결과를 보여줍니다.

以上がDeepSeek オープンソースの大規模数学モデル、高校および大学の定理証明用の新しい SOTAの詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。