Seed Prover 1.5：新たなエージェント型アーキテクチャと強化された数学的推論能力

Seed Prover 1.5：新世代の Agentic アーキテクチャ、より強力な数学推論性能

オリジナル記事 字节跳动 Seed 2025-12-24 11:43 河北

9時間で 2025 年プットナム数学コンテストの 11 問を解決

今年 7 月、字节跳动 Seed チームは IMO 2025（国際数学オリンピック）への参加を招待されました。私たちの形式化数学推論モデルである Seed Prover は、3 日間の試行を通じて、全 6 問のうち 4 問と 1 問の一部の証明を完全に解決し、公式認定の銀メダル成績を達成しました。

このほど、新世代の形式化数学推論専用モデル「Seed Prover 1.5」を発表しました。大規模な Agentic RL（エージェント型強化学習）訓練を通じて、推論能力と推論効率が著しく向上しています。前世代モデルと比較して、Seed Prover 1.5 は 16.5 時間以内に IMO 2025 の最初の 5 問に対して、完全かつコンパイル検証可能な Lean（形式化証明言語）の証明コードを生成しました。換算スコアは 35/42 で、従来の IMO 採点基準における金メダルラインに達しています。

北米の学部レベル数学コンテストであるプットナムに対しては、Seed Prover 1.5 は 9 時間で、2025 年プットナムの 12 問中 11 問について、コンパイル検証可能な Lean コードを生成しました。より体系的な評価では Seed Prover 1.5 のパフォーマンスは顕著で、完全なプットナム歴史評価セットにおいて 88% の問題を解決しました。また、修士レベルの数学難易度を代表する Fate-H および博士課程レベルの数学難易度を代表する Fate-X 評価セットにおいては、それぞれ 80% と 33% の問題を解決し、形式化数学推論モデルにおけるこれらの評価セットでの SOTA（State of the Art：最良性能）記録を刷新しました。

Seed Prover 1.5 の、複数の評価セットにおけるこれまでの他 SOTA 手法との比較（棒グラフの数字は解決した問題数を示す）

Seed Prover 1.5 の技術報告書が公開されました。今後 API を開放し、数学および AI 研究に関心のある方々にこのモデルを体験していただく予定です。

技術報告：

https://arxiv.org/abs/2512.17260

Lean 証明コード：

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

1. Agentic Prover：新しい形式化数学推論のパラダイム

大規模言語モデルはすでに自然言語で多くの数学問題を流暢に解答できるようになりましたが、複雑度が高い最先端の数学研究においては、自然言語による証明には論理の飛躍や定義の不鮮明さが生じることがあり、数学者からの完全な信頼を得るに至らない課題があります。一方、形式化された数学推論では、モデルは Lean などの形式言語を使用し、公理系内で機械的に検証可能な証明を構築することを求められます。これは、正確性の確保において自然言語による証明が及ばない圧倒的な優位性を持っています。

しかし、その反面、形式化された証明は自然言語の証明よりも遥かに困難です。「De Bruijn factor」と呼ばれる経験則によれば、通常の数学的推論 1 行を記述するには、通常 4 から 10 行に及ぶ複雑なコードへと拡張する必要があります。これはモデルが数学だけでなく、プログラミングや型理論にも精通していることを要求するものであり、この高い参入障壁により、形式化された証明の効率と成功率は依然として自然言語推論に大きく遅れをとっています。

これまでの研究において、形式化された証明器は主に 2 つのカテゴリに分類されていました。一つは「一歩ずつ進める」Step-prover で、効率が低いです。もう一つは「一気に完成させる」Whole-prover で、一度に完全な証明を生成しようとするものの、途中でエラーが発生すると全てが無駄になります。

Seed Prover 1.5 は、自然言語推論との格差を埋めるために、全く新しい Agentic Prover アーキテクチャを提案しました。これは 2 つの形式化証明手法の長所と短所のバランスを取ったものであり、モデルは Lean 言語を一つのツールとして扱い、証明プロセスの中で自ら他の多様なツールを呼び出すことができます。

Mathlib 検索ツール：プログラマーが技術文書を参照するように、モデルは Lean の膨大な数学ライブラリである Mathlib を能動的に検索し、利用可能な定理や定義を探します。これは信頼性の低い暗黙の記憶に頼るのではなく、明示的な検索を行います。

Python コード実行：計算が必要な部分においては、モデルは Python スクリプトを記述して実行し、直観を検証するのを補助します。

増分型補題検証：モデルはもはや一度に証明全体を生成することを強要されません。複雑な問題をいくつかの補題に分解し、それぞれの補題を証明するごとに、システムがそれを保持・再利用し、後の推論の基盤とします。

この設計により、モデルは戦略を柔軟に調整できます。人間のようにまず「下書き」（自然言語）を用いて推論を行い、いつでもツールを呼び出して仮説を検証し、最後に検証済みのモジュールを組み合わせて完全な形式化証明を構築することが可能になります。

