【CSDN 编者按】近日，OpenAI 发布的新语言模型 o3 在 FrontierMath 测试中正确率达到了 25%，这一事件引发了广泛讨论。而作为一位数学家，本文作者对这个问题也有着一些深刻思考。
原文链接：https://xenaproject.wordpress.com/2024/12/22/can-ai-do-maths-yet-thoughts-from-a-mathematician/
作者 | xenaproject 翻译 | 郑丽媛
出品 | CSDN（ID：CSDNnews）
上周有个大新闻：OpenAI 的新语言模型 o3 在 FrontierMath 测试中正确率达到了 25%。那么首先，让我们解释一下这意味着什么。
o3 是什么？FrontierMath 又是什么？
语言模型，例如像 ChatGPT 这样的技术，可能大多数人都已经熟悉了。你可以向它提问，而它会生成一些试图回答你问题的句子。在 ChatGPT 之前，也有过其他语言模型，但那些模型大多连通顺的句子和段落都写不好。ChatGPT 是第一个公开发布的、能够生成连贯内容的模型。自那以后，类似的模型层出不穷，而且进步速度非常快。没人知道这种快速发展还能持续多久，但许多人正为此投入巨资，因此若有人认为进展会很快放缓，恐怕是个不明智的判断。而 o3 就是其中一个最近推出的语言模型。
至于 FrontierMath，它是由 Epoch AI 上个月发布的一个秘密数据集，里面包含“数百道”高难度数学问题。关于“数百道”这个说法，引用自相关论文摘要的第一句话，但我听说当这篇论文发布时，里面的问题其实还不到 200 个；不过，也有传言称后来又增加了一些题目。作为一名一生致力于与他人公开合作研究问题的学术数学家，我对此感到有些沮丧，因为在介绍这个数据集的过程中，疑问比答案还多——例如，连这个数据集的具体规模我都无法为你提供一个清晰的描述。
不过，保持神秘是有其原因的。语言模型依赖于大型知识库进行训练，所以一旦数学问题的数据集被公开，语言模型便会将其纳入训练内容。这样一来，如果你问这个模型数据库中的某个问题，它们很可能会直接复述之前见过的答案。
FrontierMath 数据集有多难？
FrontierMath 数据集中的问题到底是什么样的？据我们了解，这些问题并不是“证明这个定理！”类型的问题，而是“找出这个数字！”类型的问题。更确切地说，论文中提到：“问题必须有明确的、可计算的答案，且答案可以被自动验证。” 在从数据集中公开的五个样本问题（论文附录 A，第 14 至 23 页）中，所有解答都是正整数（其中一个答案是 9811，另一个是 367707，另外三个答案更大——显然，这些问题的设计排除了随机猜测成功的可能性）。
这些样例问题对研究级数学家来说都不简单。我能理解这五个问题的描述，其中第三个我能比较快地解决（因为我之前见过类似的解题技巧，即一个函数将自然数n映射到αn，当且仅当α−1的p-进值为正时，这个函数在p-进数系中对n连续），第五个问题我也知道怎么做（这涉及曲线的 Weil 猜想中的一个标准技巧），但我没有去计算那个 13 位的具体答案。对于第一个和第二个问题，我知道自己做不出来，而第四个问题，我觉得如果花一些努力可能会有所进展，但最终我也没尝试，只是阅读了答案。我怀疑，即使是一个典型的聪明数学本科生也很难解决其中的任何一个问题。要解决第一个问题，我猜至少需要是解析数论领域的博士生才行。
FrontierMath 论文中还引用了一些数学家对问题难度的评价。陶哲轩（菲尔兹奖得主）表示“这些问题极其具有挑战性”，并指出它们只能由领域专家来解决（实际上，我能解决的两个样例问题也确实属于我的专长领域——算术学；而对于我专业之外的问题，我都未能解答）。然而，Borcherds（同样是菲尔兹奖得主）在论文中评论说，机器得出数值答案“与真正原创性地提出证明并不相同”。
那么，为什么要创建这样一个数据集呢？原因在于，对数百个“证明这个定理！”类型问题的答案进行评分成本很高（至少在 2024 年，人们还不相信机器能达到这种级别的批改精度，因此必须花钱聘请人工专家来评分），而检查一份列表中的数百个数字是否对应另一份列表中的数百个数字，计算机可以在一秒钟内完成。正如 Borcherds 所指出的，数学研究人员大部分时间都在尝试提出证明或想法，而不是计算数字。然而，FrontierMath 数据集仍然极具价值，因为 AI 在数学领域极度缺乏高难度的数据集，而创建这样一个数据集非常困难（或者说非常昂贵）。Frieder 等人在最近发表的一篇文章中也详细讨论了数学领域 AI 数据集的不足之处。
《Science》杂志上最近有一篇关于 FrontierMath 数据集的文章，我在其中被引用说过：“如果有一个系统能在这个数据库上拿满分，那么对数学家来而言就是‘游戏结束’。” 在这里澄清一下：我和这个数据集毫无关系，只是看过五个公开的问题，我的评论仅基于这些问题。此外，我还说：“在我看来，目前 AI 距离能够解决这些问题还很遥远……但我以前也犯过错。” 然而，就在最近，有消息称语言模型 o3 在该数据集上的得分达到了 25%，对此我感到十分惊讶。
到底发生了什么？
我感到震惊的原因在于，在我原本的认知中，目前 AI 在数学领域的能力相当于“本科以下”水平，它在处理类似于给高中生的奥赛题方面表现出色。预计在未来一年内，AI 系统通过本科数学考试几乎已成定局，原因很简单：本科数学考试的设计通常会包含一些基础题目，这些题目往往是课程中反复出现的练习，目的是确保具备基本知识的学生能够通过考试，而这样的题目对 AI 来说简直是小菜一碟。但是，从这种水平跳跃到具备高级本科/早期博士阶段的创新思维，在我看来是一个相当大的跨越。例如，最近 ChatGPT 对普特南数学竞赛的解答让我非常失望——就我观察，只有 B4 题被勉强解决，其他大多数题目的得分最多也就 1 到 2 分（满分为 10 分）。因此，我原本预计 FrontierMath 数据集在未来几年内仍然会是一个 AI 难以攻克的领域。
然而，我的兴奋很快就被 Epoch AI 的 Elliot Glazer 在 Reddit 上的一篇帖子所抚平。他声称，数据集中有 25% 的问题属于“IMO（国际数学奥林匹克）/本科水平”。这一说法有些令人困惑，因为我很难将这样的形容词应用到数据集公开的五个问题上，即便是最简单的问题也使用了 Weil 曲线猜想（或者用一种可能但极其痛苦的暴力求解方法——需要在有限域中因式分解 12 次 3 阶多项式，尽管这可以并行化计算降低难度）。这当然让我产生了一些疑问：这个秘密数据集的实际问题水平到底如何？公开的那五个问题是否具有代表性？这些问题我们可能无法得知。鉴于新信息表明 25% 的问题是本科水平，或许我应该不再感到惊讶了。但我仍期待着 AI 在这个数据集上达到 50% 的得分，因为 Elliot 所描述的“qual level”（下一个 50% 的问题）才是我关注的焦点。如果 AI 系统能在这些问题上取得突破，对我来说才算是一个重大进展。
证明这个定理！
正如 Borcherds 所指出的，即使我们最终拥有了一个能在“找到这个数字！”类型问题上超越人类的机器，它在许多研究型数学领域的应用仍然有限，因为在这些领域中的关键问题往往是“如何证明这个定理！”。在我看来，2024 年最大的成功案例是 DeepMind 的 AlphaProof，它解决了 2024 年国际数学奥林匹克竞赛（IMO）六个问题中的四个。些问题要么是“证明这个定理！”类型的问题，要么是“找到一个数并进一步证明它是正确的数”的问题。对于其中三个问题，AlphaProof 的输出还是一个完全形式化的 Lean 证明。
简单来说，Lean 是一种交互式定理证明器，包含了功能强大的数学库 Mathlib，其中收录了解决 IMO 问题所需的许多技术以及更多内容。DeepMind 系统的解答经由人工检查，确认无误，获得了满分。然而，这些问题仍然停留在高中数学的范畴；虽然题目非常困难，但解答只用到了中学阶段的数学技巧。我相信到了 2025 年，AI 能在 IMO 中达到金牌水准。不过，这也让我们不得不重新审视之前提到的“评分”问题。
谁来给 AI 打分？
想象一下 2025 年 7 月的情景：除了来自世界各地的顶尖中学生参加 IMO 外，AI 也会参赛。但希望 AI 的数量不要太多，因为参赛系统将分为两种：一种是提交计算机证明检查语言（如Lean、Rocq、Isabelle等）答案的系统；另一种是提交自然语言答案的语言模型。
这两类系统的主要区别在于：
对于使用定理证明器的系统，只要评审确认问题被正确翻译为计算机证明检查器的语言，接下来只需验证证明是否可以通过编译器运行。如果通过了，那基本可以确定这是一个“满分解答”。
对于语言模型，情况则会复杂得多。它们会输出看似令人信服的证明，但评审需要逐字逐句地仔细阅读，并手动评分。这种情况下，完全无法保证答案为“满分”。正如 Borcherds 所提醒的那样，“证明这个定理！”是数学家真正希望看到的能力，而当前语言模型在逻辑推理上的准确性至少比专家人类低一个数量级。
我非常担心，未来一两年内会出现大量语言模型生成的“黎曼猜想证明”，这些证明将在十几页正确的数学推导中夹杂着模糊或不准确的论断，而人类评审需要耗费大量精力才能找出其中的问题。相比之下，定理证明器至少在准确性上要高出一个数量级：每次我看到 Lean 不接受文献中的某个数学论证时，事实证明往往是该论证本身有问题。
事实上，作为数学家，我们希望看到的不仅是“证明这个定理！”，还希望看到“正确地证明这个定理，并用一种我们人类能够理解的方式来解释是什么让这个证明成立”。对于语言模型的方法，我非常担忧其能否做到“正确性”；而对于定理证明器的方法，我则更为担忧它是否能“以我们人类能够理解的方式”呈现。显然，在这两个方向上，我们还有很长的路要走。
目前 AI 的进展确实非常迅速，但我们距离目标还很远。我们何时能让 AI “突破本科生水平”？没人知道答案。
