划重点：
OpenAI的新模型o3在FrontierMath测试中获得了25%的分数，但其实只相当于大学预科或本科水平。
英国数学家巴扎德预计，在2025年7月的国际数学奥林匹克竞赛中，AI有望达到金牌水平。
巴扎德预计AI未来几年无法攻破FrontierMath测试，分数接近50%意味着真正重大突破。
o3在解决“求解”类型的问题上表现出色，但在“证明”的问题上，仍有很长的路要走。
在人工智能的迅猛发展中，OpenAI以其不断的创新和突破而闻名。2024年12月20日，OpenAI发布了其最新的推理模型o3，这一事件标志着该公司在人工智能技术发展史上的又一重要里程碑。o3模型作为o1模型的继承者，不仅在推理和编码能力上实现了显著提升，而且在某些条件下接近通用人工智能（AGI）的能力。
o3模型以其卓越的数学能力，成为了科技界热议的焦点。o3模型在多项基准测试中的表现，不仅刷新了人们对人工智能的认知，更是在ARC-AGI评估中取得了突破性的高分，达到了87.5%的惊人成绩，超过了人类水平的85%门槛。这一成就，无疑在社交平台上引起了一片哗然，人们惊叹于人工智能技术发展的速度和潜力。
然而，数学界对此却有着不同的声音。一些数学家对于人工智能在数学领域的应用持谨慎态度，他们普遍认为，尽管o3在解决“求解”类型的问题上表现出色，但在“证明”的问题上，即那些需要深度创新和逻辑推理的问题，o3以及当前的人工智能技术仍有很长的路要走。
比如英国数学家凯文·巴扎德（Kevin Buzzard）主导的Xena Project日前发表博客文章，称o3模型在FrontierMath测试中获得了25%的分数，这很令人惊讶，但其实并不意味着完全的突破。他认为，o3在解决“求解”类型的问题上表现出色，但在“证明”的问题上，仍有很长的路要走。（注：巴扎德在数学领域有着深厚的背景，特别是在代数数论方面。近年来，他也开始在形式证明验证领域工作，致力于将数学翻译成计算机可以理解的语言，并推广计算机辅助证明在数学研究中的应用。他因其在数学领域的贡献而获得了Whitehead Prize和Senior Berwick Prize。）
多伦多大学的助理教授丹尼尔·利特（Daniel Litt）就在社交媒体X上指出：“FrontierMath试题难吗？Epoch AI 表示，最简单的问题难度相当于国际数学奥林匹克（IMO）或普特南数学竞赛（Putnam）的水平。不过，我认为这种方法虽然能够在一定程度上反映出数学题的难度，但并不尽如人意。”
巴扎德对o3模型为何未能取得数学上的技术突破给出了自己的解释：
o3是什么？FrontierMath又是什么？
语言模型，可能大多数人都知道，是一种类似于ChatGPT的工具，用户可以向它提问，它会尝试用一些句子来给出答案。在ChatGPT之前，也有过语言模型，但总的来说，它们甚至无法写出连贯的句子和段落。ChatGPT是第一款能够写出连贯文本的公共模型。此后，出现了许多其他模型。目前，它们仍在迅速改进。这种进步还会持续多久，没有人知道，但有很多人在投入大量资金，所以赌人工智能技术的发展很快会放缓的人无疑是愚蠢的。o3就是一个新的语言模型。
FrontierMath是由Epoch AI联合超过60位全球顶尖数学家共同推出的一个全新的数学基准测试平台。这个基准测试旨在评估人工智能系统在高级数学推理方面的能力。FrontierMath包含了数百个原创的、极具挑战性的数学问题，这些问题覆盖了现代数学的多个主要分支，包括计算密集型的数论和实分析问题，以及代数几何和范畴论中的抽象问题。巴扎德指出，作为一个一生都在开放合作研究问题和与他人分享想法的学术数学家，让他感到有些沮丧的是，尽管他一生都在与他人合作解决研究问题并分享自己的想法，但因为FrontierMath的数学问题是保密数据集，他甚至没有掌握该数据集的基本信息，例如它究竟包含了多少道数学题。当然，他理解这种保密的必要性。语言模型在大量知识数据库上进行训练，一旦公开一个数学问题数据库，语言模型就会在它上面训练。如果之后向这样的模型提出数据库中的一个问题，它们可能会直接复述出它们之前看到的答案。
FrontierMath测试有多难？
FrontierMath数据集中包括什么样的数学难题？以下是目前所掌握的信息。这些问题并非“证明”类型的数学题，而是“求解”的问题。更具体地说，FrontierMath数据集中的问题必须具备明确、可计算的答案，并且能够自动验证。在公开的五个样本问题中，解决方案均为正整数（例如一个答案是9811，另一个是367707，其他答案数字甚至更大--显然人工智能随机猜测成功的可能性极低。)
即使是研究数学的学者也会发现这些样本问题颇具挑战性。巴扎德本人亲自测试了FrontierMath数据集的5道样本数学例题。他能够相对快速地解决第三个问题（他之前见过这个技巧，即自然数n映射到alpha^n的函数在n上是p-adic连续的，当且仅当alpha-1的p-adic估值是正的），他确切知道如何解决第五个问题（这是一个涉及曲线Weil猜想的标准技巧），但他没有费心去做代数运算来得出确切的13位数字答案。他知道自己解决不了第一和第二个问题，他认为如果投入一些真正的努力，可能会在第四个问题上取得进展，但最终他没有尝试，只是阅读了解决方案。他怀疑一个聪明的数学本科生会很难解决这些问题中的任何一个。要解决第一个问题，他认为，至少必须是分析数论的博士生。
FrontierMath论文中包含了一些数学家对问题难度的评价。数学家陶哲轩（Fields Medal得主）表示“这些问题极具挑战性”，并认为只有领域专家才能解决（确实，他能解决的两个样本问题都在算术领域，他的专长领域；他没有解决所有超出他领域的问题）。而英国数学家理查德·博切尔兹（Richard Borcherds，也是Fields Medal得主）也指出，机器产生数字答案“与提出原创证明并不完全相同。”
那么为何要创建这样一个数据集呢？问题在于，对“数百个”“证明这个定理！”问题的答案进行评分是昂贵的（至少在2024年，人们不会信任机器在这一水平上进行评分，因此必须支付给人类专家），而检查一个列表中的数百个数字是否与另一个列表中的数百个数字相对应，计算机可以在几秒钟内完成。正如博切尔兹所指出的，数学研究人员大部分时间都在试图提出证明或想法，而不是数字，然而FrontierMath数据集仍然非常有价值，因为人工智能在数学领域的应用极度缺乏高难度的数据集，而创建这样的数据集是一项非常艰巨的工作（或者非常昂贵）。
《科学》杂志上有一篇关于FrontierMath数据集的文章。需要澄清的是，巴扎德与该数据集并无关联，他仅接触过五个公开的问题，他的评论也是基于这些问题提出的。巴扎德曾表示：“依我之见，目前人工智能还远远未能解决这些问题……不过，我过去也曾判断失误。”在宣布o3模型在FrontierMath测试中获得了25%的分数后，巴扎德感到非常震惊。
25%的分数意味着什么？
巴扎德为何感到震惊？因为他对当前“人工智能”在数学领域的能力有一个心理预期，即它目前的水平大约在“本科或本科预科”阶段。人工智能在解决奥数问题上表现得越来越好，这类问题通常是给聪明的高中生准备的。一年内，人工智能系统通过本科数学考试是绝对明确的（尤其是因为当你设置本科数学考试时，理想情况下需要确保不要有50%的学生不及格，所以你会加入一些与学生已经见过的问题非常相似的标准问题，以确保那些对课程有基本理解的学生能够通过考试。机器将能够轻松地解答这些问题）。
但是，从这个水平跳到在高级本科/早期博士水平上提出创新想法，而不仅仅是重复标准想法，在他看来是一个相当大的飞跃。例如，他对ChatGPT在最近发布的普特南考试中给出的答案印象深刻--据他所知，只有B4问题被机器充分回答，大多数其他答案最多值得10分中的1或2分。因此，他预计这个数据集在未来几年内将保持相对不可攻克的状态。
然而，他的初步兴奋被Epoch AI的发起人、数学家艾略特·格莱泽（Elliot Glazer）在Reddit上的一个帖子所抑制。格莱泽声称，实际上数据集中有25%的问题是“IMO/本科风格的问题”。这种说法有点令人困惑，因为他很难将这样的措辞应用于数据集中公开发布的五个问题中的任何一个：即使是最简单的问题也使用了曲线的Weil猜想。鉴于这个新信息，即25%的问题是本科水平，也许巴扎德变得不感到惊讶，但他会期待当人工智能在数据集上的得分接近50%时再次感到惊讶，因为“合格水平”（qual level）对他来说，将代表一个重大突破。
证明定理！
然而，正如博切尔兹所指出的，即使我们最终拥有一台在“找出这个数字！”问题上超越人类的机器，它在许多研究数学领域中的应用仍然有限。因为在这些领域中，人们通常关心的关键问题是“如何证明这个定理！”。在巴扎德看来，2024年最大的成功案例是DeepMind的AlphaProof，它解决了2024年国际数学奥林匹克竞赛（IMO）中的六个问题中的四个。这些问题要么是“证明这个定理！”要么是“找出一个数字，并且进一步证明这个数字是正确的”，对于其中的三个问题，机器输出的是完全形式化的Lean证明。Lean是一个交互式定理证明器，拥有扎实的数学库mathlib，包含了许多解决国际数学奥林匹克竞赛问题所需的技术，DeepMind系统的解决方案经过人工检查并被验证为“满分”解决方案。
但这又让我们回到了高中阶段的挑战：尽管这些问题极具挑战性，所使用的解题方法却仅限于学校教学的范畴。在2025年，巴扎德相信我们会看到人工智能在国际数学奥林匹克竞赛达到金牌水平的表现。
谁来给人工智能评分？
在2025年7月的国际数学奥林匹克竞赛中，不仅会有来自世界各地的数百名最聪明的学生参赛，还会有机器参与。希望机器的数量不会太多。因为这些系统将分为两类：一类是提交答案给计算机证明检查器（如Lean、Rocq、Isabelle等）的系统；另一类是提交人类语言答案的语言模型。
这两种提交方式的主要区别在于：如果评分者验证了问题陈述已正确翻译成计算机证明检查器的语言，那么他们所需做的就只是检查证明是否编译通过，基本上就可以确定这是一个“满分”解决方案。对于语言模型，我们将面临类似于上面提到的普特南解决方案的情况--计算机会写出一些东西，看起来令人信服，但人类需要仔细阅读并评分，而且肯定没有保证它是一个“满分”解决方案。博切尔兹正确地提醒人工智能社区，“证明这个定理！”是我们数学家真正希望看到的，而语言模型在逻辑推理方面的准确性目前至少比专家人类低一个数量级。
巴扎德担心，一两年后，语言模型对黎曼猜想的“证明”将会不可避免地涌现，其中包含的模糊或不准确的主张将夹杂在10页正确的数学内容中，人类将不得不艰难地筛选以找到站不住脚的论述。另一方面，定理证明器至少准确一个数量级：每次巴扎德看到Lean不接受数学文献中的人类论证时，错的总是人类。
实际上，作为数学家，巴扎德希望看到的不仅仅是“证明这个定理！”。他希望看到的是“以人类理解的方式正确地证明这个定理，并解释是什么让这个证明起作用。”对于语言模型方法，巴扎德非常担心“正确地”这一点；而对于定理证明器方法，他担心的是“以我们人类理解的方式”。仍然有大量的工作要做。目前进展确实非常迅速。但我们离目标还很远。人工智能何时能“突破本科障碍”？没有人知道。（腾讯科技特约编译无忌）