新论文:Lean 验证通过不等于 AI 自然语言证明正确,含 OpenAI Navier-Stokes 案例
burny_tech · x · 2026-10-08
arXiv 论文《Navier-Stokes lost in translation》(Bastounis、Circelli、Hansen)指出 AI 自形式化(autoformalisation)的根本缺陷:
- 流程是把自然语言数学文本翻译成 Lean 等形式语言再机械验证,如 OpenAI 宣布的 Navier-Stokes 解爆破证明即用此法;但翻译本身的语义忠实性没有保证。
- 作者论证:消解数学自然语言的歧义在 Solvability Complexity Index(SCI)层级中任意高(SCI = ∞),即语义忠实的 AI 自形式化比包括停机问题(SCI = 1)在内的任何计算问题都难。
- 论文给出多个 AI 在实践中将自然语言命题与证明误译进 Lean 的实例,导致形式化验证结果与原自然语言论证不匹配。
- 结论:Lean 验证通过对原自然语言论证的正确性可能不提供任何置信度,这对当前 AI 自主数学证明的可信度构成直接质疑。
所属事件:剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(14 条相关)→
「漫话AGI」频道最新
- Anthropic 禁止「虐待模型」引争议，被批把机器拟人化、把人去人化 — DavidSacks · 2026-10-09
- 安全研究员频频撤离 AI 公司，激进派称留下才能掌舵 — ZeroStateReflex · 2026-10-09
- 开发者放话:不会编程就没资格做游戏，AI 圈吵翻 — AIandDesign · 2026-10-09
- Robocurve 联创:后劳动经济或成砍 UBI 换 GPU 的囚徒困境 — DavidDuvenaud · 2026-10-09
- 95 岁威廉·夏特纳:星际迷航 promised 的未来就在你们眼前 — PeterDiamandis · 2026-10-09
- 微软 AI 负责人 Suleyman 用一个表情回应「虐待 Claude 违规」条款 — mustafasuleyman · 2026-10-09