arXiv cs.AI· Alexander Bastounis, Fabian Circelli, Anders C. Hansen·· 8 小时前精选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）在内的任何计算问题都更难。
推荐理由
论文用可计算性层级论证自然语言数学文本的忠实翻译不可判定，并给出 Lean 形式化与原文不符的实例。
来源：arXiv cs.AI · arxiv.org