arXiv cs.AI· Alexander Bastounis, Fabian Circelli, Anders C. Hansen·· 10 天前AI 评分62
论文：Lean 验证 AI 自动形式化无法保证自然语言证明正确
Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
AI 导读
arXiv 论文指出，AI 自动形式化把自然语言数学文本翻译成 Lean 后，即使形式化证明可被机械验证，也不能保证原始自然语言论证正确。作者证明，为做到语义忠实的翻译所需的歧义消解问题在可解性复杂度指数（SCI）层级中任意高（SCI = ∞），比包括停机问题（SCI = 1）在内的任何计算问题都更难。
正文 · AI 翻译
摘要：自动形式化正越来越多地用于验证数学文本，包括由 AI 生成的文本，例如 OpenAI 宣布的 Navier-Stokes 方程解爆破证明。在此过程中，AI 系统将文本从自然语言（NL）翻译为 Lean 等形式语言。一旦完成这种翻译，用形式语言表达的论证就可以很容易地被机械验证。本文的目的是说明，由于在语义上忠实翻译存在各种困难，这一过程为何可能无法为原始 NL 论证提供任何信心。特别地，我们强调，为了解决数学 NL 文本中的歧义——这是提供语义忠实翻译所必需的——该问题在可解性复杂度指数（SCI）层级/算术层级中处于任意高的位置（SCI $= \infty$）。因此，非正式地说，提供语义忠实的 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:2610.08144 [math.AP] |
| （或 arXiv:2610.08144v1 [math.AP] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.08144 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
来自：Alexander Bastounis [查看电子邮件]
[v1]
2026 年 10 月 6 日星期二 10:58:01 UTC（1,080 KB）
来源：arXiv cs.AI · arxiv.org