Hacker News AI · 2026/10/6 10:58:01
研究指 AI 形式化验证纳维 - 斯托克斯方程存在语义失真风险
最新研究指出，将自然语言数学证明（如 OpenAI 宣称的纳维 - 斯托克斯方程解爆破证明）自动翻译为 Lean 等形式语言时，因无法解决语义歧义，可能导致验证结果与原始论证脱节。该过程被证实处于可解性复杂度指数（SCI）的最高层级，其难度理论上超过停机问题，意味着当前 AI 形式化验证在复杂数学领域缺乏可信度保障。
报道全文原始报道全文
摘要：自动形式化（Autoformalisation）正日益被用于验证数学文本，包括由 AI 生成的文本，例如 OpenAI 宣布的关于 Navier-Stokes 方程解爆破的证明。在此过程中，AI 系统将自然语言（NL）文本翻译为 Lean 等形式语言。一旦完成此翻译，即可轻松地对以形式语言表达的论证进行机械验证。本文旨在说明为何这一过程可能无法对原始 NL 论证提供任何保证，原因在于实现语义忠实翻译存在种种困难。特别是，我们强调了解决数学 NL 文本中歧义的问题——这是实现语义忠实翻译所必需的——在可解性复杂度指数（SCI）层级/算术层级中处于任意高的位置（即 SCI = ∞）。因此，非正式地说，提供语义忠实的 AI 自动形式化比任何计算问题都更难，包括停机问题（其 SCI = 1）。为了展示该结果的影响，我们提供了多个 AI 将 NL 陈述和证明错误翻译为 Lean 的实际案例，导致 NL 证明与其 Lean
验证之间出现不匹配。这些案例包括 OpenAI 宣布的 Navier-Stokes 证明。具体而言，我们表明形式化的 Lean 证明并不对应于 Navier-Stokes 方程解爆破的 NL 证明。
评论：25 页，4 幅图 主题：偏微分方程分析 (math.AP)；人工智能 (cs.AI)；逻辑 (math.LO) MSC 分类：35Q30, 03Dxx（主要）以及 68V20, 68Txx, 03B65（次要） 引用格式：arXiv.08144 [math.AP] （或对于此版本使用 arXiv.08144v1 [math.AP]） https://doi.org/10.48550/arXiv.2610.08144
通过 DataCite 发布的 arXiv DOI（待注册）
提交历史
来自：Alexander Bastounis [查看邮箱] [v1] 2026年10月6日 星期二 UTC 10:58 (1,080 KB)