DeepSeek、数学定理の自動証明モデルを公開

DeepSeekは、数学の定理を自動的に証明するAIモデル「DeepSeek-Prover-V2」を公開した。このモデルはオープンソースとして提供され、数式の形式的な証明を記述・検証するプログラミング言語「Lean 4」に対応している。

「定理証明」とは、数学的な命題が正しいことをコンピュータが論理的に確かめるタスクを指す。これは単なる計算とは異なり、複雑な推論の積み重ねが必要なため、AIにとって難易度の高い分野とされてきた。近年、大規模言語モデル（LLM）の能力向上に伴い、この分野への応用研究が活発化しており、DeepSeekの取り組みもその流れの中に位置づけられる。

DeepSeek-Prover-V2の訓練には、同社が開発した大規模言語モデル「DeepSeek-V3」が活用された。DeepSeek-V3を使って学習用データを生成するという手法をとっており、再帰的な証明探索（問題をより小さな部分に分解しながら繰り返し解を探す方法）と、強化学習（試行錯誤を通じてモデルの精度を高める手法）を組み合わせてモデルを改善している。

性能評価として、定理証明のベンチマーク「MiniF2F」において最高水準の結果を達成したと報告されている。MiniF2Fは、数学オリンピックレベルの問題などを含む標準的な評価セットであり、このベンチマークでの高スコアはモデルの実用的な証明能力を示す指標として広く参照される。

今回の公開がオープンソース形式をとっている点も注目される。研究者や開発者がモデルの詳細を確認・改変できるため、学術コミュニティでの利活用や追試研究が進みやすくなると見られる。DeepSeekはこれまでも複数のオープンモデルを公開しており、透明性の高い開発姿勢をとる企業として知られている。

AI による数学証明の自動化は、純粋な数学研究の補助にとどまらず、ソフトウェアの正確性検証や暗号理論の検証など、実用的な応用への可能性を持つ分野でもある。DeepSeek-Prover-V2がその能力をどこまで広げられるか、今後の研究コミュニティでの検証が一つの見どころとなる。

今後は、MiniF2F以外のより難度の高いベンチマークでの評価や、実際の未解決問題への適用可能性が研究上の焦点になると考えられる。オープンソースでの公開により外部からの検証・改良も加わることで、この分野の研究が加速するという見方ができる。