arXiv cs.AI· Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie, Zhi Wang, Maziar Raissi·· 11 小时前AI 评分32
超越编译：评估自然语言到 Lean 陈述形式化的忠实性
Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
AI 导读
研究提出以 Lean 编译通过加两个不同模型族 LLM 评审一致作为忠实性标准，在独立随机审计中与人类多数判断一致率达 91.5%。在 227 条大学水平陈述上测试八个系统，编译率与接受率差距为 1.3 至 29.5 个百分点，工具增强智能体编译 87.2% 但仅 57.7% 被接受。
正文 · AI 翻译
摘要：Lean 可以验证生成的声明类型正确，但无法检查它是否陈述了用户的意图。我们测量了在没有规范 Lean 目标的情况下，编译在多大程度上高估了语句自动形式化的忠实性。我们的标准要求 Lean 编译通过，并且来自不同模型家族的两个 LLM 评判者达成一致。在一次独立的随机审计中，该标准在 91.5% 的案例上与人类多数意见一致；它很少接受不忠实的输出，但会拒绝一些忠实的输出。在 227 条大学水平的语句上，八个系统在编译输出与可接受输出之间的差距从 1.3 到 29.5 个百分点不等：我们的工具增强型智能体编译了 87.2% 的语句，但只有 57.7% 被接受。对所有智能体被拒案例的人工审查确认，其 29.5 个百分点中有 23.8 个百分点是真实的翻译错误。对于七个一次性系统的差距，由 Claude Opus 5.5 结合 Lean 与 GPT-6.1 Sol 进行的两阶段审查（在这些人工标签上验证过）发现，其中六个系统的差距有 78-100% 是真实的翻译错误。当两个评判者之一的 GPT-5.2 对在其之后发布的两个模型（GPT-6 Astra 和 Claude Opus 5.5）的翻译进行评分时，它分别接受了这两个模型 83% 的语句，而一次性 GPT-5.2 仅为 21%。对于这两个模型，同样的审查仅将其 54 个被拒案例中的 4 个（7%）归类为翻译错误，因此它们测得的大部分差距是评判者错误而非翻译错误。这与这些系统出错更少而评判者并未如此的情况一致：一个系统犯的错误越少，其被拒案例中属于翻译错误的比例就越小。最后，对智能体进行的 2^3 工具消融实验表明，Lean 反馈驱动了其大部分编译增益，而这一增益中近一半未能通过语义标准。代码和数据可在 此 https URL 获取。
| 评论： | v4：使用经人工标签验证的两阶段 LLM 审查，将每个测得的差距分解为翻译错误和其他拒绝，并给出两个较晚发布的模型的结果。37 页，6 幅图，38 张表 |
| 主题： | 人工智能（cs.AI）；计算与语言（cs.CL）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2606.31002 [cs.AI] |
| （或 arXiv:2606.31002v4 [cs.AI] 为本版本） | |
| https://doi.org/10.48550/arXiv.2606.31002 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Ke Zhang [查看邮箱]
[v1]
2026 年 6 月 30 日星期二 00:27:53 UTC（257 KB）
[v2]
2026 年 9 月 3 日星期四 01:23:45 UTC（258 KB）
[v3]
2026 年 10 月 2 日星期五 23:39:05 UTC（406 KB）
[v4]
2026 年 10 月 15 日星期四 18:38:26 UTC（777 KB）
来源：arXiv cs.AI · arxiv.org