AIPress.com.cn報(bào)道

12月24日消息，字節(jié)跳動 Seed 團(tuán)隊(duì)發(fā)布了新一代形式化數(shù)學(xué)推理模型 Seed Prover 1.5。該模型基于全新的 Agentic 架構(gòu) 與大規(guī)模強(qiáng)化學(xué)習(xí)訓(xùn)練，在多項(xiàng)高難度數(shù)學(xué)評測中實(shí)現(xiàn)突破，刷新了形式化數(shù)學(xué)推理模型的性能紀(jì)錄。

今年 7 月，Seed 團(tuán)隊(duì)受邀參與 IMO 2025（國際數(shù)學(xué)奧林匹克）。當(dāng)時(shí)，Seed Prover 在 3 天內(nèi)完成了 6 道試題中的 4 道完整證明及 1 道部分證明，獲得官方認(rèn)證的 銀牌成績。

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

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

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

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

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

在此基礎(chǔ)上，Seed Prover 1.5 構(gòu)建了一套多智能體協(xié)作流程：由自然語言模型提供數(shù)學(xué)直覺，Sketch Model 生成證明結(jié)構(gòu)，Agentic Prover 并行完成形式化驗(yàn)證，從而顯著提升復(fù)雜定理的求解成功率。

Seed 團(tuán)隊(duì)表示，當(dāng)前 AI 已能在規(guī)則清晰、背景封閉的競賽型數(shù)學(xué)問題中取得突破，但距離參與真正的前沿?cái)?shù)學(xué)研究仍有差距。未來，團(tuán)隊(duì)將繼續(xù)探索 數(shù)學(xué)文獻(xiàn)發(fā)現(xiàn)、基于文獻(xiàn)的推理能力，以及大規(guī)模形式化方法，推動 AI 從“解題工具”向“數(shù)學(xué)研究助手”演進(jìn)。

目前，Seed Prover 1.5 的技術(shù)報(bào)告已在 arXiv 公開，相關(guān) Lean 證明代碼也已上線 GitHub，后續(xù)將逐步開放 API，面向數(shù)學(xué)與 AI 研究者提供體驗(yàn)。