专门为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/

文章来自于微信公众号“量子位”（ID: QbitAI)，作者 “丰色、萧萧”