o3拿下25%高分震惊数学教授，2025 IMO金牌或被AI收入囊中！

新智元报道

编辑：编辑部 JHY

【新智元导读】AI真的可以做数学了吗？来自帝国理工学院教授Kevin Buzzard在最新博文中深刻探讨了这个问题。甚至，他预测道，2025年AI能够拿下IMO金牌级水平。

OpenAI o3发布后，多个高难度基准测试的SOTA被大幅刷新。

就数学、代码、软件工程等领域而言，更是完全粉碎了满血版o1。

在这之中最引人瞩目的，便是在今年11月Epoch AI发布的数学基准Frontier Math上，准确率破纪录地达到了25.2%。

那么，这个结果到底意味着什么呢？

联手60多位数学家出题的陶哲轩，曾认为这项测试能够难住AI好多年

最近，帝国理工学院教授、数学家、IMO金牌得主Kevin Buzzard发表了一篇深度长文——AI现在能做数学了吗？

文中，他探讨了AI在数学研究中的潜力，特别是在处理复杂计算和验证方面。不过，Buzzard认为在原创性证明、深刻理解数学概念方面，依旧存在一些局限。

o3未来在数学方面的研究潜力究竟如何，或许我们能够从这篇文章中获得关键的一瞥。

o3是什么？FrontierMath又是什么？

可能大多数人都认为，语言模型就是ChatGPT之类的东西：你可以向它提出问题，它会写一些句子给你答案。

语言模型在ChatGPT之前就有了，但总的来说，它们甚至无法写出连贯的句子或段落。

之后还有很多其他模型。现在，它们仍在快速进步。

没有人知道这种情况还会持续多久，但有很多人在这个游戏中投入了大量资金，因此，如果打赌进展会很快放缓，那就太傻了。

论文链接：https://arxiv.org/abs/2411.04872

之所以要进行「保密」，是有原因的。

大语言模型的训练要依赖于大型的知识数据库，因此一旦你将数据集公开，这些语言模型就会在上面进行训练。

如果你向这样的模型提出来自数据集中的问题，它们可能会直接复述出已经看到的答案。

这个数据集有多难？

那么，FrontierMath数据集中的问题是什么样的呢？

我们知道的是，这些问题不是「证明这个定理」问题，而是「找到这个数字」问题。更准确地说，「问题必须具有清晰且可计算的答案，并且能够被自动验证。」

对于数据集中公开的5个示例问题，通过随机猜测的方式几乎上不可能成功。而且对于专业数学家来说也不简单。

Buzzard称，自己可以理解这5个问题的题意，并能较为轻松地完成第三道题——他以前见过这个技巧。

简单来说就是，函数将自然数n映射到α^n，当且仅当α-1的p进值为正时，该函数在n上是p进连续的。

而且，他也完全知道如何解决第五个问题——这是一个涉及曲线Weil猜想的标准技巧，但没有去算出确切的13位数答案。

对于第一个和第二个问题，Buzzard承认自己并不会做；至于第四个问题，如果花很多力气去研究的话可能会有进展，不过他最终没有尝试，只是看了看答案。

Buzzard怀疑道，即便是非常聪明的数学本科生，可能连其中的一个问题都无法完成。

比如第一个问题，就需要是解析数论领域的博士生才有可能。

FrontierMath论文中引用了一些数学家对这些问题难度的评价。就连菲尔兹奖得主陶哲轩表示：「这些问题极具挑战性，只有领域专家才能解决」。

确实，Buzzard称自己能解决的两个示例问题都在专业领域，比如算术；而对那些不在专业范围内的问题，一个都没解决。

不过，同是菲尔兹奖得主的Borcherds也在论文中提到，机器所生成数值答案「并不完全等同于提出了原创性的证明」。

那么，为什么要制作这样一个数据集呢？

问题在于，对「数百」个「证明这个定理」问题的答案进行评分成本非常高。至少在2024年，人们还不会信任机器在这种复杂程度下进行评分，因此必须花钱聘请人类专家来完成。

相比之下，检查一个列表中的数百个数字是否与另一个列表中的相对应，计算机可以在一秒钟内完成。

正如Borcherds所指出的，数学研究人员的大部分时间都是在尝试提出证明或构思想法，而不是处理数字。

不过，由于在数学领域，AI迫切需要高难度的数据集，而创建这样一个数据集是非常困难的，或者说是非常昂贵的。因此，FrontierMath数据集仍然非常有价值。

在最近的一篇论文中，Frieder等人深入讨论了数学领域AI数据集的不足之处。

论文链接：https://arxiv.org/pdf/2412.15184

此外，Science上也有一篇关于FrontierMath数据集的文章，其中引用了Buzzard的话：「如果有一个系统能够在这个数据集上取得满分，那数学家的时代就结束了。」

没想到，就在论文发出的一个多月之后，OpenAI突然宣布o3在这个数据集上取得了破纪录的25.2%准确率。

