OpenAI o3发布后，多个高难度基准测试的SOTA被大幅刷新。
就数学、代码、软件工程等领域而言，更是完全粉碎了满血版o1。
在这之中最引人瞩目的，便是在今年11月Epoch AI发布的数学基准Frontier Math上，准确率破纪录地达到了25.2%。
那么，这个结果到底意味着什么呢？
联手60多位数学家出题的陶哲轩，曾认为这项测试能够难住AI好多年
最近，帝国理工学院教授、数学家、IMO金牌得主Kevin Buzzard发表了一篇深度长文——AI现在能做数学了吗？
文中，他探讨了AI在数学研究中的潜力，特别是在处理复杂计算和验证方面。不过，Buzzard认为在原创性证明、深刻理解数学概念方面，依旧存在一些局限。
o3未来在数学方面的研究潜力究竟如何，或许我们能够从这篇文章中获得关键的一瞥。
o3是什么？FrontierMath又是什么？
可能大多数人都认为，语言模型就是ChatGPT之类的东西：你可以向它提出问题，它会写一些句子给你答案。
语言模型在ChatGPT之前就有了，但总的来说，它们甚至无法写出连贯的句子或段落。
之后还有很多其他模型。现在，它们仍在快速进步。
没有人知道这种情况还会持续多久，但有很多人在这个游戏中投入了大量资金，因此，如果打赌进展会很快放缓，那就太傻了。
Epoch AI在11月宣布， 其精心挑选了「数百」个数学难题， 组成了保密的FrontierMath数据集。
论文链接：
之所以要进行「保密」，是有原因的。
大语言模型的训练要依赖于大型的知识数据库，因此一旦你将数据集公开，这些语言模型就会在上面进行训练。
如果你向这样的模型提出来自数据集中的问题，它们可能会直接复述出已经看到的答案。
这个数据集有多难？
那么，FrontierMath数据集中的问题是什么样的呢？
我们知道的是，这些问题不是「证明这个定理」问题，而是「找到这个数字」问题。更准确地说，「问题必须具有清晰且可计算的答案，并且能够被自动验证。」
对于数据集中公开的5个示例问题，通过随机猜测的方式几乎上不可能成功。而且对于专业数学家来说也不简单。
Buzzard称，自己可以理解这5个问题的题意，并能较为轻松地完成第三道题——他以前见过这个技巧。
简单来说就是，函数将自然数n映射到α^n，当且仅当α-1的p进值为正时，该函数在n上是p进连续的。
而且，他也完全知道如何解决第五个问题——这是一个涉及曲线Weil猜想的标准技巧，但没有去算出确切的13位数答案。
对于第一个和第二个问题，Buzzard承认自己并不会做；至于第四个问题，如果花很多力气去研究的话可能会有进展，不过他最终没有尝试，只是看了看答案。
Buzzard怀疑道，即便是非常聪明的数学本科生，可能连其中的一个问题都无法完成。
比如第一个问题，就需要是解析数论领域的博士生才有可能。
FrontierMath论文中引用了一些数学家对这些问题难度的评价。就连菲尔兹奖得主陶哲轩表示：「这些问题极具挑战性，只有领域专家才能解决」。
确实，Buzzard称自己能解决的两个示例问题都在专业领域，比如算术；而对那些不在专业范围内的问题，一个都没解决。
不过，同是菲尔兹奖得主的Borcherds也在论文中提到，机器所生成数值答案「并不完全等同于提出了原创性的证明」。
那么，为什么要制作这样一个数据集呢？
问题在于，对「数百」个「证明这个定理」问题的答案进行评分成本非常高。至少在2024年，人们还不会信任机器在这种复杂程度下进行评分，因此必须花钱聘请人类专家来完成。
相比之下，检查一个列表中的数百个数字是否与另一个列表中的相对应，计算机可以在一秒钟内完成。
正如Borcherds所指出的，数学研究人员的大部分时间都是在尝试提出证明或构思想法，而不是处理数字。
不过，由于在数学领域，AI迫切需要高难度的数据集，而创建这样一个数据集是非常困难的，或者说是非常昂贵的。因此，FrontierMath数据集仍然非常有价值。
在最近的一篇论文中，Frieder等人深入讨论了数学领域AI数据集的不足之处。
论文链接：
此外，Science上也有一篇关于FrontierMath数据集的文章，其中引用了Buzzard的话：「如果有一个系统能够在这个数据集上取得满分，那数学家的时代就结束了。」
没想到，就在论文发出的一个多月之后，OpenAI突然宣布o3在这个数据集上取得了破纪录的25.2%准确率。
整个AI数学圈，都为之震惊，包括Buzzard本人也是。
发生了什么？
在数学领域，Buzzard对「AI」能力的认知是「本科生或预科生」的水平。
o3在解决为优秀高中生设计的「奥林匹克式」问题方面，表现得非常出色。
毫无悬念的是，AI系统在一年之内就能通过本科数学考试。
因为，在设计本科数学考试时，通常需要确保不至于有50%的学生都不及格，因此会加入一些标准化问题（和学生们已经见过的非常相似），从而帮助那些对课程有基本理解的学生能通过考试。在这些问题上，机器很容易取得高分。
但要从这一水平跨越到高级本科或早期博士阶段，并提出创新性想法，而不仅仅是重复利用标准化的思路，将需要一个相当大的飞跃。
毕竟在普特南竞赛（美加知名大学生数学竞赛）中， o1 pro仅对「B4」这道题给出了还算不错的解答，其他大多数答案最多只能得一两分（满分10分）。
上下滑动查看
因此，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拒绝接受数学文献中的某个人类论证时，错误的总是人类。
事实上，数学家希望看到的不仅仅是「证明这个定理！」，而是希望看到「正确地证明这个定理，并以人类能够理解的方式解释其成立原因」。
对于语言模型方法，我非常担心「正确性」；而对于定理证明器的方法，我则担心「是否能够以人类能够理解的方式呈现」。
目前进展非常迅速，但我们在这一领域仍然有大量工作要做。
至于何时才能「跨越本科生水平这道坎」？没有人知道。
还没有评论，来说两句吧...