1. 首頁 > 生活百科 > >

字節Seed數學新模型，SOTA了

人工智能中國電信天翼ai

字節Seed數學新模型，SOTA了

文章圖片

字節Seed數學新模型，SOTA了

文章圖片

字節Seed數學新模型，SOTA了

文章圖片

【字節Seed數學新模型，SOTA了】字節Seed數學新模型，SOTA了

文章圖片


時令 發自 凹非寺
量子位 | 公眾號 QbitAI
不僅能達IMO金牌水準 ， 更能解決普特南數學競賽難題 ， 甚至超越頂尖模型o4-mini！
字節發布全新復雜數學解決模型——Seed-Prover 。

該模型全面超越了谷歌的AlphaGeometry2 ， 并在MiniF2F數據集上實現了驚人的100%正確率 。
不僅如此 ， Seed-Prover還展現了其卓越的泛化能力：
成功解決了78.1%的歷年IMO難題； 在普特南數學競賽中的成績達到其他主流模型的4倍； 在MiniCTX-2數據集上 ， 以81.8%的高正確率遠超基準模型o4-mini 。
對此 ， 前谷歌成員Deedy Das驚嘆道：字節真不愧是唯一一家專為IMO發表完整論文的AI實驗室！

Seed-Prover模型框架Seed-Prover是一個專注于使用Lean 4進行形式化推理的大型語言模型 。
Lean 4允許用戶精確定義數學對象和定理 ， 并通過機器自動驗證推理步驟的嚴謹性與正確性 。
相較于先前的研究 ， Seed-Prover最顯著的區別在于采用了引理式證明作為證明范式 ， 從而將引理置于推理過程的核心 。
簡單來說 ， 就是在進行推理時 ， 先要求模型生成一些有用的引理 ， 每個引理由 “lemma” 關鍵字引入， 然后再使用 “theorem” 通過應用生成的引理來生成主要證明 。

這種方法具有幾個關鍵優勢：
1、它可以清晰地識別已成功證明的引理和需要進一步完善的引理 。
2、由于引理是模塊化的 ， 它們可以獨立編譯、獨立存儲和自由組合 。
3、證明引理的過程可能為模型提供靈感 ， 以證明其他未證引理或解決主要問題 。
為了實現Seed-Prover的工作流程 ， 研究人員為每個難題建立了一個引理池 ， 存儲來自所有推理運行的綜合數據 ， 包括引理陳述、引理名稱、完整證明、證明難度和依賴關系 。
根據可用的推理資源和問題難度 ， 字節還開發了三個級別的策略：輕量推理、中等推理和重量級推理 。

由于Lean在幾何支持方面存在不足 ， Seed-Prover集成了一個專用的幾何推理引擎Seed-Geometry 。
它采用了前向鏈推理的引擎架構：即系統通過檢查適用的規則來推導所有已知事實 ， 直到得出結論 。
此外 ， Seed-Geometry還具有反向追蹤事實依賴關系的能力 ， 能夠識別一個幾何問題中最小的依賴關系結構 ， 從而將問題本身的上下文與解決該問題所需的輔助構造有效區分開來 。
基于上述工作 ， Seed-Geometry建立了一個包含2.3億個需要輔助構造的獨特幾何問題的庫 。
這是通過利用過去20多年數學奧林匹克競賽的統計數據 ， 并在其專用領域特定語言定義的幾何空間中進行廣泛搜索實現的 。
基于這一專屬幾何數據訓練得到的Seed模型 ， 成為了一個高效的神經-符號混合幾何證明器 。
它可以補全缺失的輔助構造元素 ， 并借助幾何推理引擎 ， 按步驟進行前向推理 ， 最終完成整個幾何問題的形式化證明 。
達IMO金牌水準研究團隊使用Seed-Prover與Seed-Geometry參加了IMO 2025 ， 成功證明了6道題中的5道 ， 達到了IMO金牌水準 。
根據IMO-AG-50的統計方法 ， 在2000年至2024年IMO幾何問題中 ， Seed-Geometry (SG) 解決了43道題 ， 比AlphaGeometry 2 (AG2) 多解決1道 。

對于2000年至2022年難度大的多的IMO候選題中的幾何題 ， AlphaGeometry 2解決了19道 ， 而Seed-Geometry解決了22道 。

此外 ， 值得注意的是 ， Seed-Geometry還在2秒內解出了IMO 2025第2題——IMO中表現最差的兩道題中的一道 。
除此之外 ， 對于MiniF2F測試集 ， Seed-Prover達到了幾乎百分百的正確率 。

參考鏈接：[1
https://x.com/deedydas/status/1951829325839499753[2
https://www.alphaxiv.org/pdf/2507.23726
— 完 —
量子位 QbitAI · 頭條號簽約
關注我們 ， 第一時間獲知前沿科技動態

    推薦閱讀