專門爲 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/