Seed Prover 1.5 が FATE-H 問題に対してツールを呼び出す例

Seed Prover 1.5 の強力な能力は、大規模な Agentic RL（強化学習）に由来します。構築された環境において、モデルは膨大な自己探索と訓練を行いました。Lean コンパイラが絶対的に客観的な「正解/不正解」のフィードバックを提供するため、これが強化学習にとって最良のリワード信号となります。実験によると、RL 訓練ステップ数が増加するにつれ、モデルの訓練セットにおける証明通過率は初期の 50% から約 90% にまで上昇しました。

Agentic RL はさらに大幅な効率向上をもたらしました。比較テストにおいて、Seed Prover 1.5 はわずかな計算リソースしか必要とせず、Putnam や Fate のような高難易度データセット上で、膨大な計算力を消費した前世代の Seed Prover モデルを打ち負かすことができました。これは、Seed Prover 1.5 が推論能力と効率性の両面で新たな段階へと到達し、形式化証明がさらに実用化の方向へ進んだことを示しています。

Seed Prover 1.5 は、効率と効果の両面で Seed Prover 1.0 を明確に上回っています (pass@8*8 は約 0.4 GPU days/problem の計算力に相当)。

1. Sketch Model：自然言語と形式言語の境界を突破する

Agentic Prover の支援があるとはいえ、モデルが数万行に及ぶ複雑な定理証明に取り組む際、直接完全な形式化コードを生成することは依然として大きな課題です。この難題を解決するため、私たちは人間の数学者が問題を解決する様子を模倣した Sketch Model を訓練しました：まず高レベルの証明フレームワークを構築し、その後で詳細を補完するというアプローチです。

このモデルは自然言語による証明を、独立した複数のより低難易度の引理に分解し、具体的な証明プロセスは一時的にスキップして全体の論理的骨格のみを保持します。その利点は明白です：本来は解くことが困難な複雑な命題を、著しく難度が低下したサブゴールへと変換できる点にあります。

優れた「証明アーキテクト」を訓練するために、私たちは混合された報酬信号を用いた強化学習戦略を採用しました：

シグナル 1: Lean コンパイラが生成されたスケッチが完全に正しいか検証する。

シグナル 2: 自然言語 Prover が各引理を順次チェックし、数学的に不成立な引理が一つでも発見されれば、そのスケッチ全体が却下される。

シグナル 3: 長文の思考連鎖 (Chain of Thought) に基づく Rubric 評価モデルを導入し、意味論的観点からスケッチの品質を評価する——引理が自然言語証明と整合しているか、分解の粒度が適切か、そして実際に元の問題の難度が低下したかを考慮する。

最終的に、スケッチが形式検証、数学的正しさ、および総合評価のすべての要件を満たした場合にのみ、正の報酬が付与されます。

Sketch Model を基盤として、私たちは効率的なテストワークフローを構築し、階層化されたマルチエージェント協調システムを形成しました：

Natural Language Prover は高レベルの数学的直感と自然言語による証明を提供する役割を担います。

Sketch Model は自然言語を形式化された引理構造へと変換します。

Agentic Prover は分解された各引理を並列に攻略します。

もし特定の引理が証明しにくい場合、システムは Sketch Model を再帰的に呼び出して再度分解を行います。この「分割統治」戦略は、長文生成における誤差の累積問題を回避するだけでなく、推論の並列度と成功率も向上させます。

1. 未来展望：AI による未解決数学問題の解決

既存の AI システムはすでに「ルールが明確で背景が閉じた」数学問題、すなわち IMO や Putnam などの競技問題を比較的よく解くことができますが、人間専門家のレベルに匹敵する数学的貢献を行うにはまだ大きな隔たりがあります。この限界は、最先端の数学研究における「依存性 (dependency)」の問題に由来します。「特定の先験知識を必要とせずに解決できる」競技問題とは異なり、最先端の数学発展を推進するには、多くの関連論文からの洞察を総合的に統合する必要があります。

AI を単なる「問題解決者」から真の「研究者」へと進化させるためには、以下の 3 つの相互に関連する核心的な課題を解決する必要があります：

文献発見：モデルが膨大な数学文献の中から、最も影響力がありかつ関連性の高い論文を識別できるようにすること。

文献に基づく推論：既存の論文を基盤とし、次の数学的推論へと進めるモデルを実現する。

規模形式化：モデルが既存の論文から導き出した新たな結果を形式化コードに変換するためのスケーラブルな手法を開発する。

我々はこれらの主要な課題について今後さらに探索・研究を進めていく。近い将来、AI が人類の数学者と共に協力し、未解決の数学的予想への挑戦に乗り出すことを期待している。

原文を読む

WeChat で開くにはこちらへ