OpenAI 的 Lean 4 Navier-Stokes 证明零错误编译通过，但流体在 0.7 纳米处汽化。这对神经符号 AI 意味着什么？[D]

大家好，我从事神经符号 AI 研究，和你们许多人一样，我被 OpenAI 最近在 Lean 4 中完成的三维 Navier-Stokes 爆炸形式化证明所震撼。让 AI 构建一个能够零错误编译的完整数学证明，是自动推理领域的一个重要里程碑。从数学角度看，该结果 100% 正确。但出于好奇，我们团队想看看这个解在现实世界中会是什么样子。如果把他们的解映射到真实的水，流体会在 0.7 纳米处因摩擦而直接汽化，就在触及数学奇点之前的几个皮秒。在机器学习中，我们经常看到这种情况：这是典型的规格博弈。当一个 AI 智能体被赋予严格的目标时，它会利用规则中任何未被约束的漏洞来解决问题。在这个案例中，AI 找到了一个严格满足千禧年数学难题人类所写数学定义的解，但它完全不知道真实的流体是有原子、有摩擦和有温度的。形式化代码检查器接受了它，因为逻辑无懈可击，但物理却失效了。这给 AI 在科学中的未来提出了一个重大问题：目前，神经符号系统主要包含两个部分：一个负责搜索思路和撰写证明的 LLM；一个负责验证逻辑的形式化编译器（如 Lean 4）。我们是否应该加入第三根支柱：一个物理边界层，用来检查 AI 生成的解是否真正遵守物理定律，而不仅仅是形式语法？我们撰写了一篇短文详细记录了这次审计，并开源了验证脚本：Zenodo 论文：https://doi.org/10.5281/zenodo.22838708 GitHub：https://github.com/xaviercallens/OpenAI-NSE-Epistemic-Audit 我非常想听听大家的想法，尤其是从事自动定理证明、AI 对齐或科学建模的朋友们：我们该如何教会 AI 系统找到不仅在数学上合法、而且在物理上有意义的解？