数学家称 OpenAI 的 Navier-Stokes 证明在数学转代码时出现误译

一个数学家团队声称，OpenAI 在发布其对纳维-斯托克斯问题的证明时，似乎犯了一个细微的错误。这个错误并不意味着证明不正确，也不意味着 OpenAI 没有正确解决该问题，但它确实让人质疑 AI 模型生成的数学结果是否总能被信赖。

“对于所有这些由大语言模型生成的证明，必须做的是它们必须由人类来阅读，而这给数学家带来了巨大的额外负担，”剑桥大学的 Anders Hansen 说。

9 月 8 日，OpenAI 宣布它找到了纳维-斯托克斯问题的解决方案，这是数学中最著名的未解问题之一。它发布了两个版本的证明——一个用“自然语言”写成，即像人类数学家那样用英语和数学符号的组合来写，另一个用计算机代码 Lean 写成。Lean 证明本应是自然语言版本的形式化，使计算机能够机械地验证其所有逻辑陈述均为真。Hansen 和他的团队说，问题在于两者并不匹配。

“这个形式化过程试图取代同行评审，”同样来自剑桥大学的团队成员 Fabian Circelli 说。“同行评审意味着由人类的眼睛来审视证明。但我们在这篇论文中表明，使用这类 AI 自动形式化无法起到同样的作用。”

需要明确的是，研究人员并不是说 OpenAI 未能解决纳维-斯托克斯问题。完全有可能自然语言证明和 Lean 证明都提供了解决方案，就像毕达哥拉斯定理有数百个有效证明一样。相反，他们的观点更为微妙：OpenAI 的模型在转换为 Lean 时“误译”了。

“我们并不是说自然语言证明是错的，”Hansen 说。“我们也不是说它是对的。”问题在于 OpenAI 将这两个证明呈现为完全相同，在 Github 上声明“此仓库包含 [论文]‘纳维-斯托克斯的有限时间爆破’中所呈现结果的 Lean 4 形式化”。

Hansen 说，这种误译之所以发生，是因为 AI 必须生成一个能够“编译”的 Lean 证明，即计算机代码完全自洽且不产生错误。如果在自动形式化过程中，AI 发现证明中有一段无法编译，它会尝试寻找变通办法，即使这意味着偏离自然语言写成的证明。

该团队的具体主张集中在证明中称为引理 8.6 的部分。在自然语言证明中，这一部分的一个方程要求某个值小于 m + 4，其中 m 是整数。在 Lean 证明中，对应的值被要求小于 m + 5，这在数学上更弱。

要理解原因，不妨设想有人要求你解方程 x + 3 = 6，答案是 x = 3。可以写出一个证明，说明 x 必定小于 4，也可以写出一个证明，说明 x 必定小于 5。这两个都是完全正确的数学陈述，但它们说的是不同的事情。后一个证明允许 x 有更多可能的答案，因此在数学上更弱。

OpenAI 向《新科学家》表示，它知道自然语言证明与 Lean 代码之间存在不一致，但这并不意味着任何一个证明无效。它表示，一旦发现自然语言证明中的错误，就会予以纠正，并将继续推进该公司本周发布的 722 篇数学论文的形式化工作，其中只有部分论文附有 Lean 证明，而这些证明本身也未经人工检查。

证明堆里的针

发现这一分歧的过程有些超现实：先让 ChatGPT 寻找自然语言证明与 Lean 证明之间可能存在的差异，然后人工逐一核查。ChatGPT 提出的许多差异经检查后其实是一致的。“手动梳理所有这些内容简直是一场噩梦，”Hansen 说。

总的来说，团队花了大约两周时间才确认一处真正的差异，而 OpenAI 称其智能体生成这些证明只用了 88 小时。“OpenAI 吹嘘他们能多快生成这个结果，但这只是整个过程的一部分，”团队成员、伦敦国王学院的Alexander Bastounis 说。

如果数学家要信任这些结果，回答 AI 模型能否准确自动形式化数学这一问题就至关重要。Anders 及其团队已经证明，ChatGPT 有可能生成一个与原始自然语言证明不匹配的 Lean 版本证明，并在过程中悄悄改变逻辑论证以掩盖任何错误。“它想帮我，但这样做反而帮了倒忙，”Hansen 说。

如果这种情况发生在一个冗长而复杂的证明中，任何人若不详细检查两个版本，就很难注意到。由于 OpenAI 刚刚发布的 722 篇论文，这个问题变得更加紧迫。Hansen 说，如果我们认为‘所有这些现在都是真的，我们唯一需要做的就是读论文’，那就危险了。“做科学的目的，是让人类理解世界如何运作，以便做出有依据的决策。如果我们失去了这种理解，我们还在做什么？”

伦敦帝国理工学院的Kevin Buzzard 指出，在这类讨论中，区分定理的陈述与其证明很重要。例如，著名的费马大定理的陈述是：对于正整数 a、b、c 和 n，aⁿ + bⁿ = cⁿ 仅当 n 为 1 或 2 时成立。这很容易转换为 Lean 并可以轻松检查。一旦你确认 Lean 中的某个陈述是正确的，如果该陈述的证明能够编译通过，你就可以确信该证明为真。

正如 Hansen 及其团队所指出的，问题在于这并不能告诉你以 PDF 文档形式发表的证明的自然语言版本是否正确。“我相信 Navier-Stokes 问题已被正确解决，”Buzzard 说。“但我对 PDF 中所描述的证明是否正确远没有那么有信心。”

Hansen 表示，他希望 OpenAI 能“非常认真地”对待该团队的工作，并且必须在开发稳健的自动形式化技术方面做更多工作。“我们有解决方案了吗？还没有。是否有可能以可控的方式做到这一点？是的，有可能，但实现这一目标的最佳且终极的方式完全未知。”