autoformalisation

本文论证了用 Lean 对 AI 自动形式化进行验证，并不能保证原始自然语言证明的正确性：语义忠实的翻译在可解性复杂度指数层级中是不可判定的。作者展示了实际存在的 AI 误译案例，其中包括 OpenAI 宣布的 Navier–Stokes 爆炸证明中的一处不一致。

介绍了FaithformBench，一个用于评估数学思维链自动形式化系统忠实度的基准，通过测量扰动步骤上的有效性与无效性保持来评估。应用于八个AF系统后，揭示了普遍的“谄媚”现象，即无效输入被静默纠正。