谷歌數(shù)學(xué)AI登Nature：IMO金牌幾何水平，定理證明超越吳文俊法

夢(mèng)晨 2024-01-18 19:58:33 來(lái)源：量子位

夢(mèng)晨 發(fā)自 凹非寺
量子位 | 公眾號(hào) QbitAI

谷歌DeepMind再發(fā)Nature，Alpha系列AI重磅回歸，數(shù)學(xué)水平突飛猛進(jìn)。

AlphaGeometry，無(wú)需人類演示達(dá)到IMO金牌選手的幾何水平。

有當(dāng)年AlphaZero無(wú)需人類知識(shí)學(xué)圍棋《Mastering the game of Go without human knowledge》的感覺(jué)了。

具體來(lái)說(shuō)，30道IMO難度的幾何定理證明題，AlphaGeometry做對(duì)25道，人類金牌選手平均25.9道，之前SOTA方法（1978年的吳文俊法）做對(duì)10道。

IMO金牌得主陳誼廷（Evan Chen）負(fù)責(zé)評(píng)估AI生成的答案，他評(píng)價(jià)到：

AlphaGeometry的輸出令人印象深刻，既可驗(yàn)證又干凈。過(guò)去的人工智能解決方案偶然性很大，輸出有時(shí)是正確的，需要人工檢查。

AlphaGeometry沒(méi)有這個(gè)弱點(diǎn)，它的解決方案具有機(jī)器可驗(yàn)證的結(jié)構(gòu)，并且是人類可讀的……它像學(xué)生一樣使用帶有角度和相似三角形的經(jīng)典幾何規(guī)則。

除成績(jī)亮眼之外，這項(xiàng)研究中還有三個(gè)重點(diǎn)引起業(yè)界關(guān)注：

• 無(wú)需人類演示，也就是只用了AI合成數(shù)據(jù)訓(xùn)練，延續(xù)了AlphaZero自學(xué)圍棋的方式。
• 大模型結(jié)合其他AI方法，與AlphaGo和OpenAI Q*傳聞相似。
• 與許多先前方法不同，AlphaGeometry可以生成人類可讀的證明過(guò)程，且模型和代碼都開源。

團(tuán)隊(duì)認(rèn)為，AlphaGeometry提供了一個(gè)實(shí)現(xiàn)高級(jí)推理能力、發(fā)現(xiàn)新知識(shí)的潛在框架。

這可能有助于推動(dòng)人工智能的定理證明——被視為構(gòu)建AGI的關(guān)鍵一步。

另外，量子位在與作者團(tuán)隊(duì)交流過(guò)程中，打聽到了是否真的會(huì)讓AlphaGeometry去參加一屆IMO競(jìng)賽，就像當(dāng)年AlphaGo挑戰(zhàn)人類圍棋冠軍一樣。

他們表示正在努力提高系統(tǒng)的能力，還需要讓AI能解決幾何之外更廣泛的數(shù)學(xué)問(wèn)題。

AI證明幾何也畫輔助線

此前AI系統(tǒng)不能很好解決幾何問(wèn)題，卡就卡在缺乏優(yōu)質(zhì)訓(xùn)練數(shù)據(jù)。

人類學(xué)習(xí)幾何可以借助紙和筆，在圖像上使用現(xiàn)有知識(shí)來(lái)發(fā)現(xiàn)新的、更復(fù)雜的幾何屬性和關(guān)系。

谷歌團(tuán)隊(duì)為此用生成了10億個(gè)隨機(jī)幾何對(duì)象圖，以及其中點(diǎn)和線間的所有關(guān)系，最終篩選出1億不同難度的獨(dú)特定理和證明，AlphaGeometry在這些數(shù)據(jù)上完全從頭訓(xùn)練。

系統(tǒng)由兩個(gè)模塊組成，相互配合尋找復(fù)雜的幾何證明。

