字節(jié)Seed數(shù)學(xué)新模型，SOTA了

時(shí)令 2025-08-04 17:13:05 來(lái)源：量子位

時(shí)令 發(fā)自 凹非寺

量子位 | 公眾號(hào) QbitAI

不僅能達(dá)IMO銀牌水準(zhǔn)，更能解決普特南數(shù)學(xué)競(jìng)賽難題，甚至超越頂尖模型o4-mini！

字節(jié)發(fā)布全新復(fù)雜數(shù)學(xué)解決模型——Seed-Prover。

該模型全面超越了谷歌的AlphaGeometry2，并在MiniF2F數(shù)據(jù)集上實(shí)現(xiàn)了驚人的100%正確率。

不僅如此，Seed-Prover還展現(xiàn)了其卓越的泛化能力：

• 成功解決了78.1%的歷年IMO難題；
• 在普特南數(shù)學(xué)競(jìng)賽中的成績(jī)達(dá)到其他主流模型的4倍；
• 在MiniCTX-2數(shù)據(jù)集上，以81.8%的高正確率遠(yuǎn)超基準(zhǔn)模型o4-mini。

對(duì)此，前谷歌成員Deedy Das驚嘆道：字節(jié)真不愧是唯一一家專為IMO發(fā)表完整論文的AI實(shí)驗(yàn)室！

Seed-Prover模型框架

Seed-Prover是一個(gè)專注于使用Lean 4進(jìn)行形式化推理的大型語(yǔ)言模型。

Lean 4允許用戶精確定義數(shù)學(xué)對(duì)象和定理，并通過(guò)機(jī)器自動(dòng)驗(yàn)證推理步驟的嚴(yán)謹(jǐn)性與正確性。

相較于先前的研究，Seed-Prover最顯著的區(qū)別在于采用了引理式證明作為證明范式，從而將引理置于推理過(guò)程的核心。

簡(jiǎn)單來(lái)說(shuō)，就是在進(jìn)行推理時(shí)，先要求模型生成一些有用的引理，每個(gè)引理由 “l(fā)emma” 關(guān)鍵字引入 ，然后再使用 “theorem” 通過(guò)應(yīng)用生成的引理來(lái)生成主要證明。

這種方法具有幾個(gè)關(guān)鍵優(yōu)勢(shì)：

1、它可以清晰地識(shí)別已成功證明的引理和需要進(jìn)一步完善的引理。

2、由于引理是模塊化的，它們可以獨(dú)立編譯、獨(dú)立存儲(chǔ)和自由組合。

3、證明引理的過(guò)程可能為模型提供靈感，以證明其他未證引理或解決主要問(wèn)題。

為了實(shí)現(xiàn)Seed-Prover的工作流程，研究人員為每個(gè)難題建立了一個(gè)引理池，存儲(chǔ)來(lái)自所有推理運(yùn)行的綜合數(shù)據(jù)，包括引理陳述、引理名稱、完整證明、證明難度和依賴關(guān)系。

根據(jù)可用的推理資源和問(wèn)題難度，字節(jié)還開(kāi)發(fā)了三個(gè)級(jí)別的策略：輕量推理、中等推理和重量級(jí)推理。

由于Lean在幾何支持方面存在不足，Seed-Prover集成了一個(gè)專用的幾何推理引擎Seed-Geometry。

它采用了前向鏈推理的引擎架構(gòu)：即系統(tǒng)通過(guò)檢查適用的規(guī)則來(lái)推導(dǎo)所有已知事實(shí)，直到得出結(jié)論。

此外，Seed-Geometry還具有反向追蹤事實(shí)依賴關(guān)系的能力，能夠識(shí)別一個(gè)幾何問(wèn)題中最小的依賴關(guān)系結(jié)構(gòu)，從而將問(wèn)題本身的上下文與解決該問(wèn)題所需的輔助構(gòu)造有效區(qū)分開(kāi)來(lái)。

基于上述工作，Seed-Geometry建立了一個(gè)包含2.3億個(gè)需要輔助構(gòu)造的獨(dú)特幾何問(wèn)題的庫(kù)。

這是通過(guò)利用過(guò)去20多年數(shù)學(xué)奧林匹克競(jìng)賽的統(tǒng)計(jì)數(shù)據(jù)，并在其專用領(lǐng)域特定語(yǔ)言定義的幾何空間中進(jìn)行廣泛搜索實(shí)現(xiàn)的。

基于這一專屬幾何數(shù)據(jù)訓(xùn)練得到的Seed模型，成為了一個(gè)高效的神經(jīng)-符號(hào)混合幾何證明器。

它可以補(bǔ)全缺失的輔助構(gòu)造元素，并借助幾何推理引擎，按步驟進(jìn)行前向推理，最終完成整個(gè)幾何問(wèn)題的形式化證明。

達(dá)IMO銀牌水準(zhǔn)

研究團(tuán)隊(duì)使用Seed-Prover與Seed-Geometry參加了IMO 2025，完整解決了6道題中的4 道以及一道題的部分證明，在比賽規(guī)定時(shí)間內(nèi)達(dá)到了IMO銀牌水準(zhǔn)。

根據(jù)IMO-AG-50的統(tǒng)計(jì)方法，在2000年至2024年IMO幾何問(wèn)題中，Seed-Geometry (SG) 解決了43道題，比AlphaGeometry 2 (AG2) 多解決1道。

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

此外，值得注意的是，Seed-Geometry還在2秒內(nèi)解出了IMO 2025第2題。

除此之外，對(duì)于MiniF2F測(cè)試集，Seed-Prover達(dá)到了幾乎百分百的正確率。

參考鏈接：
[1]https://x.com/deedydas/status/1951829325839499753
[2]https://www.alphaxiv.org/pdf/2507.23726