Kurt Gödel：AI 时代无法逾越的数学边界
Infinities, impossibilities, and the man in the white linen suit
Kurt Gödel 晚年因坚信食物被下毒而绝食身亡，这位逻辑学巨匠用不完备性定理证明了数学系统存在无法自证的真理盲区。从 David Hilbert 的完美机器梦想到 Alan Turing 图灵机的诞生，再到如今耗资万亿美元的 AI 热潮，Gödel 的洞见揭示了规则系统的根本局限：任何基于规则的体系（包括 AI）都存在无法被自身证明的真命题。当 Jürgen Schmidhuber 提出 Gödel machine 试图让 AI 自我改写时，那个“绝对保证”的幻梦再次面临挑战。在 AI 被视为单纯规模问题的今天，重温这些关于无限与不可能的思考，或许能让我们对智能的本质保持一份清醒。
任何足够强大以处理基础算术的规则体系，都会包含一些真实却无法被证明的陈述，这不是因为规则选择不当，而是规则系统本身的结构特征。
HN 评论区
62- jsrozner
有人真正看过 Shai Ben David (SBD) 的结果吗？我最近在一门关于不完备性的课程中，把它作为期末项目研究了一番。在我看来，这其实没那么有趣。
要让“可学习性”变得不可判定，连续统的基数（实数的大小）必须大于所有有限 k 对应的 \aleph_k。ZFC 公理体系对此并无定论（连续统假设 CH 独立于 ZFC），所以这是一种可能的世界设定，因此可学习性确实可能不可判定。
但假设连续统的大小是，比如，\aleph_3（在这种情况下 CH 为假，但并非“荒谬地假”），那么 SBD 展示了如何构建一种压缩方案，因此他们的 EMX（估计最大值问题）就是“可学习的”。然而，他们证明存在的那种压缩方案（仅仅是一个被证明存在的函数）实际上是无法编码的，因为它需要调用良序定理来识别最大元素。所以，不存在能解决该问题的算法（尽管确实存在一个能解决问题的函数）。
这项成果，若无进一步的工作，并不能直接说明哪些类型的问题其抽象概念是可以被学习的。而抽象正是理解和解决问题的核心。
参见：https://arxiv.org/pdf/1909.08410（第 5 节）
- azakai
我觉得整体论点有些牵强。
是的，形式数学确实存在这样的局限。我们不能指望机器是完美的，也不能指望它是可证明完美的。但业界并没有这样假设。为什么要这样假设呢？自然智能本身也不完美，也无法被证明完美。
很多时候，测量就足够了，不必追求确定性。我们无法证明一个程序总会终止，但我们可以检查它在特定执行中是否终止。
近似往往也是我们要的全部。即使我们无法证明训练一个网络的成功率能超过 50%，如果我们能多次尝试（使用不同的数据、初始随机权重、训练技巧或其他方法），那么我们就可以指数级地降低这种风险。（我不确定我们是否有成功的保证，但这正是我们的希望，而且据我所知，没有任何东西表明这是不可能的，这与“完美可证明性”不同。）
最后，完美可证明性或许确实适用于我们关心的那些问题。Gödel、Turing 等人的证明依赖于寻找那些我们无法证明的罕见情况——精心构造的病态案例——但也许人类行为并不属于这一集合。人类行为可能不是证明或可学习性的病态案例。
- zeitgeistcowboy
是的，但计算机系统、工具或 AI 真的需要被证明是正确的，或者 100% 保证不会造成伤害才有用吗？替代方法（人类、简单规则）也做不到这一点。完美往往是“足够好”的敌人。这里只是讲点实用主义。
- skippyfish
除了看起来像是 100% AI 生成的之外，这篇文章对 Gödel 论证的使用非常牵强附会，我认为文章末尾的以下段落最能体现这一点：
“这四条线索共同源于 Gödel 在 1931 年证明、Turing 在 1936 年进一步阐明的内容。基于规则的系统无法完全解释自身。一个系统无法认证自身的可信度。一个学习框架无法确定自身的边界。一个安全策略无法验证自身的完备性。
神经网络感觉上是有机而非规则化的这一事实，丝毫不能缓和上述观点。模型的权重是数字，其训练是算术运算，所有这些都运行在 von Neumann 对 Turing 虚构设备的实现之上。AI 并非邻近于这种数学。AI 就是由它构成的。
AI 行业，可以理解地，宁愿不去深究这一点。”
这完全是个非 sequitur（逻辑跳跃）。Gödel 的论证甚至没那么深刻：它只是说，一个足以嵌入标准自然数算术的公理系统，必须独立于某个构造出的句子，也就是说，无论该句子是真还是假，系统的运行结果都一样，而你无法从其公理中判断这两种情况哪种正在生效。虽然这对哲学家来说很糟糕，但这并不会让数学在实用意义上变得没那么有用、没那么可靠或没那么正确。它对 AI 行业今天所承诺的任何东西都没有实际影响。
- jibal
Turing 证明的是：没有图灵机（TM）能判定所有图灵机是否停机……而不是说没有图灵机能判定某个特定的图灵机是否停机……这是一个对证明的常见误解。类比来说，虽然我们无法证明没有任何 AI 是有害的或无害的，但我们可以证明某些特定的 AI 是有害的或无害的。