arXiv · AI· Alexander Bastounis, Fabian Circelli, Anders C. Hansen·· 12 天前精选AI 评分69
Navier-Stokes 方程在 AI 自动形式化中的翻译谬误：为何 Lean 验证不能保证自然语言证明的正确性
Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
AI 导读
论文分析了 AI 自动形式化在验证数学文本时的局限性，指出将自然语言准确翻译为 Lean 形式语言以消除数学歧义在计算复杂度上极难。作者通过实例展示了 AI 在翻译自然语言陈述和证明时可能产生偏差，导致形式验证结果与原始自然语言证明不符，其中包括 OpenAI 公布的 Navier-Stokes 方程解爆破证明，其形式化后的 Lean 证明并未对应自然语言版本的证明内容。
推荐理由
论文指出 AI 自动形式化存在语义忠实性难题，并论证了 OpenAI 公布的 Navier-Stokes 方程证明在形式化过程中出现了不匹配。
来源：arXiv · AI · arxiv.org