DeepSeek、再起的証明探索と新ベンチマークProverBenchを備えたDeepSeek-Prover-V2をリリース

DeepSeek AIは、Lean 4による形式的定理証明のためのオープンソースの大規模言語モデル、DeepSeek-Prover-V2を発表しました。本モデルは再帰的な定理証明パイプラインを採用しており、DeepSeek-V3を用いて複雑な定理をサブゴールに分解し形式化することで高品質な初期化データを生成します。次に、7Bパラメータのモデルがこれらのサブゴールを証明し、完全な証明とDeepSeek-V3によるChain-of-Thought推論をペアにして学習に使用します。バイナリフィードバックを用いた強化学習により、さらにモデルを洗練します。671Bパラメータ版はMiniF2F-testで88.9%の精度を達成し、PutnamBenchの問題658問中49問を解きました。また、DeepSeekは数学的推論を評価するためのベンチマークデータセットProverBenchも導入しました。これはAIMEコンペティションや教科書からの325問の問題で構成されています。モデルは7Bパラメータと671Bパラメータの2つのサイズで利用可能です。