近日，AI 初創(chuàng)公司 Axiom 宣布其模型在沒有人類干預(yù)的情況下，自動完成了兩個數(shù)學(xué)猜想的證明——埃爾德什問題（Erd?s Problem）中的 481 號和 124 號。

據(jù)稱，481 號問題僅用時 5 小時，代碼量為 656 行；124 號問題則耗時超 24 小時。值得關(guān)注的是，這些證明均通過 Lean 驗證，Lean 的特點是其形式化證明過程無需人工干預(yù)，為數(shù)學(xué)正確性提供了保障。

（X）

據(jù)悉，本次完成兩個數(shù)學(xué)猜想的證明的并不是 Axiom 推出的 API 或完整的產(chǎn)品，而是一個由多個模型組成的系統(tǒng)，包括 Axiom 的通過強(qiáng)化學(xué)習(xí)后訓(xùn)練研發(fā)的模型。

該公司 CEO 洪樂潼（Carina Hong）對 DeepTech 表示：“六百多行代碼對于形式化的證明來說，算是比較簡潔和漂亮的證明。”

（X）

該證明在社交媒體發(fā)布后，有用戶評價稱“埃爾德什問題的精簡形式化令人耳目一新”，也有用戶評價本次證明是一個“好的起點”，還有用戶這樣評價：“幾周前 OpenAI 曾稱聲稱用 GPT-5 解決了埃爾德什問題，但社區(qū)指出它只檢索了現(xiàn)有文獻(xiàn)。而 Axiom 實際上證明了這個問題。”

圖丨X 上用戶評論（X）

埃爾德什問題是匈牙利數(shù)學(xué)家保羅·埃爾德什（Paul Erd?s）提出的一系列懸而未決的數(shù)學(xué)猜想，長期被視為檢驗推理能力的試金石。

圖丨埃爾德什問題 481 號（Erd?s Problem）

481 號問題是一個社區(qū)近 45 年未被解決的問題，即某種迭代算術(shù)過程是否必然在某一步產(chǎn)生重復(fù)，從而進(jìn)入循環(huán)或重復(fù)狀態(tài)。

圖丨Axiom 模型證明的 481 號問題（洪樂潼）

而 124 號問題是：考慮若干整數(shù)基數(shù) (d_1 < d_2 < cdots < d_r)（且每個 (d_i ge 3)），構(gòu)造由這些基數(shù)的不同比例冪構(gòu)成的序列。這是一個近 30 年未被解決的問題，也是最近比較火熱的話題之一。

幾天前，我們對 Harmonic 公司開發(fā)的 Aristotle 模型自主解決埃爾德什問題 124 號進(jìn)行了報道，該公司由 Robinhood 的 CEO 弗拉德·特涅夫（Vlad Tenev）創(chuàng)立。

圖丨埃爾德什問題 124 號（Erd?s Problem）

“關(guān)于 124 號問題，我們跑了超過一天的時間，中途一定是走到某個‘死胡同’里了。盡管目前跑出來的證明比較長，不如我們期望的簡練，但至少它跑出來了。”洪樂潼說。

圖丨Axiom 模型證明的 124 號問題（洪樂潼）

Axiom 是一家成立不到 4 個月的公司，據(jù)公開資料其目前已融資 6,400 萬美元的種子輪融資，成員不到 20 人。該公司 CEO 洪樂潼是 00 后，她在美國麻省理工學(xué)院獲得數(shù)學(xué)和物理雙學(xué)士學(xué)位，并在英國牛津大學(xué)獲得神經(jīng)科學(xué)碩士學(xué)位。此前，她曾在美國斯坦福大學(xué)攻讀數(shù)學(xué)和法學(xué)博士學(xué)位，后輟學(xué)。

Axiom 官網(wǎng)稱，其創(chuàng)新性體現(xiàn)在通過融合 AI、編程語言和數(shù)學(xué)，開發(fā)能夠解決復(fù)雜數(shù)學(xué)問題的人工智能系統(tǒng)，其初始模型是 AI 數(shù)學(xué)家。一方面，其可啟發(fā)人類數(shù)學(xué)家的科研靈感，另一方面可成為人類數(shù)學(xué)家的合作者，而非替代者。最新公開消息顯示，著名數(shù)學(xué)家小野健（Ken Ono）剛從美國弗吉尼亞大學(xué)離職加入 Axiom 擔(dān)任創(chuàng)始數(shù)學(xué)家，他曾在 2020 年擔(dān)任洪樂潼研究項目的導(dǎo)師。

該公司官網(wǎng)提到，我們現(xiàn)在處于一個“數(shù)學(xué)發(fā)現(xiàn)”的時代。其在博客中曾提到過一個想法：人類在自然語言中進(jìn)行推理，而該公司的模型在進(jìn)行形式化推理時，會把自然語言的推理過程轉(zhuǎn)化為形式化代碼。在這個過程中，形式化代碼的運(yùn)行結(jié)果會反饋回來，進(jìn)而影響人類在自然語言推理上的直覺和思考方式。

實際上，這個過程可以拓展到更廣泛的應(yīng)用領(lǐng)域，比如金融、量化交易、芯片、硬件和軟件的形式驗證、物理定律的形式化推導(dǎo)等。

自動形式化是近年來被關(guān)注新的方向，其把自然語言的證明轉(zhuǎn)換到 Lean 語言中，這個過程與證明和形式化證明同樣重要，且在一個系統(tǒng)中同時訓(xùn)練，而不是分開訓(xùn)練。

洪樂潼對 DeepTech 解釋道：“我們對數(shù)據(jù)主要依賴自動生成，無論是從自然語言到形式化的自動轉(zhuǎn)換，還是在形式化的基礎(chǔ)上自動生成 100 到 1,000 倍的變體，甚至可以借鑒類似編譯器中的想法和手段。”

據(jù)了解，Axiom 目前正在設(shè)計內(nèi)部的基準(zhǔn)數(shù)據(jù)集，旨在用更難的數(shù)據(jù)集來挑戰(zhàn)其模型能否進(jìn)一步突破極限。此外，他們還希望讓猜想和證明可以做持續(xù)的非對稱自我博弈以及事后重演。

洪樂潼認(rèn)為，AI for Maths 是 AI for Science 的理論層和算法層，她表示：“大家可能覺得解決了埃爾德什問題很了不起，但我認(rèn)為這只能說明模型具備了一定的能力，但我們也必須清醒地看到，它距離成為真正的 AI 數(shù)學(xué)家還有一定的距離，比如在數(shù)論、代數(shù)幾何、代數(shù)拓?fù)洹⑽⒎滞負(fù)涞确较蛏衔覀冞€有很大的進(jìn)步空間。”

從融資規(guī)模與公司體量來看，Axiom 當(dāng)前進(jìn)展已引發(fā)行業(yè)關(guān)注。后續(xù)能否進(jìn)一步與競爭對手拉開差距并形成落地產(chǎn)品，還需多一些的耐心與觀察。

參考資料：

https://x.com/carinalhong/status/1995905801719066763?s=46

https://b.capital/why-we-invested/toward-mathematical-superintelligence-why-we-invested-in-axiom/

https://axiommath.ai/

https://www.erdosproblems.com/

https://techfundingnews.com/axiom-math-ai-mathematician-64m-seed/

https://www.wsj.com/tech/ai/math-ken-ono-carina-hong-axiom-startup-649bc417

運(yùn)營/排版：何晨龍