小细节专门为 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），作者：丰色 萧箫
广告声明：文内含有的对外跳转链接（包括不限于超链接、二维码、口令等形式），用于传递更多信息，节省甄选时间，结果仅供参考，IT之家所有文章均包含本声明。
本文由LinkNemo爬虫[Echo]采集自[https://www.ithome.com/0/735/700.htm]
