研究称AI自动形式化通过Lean验证不保证原证明正确

Alexander Bastounis、Fabian Circelli 与 Anders C. Hansen 发表论文，论证 AI 将自然语言数学证明自动形式化为 Lean 等形式语言时，即使形式化论证能被机械验证，也不能保证原始自然语言证明被忠实表达、因此正确。作者称语义忠实的翻译存在多种困难，并列举了 AI 误译案例，其中包括 OpenAI 宣布的 Navier-Stokes 证明，称其对应的 Lean 证明与自然语言证明不对应。 作者还基于论文摘要将数学文本的歧义消解置于 SCI=∞ 层级。该论证基于论文摘要，作者观点尚属其声称，案例对应关系未经验证。

AI 根据报道生成 · 1 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。