丰色 萧箫 发自 凹非寺 量子位 | 公众号 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像人类一样获得金牌
