中国AI企業DeepSeekは、数学定理証明に特化した最新モデル「DeepSeek-Prover-V2」を発表した。本モデルは、Putnamベンチマークで従来記録を大幅に上回る49問を解き、競合モデルKimina-Proverの10問を圧倒した。特に注目すべきは、7Bという小型モデルが、推論強化学習を通じて671Bモデルでも解けなかった13問を非CoT（思考連鎖なし）モードで解決した点である。
この7Bモデルは、DeepSeek-Prover-V1.5ベースに、強化学習段階で671Bモデルから収集したデータを用いて微調整された。結果として、有限基数を扱う問題において独自の推論パターンを発揮し、大規模モデルとは異なるアプローチで課題解決に成功している。
Prover-V2は、形式化されたLeanコード生成と非形式的な自然言語推論の双方を統合する構造を持ち、DeepSeek-V3を基盤として子目標分解による冷スタートデータ生成と強化学習を組み合わせた。この冷スタートデータは、問題を細分化し、それぞれを小型モデルで解決、再統合するという手法を取る。学習プロセスは、非CoTモードによる効率的なデータ収集と、CoTモードによる複雑推論の強化という二段構えで行われ、GRPOアルゴリズムを活用した強化学習によって高精度な証明生成が実現された。
さらに、教育応用を想定した新たなベンチマークデータセット「ProverBench」も同時に発表された。これは、米国数学コンテスト（AIME）や教科書問題を形式化した325問からなり、高校・大学初級レベルの定理証明性能を広く評価できる基盤となっている。
Prover-V2はminiF2Fで88.9%の通過率を記録し、GitHub上では12時間で350を超えるスターを獲得。コミュニティからも高い評価を受けており、形式数学分野におけるDeepSeekの存在感をさらに強めている。
