OpenAI 的数学解答尚未达到学界标准

当 OpenAI 本周发布数百份针对全球最困难数学问题的所谓解答时，这家前沿实验室表示，为避免其模型上一次解决领域长期未解问题时引发的争议，已征询一个由顶尖数学家组成的顾问小组意见。

但 OpenAI 未能达到这些标准，尤其是在数学家强调数学结果必须可由人类理解这一点上。这尤其令人担忧，因为一篇新论文指出，OpenAI 模型据称解决的一道价值百万美元的问题中，其自然语言解答与形式化表达的解答之间存在缺口。

由普林斯顿大学高等研究院托管的数学与人工智能顾问组（Advisory Group on Mathematics and Artificial Intelligence，AGMAI），由来自全球不同机构的九位知名研究人员组成。

该组织于 9 月底发布了关于前沿实验室解决数学问题的准则。AGMAI 在谈及最新一批证明的声明中表示：“最终，应由数学界评估我们的建议在多大程度上得到了成功遵循。”

然而，该组织的首项要求是“停止在专有模型上测试高阶数学问题”。OpenAI 的发布内容明确写道，它正在使用数学领域的开放研究问题评估其专有模型。

当 TechCrunch 要求对 OpenAI 最新一批证明发布作出更全面的评估时，该顾问组没有回应。这家实验室显然遵循了其中部分原则，包括尽快发布结果，以及提供模型如何得出结论的信息。但并非全部如此：719 份手稿中，仅有 10 份包含模型思维链的发布内容。

对于人们尚无法理解的论文，数学家建议应将证明形式化；但 OpenAI 发布的证明中，只有 42% 尚未经历这一过程。

归根结底，按照 AGMAI 的原则，OpenAI 在发布证明时是否正在“承担确保人类理解将会随之而来的责任”，仍不明确。AGMAI 建议 OpenAI 协助资助人类数学家的工作，因为这些数学家对于让实验室的解答在任何实际意义上变得有意义都是必不可少的。

“问题正被 AI 提示词操作者自主解决；一旦最初的目标被‘解决’，他们就对更广泛的领域本身不再感兴趣，也不足够理解 AI 输出，因而无法回答有关结果的问题、进行报告，或以其他方式与该领域的其他成员互动，”曾批评 OpenAI 方法的知名数学家陶哲轩在发布后于社交媒体上写道。

剑桥大学和伦敦国王学院数学家本周发布的一篇论文，对前沿实验室处理这些挑战的方式提出质疑，正是这一问题的例证。

当 AI 模型解决数学问题时，它们首先生成一份“自然语言”解释，随后尝试用 Lean 表达该结果。Lean 是一种编程语言，理论上可通过将证明作为代码编译，来确认其准确性。

然而，模型将自然语言证明翻译为代码的方式可能存在问题；这篇论文记录了至少两处不一致，涉及 OpenAI 针对一道源自 Navier-Stokes 方程的问题所提供解答中的自然语言证明与 Lean 代码。Navier-Stokes 方程用于描述流体的复杂行为。

这些不一致未必能够推翻其中任何一个解答，但它们确实引发了疑问：在没有人类参与的情况下，我们是否能简单地依赖模型将自己的解答形式化。这也是 AGMAI 要求 OpenAI“纳入将自然语言与形式化产物相互关联的机器可读元数据”的原因之一，而这家前沿实验室并未在此次发布中这样做。

“由于误译现象——正如本文所强调的那样——OpenAI 的自然语言证明以及其他自动形式化的 Lean 证明，表面上不应被信任，除非它们接受与其他证明相同的同行评审流程和审查，”这篇题为“迷失在翻译中”的论文作者总结道。

数学家强调，当人类发现新结果时，他们会对结果负责，并通过论文、报告和研讨会与更广泛的学术共同体互动。这一过程能够增进对解答的理解，发现可用于解决其他问题的策略，并使新知识能够应用于实践领域。

