豐色 蕭簫 發自 凹非寺

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

獎金足足1000萬美元那種！

該比賽號稱要「代表新的圖靈測試」，怎麼比？

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

可別小看這一賽事，就連數學大牛陶哲軒都來了，並在官網傾力推薦：

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

訊息一出，網友們是相當興奮。

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

所謂「重賞之下，必有勇夫」，有著自己路數的AI也著實令人期待。

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

這項比賽的簡稱AI-MO。

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

為什麼選IMO為基準？

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

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

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

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

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

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

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

剩餘「實現了關鍵里程碑」的AI模型們則瓜分剩下的進步獎，總金額也是500萬美元。

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

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

不過需要注意的是，AI-MO並非IMO官方發起的比賽。

其真正的發起機構是XTX Markets，一家位於英國倫敦、搞機器學習量化交易的非銀行金融機構。

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

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

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

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

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

有悲觀的網友則直接斷言：

比賽是挺酷的，但五年內應該沒有誰能做到。

與此同時，有人也認為：

訓練出這樣一個模型並不算難，難的是獲取和處理資料，畢竟這些題目不單單涉及文字，還包括很多複雜含義的圖像和符號。

一切皆等2024年揭曉。

值得一提的是，AI-MO並非第一場AI挑戰IMO的比賽。

2019年，OpenAI、微軟、史丹佛大學和Google等高校機構的幾位研究人員，就已經發起過一場名為IMO Grand Challenge的比賽了。

此前挑戰尚未有人成功

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

來看看這場數學比賽為AI設立的5點規則：

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

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

關於得分。AI的每個證明題都會在10分鐘內被判斷對錯，因為這也是IMO裁判評分的時間。與人類不同，AI沒有「部分得分」這一說法。

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

關於可復現性。AI必須開源，並在IMO第一天結束前公開模型、而且可復現。要求AI不能聯網。

關於挑戰本身。最大的挑戰是讓AI像人類一樣獲得金牌🏅。

這場比賽由7位AI研究學者和數學家發起：

OpenAI的Daniel Selsam、微軟的Leonardo de Moura、帝國理工學院的Kevin Buzzard、匹茲堡大學的Reid Barton、史丹佛大學的Percy Liang、GoogleAI的Sarah Loos和拉德堡德大學的Freek Wiedijk。

如今4年過去，陸陸續續也收到了一些參賽者的關注。

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

甚至有建議認為這場比賽要不要設立一個「簡單模式」：

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

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

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

又像是OpenAI研究員（當時還在微軟）Dan Selsam和Jesse Michael Han，也曾經針對AI解IMO幾何題研究了一段時間，並總結了一篇部落格。

這篇部落格介紹了他們如何搗鼓出一個幾何求解器，以及設計幾何求解器的步驟，具體包括：

幾何表示、約束求解、演算法選擇、求解器架構、挑戰與解決方案。

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

此外，還介紹瞭如何根據不同的IMO幾何題型選擇合適的求解演算法，等等。

但即便如此，這篇部落格並沒有給出具體的求解方案，只在結論處說明「求解器有可能實現贏得IMO金牌的目標」。

而且，上述挑戰者針對的幾何題，也只佔據IMO題型的四分之一（還有代數、組合和數論）……

雖然發起4年，仍然沒有一個真正的AI「IMO全能選手」出現，不過作為這個點子的鼻祖，IMO Grand Challenge仍然在業界掀起了不少波瀾。

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

是時候給「AI挑戰IMO」整點刺激的了！

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

不知道在金錢💰的驅動下，業界是否真會出現一個能解困難數學題的AI，併成功超越一眾人類奪得IMO金牌。

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

參考連結：

[1]https://twitter.com/AlexanderGerko/status/1729113193706832265

[2]https://imo-grand-challenge.github.io/

[3]https://aimoprize.com/