整个AI数学圈，都为之震惊，包括Buzzard本人也是。

发生了什么？

在数学领域，Buzzard对「AI」能力的认知是「本科生或预科生」的水平。

o3在解决为优秀高中生设计的「奥林匹克式」问题方面，表现得非常出色。

毫无悬念的是，AI系统在一年之内就能通过本科数学考试。

因为，在设计本科数学考试时，通常需要确保不至于有50%的学生都不及格，因此会加入一些标准化问题（和学生们已经见过的非常相似），从而帮助那些对课程有基本理解的学生能通过考试。在这些问题上，机器很容易取得高分。

但要从这一水平跨越到高级本科或早期博士阶段，并提出创新性想法，而不仅仅是重复利用标准化的思路，将需要一个相当大的飞跃。

因此，Buzzard原本预计这个数据集在接下来的几年内仍然是难以攻破的。

但还是激动早了。

Epoch AI的Elliot Glazer在Reddit发帖声称数据集中实际上有25%的问题是「IMO/本科生风格的问题」。

这个说法有点令人困惑，因为很难将这样的形容词，对应到公开发布的5个问题中的任何一个。

即使是最简单的一个，也涉及到了Weil曲线猜想（或是通过暴力计算论证——勉强可行但会非常痛苦，因为它需要在有限域上分解10^12个三多次项式）。

那么问题来了，这个数据集中问题的实际水平到底是什么？或者换句话说，这五个公开问题是否真的具有代表性？我们无从得知。

考虑到这一新的信息，即25%的问题是本科水平，Buzzard称自己对o3取得的成绩也就不那么惊讶了。

不过，他表示，还是很期待AI能够在数据集上达到50%的准确率。因为在「博士资格考试」上的表现（也就是Elliot Glazer所描述的接下来50%的问题），正是Buzzard希望从这些系统中看到的。

证明这个定理！

然而，正如Borcherds指出的那样，即使我们最终得到了一台在「找到这个数字」方面超越人类的机器， 它在许多数学研究领域的适用性也将十分有限，因为这些领域的核心问题通常是如何「证明这个定理」。

在Buzzard看来，2024年最成功的案例是DeepMind的AlphaProof——它解决了2024年国际数学奥林匹克（IMO）六道题中的四道。

在这些问题中，既有「证明这个定理」, 也有「找到一个数字并证明它的正确性」。对于其中的三道题，机器的输出是完全形式化的Lean证明。

交互式定理证明器Lean拥有一个完善的数学库mathlib，其中就包含有能够解决IMO以及其他问题所需的众多技术。

最终，DeepMind系统的解答经过人工检查后被验证为「满分」答案。

不过，这相当于让我们又回到了高中——尽管题目极难，但解题只需使用高中水平的技术。

Buzzard认为，我们将会在2025年看到IMO金牌水平的机器。

但同时，这也迫使我们不得不重新面对之前提到的「评分难题」。

谁给机器打分？

可以设想，在2025年7月的国际数学奥林匹克大赛（IMO）上，除了数百名世界上最聪明的中学生之外，还会有机器参赛。但希望数量不会太多。

这些系统将分为两种类型：

• 以计算机证明检查器（如Lean、Rocq、Isabelle等）的语言提交答案的系统

• 以人类的语言提交答案的大语言模型

这两种提交方式之间最大的区别在于：

• 对于已被正确翻译为计算机证明检查器语言的题目陈述，评审只需检查证明能否通过编译，基本上就可以确定这是不是一个「满分」答案了。

• 对于大语言模型，评审将面临类似普特南竞赛解答的情况——计算机会写出一些看起来很有说服力的内容，但人类需要仔细阅读并评分，而且并不能保证这会是一个「满分」答案。

Borcherds提醒AI社区「证明这个定理！」是数学家真正希望看到的，这是非常正确的。

目前在逻辑推理方面，大语言模型的准确度至少比人类专家低一个数量级。

我担心，在一两年之内会不可避免地出现语言模型「证明」黎曼猜想的浪潮。这些模糊或不准确的「证明」可能会夹杂10页正确的数学内容中，而人类不得不耗费大量的精力才能把它们找出来。

另一方面，定理证明器的准确性至少高一个数量级：每当看到Lean拒绝接受数学文献中的某个人类论证时，错误的总是人类。

事实上，数学家希望看到的不仅仅是「证明这个定理！」，而是希望看到「正确地证明这个定理，并以人类能够理解的方式解释其成立原因」。

对于语言模型方法，我非常担心「正确性」；而对于定理证明器的方法，我则担心「是否能够以人类能够理解的方式呈现」。

目前进展非常迅速，但我们在这一领域仍然有大量工作要做。

至于何时才能「跨越本科生水平这道坎」？没有人知道。

参考资料：

https://xenaproject.wordpress.com/2024/12/22/can-ai-do-maths-yet-thoughts-from-a-mathematician/