剛剛！字節跳動 Seed Prover 1.5 發布

AIPress.com.cn報道

12月24日消息，字節跳動 Seed 團隊發布了新一代形式化數學推理模型 Seed Prover 1.5。該模型基于全新的 Agentic 架構 與大規模強化學習訓練，在多項高難度數學評測中實現突破，刷新了形式化數學推理模型的性能紀錄。

今年 7 月，Seed 團隊受邀參與 IMO 2025（國際數學奧林匹克）。當時，Seed Prover 在 3 天內完成了 6 道試題中的 4 道完整證明及 1 道部分證明，獲得官方認證的 銀牌成績。

而在最新一代模型中，Seed Prover 1.5 進一步將成績推向新高度：在 16.5 小時 內，對 IMO 2025 前 5 道題生成了 完整、可編譯驗證的 Lean 證明代碼，換算得分為 35/42，達到以往評分體系下IMO的金牌分數線。

在北美本科數學競賽 Putnam 中，Seed Prover 1.5 同樣表現突出。模型用時約 9 小時，對 12 道賽題中的 11 道生成了可驗證的 Lean 代碼。更系統的評估顯示，該模型在 Putnam 歷史評估集上的解題率達到 88%；在代表碩士與博士數學難度的 Fate-H 與 Fate-X 評測集中，分別解決了 80% 和 33% 的問題，刷新了多個評測集上的 SOTA 紀錄。

此次能力躍升，核心來自 Seed 團隊提出的 Agentic Prover 架構。不同于傳統形式化證明中“逐步生成”或“一次成型”的兩種極端方式，Seed Prover 1.5 將 Lean 語言視作一種可調用工具，允許模型在證明過程中靈活使用 Mathlib 定理檢索、Python 計算驗證、增量式引理保存與復用 等多種能力。這種設計使模型能夠在復雜推理中不斷修正路徑，顯著提升成功率與效率。

在訓練方法上，Seed Prover 1.5 采用了 大規模 Agentic 強化學習（RL）。官方表示，Lean 編譯器提供了絕對客觀的“對/錯”反饋，為強化學習提供了高質量的獎勵信號。隨著RL訓練步數增加，模型在訓練集上的證明通過率從 50% 提升至近 90%，同時在高難度任務中以更低算力消耗，超越上一代模型。

為進一步縮小自然語言與形式語言之間的鴻溝，Seed 團隊還訓練了 Sketch Model。該模型模擬人類數學家的工作方式，先生成高層證明框架，再將復雜命題拆解為多個可并行求解的引理。

在此基礎上，Seed Prover 1.5 構建了一套多智能體協作流程：由自然語言模型提供數學直覺，Sketch Model 生成證明結構，Agentic Prover 并行完成形式化驗證，從而顯著提升復雜定理的求解成功率。

Seed 團隊表示，當前 AI 已能在規則清晰、背景封閉的競賽型數學問題中取得突破，但距離參與真正的前沿數學研究仍有差距。未來，團隊將繼續探索 數學文獻發現、基于文獻的推理能力，以及大規模形式化方法，推動 AI 從“解題工具”向“數學研究助手”演進。

目前，Seed Prover 1.5 的技術報告已在 arXiv 公開，相關 Lean 證明代碼也已上線 GitHub，后續將逐步開放 API，面向數學與 AI 研究者提供體驗。