arXiv cs.AI· Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie, Zhi Wang, Maziar Raissi·· 12 小时前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% 被接受。
正文 · 原文
Abstract:Lean verifies that a generated declaration is well typed, but cannot check whether it states what the user intended. We measure how far compilation overstates faithfulness in statement autoformalization without canonical Lean targets. Our criterion requires Lean compilation and agreement of two LLM judges from different model families. On an independent random audit, it agrees with the human majority on 91.5% of cases; it rarely accepts an unfaithful output but rejects some faithful ones. Across eight systems on 227 university-level statements, the gap between compiling and accepted outputs ranges from 1.3 to 29.5 percentage points: our tool-augmented agent compiles 87.2% of the statements, but only 57.7% are accepted. Human review of all the agent's rejections confirms that 23.8 of its 29.5 points are real translation errors. For the gaps of the seven one-shot systems, a two-stage review by Claude Opus 5.5 with Lean and GPT-6.1 Sol, validated on these human labels, finds that 78-100% are real translation errors for six of them. When GPT-5.2, one of the two judges, grades the translations of two models released after it, GPT-6 Astra and Claude Opus 5.5, it accepts 83% of the statements for each, against 21% for one-shot GPT-5.2. For these two models, the same review classifies only 4 of their 54 rejections (7%) as translation errors, so most of their measured gap is judge errors rather than translation errors. This is consistent with these systems erring less while the judge does not: the fewer errors a system makes, the smaller the share of its rejections that are translation errors. Finally, a 2^3 tool ablation of the agent shows that Lean feedback drives most of its compilation gain, and that nearly half of this gain fails the semantic criterion. Code and data are available at this https URL.
| Comments: | v4: adds a decomposition of each measured gap into translation errors and other rejections, using a two-stage LLM review validated on human labels, and results for two models released later. 37 pages, 6 figures, 38 tables |
| Subjects: | Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2606.31002 [cs.AI] |
| (or arXiv:2606.31002v4 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2606.31002 arXiv-issued DOI via DataCite |
Submission history
From: Ke Zhang [view email]
[v1]
Tue, 30 Jun 2026 00:27:53 UTC (257 KB)
[v2]
Thu, 3 Sep 2026 01:23:45 UTC (258 KB)
[v3]
Fri, 2 Oct 2026 23:39:05 UTC (406 KB)
[v4]
Thu, 15 Oct 2026 18:38:26 UTC (777 KB)
来源：arXiv cs.AI · arxiv.org