OpenAI 在其 Navier-Stokes 证明中将数学误译为代码

一组数学家声称，OpenAI在发布其Navier-Stokes问题的证明时似乎犯了一个细微的错误。该错误并不意味着证明是不正确的，或者OpenAI没有正确解决该问题，但它确实让人怀疑AI模型生成的数学结果是否始终可以信赖。

“所有这些大语言模型生成的证明都必须由人类阅读，这给数学家带来了巨大的额外负担，”University of Cambridge的Anders Hansen说。

9月8日，OpenAI宣布其已找到了Navier-Stokes问题的解，这是数学界最著名的开放问题之一。它发布了两个版本的证明——一个是用“自然语言”编写的（即人类数学家常用的英语和数学符号的结合），另一个是用计算机代码Lean编写的。Lean证明旨在作为自然语言版本的形式化，允许计算机机械地验证其所有逻辑陈述是否真实。Hansen和他的团队表示，问题在于两者并不匹配。

“这一形式化过程正试图取代同行评审，”团队成员、同样来自University of Cambridge的Fabian Circelli说。“同行评审意味着人类眼睛会审视这些证明。但我们在本文中展示的是，使用这种类型的AI自动形式化无法达到同样的目的。”

需要明确的是，研究人员并不是说OpenAI未能解决Navier-Stokes问题。自然语言证明和Lean证明都有可能提供了一个解，就像Pythagoras’s theorem有数百个有效的证明一样。相反，他们的观点更为微妙：OpenAI的模型在转换为Lean时发生了“误译”。

“我们并不是说自然语言证明是错误的，”Hansen说。“我们也没有说它是正确的。”问题在于OpenAI将这两个证明呈现为完全相同，并在Github上称“此存储库包含[论文]‘Finite time blowup for Navier–Stokes’中呈现的结果的Lean 4形式化”。

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

该团队的具体主张取决于证明中被称为Lemma 8.6的部分。在自然语言证明中，该部分的一个等式要求某个值低于m + 4，其中m是一个整数。而在Lean证明中，等效值被要求低于m + 5，这在数学上更弱。

为了理解原因，想象一下被要求解方程x + 3 = 6，其答案是x = 3。可以写一个证明说x必须小于4，也可以证明x必须小于5。这两个在数学上都是完全正确的陈述，但它们表达的意思不同。后者的证明允许x有更多可能的答案，使其在数学上更弱。

OpenAI告诉New Scientist，它意识到了自然语言证明与Lean代码之间的不匹配，但这并不意味着任何一个证明是无效的。它表示，一旦发现自然语言证明中的任何错误，它将予以纠正，并将继续形式化该公司本周发布的722篇数学论文，其中只有一部分附带了Lean证明，而这些证明本身尚未经过人工检查。