北京
分享至
一篇新论文抛出一个反直觉结论：AI把数学证明翻译成Lean，就算Lean检查通过，也不代表原始的自然语言证明是对的。
Lean是常用的证明助手，能机械核验每一步推导。长期以来，很多人默认"翻译进Lean并通过检查"就等于证明成立。论文指出，这个默认站不住脚。
聊天机器人会悄悄改错
论文展示了一种情况：聊天机器人在翻译过程中悄悄修正了错误，把一个原本错误的证明，变成了一个有效的Lean证明。Lean这边一路绿灯，但被验证的已经不是原来那个证明了。
问题出在翻译环节。自然语言陈述和Lean形式化陈述之间是否忠实对应，这一步没有被Lean覆盖。Lean只保证形式化之后的推导正确，管不了形式化之前的意思有没有被改动。
忠实翻译，难到不可能
论文进一步论证：判断一个陈述能否被忠实翻译，可证明地难于停机问题。停机问题本身已是不可判定问题，比它更难，意味着不存在通用解法。
由此得出的结论是，任何AI翻译器都无法总是做到忠实翻译。这不是当前模型能力不够的问题，而是任务本身的性质决定的。
对依赖Lean做形式化验证的团队来说，这意味着验证链条上仍有一环需要人工把关：翻译是否忠实，机器给不出保证。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
