陶哲軒支持！AI奧林匹克數(shù)學獎來了，獎金500萬美元，尋找能得IMO金牌的大模型

豐色 2023-11-28 15:35:06 來源：量子位

豐色 蕭簫 發(fā)自 凹非寺

量子位 | 公眾號 QbitAI

專門為AI設(shè)立的IMO國際奧林匹克數(shù)學競賽來了——

獎金足足1000萬美元那種！

該比賽號稱要“代表新的圖靈測試”，怎么比？

和人類最聰明的數(shù)學小天才們正面PK，拿到同樣標準的金牌。

可別小看這一賽事，就連數(shù)學大牛陶哲軒都來了，并在官網(wǎng)傾力推薦：

這個比賽提供了一套鑒別AI解決問題策略的基準，而這正是我們現(xiàn)在需要的。

消息一出，網(wǎng)友們是相當興奮。

如IMO主席所說：到底哪個大模型能和世界上最聰明的一波年輕人相媲美？

所謂“重賞之下，必有勇夫”，有著自己路數(shù)的AI也著實令人期待。

AI參賽IMO，最高拿500萬美元

這項比賽的簡稱AI-MO。

它的初衷就是推動大語言模型的數(shù)學推理能力，鼓勵開發(fā)能夠匹配人類數(shù)學最高水平（IMO競賽）的新AI模型。

為什么選IMO為基準？

IMO的題目一般分為代數(shù)、幾何、數(shù)論和組合數(shù)學四大類，不需要高等數(shù)學知識，但需要參賽者有正確的思維方式和數(shù)學素養(yǎng)。

統(tǒng)計顯示，其金牌獲得者奪得菲爾茲獎的可能性是普通劍橋博士畢業(yè)生的50倍。

此外，有一半的菲爾茲獎獲得者曾參加過IMO競賽。

基于該比賽，這項專門為AI舉辦的AI-MO大賽將于2024年初開放。

組委會要求，參加的AI模型必須和人類選手采用相同的格式處理題目，并且必須生成人類可讀的最終答案，然后由專家小組使用IMO標準對其進行評分。

比賽結(jié)果將隨明年7月在英國巴斯舉行的第65屆IMO大會一同揭曉。

最終，達到金牌水平的AI將獲得500萬美元的大獎。

剩余“實現(xiàn)了關(guān)鍵里程碑”的AI模型們則瓜分剩下的進步獎，總金額也是500萬美元。

值得一提的是，為了拿到獲獎資格，參賽者必須遵守AI-MO公共共享協(xié)議，也就是獲獎模型必須得開源。

至于具體的規(guī)則，組委會還在商議中，以及目前官方還在招募顧問委員會成員（特別需要數(shù)學家、AI和機器學習專家）和領(lǐng)導這項比賽的總監(jiān)，都是付費的且可以完全遠程，不知道哪些大佬會加入。

不過需要注意的是，AI-MO并非IMO官方發(fā)起的比賽。

其真正的發(fā)起機構(gòu)是XTX Markets，一家位于英國倫敦、搞機器學習量化交易的非銀行金融機構(gòu)。

別的不說，XTX Markets主打一個豪氣。

它還在去年和牛津大學一起設(shè)立了一個專門鼓勵女學生研究數(shù)學的獎學金。

而對于比賽本身，有網(wǎng)友也開始了一波猜測：哪個AI模型最有希望？

帶Wolfram插件的GPT-4第一個被拎出來，不過它也最先被潑了冷水。

但，它背后的OpenAI還是被人看好（盡管大型科技公司并不是該比賽的目標受眾）。

有悲觀的網(wǎng)友則直接斷言：

比賽是挺酷的，但五年內(nèi)應(yīng)該沒有誰能做到。

與此同時，有人也認為：

訓練出這樣一個模型并不算難，難的是獲取和處理數(shù)據(jù)，畢竟這些題目不單單涉及文本，還包括很多復雜含義的圖像和符號。

一切皆等2024年揭曉。

值得一提的是，AI-MO并非第一場AI挑戰(zhàn)IMO的比賽。

2019年，OpenAI、微軟、斯坦福大學和谷歌等高校機構(gòu)的幾位研究人員，就已經(jīng)發(fā)起過一場名為IMO Grand Challenge的比賽了。

此前挑戰(zhàn)尚未有人成功

IMO Grand Challenge，同樣是為了找到能拿下IMO金牌的AI而設(shè)立的比賽。

