何が起きたか
DeepSeek AIが、証明支援系Lean 4上で動作する形式的定理証明モデル「DeepSeek-Prover-V2」を、7Bと671Bの2サイズで公開しました。あわせて325問の数学問題からなる新ベンチマーク「ProverBench」もリリースされています。325問のうち15問は2024年・2025年のAIME(米国招待数学試験)から形式化されたもので、残り310問は教科書や教育用教材からの選定です。
なぜ重要か
LLMの数学能力は「自然言語で答えを当てる」段階から「機械的に検証可能な証明を構築する」段階へと軸足が移りつつあります。DeepSeek-Prover-V2-671Bは、MiniF2F-testで88.9%という正答率を出し、これは曖昧さを許容しない形式証明の領域でLLMが実用域に近づいてきたことを意味します。生成結果が正しいかを人手レビューに頼らずLean 4側で機械検証できるため、ハルシネーションが致命傷となる領域への応用可能性が広がります。
技術的な要点：自己生成データの再帰的活用
学習パイプラインの中核は、DeepSeek-V3に複雑な定理を扱いやすい部分目標(サブゴール)へ分解させ、その高レベル証明手順をLean 4で形式化させる点にあります。各サブゴールの探索には計算負荷の軽い7Bモデルを充てる役割分担を取り、V3の思考過程(chain-of-thought)と完成した形式証明をペアにした合成データセットを作っています。さらに、7Bが単体では解けなかった難問でもサブゴール単位の証明を結合して完全証明を再構築し、強化学習段階では「正解か不正解か」の二値報酬で精度を引き上げています。671Bモデルが達成した最高水準の数字は、この再帰的なデータ生成と検証の循環を回せた点に支えられています。
💼 事業会社視点：これは自社にどう効くか
形式的検証とLLMの融合は、SaaSやフィンテック、受託開発の事業責任者にとって直接の論点になります。生成AIの導入が止まる原因の多くは「アウトプットの正しさを誰がどう保証するか」であり、Lean 4のように機械検証可能な系へ落とし込めれば、レビュー工数の削減と監査適合性の両立が見えてきます。
国内の受託開発各社は、業務ロジックの仕様記述や金融計算の不変条件チェックといった「事故れば賠償」の領域に、Prover系モデルを試験投入する余地があります。SaaSベンダーであれば、料金計算・割引ロジックの検証にLLM+形式検証を組み合わせ、リリース前回帰の自動化を打ち出せる差別化ポイントです。
経営層が今動くべきは、(1)社内の「正しさが事業価値に直結する処理」の棚卸し、(2)Lean 4やCoqに触れる人材の確保、(3)671Bを自社推論する体力がない場合のクラウド推論コスト見積もり、の3点です。671Bは商用クラウドGPUでも運用負荷が重く、まずは7Bモデルでの社内PoCから入るのが現実的な経路となります。