最近、ビットテイダンのSeedチームは最新の形式的な数学推論モデル「Seed Prover1.5」をリリースし、数学的推論分野における重要な進歩を示しました。このモデルの登場は、大規模なAgentic強化学習の深い探求に起因しており、推論能力と効率の両方で著しく向上しました。

2025年の国際数学オリンピック（IMO）に参加した際に、Seed Proverはその優れた性能を発揮しました。わずか3日間で6問中の4問を解決し、1問については部分的な証明を実施し、最終的に公式認定の銀メダルを獲得しました。一方、Seed Prover1.5は16.5時間かけてIMO2025の最初の5問に対して完全なコンパイル可能な検証用Lean証明コードを生成し、金メダルの基準を満たしました。

QQ20251224-141739.png

さらに注目すべきは、Seed Prover1.5が2025年のプットナム数学コンテストにおいても優れた成績を収めたことです。わずか9時間で12問中の11問について、コンパイル可能な検証用Leanコードを生成しました。この結果は、形式的数学推論モデルが複数の評価セットで記録された最高の成績であり、特に修士および博士課程の学生レベルの数学難易度を持つ評価セットでは、それぞれ80％および33％の問題を解決しました。

Seed Prover1.5の革新点は、新しいAgentic Proverアーキテクチャにあります。このアーキテクチャは、自然言語の推論と形式的証明の利点を組み合わせています。これまでの形式的証明器とは異なり、Seed Prover1.5は証明プロセス中に柔軟にさまざまなツールを呼び出すことができます。例えば、膨大な数学ライブラリMathlibを積極的に検索したり、Pythonコードを実行して検証を補助したりします。増分的な補題検証により、このモデルは複雑な問題をいくつかの補題に分解し、段階的に形式的証明を構築します。

また、Seed Prover1.5にはSketch Modelが導入されており、これは人間の数学者の解決方法を模倣しています。このモデルは自然言語による証明を高次の証明フレームワークに変換し、複雑な定理の証明の難易度を大幅に下げます。このような「分割統治」戦略により、Seed Prover1.5は長文を生成する際のエラーの蓄積を効果的に回避できます。

技術報告:

https://arxiv.org/abs/2512.17260

Lean証明コード:

https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver-1.5/Putnam2025.zip