金磊 發(fā)自 凹非寺量子位 | 公眾號 QbitAI
不得了，這個名叫Gauss（高斯）的新AI Agent，有點(diǎn)殺瘋了的感覺。
因?yàn)樗挥昧巳艿臅r間，就完成了陶哲軒和Alex Kontorovich提出的數(shù)學(xué)挑戰(zhàn)——
在Lean中形式化強(qiáng)素?cái)?shù)定理（Prime Number Theorem，PNT）。
要知道，陶哲軒和Kontorovich在2024年1月提出這個挑戰(zhàn)后，足足花了18個月（今年7月）的時間，也才取得階段性的進(jìn)展。
那么這個Gauss到底是什么來頭？
它的背后是一家叫做Math的AI公司，據(jù)介紹，Gauss是首個可以協(xié)助頂級數(shù)學(xué)家進(jìn)行形式驗(yàn)證的自動形式化（autoformalization）Agent：
這里的形式化（formalization），指的是把人類寫的數(shù)學(xué)內(nèi)容轉(zhuǎn)換成一種機(jī)器可讀、可檢查、嚴(yán)密無歧義的形式語言，然后利用計(jì)算機(jī)幫助驗(yàn)證其正確性。
而陶哲軒和Alex Kontorovich之所以目前僅取得階段性進(jìn)展，問題就卡在了復(fù)分析（complex analysis）的核心難題上。
而這個Gauss作為硅基生命，它的特點(diǎn)就是可以不停的工作，極大地壓縮了以前只有頂尖形式化專家才能完成的工作量；與此同時，Gauss還形式化了上面提到的復(fù)分析中關(guān)鍵的缺失結(jié)果。
這就是為什么它能三周解決陶哲軒18個月都未能完成的數(shù)學(xué)挑戰(zhàn)的原因了。
Gauss是如何實(shí)現(xiàn)的？
目前Math公司官方并沒有發(fā)布具體的技術(shù)報(bào)告。
但從最終結(jié)果來看，Gauss生成了大約25000行Lean代碼，包含上千個定理和定義。
要知道，這種規(guī)模的形式化證明，以前往往需要多年才能完成。
歷史上最大的單個形式化項(xiàng)目（往往需要跨甚至10年的時間），也只是比這大一個數(shù)量級（最多50萬行代碼）。
相比之下，Lean的標(biāo)準(zhǔn)數(shù)學(xué)庫Mathlib有約200萬行代碼，包含35萬個定理，但卻由600多位貢獻(xiàn)者花了8年時間才建立起來。
為了支撐Gauss的運(yùn)行，團(tuán)隊(duì)還和Morph Labs合作開發(fā)了Trinity環(huán)境基礎(chǔ)設(shè)施。
因?yàn)橐孏auss如此大規(guī)模運(yùn)行，會涉及數(shù)千個并發(fā)Agent，且每個Agent都有自己的Lean運(yùn)行環(huán)境，會消耗數(shù)TB的集群內(nèi)存，是一個極其復(fù)雜的系統(tǒng)工程挑戰(zhàn)。
Math團(tuán)隊(duì)還表示：
Gauss將大幅縮短完成大型數(shù)學(xué)項(xiàng)目所需的時間。隨著算法不斷進(jìn)步，我們計(jì)劃在未來12個月內(nèi)，讓形式化代碼的總量提升100到1000倍。這將成為新范式的訓(xùn)練場——走向“可驗(yàn)證的超級智能”和“通才型機(jī)器數(shù)學(xué)家”。
而就在剛剛，陶哲軒本人在Mastodon上對形式化相關(guān)的問題做了一番解釋（以下為陶哲軒的陳述）。
任何復(fù)雜的項(xiàng)目往往都有明確陳述的目標(biāo)和隱含的未陳述目標(biāo)。例如，一個Lean形式化項(xiàng)目的明確目標(biāo)可能是獲得某個數(shù)學(xué)命題X的形式化證明；但通常還有一些未陳述的目標(biāo)，例如以適合上游到 Mathlib 庫的方式形式化X的關(guān)鍵子命題和定義X1, X2, …；學(xué)習(xí)如何使用各種協(xié)作工具和分配任務(wù)；有機(jī)地發(fā)現(xiàn)X證明的更精細(xì)結(jié)構(gòu)，這在以前的非形式化證明中可能沒有被強(qiáng)調(diào)；為新手形式化者提供實(shí)際培訓(xùn)和經(jīng)驗(yàn)；以及更普遍地建立一個精通形式化藝術(shù)的人類社區(qū)。
過去，通常沒有必要闡明這些隱含目標(biāo)，因?yàn)檫@些目標(biāo)的實(shí)現(xiàn)與明確目標(biāo)的實(shí)現(xiàn)之間存在很強(qiáng)的經(jīng)驗(yàn)相關(guān)性。在形式化項(xiàng)目的例子中，幾乎任何以人為中心的努力來實(shí)現(xiàn)明確目標(biāo)，最終都會自然而然地實(shí)現(xiàn)上述大部分隱含目標(biāo)。因此，明確目標(biāo)有效地成為了更廣泛實(shí)際目標(biāo)的可行替代。
然而，隨著功能強(qiáng)大的AI工具的出現(xiàn)，情況正在發(fā)生變化，這些工具采用與人類截然不同的方法。這些工具可以被指示去解決一個明確的目標(biāo)，而不必實(shí)現(xiàn)如果由人類團(tuán)隊(duì)執(zhí)行任務(wù)時可能同時實(shí)現(xiàn)的所有隱含目標(biāo)。事實(shí)上，AI優(yōu)化算法的性質(zhì)決定了它們甚至可能以犧牲所有隱含目標(biāo)為代價，在明確目標(biāo)上取得高績效。（參見古德哈特定律：“當(dāng)一個衡量標(biāo)準(zhǔn)成為目標(biāo)時，它就不再是一個好的衡量標(biāo)準(zhǔn)?！保?/p>
鑒于這些工具的日益部署，這向我表明，項(xiàng)目組織者現(xiàn)在需要付出更大的努力，明確闡述項(xiàng)目的所有目標(biāo)，而不僅僅是名義上的目標(biāo)。在某些情況下，這些目標(biāo)甚至可能最初對組織者自己來說并不明顯，可能需要參與者之間進(jìn)行一些討論。而有興趣用其AI工具測試此類項(xiàng)目的外部各方，則應(yīng)提前與組織者協(xié)調(diào)，以防他們遺漏了一個或多個其工具不會優(yōu)化的關(guān)鍵隱含目標(biāo)。
創(chuàng)始人是ICML’25時間檢驗(yàn)獎作者
值得一提的是，Math這家公司的老板也是有點(diǎn)實(shí)力在身上的。
因?yàn)樗悄孟陆衲闍I定會ICML時間檢驗(yàn)獎?wù)撐牡淖髡咧?，Christian Szegedy。
這篇論文是他和另一位作者Sergey Loffe在2015年提出的Batch Normalization（批次歸一化，簡稱BatchNorm）。
如今，這篇論文的引用量超過6萬次，是深度學(xué)習(xí)發(fā)展史上一個里程碑式的突破，極大地推動了深層神經(jīng)網(wǎng)絡(luò)的訓(xùn)練和應(yīng)用。
可以說它是讓深度學(xué)習(xí)從小規(guī)模實(shí)驗(yàn)，走向大規(guī)模實(shí)用化和可靠性的關(guān)鍵技術(shù)之一。
當(dāng)然，網(wǎng)友們看罷Gauss之后雖然驚呼Amazing，但同時也在喊官方趕緊把論文公開嘍。
至于更細(xì)節(jié)的技術(shù)內(nèi)容，我們可以蹲一波了~
參考鏈接：[1]https://x.com/mathematics_inc/status/1966194751847461309[2]https://www.math.inc/gauss[3]https://www.math.inc/vision
