谷歌AI拿下IMO銀牌，僅差一分得金！第四題僅用時(shí)19秒

西風(fēng) 2024-07-26 08:48:08 來(lái)源：量子位

白交 西風(fēng) 發(fā)自 凹非寺

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

剛剛，大模型再次攻下一城！

谷歌DeepMind宣布，他們數(shù)學(xué)AI“摘得”IMO（國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽）銀牌，并且距離金牌僅一分之差！

是的，沒(méi)有聽(tīng)錯(cuò)！就是難到絕大多數(shù)人類(lèi)的奧數(shù)題。要知道今年IMO全部609名參賽者，也僅有58位達(dá)到了金牌水平。

此次，谷歌AI解決了2024 IMO競(jìng)賽6道題目中的4道，而且一做一個(gè)滿分，總共獲得28分。（滿分42分，金牌分?jǐn)?shù)線29分）

其中第四題幾何題，AI僅僅用時(shí)19秒？！

而號(hào)稱(chēng)本屆最難的第六題，今年僅有五名參賽者拿下，它也完全答對(duì)。

此次的成績(jī)還得到了IMO組委的專(zhuān)業(yè)認(rèn)證——由IMO金牌得主、菲爾茲獎(jiǎng)獲得者Timothy Gowers教授和兩屆IMO金牌得主、2024 IMO問(wèn)題選擇委員會(huì)主席Joseph Myers博士進(jìn)行評(píng)分。

Timothy Gowers教授直接驚嘆：遠(yuǎn)遠(yuǎn)超過(guò)我認(rèn)知的最先進(jìn)水平。

來(lái)康康是如何做到的？

谷歌拿下IMO銀牌，Alpha家族新成員問(wèn)世

此次拿下IMO銀牌的是谷歌兩位Alpha家族成員，他們各自數(shù)業(yè)有專(zhuān)攻。

• AlphaProof，Alpha家族新成員，基于強(qiáng)化學(xué)習(xí)的形式數(shù)學(xué)推理系統(tǒng)。
• AlphaGeometry 2，此前AlphaGeometry改進(jìn)版，專(zhuān)門(mén)用于解決幾何問(wèn)題。

先來(lái)認(rèn)識(shí)一下新成員——AlphaProof。

它是一個(gè)自訓(xùn)練系統(tǒng)，能用形式語(yǔ)言Lean來(lái)證明數(shù)學(xué)陳述。它能將預(yù)先訓(xùn)練好的語(yǔ)言模型與AlphaZero強(qiáng)化學(xué)習(xí)算法結(jié)合在一起。

團(tuán)隊(duì)通過(guò)微調(diào)Gemini，能自動(dòng)將自然語(yǔ)言陳述轉(zhuǎn)換為形式語(yǔ)言Lean陳述，由此創(chuàng)建了一個(gè)大型數(shù)學(xué)題庫(kù)。

當(dāng)遇到問(wèn)題時(shí)，AlphaProof會(huì)生成解決方案候選，然后通過(guò)搜索Lean中可能的證明步驟來(lái)證明或反駁這些候選。

每個(gè)找到并驗(yàn)證的證明都會(huì)用于強(qiáng)化AlphaProof的語(yǔ)言模型，從而提高其解決后續(xù)更具挑戰(zhàn)性的問(wèn)題的能力。

在比賽的前幾周內(nèi)，它就這么循環(huán)往復(fù)地用數(shù)百萬(wàn)個(gè)IMO級(jí)別題目進(jìn)行了訓(xùn)練。

比賽期間也應(yīng)用了訓(xùn)練循環(huán)，不斷強(qiáng)化自身證明，直到找到完整的解決方案。

再來(lái)了解一下進(jìn)化之后的AlphaGeometry 2。它是一個(gè)神經(jīng)-符號(hào)混合系統(tǒng)，其中語(yǔ)言模型基于Gemini。

它的前身1.0今年還登上了Nature：無(wú)需人類(lèi)演示達(dá)到IMO金牌選手的幾何水平。

跟上一個(gè)版本比，它使用了更大一數(shù)量級(jí)的合成數(shù)據(jù)進(jìn)行從頭訓(xùn)練。而它采用的符號(hào)引擎比其前代快兩個(gè)數(shù)量級(jí)。當(dāng)遇到新問(wèn)題時(shí)，會(huì)使用一種新的知識(shí)共享機(jī)制來(lái)實(shí)現(xiàn)不同搜索樹(shù)的高級(jí)組合，以解決更復(fù)雜的問(wèn)題。

在正式比賽之前，它就已經(jīng)可以解決過(guò)去25年所有IMO幾何問(wèn)題中的83%，而其前身的解決率僅為53%。

今年IMO賽事中，它僅用了19秒就完成了第四個(gè)問(wèn)題。

接著就來(lái)看看，此次IMO這兩位是如何配合發(fā)揮的。

首先，問(wèn)題被手動(dòng)翻譯成正式的數(shù)學(xué)語(yǔ)言，以便系統(tǒng)理解。

我們知道人類(lèi)比賽時(shí)，分兩次提交答案，每次有4.5個(gè)小時(shí)。

