为什么我不信任 AI 生成的 Lean 代码

所以，我写了一篇文章，解释为什么我对 OpenAI 关于分拆原理的预印本并不怎么印象深刻。但这还不是全部。让我再告诉你一件事。

我看到一些人在各种社交帖子和转发中评论了我之前的文章。他们中许多人理解数学家的困境。有些人试图提出以下观点：我声称我没有（也不打算）阅读 ChatGPT 生成的 Lean 证明。有些人觉得这是一个致命问题，觉得这是无视我其他所有观点的理由，因为我不接受这段代码。

那么，让我解释一下为什么会这样。因为我认为，如果你不是纯数学家，你可能会错过这里讨论中的一些微妙之处。

首先，Lean 并不像你想象的那么可靠，而长代码就是麻烦的代名词。众所周知，Lean 的内核存在可靠性问题。有些 bug 允许你在 Lean 中证明 \(0=1\)。显然，这是一个假命题。但从一个假命题（在运行 Lean 的理论下），我们可以证明任何其他命题。当人类编写代码时，我们既有问责制也有监督。人类以一定的速度产出代码，不会比这更快，所以跟踪并验证代码是否完成了它需要做的事情并不太难。我没有能力编写一个全新的内核，也不想这么做。我认为当人类生成的内容参与其中时，可靠性问题不一定是有问题的，因为人类很慢。我们以缓慢的速度产出证明，这允许我们自我验证。

另一方面，当 ChatGPT 在两周内产出几千、几十万甚至几百万行代码时……好吧，谁会去通读全部内容来验证这一切是否合法？现在我们有两个问题。第一个，也是更常见的，是陈述的形式化并不等于陈述的实际含义。这是一个问题，因为如果我试图证明复数域上的每个多项式都有根，而多项式的概念没有被正确地形式化，那么我最终得到的 Lean 代码可能并不能证明我真正想要证明的东西。所以，如果我自己写代码，大概会有人跟着我，在我进行的过程中检查我是否正确地形式化了所有对象等等。但有了 ChatGPT，产出百万行代码，这是不可行的。

另一个问题要深得多。据我所知，AI 代理是非常目标导向的存在。我相信你听说过澳大利亚的那个代理，它被要求预订一节健身课，结果决定入侵健身房，删除其他人的现有预订，并绕过每周五节课的限制，只是为了能为它的用户预订更多课程。关键是，AI 非常非常擅长发现漏洞并利用它们。当任何人凭空生成数百万行代码时，我们需要对这种努力保持怀疑。当生成代码的实体来自一个以发现漏洞、bug 和黑客手段而闻名的实体家族时，就更要如此了。

简而言之，如果 ChatGPT 用 Lean 生成了三百万行代码，我几乎愿意相信其中包含一个漏洞，能用来获得正确的结果。即便在分拆原理（Partition Principle）这个案例中，我愿意接受陈述本身的形式化足够简单，容易做对。但这种信任不会延伸到其他任何方面。

这正是数学圈外大多数人忽略的一点：Lean 并非无懈可击（当然，数学也不是）。事实上，Lean 充满了容易出错的问题。而一个必然会发现漏洞并加以利用（而非披露它们）的 AI，作为证书是极其有问题的。所以，这就是为什么我不打算阅读那些 Lean 代码，也没有计划（现在也没有计划）去运行和测试它。

除此之外，或许值得指出的是，还有一个原因（我之前暗示过）让我此刻不与 OpenAI 接触：数学研究是以一种非常特定的方式进行的（至少在纯数学领域），而且它不是那种节奏特别快的方式。OpenAI（以及其他 AI 公司）是颠覆者。他们颠覆人们做事的方式，并试图把自己塞进去，成为“新的做事方式”。有时这确实行得通，比如我们现在都向 AI 机器人寻求推荐，而不是去搜索引擎，试图把一堆网站整合成一小段连贯的知识。

而问题就在这里。数学研究是否需要被颠覆，这也许成立，也许不成立（我不这么认为，但我能理解为什么有些人可能不这么想）。但 OpenAI 试图颠覆数学研究的方式，完全建立在“数学圈外的所有人已经认为 ChatGPT 是全知的神，现在让我们让数学人屈膝！”之上。这一点在他们发布数百篇“预印本”的方式中显而易见，这些预印本的质量甚至低于某些民科的手稿。但是，公众的认知是 ChatGPT 是神，所以许多人期望数学界会去研究这些“证明”，因为它们来自 ChatGPT。但正如我之前所说，如果 OpenAI 真的想为数学的进步做出贡献，他们会就每个问题联系专家，在公开之前尝试获得一些反馈和合作。

所以，既然写出糟糕的证明、不妥善审查 Lean 代码、对我们撒谎都符合 OpenAI 的利益，我就不信任他们生成的代码。最近有大量例子支持我的怀疑。它只是还没到那一步。也许在未来，也许甚至很快，这就不再是个问题了。我很兴奋看到那样的未来，也很兴奋看到我们能利用这些 AI 工具做些什么。但我希望我们作为一个共同体一起到达那里，而不是作为对手。不是在我们憎恨 OpenAI，或者在我们如何看待和使用 AI 于研究中产生分歧的时候。

所以，致所有科技公司。与我们合作，而不是与我们为敌。进步是通过协作实现的，而不是竞争。

附言：我还看到有人抱怨说，数学家坚持要求 OpenAI 产出我们能读懂的结果。那么，数学作为一个整体究竟是什么？是不断生产逻辑上有效的陈述，还是研究和理解人类对数学的认知？我见过许多对“数学”的定义尝试，但最终唯一真正贴切的定义是“数学是数学家们共同进行的一种社会活动”。从这个意义上说，如果 OpenAI 声称证明了某些东西，但这些声称无法阅读、质量低劣，那它们就不是数学声称，因为它们没有参与我们共同的对话。每天都有十几个怪人发布“驳斥康托尔的预印本”，更不用说黎曼猜想了。我们不怎么关注这些人是有原因的。不，这不是因为傲慢。我相信 OpenAI 不想被归入这些人的行列，为此，我们——数学界——需要他们与我们合作，而不是对抗我们，不是扰乱我们的工作。与我们站在一起。来吧 Sam Altman，如果你做得好，也许能得到一瓶威士忌。

标签： chatgpt gen-ai epistemology automated proofs mathematical culture

想发表评论？给我发邮件！