來看看這場數(shù)學比賽為AI設(shè)立的5點規(guī)則：

關(guān)于格式。為了確保證明過程的嚴謹性和可驗證性，問題和證明都需要通過形式化（formal，機器可驗證）的方式來完成。

也就是說，IMO問題會通過Lean定理證明器，將問題轉(zhuǎn)變成基于Lean編程語言的表達輸入給AI，AI同樣需要用Lean編程語言寫出證明。

關(guān)于得分。AI的每個證明題都會在10分鐘內(nèi)被判斷對錯，因為這也是IMO裁判評分的時間。與人類不同，AI沒有“部分得分”這一說法。

關(guān)于資源。和人類一樣，AI每天需要用4.5小時解決3道題（共比賽兩天），計算資源沒有限制。

關(guān)于可復現(xiàn)性。AI必須開源，并在IMO第一天結(jié)束前公開模型、而且可復現(xiàn)。要求AI不能聯(lián)網(wǎng)。

關(guān)于挑戰(zhàn)本身。最大的挑戰(zhàn)是讓AI像人類一樣獲得金牌。

這場比賽由7位AI研究學者和數(shù)學家發(fā)起：

OpenAI的Daniel Selsam、微軟的Leonardo de Moura、帝國理工學院的Kevin Buzzard、匹茲堡大學的Reid Barton、斯坦福大學的Percy Liang、谷歌AI的Sarah Loos和拉德堡德大學的Freek Wiedijk。

如今4年過去，陸陸續(xù)續(xù)也收到了一些參賽者的關(guān)注。

不過，雖然不少AI和數(shù)學研究者都試圖挑戰(zhàn)過這一領(lǐng)域、或是領(lǐng)域中的一個小目標，但距離最終的奪得IMO冠軍目標都還有很遠。

甚至有建議認為這場比賽要不要設(shè)立一個“簡單模式”：

例如，研究者Xi Wang嘗試過使用幾種現(xiàn)有的SMT求解器來做IMO真題，但效果一般。

當時現(xiàn)有的AI雖然能證明一些不太困難的IMO真題，如證明拿破侖定理（以任意三角形各邊為邊分別向外側(cè)作正三角形，則它們的中心連線必構(gòu)成一個正三角形）。

但在證明其他的一些真題如IMO 2019的幾何題時，現(xiàn)有的幾個求解器就做不出來、或是超時了半小時。

又像是OpenAI研究員（當時還在微軟）Dan Selsam和Jesse Michael Han，也曾經(jīng)針對AI解IMO幾何題研究了一段時間，并總結(jié)了一篇博客。

這篇博客介紹了他們?nèi)绾螕v鼓出一個幾何求解器，以及設(shè)計幾何求解器的步驟，具體包括：

幾何表示、約束求解、算法選擇、求解器架構(gòu)、挑戰(zhàn)與解決方案。

例如其中的幾何表示，就是將幾何問題表示為計算機可以理解并處理的格式，反過來也一樣，包括用幾何求解器自動將編程語言轉(zhuǎn)換為圖表、便于人類閱讀：

此外，還介紹了如何根據(jù)不同的IMO幾何題型選擇合適的求解算法，等等。

但即便如此，這篇博客并沒有給出具體的求解方案，只在結(jié)論處說明“求解器有可能實現(xiàn)贏得IMO金牌的目標”。

而且，上述挑戰(zhàn)者針對的幾何題，也只占據(jù)IMO題型的四分之一（還有代數(shù)、組合和數(shù)論）……

雖然發(fā)起4年，仍然沒有一個真正的AI“IMO全能選手”出現(xiàn)，不過作為這個點子的鼻祖，IMO Grand Challenge仍然在業(yè)界掀起了不少波瀾。

Alex Gerko坦言，IMO Grand Challenge也正是他舉辦AI-MO的契機：

是時候給“AI挑戰(zhàn)IMO”整點刺激的了！

當然，這次AI-MO的獎金也確實引起了IMO Grand Challenge舉辦方和不少挑戰(zhàn)者的注意：

不知道在金錢的驅(qū)動下，業(yè)界是否真會出現(xiàn)一個能解困難數(shù)學題的AI，并成功超越一眾人類奪得IMO金牌。

從目前實力來看，你認為哪家的AI最有可能率先拔得頭籌？

參考鏈接：
[1]https://twitter.com/AlexanderGerko/status/1729113193706832265
[2]https://imo-grand-challenge.github.io/
[3]https://aimoprize.com/