而谷歌這兩個(gè)系統(tǒng)先是在幾分鐘內(nèi)解決了一個(gè)問(wèn)題，其他問(wèn)題則是花了三天時(shí)間。

最終，AlphaProof通過(guò)確定答案并證明其正確性，解決了兩道代數(shù)題和一道數(shù)論題。

其中包括比賽中最難的一道題，也就是，今年的IMO比賽中僅有五名選手解出的第六題。

AlphaGeometry 2解決了幾何問(wèn)題，而兩道組合問(wèn)題仍未解決。

除此之外，谷歌團(tuán)隊(duì)還試驗(yàn)了一種基于Gemini的自然語(yǔ)言推理系統(tǒng)。換言之，無(wú)需將問(wèn)題翻譯成形式語(yǔ)言，并且可以跟其他AI系統(tǒng)結(jié)合使用。

團(tuán)隊(duì)表示，他們接下來(lái)還會(huì)探索更多用于推進(jìn)數(shù)學(xué)推理的AI方法。

而關(guān)于AlphaProof的更多技術(shù)細(xì)節(jié)，也計(jì)劃很快發(fā)布。

網(wǎng)友：不懂?dāng)?shù)學(xué)但大受震撼

看到這兩個(gè)系統(tǒng)的表現(xiàn)，網(wǎng)友們紛紛表示“不懂?dāng)?shù)學(xué)但大受震撼”。

AI程序員Devin團(tuán)隊(duì)Cognition AI聯(lián)合創(chuàng)始人Scott Wu表示：

這樣的結(jié)果真是令人驚嘆。小時(shí)候，奧林匹克競(jìng)賽就是我的全部。從未想過(guò)它們會(huì)在10年后被人工智能解決。

OpenAI科學(xué)家Noam Brown也開(kāi)麥祝賀：

不過(guò)，也有網(wǎng)友表示，如果按照標(biāo)準(zhǔn)比賽時(shí)間（競(jìng)賽分兩天進(jìn)行，每天四個(gè)半小時(shí)，每天解決三個(gè)題），這兩個(gè)AI系統(tǒng)實(shí)際上只能解決6個(gè)問(wèn)題中的一個(gè)。

這一說(shuō)法立刻得到了部分網(wǎng)友反駁：

在此情境中，速度不是主要關(guān)注點(diǎn)。如果浮點(diǎn)操作次數(shù)（flops）保持不變，增加計(jì)算資源會(huì)縮短解決問(wèn)題所需的時(shí)間。

針對(duì)這一點(diǎn)，也有網(wǎng)友疑問(wèn)道：

兩個(gè)AI系統(tǒng)沒(méi)能解答出組合題，是訓(xùn)練的問(wèn)題還是計(jì)算資源不夠，時(shí)間上不行？或者還存在其他限制嗎？

Timothy Gowers教授發(fā)推文給出了他的看法：

如果允許人類(lèi)參賽者在每個(gè)問(wèn)題上花費(fèi)更多時(shí)間，他們的得分無(wú)疑會(huì)更高。然而，對(duì)于AI系統(tǒng)來(lái)說(shuō)，這已經(jīng)遠(yuǎn)超以往自動(dòng)定理證明器的能力；其次，隨著效率的提高，所需時(shí)間有望進(jìn)一步縮短。

不過(guò)前兩天大模型還困于“9.11和9.9哪個(gè)數(shù)字更大？”這么一個(gè)小學(xué)題，怎么這一邊大模型又能解決奧數(shù)級(jí)別的難題了？！

失了智，然后現(xiàn)在怎么又靈光乍現(xiàn)，恢復(fù)了智？

英偉達(dá)科學(xué)家Jim Fan給出解釋?zhuān)菏?strong>訓(xùn)練數(shù)據(jù)分布的問(wèn)題。

谷歌的這個(gè)系統(tǒng)是在形式證明和領(lǐng)域特定符號(hào)引擎上進(jìn)行訓(xùn)練的。某種程度上說(shuō)，它們?cè)诮鉀Q奧林匹克競(jìng)賽方面高度專(zhuān)業(yè)化，即使它們建立在通用大模型基礎(chǔ)上。

而像GPT-4o的訓(xùn)練集中混有大量GitHub代碼數(shù)據(jù)，可能遠(yuǎn)遠(yuǎn)超過(guò)數(shù)學(xué)數(shù)據(jù)。在軟件版本中，“v9.11>v9.9”，這可能會(huì)嚴(yán)重扭曲分布。所以說(shuō)，這個(gè)錯(cuò)誤還算說(shuō)得過(guò)去。

對(duì)于這一奇怪現(xiàn)象，他將其形容為

我們發(fā)現(xiàn)了一個(gè)非常奇特的區(qū)域，就像一顆看起來(lái)像地球卻遍布奇異山谷的系外行星。

還有熱心的網(wǎng)友cue了下OpenAI，也許你們也可以嘗試……

對(duì)此，奧特曼的回復(fù)是：

參考鏈接：
[1]https://x.com/googledeepmind/status/1816498082860667086?s=46
[2]https://x.com/jeffdean/status/1816498336171753948?s=46
[3]https://x.com/quocleix/status/1816501362328494500?s=46
[4]https://x.com/drjimfan/status/1816521330298356181?s=46
[5]https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/