• 語(yǔ)言模型，預(yù)測(cè)可用來(lái)解決問(wèn)題的幾何結(jié)構(gòu)（也就是添加輔助線）。
• 符號(hào)推理引擎，使用邏輯規(guī)則推導(dǎo)出結(jié)論。

一作Trieu Trinh介紹，AlphaGeometry的運(yùn)作過(guò)程類似人腦分為快與慢兩種類型。

也就是諾貝爾經(jīng)濟(jì)學(xué)獎(jiǎng)得主丹尼爾·卡尼曼的暢銷書《思考快與慢》中普及的“系統(tǒng)1、系統(tǒng)2”概念。

系統(tǒng)1提供快速、直觀的想法，系統(tǒng)2提供更加深思熟慮、理性的決策。

一方面，語(yǔ)言模型擅長(zhǎng)識(shí)別數(shù)據(jù)中的模式和關(guān)系，可以快速預(yù)測(cè)潛在有用的輔助結(jié)構(gòu)，但通常缺乏嚴(yán)格推理或解釋其決策的能力。

另一方面，符號(hào)推理引擎基于形式邏輯并使用明確的規(guī)則來(lái)得出結(jié)論。它們是理性且可解釋的，但它們緩慢且不靈活，尤其是在獨(dú)自處理大型、復(fù)雜的問(wèn)題時(shí)。

例如在解決一道IMO 2015年的競(jìng)賽題時(shí)，藍(lán)色部分為AlphaGeometry的語(yǔ)言模型添加的輔助結(jié)構(gòu)，綠色部分是最終證明的精簡(jiǎn)版，共有109個(gè)步驟。

在做題過(guò)程中，AlphaGeometry還發(fā)現(xiàn)了2004年IMO競(jìng)賽題中一個(gè)未使用的前提條件，并因此發(fā)現(xiàn)了更廣義的定理版本。

不需要O是BC的中點(diǎn)這個(gè)條件，就能證明P、B、C共線。

另外研究還發(fā)現(xiàn)，對(duì)于人類得分最低的3個(gè)問(wèn)題，AlphaGeometry也需要非常長(zhǎng)的證明過(guò)程和添加非常多的輔助結(jié)構(gòu)才能解決。

但在相對(duì)簡(jiǎn)單的問(wèn)題上，人類平均得分和AI生成的證明長(zhǎng)度之間沒(méi)有顯著相關(guān)性?(p?=??0.06)。

One More Thing

對(duì)于AlphaGeometry與AlphaGo的聯(lián)系和區(qū)別，在與團(tuán)隊(duì)交流過(guò)程中，谷歌科學(xué)家Quoc Le介紹到：

他們都是在一個(gè)非常復(fù)雜的決策空間中搜索，但AlphaGo的方法更傳統(tǒng)（注：神經(jīng)網(wǎng)絡(luò)負(fù)責(zé)模式識(shí)別），AlphaGeometry中的神經(jīng)網(wǎng)絡(luò)負(fù)責(zé)建議下一步要采取的行動(dòng)，指導(dǎo)搜索算法在決策空間中向正確的方向移動(dòng)。

雖然這次成果隨Alpha系列命名，第一單位也是Google DeepMind，但其實(shí)作者主要是前谷歌大腦成員。

Quoc Le大神不用過(guò)多介紹，一作Trieu Trinh與通訊作者Thang Luong都在谷歌工作了六七年，Thang Luong自己高中時(shí)也是IMO選手。

兩位華人作者中，何河是紐約大學(xué)助理教授。吳宇懷此前參與了谷歌數(shù)學(xué)大模型Minerva研究，現(xiàn)在已經(jīng)離開谷歌加入馬斯克團(tuán)隊(duì)，成為xAI的聯(lián)合創(chuàng)始人之一。

論文地址：
https://www.nature.com/articles/s41586-023-06747-5

參考鏈接：
[1]https://www.nature.com/articles/d4186-024-00141-5
[2]https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry