專門為 AI 設(shè)立的 IMO 國際奧林匹克數(shù)學(xué)競賽來了 ——
獎金足足 1000 萬美元那種！
該比賽號稱要“代表新的圖靈測試”，怎么比？
和人類最聰明的數(shù)學(xué)小天才們正面 PK，拿到同樣標(biāo)準(zhǔn)的金牌。
可別小看這一賽事，就連數(shù)學(xué)大牛陶哲軒都來了，并在官網(wǎng)傾力推薦：
這個比賽提供了一套鑒別 AI 解決問題策略的基準(zhǔn)，而這正是我們現(xiàn)在需要的。
消息一出，網(wǎng)友們是相當(dāng)興奮。
如 IMO 主席所說：到底哪個大模型能和世界上最聰明的一波年輕人相媲美？
所謂“重賞之下，必有勇夫”，有著自己路數(shù)的 AI 也著實(shí)令人期待。
AI 參賽 IMO，最高拿 500 萬美元
這項(xiàng)比賽的簡稱 AI-MO。
它的初衷就是推動大語言模型的數(shù)學(xué)推理能力，鼓勵開發(fā)能夠匹配人類數(shù)學(xué)最高水平（IMO 競賽）的新 AI 模型。
為什么選 IMO 為基準(zhǔn)？
IMO 的題目一般分為代數(shù)、幾何、數(shù)論和組合數(shù)學(xué)四大類，不需要高等數(shù)學(xué)知識，但需要參賽者有正確的思維方式和數(shù)學(xué)素養(yǎng)。
統(tǒng)計(jì)顯示，其金牌獲得者奪得菲爾茲獎的可能性是普通劍橋博士畢業(yè)生的 50 倍。
此外，有一半的菲爾茲獎獲得者曾參加過 IMO 競賽。
基于該比賽，這項(xiàng)專門為 AI 舉辦的 AI-MO 大賽將于 2024 年初開放。
組委會要求，參加的 AI 模型必須和人類選手采用相同的格式處理題目，并且必須生成人類可讀的最終答案，然后由專家小組使用 IMO 標(biāo)準(zhǔn)對其進(jìn)行評分。
比賽結(jié)果將隨明年 7 月在英國巴斯舉行的第 65 屆 IMO 大會一同揭曉。
最終，達(dá)到金牌水平的 AI 將獲得 500 萬美元的大獎。
剩余“實(shí)現(xiàn)了關(guān)鍵里程碑”的 AI 模型們則瓜分剩下的進(jìn)步獎，總金額也是 500 萬美元。
值得一提的是，為了拿到獲獎資格，參賽者必須遵守 AI-MO 公共共享協(xié)議，也就是獲獎模型必須得開源。
至于具體的規(guī)則，組委會還在商議中，以及目前官方還在招募顧問委員會成員（特別需要數(shù)學(xué)家、AI 和機(jī)器學(xué)習(xí)專家）和領(lǐng)導(dǎo)這項(xiàng)比賽的總監(jiān)，都是付費(fèi)的且可以完全遠(yuǎn)程，不知道哪些大佬會加入。
不過需要注意的是，AI-MO 并非 IMO 官方發(fā)起的比賽。
其真正的發(fā)起機(jī)構(gòu)是 XTX Markets，一家位于英國倫敦、搞機(jī)器學(xué)習(xí)量化交易的非銀行金融機(jī)構(gòu)。
別的不說，XTX Markets 主打一個豪氣。
它還在去年和牛津大學(xué)一起設(shè)立了一個專門鼓勵女學(xué)生研究數(shù)學(xué)的獎學(xué)金。
而對于比賽本身，有網(wǎng)友也開始了一波猜測：哪個 AI 模型最有希望？
帶 Wolfram 插件的 GPT-4 第一個被拎出來，不過它也最先被潑了冷水。
但，它背后的 OpenAI 還是被人看好（盡管大型科技公司并不是該比賽的目標(biāo)受眾）。
有悲觀的網(wǎng)友則直接斷言：
比賽是挺酷的，但五年內(nèi)應(yīng)該沒有誰能做到。
與此同時，有人也認(rèn)為：
訓(xùn)練出這樣一個模型并不算難，難的是獲取和處理數(shù)據(jù)，畢竟這些題目不單單涉及文本，還包括很多復(fù)雜含義的圖像和符號。
一切皆等 2024 年揭曉。
值得一提的是，AI-MO 并非第一場 AI 挑戰(zhàn) IMO 的比賽。
2019 年，OpenAI、微軟、斯坦福大學(xué)和谷歌等高校機(jī)構(gòu)的幾位研究人員，就已經(jīng)發(fā)起過一場名為 IMO Grand Challenge 的比賽了。
此前挑戰(zhàn)尚未有人成功
IMO Grand Challenge，同樣是為了找到能拿下 IMO 金牌的 AI 而設(shè)立的比賽。
來看看這場數(shù)學(xué)比賽為 AI 設(shè)立的 5 點(diǎn)規(guī)則：
關(guān)于格式。為了確保證明過程的嚴(yán)謹(jǐn)性和可驗(yàn)證性，問題和證明都需要通過形式化（formal，機(jī)器可驗(yàn)證）的方式來完成。
也就是說，IMO 問題會通過 Lean 定理證明器，將問題轉(zhuǎn)變成基于 Lean 編程語言的表達(dá)輸入給 AI，AI 同樣需要用 Lean 編程語言寫出證明。
關(guān)于得分。AI 的每個證明題都會在 10 分鐘內(nèi)被判斷對錯，因?yàn)檫@也是 IMO 裁判評分的時間。與人類不同，AI 沒有“部分得分”這一說法。
關(guān)于資源。和人類一樣，AI 每天需要用 4.5 小時解決 3 道題（共比賽兩天），計(jì)算資源沒有限制。
關(guān)于可復(fù)現(xiàn)性。AI 必須開源，并在 IMO 第一天結(jié)束前公開模型、而且可復(fù)現(xiàn)。要求 AI 不能聯(lián)網(wǎng)。
關(guān)于挑戰(zhàn)本身。最大的挑戰(zhàn)是讓 AI 像人類一樣獲得金牌??。
這場比賽由 7 位 AI 研究學(xué)者和數(shù)學(xué)家發(fā)起：
OpenAI 的 Daniel Selsam、微軟的 Leonardo de Moura、帝國理工學(xué)院的 Kevin Buzzard、匹茲堡大學(xué)的 Reid Barton、斯坦福大學(xué)的 Percy Liang、谷歌 AI 的 Sarah Loos 和拉德堡德大學(xué)的 Freek Wiedijk。
如今 4 年過去，陸陸續(xù)續(xù)也收到了一些參賽者的關(guān)注。
不過，雖然不少 AI 和數(shù)學(xué)研究者都試圖挑戰(zhàn)過這一領(lǐng)域、或是領(lǐng)域中的一個小目標(biāo)，但距離最終的奪得 IMO 冠軍目標(biāo)都還有很遠(yuǎn)。
甚至有建議認(rèn)為這場比賽要不要設(shè)立一個“簡單模式”：
例如，研究者 Xi Wang 嘗試過使用幾種現(xiàn)有的 SMT 求解器來做 IMO 真題，但效果一般。
當(dāng)時現(xiàn)有的 AI 雖然能證明一些不太困難的 IMO 真題，如證明拿破侖定理（以任意三角形各邊為邊分別向外側(cè)作正三角形，則它們的中心連線必構(gòu)成一個正三角形）。
但在證明其他的一些真題如 IMO 2019 的幾何題時，現(xiàn)有的幾個求解器就做不出來、或是超時了半小時。
又像是 OpenAI 研究員（當(dāng)時還在微軟）Dan Selsam 和 Jesse Michael Han，也曾經(jīng)針對 AI 解 IMO 幾何題研究了一段時間，并總結(jié)了一篇博客。
這篇博客介紹了他們?nèi)绾螕v鼓出一個幾何求解器，以及設(shè)計(jì)幾何求解器的步驟，具體包括：
幾何表示、約束求解、算法選擇、求解器架構(gòu)、挑戰(zhàn)與解決方案。
例如其中的幾何表示，就是將幾何問題表示為計(jì)算機(jī)可以理解并處理的格式，反過來也一樣，包括用幾何求解器自動將編程語言轉(zhuǎn)換為圖表、便于人類閱讀：
此外，還介紹了如何根據(jù)不同的 IMO 幾何題型選擇合適的求解算法，等等。
但即便如此，這篇博客并沒有給出具體的求解方案，只在結(jié)論處說明“求解器有可能實(shí)現(xiàn)贏得 IMO 金牌的目標(biāo)”。
而且，上述挑戰(zhàn)者針對的幾何題，也只占據(jù) IMO 題型的四分之一（還有代數(shù)、組合和數(shù)論）……
雖然發(fā)起 4 年，仍然沒有一個真正的 AI“IMO 全能選手”出現(xiàn)，不過作為這個點(diǎn)子的鼻祖，IMO Grand Challenge 仍然在業(yè)界掀起了不少波瀾。
Alex Gerko 坦言，IMO Grand Challenge 也正是他舉辦 AI-MO 的契機(jī)：
是時候給“AI 挑戰(zhàn) IMO”整點(diǎn)刺激的了！
當(dāng)然，這次 AI-MO 的獎金也確實(shí)引起了 IMO Grand Challenge 舉辦方和不少挑戰(zhàn)者的注意：
不知道在金錢??的驅(qū)動下，業(yè)界是否真會出現(xiàn)一個能解困難數(shù)學(xué)題的 AI，并成功超越一眾人類奪得 IMO 金牌。
從目前實(shí)力來看，你認(rèn)為哪家的 AI 最有可能率先拔得頭籌？
參考鏈接：
[1]https://twitter.com/AlexanderGerko/status/1729113193706832265
[2]https://imo-grand-challenge.github.io/
[3]https://aimoprize.com/
本文來自微信公眾號：量子位 （ID：QbitAI），作者：豐色 蕭簫
廣告聲明：文內(nèi)含有的對外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時間，結(jié)果僅供參考，IT之家所有文章均包含本聲明。