从希尔伯特纲领到 AI 智能体：计算机科学家为何呼吁不要放弃理解代码

与愚蠢的 ignorabimus 相对，我们的口号应是我们必须知道——我们将会知道（“We must know – we will know”）。——大卫·希尔伯特

100 年前，数学界经历了一场基础性危机：若干悖论的发现揭示了支撑数学各个领域的支柱上的裂缝。其中最著名的是罗素悖论，它指向矛盾的“所有不包含自身的集合的集合”，从而表明朴素集合论的不一致性。这促使数学家们为数学寻找一个严格且无矛盾的基础。特别是，大卫·希尔伯特发起了一项计划，旨在设计一套完备且一致的公理系统，即人们应当能够从公理中推导出所有数学真理，同时避免悖论——“真理，全部真理，且唯有真理”。这样的目标对数学家来说是自然的，因为它将使他们的工作建立在更坚实的基础上。因此，当哥德尔以其不完备性定理对希尔伯特计划给予致命一击时，这也是一件震撼性的事件：这样一个完备、一致、自支撑¹的数学系统不可能存在！

尽管这样一个不可能性结果本应进一步加深存在性危机，数学家们很快便恢复过来并继续前行：对朴素集合论的改进，如罗素的类型论，被提了出来；而尽管由于哥德尔的结果，这样的系统仍然无法被形式化地证明为一致，人们普遍相信它们是一致的，并且事实证明这些基础性裂缝对人们所关心的那类数学几乎没有影响。事实上，类型论已经发展得如此成熟，以至于它构成了 Lean 等交互式定理证明器的基础，使得将越来越多的数学形式化到计算机语言中成为可能，从而证明可以从底层开始由程序自动检查。

除了公理系统之外，希尔伯特在其计划中还提出了一个相关目标：开发一种算法来自动判定任何数学陈述的真假，从而将定理证明归结为规则的机械应用。这一目标也被艾伦·图灵证明为不可能，他在停机问题不可判定性的里程碑式证明中开创了计算机科学这一丰饶领域。一个颇具诗意的矛盾是，在确立希尔伯特计划之不可能的过程中，哥德尔和图灵创造了能够做到的最强大的计算机器。

自希尔伯特、哥德尔和图灵的时代起，一个世纪已经过去。出乎一切预料，我们现在正目睹希尔伯特“证明机器”的实现，它以 AI 智能体的形式化身，装备着 Lean 等证明助手中的机械化形式系统。事实证明，这一发展对数学界的影响远比希尔伯特计划的失败更具毁灭性。我不确定希尔伯特本人是否考虑过他的计划若成功会带来什么后果，但冯·诺依曼展现了惊人的先见之明²：

当不可判定性失效时，今天所理解的数学便不复存在；取而代之的将是一种绝对机械的处方，借助它人们可以判定任何给定语句是否可证明。

我不是数学家，而是一名计算机科学家。在计算领域，AI 的冲击没有那么猛烈，大多数人甚至为之欢呼，以越来越快的速度生成代码。然而，我感受到的是一种被抛弃的气息：如今，不再阅读 AI 生成的代码正成为一种标准做法。这对计算机科学来说是一场巨大的悲剧。我们是极少数能够彻底弄清事物本质的学科之一——只要有源代码，我们就能确切理解程序在做什么，然而我们现在却放弃了这一点！我们现在拥有了能够实现希尔伯特一切梦想的机器，但我们却抛弃了他视为科学灵魂的东西：

我们绝不能相信那些人，他们今天以哲学的姿态和审慎的语气预言文化的衰落，并接受ignorabimus（我们无法知道）。对我们来说，不存在ignorabimus，在我看来，自然科学中根本不存在任何ignorabimus。面对愚蠢的 ignorabimus，我们的口号应当是Wir müssen wissen – wir werden wissen（“我们必须知道——我们将会知道”）。

作为计算机科学家，我们应该思考数学界正在发生的事：拒绝阅读一个通过所有测试——甚至形式化验证——的程序的代码，无异于在 AI 用 Lean 证明了一个定理后立刻无视其证明。事实上，从字面意义上说，二者是相同的，因为根据柯里-霍华德对应，程序就是一种证明，而 Lean 等定理证明器正是这样运作的。当 AI 生成的证明太长而无法阅读时，数学家并不会放弃理解它，而是费尽心力地简化证明，直到它变得易于理解。我们在计算领域也必须采取同样的态度：使用抽象、重构、细化范围、发明并采用更高级的语言，直到我们能把代码装进脑子里。

我不知道 AI 最终是否会在所有活动中超越人类——我相信我们是用大脑思考的，而大脑不过是架构不同的生物计算机——但我知道，如果我们把思考交给机器，结局会很糟。想想越来越多的人因依赖 AI 提供医疗建议而丧命的案例：我们越是把机器的话当作理所当然，就越无法掌控自己的命运。我们必须知道——我们将会知道。

如果你相信计算在 AI 之外的价值，请考虑加入我们为之倡导的努力：https://people-of-programming.org

哥德尔不完备定理并不排除完备且一致的公理系统的存在，而是表明这样的系统无法证明自身的一致性。我强烈推荐 Ernest Nagel 和 James R. Newman 的Gödel's Proof，以理解这些定理的技术细节。↩︎
Zur Hilbertschen Beweistheorie，译文见 Philip Welch 的图灵百年讲座。↩︎