Seed Prover 1.5：新たなエージェント型アーキテクチャと強化された数学的推論能力
字节跳动 Seed が発表した「Seed Prover 1.5」は、Agentic アーキテクチャと強化学習を組み合わせ、形式化数学証明において IMO や Putnam などの難問で SOTA を更新する画期的な成果を示した。
キーポイント
Agentic Prover の新アーキテクチャ
従来の単発生成や逐次ステップ生成の限界を克服し、Mathlib 検索、Python 実行、引理検証などのツールを自律的に活用する「Agentic」な証明プロセスを採用した。
大規模 Agentic RL による性能向上
Lean コンパイラの厳格なフィードバックを活用した強化学習により、証明成功率が 50% から 90% へ劇的に向上し、計算リソース効率も大幅に改善された。
難問コンテストでの SOTA 達成
IMO 2025 の前 5 問で金メダル相当の成績を収め、Putnam 2025 では 12 問中 11 問を 9 時間で解決。Fate-H/X 評価セットでも既存モデルを凌駕する結果を出した。
形式化数学の現実的活用への道
自然言語証明の曖昧さを排除し、機械検証可能な Lean コードを生成することで、高度な数学研究における AI の信頼性と実用性を飛躍的に高めた。
Sketch Model：分层证明架构
通过模拟人类数学家先构建框架再补细节的方式，将复杂命题拆解为独立的引理子目标，显著降低推理难度并规避长文本错误累积。
混合奖励强化学习策略
训练Sketch Model采用三重信号：Lean编译器验证形式正确性、自然语言Prover检查数学逻辑、以及基于思维链的Rubric评分模型评估语义质量与拆解粒度。
迈向开放数学研究的挑战
AI要从解决封闭竞赛题进化为真正的研究者，需攻克文献发现、基于文献推理及大规模形式化转化三大核心难题。
影響分析・編集コメントを表示
影響分析
この発表は、AI が数学的推論において単なる「答え合わせ」から「厳密な証明生成」へとパラダイムシフトしたことを示す画期的な事例です。特に Agentic アーキテクチャと強化学習の組み合わせが、形式化言語の複雑さを克服し、信頼性の高い AI 数学者の実現に向けた重要な一歩となりました。
編集コメント
形式化数学証明の分野で、単なる推論能力を超えて「検証可能性」を担保する実用的な AI システムが誕生しました。特に Agentic アプローチによるツール活用は、今後他の専門領域への応用も期待される重要な技術的転換点です。
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
- 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 の計算力に相当)。
- 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 を再帰的に呼び出して再度分解を行います。この「分割統治」戦略は、長文生成における誤差の累積問題を回避するだけでなく、推論の並列度と成功率も向上させます。
- 未来展望：AI による未解決数学問題の解決
既存の AI システムはすでに「ルールが明確で背景が閉じた」数学問題、すなわち IMO や Putnam などの競技問題を比較的よく解くことができますが、人間専門家のレベルに匹敵する数学的貢献を行うにはまだ大きな隔たりがあります。この限界は、最先端の数学研究における「依存性 (dependency)」の問題に由来します。「特定の先験知識を必要とせずに解決できる」競技問題とは異なり、最先端の数学発展を推進するには、多くの関連論文からの洞察を総合的に統合する必要があります。
AI を単なる「問題解決者」から真の「研究者」へと進化させるためには、以下の 3 つの相互に関連する核心的な課題を解決する必要があります：
文献発見：モデルが膨大な数学文献の中から、最も影響力がありかつ関連性の高い論文を識別できるようにすること。
文献に基づく推論：既存の論文を基盤とし、次の数学的推論へと進めるモデルを実現する。
規模形式化：モデルが既存の論文から導き出した新たな結果を形式化コードに変換するためのスケーラブルな手法を開発する。
我々はこれらの主要な課題について今後さらに探索・研究を進めていく。近い将来、AI が人類の数学者と共に協力し、未解決の数学的予想への挑戦に乗り出すことを期待している。
原文を読む
WeChat で開くにはこちらへ
原文を表示
原创 字节跳动Seed 2025-12-24 11:43 河北
9小时解决11道2025普特南竞赛题
今年 7 月，字节跳动 Seed 团队受邀参加了 IMO 2025。我们的形式化数学推理模型 Seed Prover 通过 3 天的尝试，完整解决了 6 道题目中的 4 道以及一道题的部分证明，达到官方认证的银牌成绩。
近日，我们推出新一代形式化数学推理专用模型 Seed Prover 1.5 ，通过大规模的 Agentic RL 训练，其推理能力和推理效率取得显著进步。相比上一代模型，Seed Prover 1.5 在 16.5 小时内，针对 IMO 2025 的前 5 道题目生成了完整可编译验证的 Lean 证明代码，换算成绩为 35/42，达到此前 IMO 评分标准的金牌分数线。
针对北美本科级别数学竞赛 Putnam，Seed Prover 1.5 用时 9 小时，对 12 道 Putnam 2025 赛题中的 11 道生成了可编译验证的 Lean 代码。更系统的评估中，Seed Prover 1.5 表现出色：它在完整的 Putnam 历史评估集上解决了 88% 的问题，在代表硕士数学难度的 Fate-H 和代表博士生数学难度的 Fate-X 评估集上，分别解决了 80% 和 33% 的问题，刷新了形式化数学推理模型在这几个评测集上的 SOTA 表现。
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
- Agentic Prover：一种新的形式化数学推理范式
大语言模型已能用自然语言流畅解答不少数学问题，不过，面对复杂度极高的前沿数学研究，自然语言证明常出现逻辑跳跃或定义模糊的问题，导致难以完全获得数学家的信任。形式化数学推理则要求模型使用 Lean 等形式语言，构建可在公理系统中机械验证的证明，这意味着其在确保正确性上有着自然语言证明无法比及的优势。
但也正因如此，形式化证明比自然语言证明更加困难。根据“De Bruijn factor”经验法则，一行普通的数学推导，通常需要扩展成 4 到 10 行复杂的代码。这需要模型不仅懂数学，还要精通编程和类型论，而这一高门槛导致形式化证明在效率和成功率上一直远落后于自然语言推理。
以往的研究中，形式化证明器通常分为两类：一类是“步步为营”的 Step-prover，效率很低；一类是“一气呵成”的 Whole-prover，尝试一次性生成完整证明，一旦中间出错则前功尽弃。
Seed Prover 1.5 提出了一种全新的 Agentic Prover 架构来弥合与自然语言推理的差距，其平衡了两种形式化证明方式的优缺点：模型将 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 算力)
- Sketch Model：打通自然语言与形式语言的界限
虽有 Agentic Prover 加持，但模型面对动辄需要上万行代码的复杂定理证明，直接生成完整的形式化代码仍是一个巨大的挑战。为解决这一难题，我们训练了一个 Sketch Model，模拟人类数学家解决问题的方式：先构建高层的证明框架，再补充细节。
这一模型可将自然语言证明拆解为若干个独立的、难度更低的引理，并暂时跳过具体证明，仅保留整体的逻辑骨架。其好处显而易见：将原本不可解的复杂命题，转化成了难度显著降低的子目标。
为训练出优秀的“证明架构师”，我们采用了一种混合奖励信号的强化学习策略：
信号一：Lean 编译器验证生成的草图是否完全正确。
信号二：自然语言 Prover 会逐一检查引理，一旦发现任一引理在数学上不成立，整个草图即被否决。
信号三：引入基于长思维链的 Rubric 评分模型，从语义层面评估草图的质量——考量引理是否与自然语言证明对齐、拆解的粒度是否合适、是否真正降低了原题的难度。
最终，当草图在形式验证、数学正确性和整体评分上均满足要求时，才会获得正向奖励。
基于 Sketch Model，我们还构建了一套高效的测试工作流，形成一个分层级的多智能体协作系统：
Natural Language Prover 负责提供高层的数学直觉和自然语言证明。
Sketch Model 将自然语言转化为形式化的引理结构。
Agentic Prover 并行地攻克每一个被拆解出的引理。
如果某个引理太难证明，系统会递归地调用 Sketch Model 再次进行拆解。这种“分而治之”的策略，不仅规避了长文本生成的错误累积问题，更提升了推理的并行度和成功率。
- 未来展望：AI 解决开放数学问题
现有 AI 系统虽已能较好解决“规则清晰、背景封闭”的数学题目，如 IMO 或 Putnam 等竞赛题，但其距离做出媲美人类专家的数学贡献仍有很大距离。这种局限性源于前沿数学研究中的“依赖性问题”——与解决“无需特定先验知识即可求解”的竞赛题不同，推动前沿数学的发展往往需要综合大量相关论文中的洞见。
为了让 AI 从“做题家”进化为真正的“研究者”，我们还需要解决三个相互关联的核心挑战：
文献发现：让模型能从大量数学文献中识别出最具影响力和相关性的论文。
基于文献的推理：让模型能立足于已有的论文，进行下一步的数学推理。
规模形式化：开发可扩展的方法，将模型从既有论文中推导出的新结果转化为形式化代码。
我们后续将对这几大难题进行探索研究。期待在不远的将来，AI 能够协助人类数学家，共同向开放性数学猜想发起冲击。
阅读原文
跳转微信打开
関連記事
今日のまとめ
AI日報で今日の重要ニュースをまとめ読み