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

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

豐色 蕭簫 發自 凹非寺

量子位 | 公眾號 QbitAI

專門為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、微軟、斯坦福大學和谷歌等高校機構的幾位研究人員，就已經發起過一場名為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、谷歌AI的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/