DeepSeek-Prover-V2：形式的および非形式的な数学的推論のギャップを埋める

DeepSeek-R1は、非形式的な推論においてAIの能力を大幅に向上させましたが、形式的な数学的推論は依然としてAIにとって課題的なタスクです。これは、検証可能な数学的証明を生成するには、深い概念的理解と、正確で論理的な推論を構築する能力の両方が必要だからです。ただし、最近、DeepSeek-Prover-V2という、数学的直感を厳密で検証可能な証明に変換できるオープンソースAIモデルがDeepSeek-AIの研究者によって導入されました。この記事では、DeepSeek-Prover-V2の詳細と将来の科学的発見への潜在的な影響について説明します。

形式的な数学的推論の課題

数学者は、直感、ヒューリスティクス、ハイレベルな推論を使用して問題を解決します。このアプローチにより、明らかなステップや近似を省略できます。ただし、形式的な定理証明には異なるアプローチが必要です。完全な精度が必要であり、各ステップが明示的に記述され、曖昧さなく論理的に正当化される必要があります。

最近の大規模言語モデル（LLM）の進歩により、自然言語推論を使用して複雑な数学の問題を解決できることが示されています。ただし、LLMは依然として、直感的な推論を形式的な証明に変換するのに苦労しています。これは、非形式的な推論がしばしばショートカットや省略されたステップを含み、形式的なシステムでは検証できないためです。

DeepSeek-Prover-V2は、この問題を解決するために、非形式的な推論と形式的な推論の強みを組み合わせます。複雑な問題を小さな管理可能な部分に分解し、形式的な検証に必要な精度を維持します。このアプローチにより、人間の直感と機械検証可能な証明のギャップを埋めることが容易になります。

定理証明への新しいアプローチ

本質的に、DeepSeek-Prover-V2は、非形式的な推論と形式的な推論の両方を含む独自のデータ処理パイプラインを使用します。パイプラインは、一般目的のLLMであるDeepSeek-V3で開始され、数学的問題を自然言語で分析し、ステップを分解し、それらのステップを機械が理解できる形式言語に翻訳します。

問題全体を一度に解決しようとしない代わりに、システムは「サブゴール」と呼ばれる一連の中間的な補題に分解します。これらの補題は、最終的な証明に向けてのステップストーンとして機能します。このアプローチは、人間の数学者が難しい問題に取り組む方法を模倣しており、すべてを一度に解決しようとしない代わりに、管理可能なチャンクで作業します。

このアプローチが特に革新的なのは、トレーニングデータを合成する方法です。複雑な問題のすべてのサブゴールが成功裏に解決されると、システムはこれらの解決策を完全な形式的な証明に結合します。この証明は、DeepSeek-V3の元の推論プロセスと組み合わせて、高品質の「コールドスタート」トレーニングデータを作成するために使用されます。

数学的推論のための強化学習

初期トレーニングの後、DeepSeek-Prover-V2は、強化学習を使用してさらにその能力を向上させます。モデルは、解決策が正しいかどうかについてのフィードバックを受け取り、このフィードバックを使用して、どのアプローチが最も効果的かを学習します。

ここでの課題の1つは、生成された証明の構造が、推論プロセスによって示唆された補題分解と常に一致しないことです。この問題を解決するために、研究者はトレーニング段階で一貫性の報酬を含め、構造的な不一致を減らし、最終的な証明にすべての分解された補題を含めることを強制しました。この一致アプローチは、複数のステップが必要な複雑な定理に特に効果的です。

パフォーマンスと実世界での能力

DeepSeek-Prover-V2のパフォーマンスは、既存のベンチマークでその優れた能力を示しています。モデルはMiniF2F-testベンチマークで優れた結果を達成し、PutnamBenchの658個の問題のうち49個を解決しました。PutnamBenchは、ウィリアム・ローウェル・プットナム数学コンペティションの問題のコレクションです。

さらに印象的なのは、最近のアメリカン・インビテーショナル・マサイムズ・エクザミネーション（AIME）競技の15個の問題でモデルを評価した結果です。モデルは6個の問題を解決しました。また、DeepSeek-V3は、多数決を使用してこれらの問題のうち8個を解決しました。これは、形式的な数学的推論と非形式的な数学的推論のギャップがLLMで急速に狭まっていることを示唆しています。ただし、モデルはまだ組み合わせ問題のパフォーマンスを改善する必要があります。これは、将来の研究が重点を置くべき分野です。

ProverBench：AIの数学における新しいベンチマーク

DeepSeekの研究者はまた、LLMの数学的問題解決能力を評価するための新しいベンチマークデータセットを導入しました。このベンチマーク、ProverBenchは、325個の形式化された数学的問題で構成されています。これには、最近のAIME競技の15個の問題や教科書、教育用チュートリアルからの問題が含まれます。これらの問題は、数論、代数、微積分、実解析などをカバーしています。AIMEの問題を含めることは特に重要です。なぜなら、モデルは単に知識の再現ではなく、創造的な問題解決能力を評価するからです。

オープンソースへのアクセスと将来的な影響

DeepSeek-Prover-V2は、オープンソースで利用可能であるため、魅力的な機会を提供します。Hugging Faceなどのプラットフォームでホストされているこのモデルは、研究者、教育者、開発者を含む幅広いユーザーにアクセス可能です。7億パラメータの軽量バージョンと671億パラメータの強力なバージョンの両方が用意されているため、DeepSeekの研究者は、さまざまな計算リソースを持つユーザーも利点を得られるようにしています。このオープンソースアクセスは、実験を促進し、開発者が数学的問題解決のための高度なAIツールを作成できるようにします。したがって、このモデルは、数学研究の革新を推進し、研究者が複雑な問題に取り組み、新しい洞察を得る可能性を高めることができます。

AIと数学研究への影響

DeepSeek-Prover-V2の開発は、数学研究だけでなくAIにも重大な影響を及ぼします。モデルの形式的な証明を生成する能力は、数学者が難しい定理を解決するのを支援し、検証プロセスを自動化し、さらには新しい予想を提案するのを支援する可能性があります。また、DeepSeek-Prover-V2を作成するために使用された技術は、論理的推論に依存する他の分野での将来のAIモデルの開発に影響を与える可能性があります。

研究者は、モデルをさらに難しい問題、たとえば国際数学オリンピアード（IMO）レベルの問題に取り組むことができるように拡大することを目指しています。これにより、AIの定理証明能力がさらに向上する可能性があります。DeepSeek-Prover-V2のようなモデルが進化し続けるにつれて、数学とAIの両方の分野の未来を再定義し、理論的研究から技術への実用的な応用まで、さまざまな分野の進歩を促進する可能性があります。

まとめ

DeepSeek-Prover-V2は、AI駆動の数学的推論における重要な進歩です。非形式的な直感と形式的な論理を組み合わせて、複雑な問題を分解し、検証可能な証明を生成します。ベンチマークでのその優れたパフォーマンスは、数学者を支援し、証明の検証を自動化し、さらには分野での新しい発見を促進する可能性を示しています。オープンソースモデルとして、幅広いユーザーにアクセス可能であり、AIと数学の両方の分野での革新と新しい応用の魅力的な可能性を提供しています。