哈佛大学数学教授 Melanie Wood 对 TechCrunch 表示，当模型被提示去解决一个困难问题并输出解答时，“在发布之时，人类尚未理解这些解答，而现在工作才刚刚开始”。

When OpenAI released hundreds of claimed solutions to some of the world’s hardest math problems this week, the frontier lab said that it had consulted an advisory group of elite mathematicians to avoid the controversy that came with the last time one of its models solved a long-standing problem in the field.

But OpenAI fell short of those standards, particularly where the mathematicians emphasized the need for human understanding of a mathematical result. That’s especially concerning after a new paper highlighted gaps between the natural language and formally expressed solution to a million-dollar problem ostensibly solved by OpenAI’s models.

The Advisory Group on Mathematics and Artificial Intelligence (AGMAI), hosted by Princeton University’s Institute for Advanced Studies, is made up of nine prominent researchers at institutions around the world.

The organization released guidelines for frontier labs solving math problems at the end of September. In a statement on the latest set of proofs, the AGMAI said that “it is ultimately up to the mathematical community to assess the extent to which our recommendations were followed successfully.”

However, the organization’s first request was “to stop testing advanced mathematical problems on proprietary models.” OpenAI’s release explicitly says that it is evaluating its proprietary models using open research problems in mathematics.

The advisory group did not respond when asked by TechCrunch for a more thorough evaluation of OpenAI’s latest proof release. The lab clearly followed some of its principles, including releasing results as soon as possible and including information about how the models reached their conclusions. But not for all of them: Just 10 of the 719 manuscripts included releases of the model’s chain of thought.

For papers that people don’t understand, the mathematicians suggested the proofs should be formalized — but just 42% of the proofs released by OpenAI had not undergone this process.

Ultimately, it’s still not clear that OpenAI is taking “responsibility for ensuring that human understanding will follow” when releasing its proofs, in accordance to the AGMAI principles. AGMAI suggested that OpenAI should help fund the work of human mathematicians who will be required to make the lab’s solutions meaningful in any real way.

“Problems are being solved autonomously by AI prompters who have no interest in the broader field itself once their initial target is ‘solved’, and do not understand the AI output well enough to answer questions on the result, give talks, or otherwise interact with the rest of the field,” Terence Tao, a prominent mathematician who has criticized OpenAI’s approach, wrote on social media after the release.

That problem is exemplified by a paper released this week by mathematicians at the University of Cambridge and King’s College in London that questions the way frontier labs are approaching these challenges.

When AI models solve mathematical problems, they first create a “natural language” explanation, then try to express that result in Lean, a programming language that in theory confirms the accuracy of the proof by compiling it as code.

However, there may be problems with the way the models translate their natural language proofs into code; this paper documents at least two discrepancies between the natural language proof and the Lean code behind the solution OpenAI has offered to a problem derived from the Navier-Stokes equations that describe the complex behavior of fluids.

These discrepancies don’t necessarily disprove either solution, but they do raise questions on whether we can simply rely on models to formalize their own solutions without human involvement. That’s one reason that AGMAI asked OpenAI to “include machine-readable metadata correlating the natural language and formal artifacts,” something that the frontier lab did not do with these releases.

“Because of the phenomenon of mistranslations — as highlighted in this paper — the NL proof by OpenAI and
other autoformalised Lean proofs should not prima facie be trusted without the same peer review process and
scrutiny that other proofs are subjected to,” the authors of the “lost in translation” paper conclude.

Mathematicians stress that when new results are discovered by humans, they take responsibility for them and engage with the broader community through papers, talks, and seminars. That process increases understanding of the solutions, finds strategies that can be used to solve other problems, and allows the new knowledge to be applied in practical fields.

When a model is prompted to solve a hard problem and spits out a solution, “there is not human understanding of them at the point of release, and now the work begins,” Harvard University mathematics professor Melanie Wood told TechCrunch.