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

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

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

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

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

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

Seed-Prover模型框架

Seed-Prover是一個專注于使用Lean 4進行形式化推理的大型語言模型。

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

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

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

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

1、它可以清晰地識別已成功證明的引理和需要進一步完善的引理。

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

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

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

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

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

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

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

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

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

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

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

達IMO銀牌水準(zhǔn)

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

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

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

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

除此之外，對于MiniF2F測試集，Seed-Prover達到了幾乎百分百的正確率。