arXiv cs.AI· Martin Amster, One An, Holly Baker, Fernanda Graciolli, Simon Henniger, Nada Amin·· 3 天前AI 评分29
claimcheck：衡量并提升规格说明的忠实度
claimcheck: Measuring and Improving Specification Faithfulness
AI 导读
研究者构建了覆盖 Dafny、Lean 4、Isabelle 和 Rocq 四种形式语言的规格形式化端到端基准，共 3,234 行，每行将自然语言需求与形式化产物配对，其中三分之一为保持语义的改写。他们提出 claimcheck，先将形式化产物翻译回英文，再由独立 judge 模型判断其与需求是否表达同一保证，在四种语言上较单次调用基线提升 8.2 至 9.8 个百分点的宏召回率。
正文 · AI 翻译
摘要：形式化验证证明程序满足其规约，但对规约是否捕捉到作者的本意却只字不提。随着 LLM 越来越多地同时编写代码和规约，作者的自然语言需求与规约之间的鸿沟成为现实风险。一个比所要求性质更窄的机器可验证证明毫无价值，却能通过所有检查。弥合规约形式化问题就是要弥合这一鸿沟：给定自然语言需求，生成含义与之匹配的形式化产物。为衡量这一鸿沟，我们整理了一个端到端基准，涵盖四种形式化语言：Dafny 合约以及 Lean 4、Isabelle 和 Rocq 定理陈述。其 3,234 行中的每一行都将一条自然语言需求与一个形式化产物以及一个通过执行、证明或其所来源的基准确立的标签配对。其中三分之一的行是对该产物的保义重写，且保留忠实标签，因此评判者无法通过检测某行是否被编辑过来打分。我们提出 claimcheck，一个检测错误形式化的工具：形式化产物由一个从未见过需求的模型翻译回平实英语，再由另一个模型（评判者）判定该非形式化表述与需求是否表达相同的保证。在全部四种语言上，相比单次调用同时给出需求和产物，其宏召回率提升 8.2 至 9.8 个百分点；相比单次调用同时给出相同的保义重写列表，提升 4.2 至 6.0 个百分点。同时向评判者展示产物会损失 1.4 至 4.5 个百分点。在四个同时看到产物的评判者中，随着评判者变强，增益缩小，最强评判者与知情单次调用的差距在 1 个百分点以内。
| 主题： | 计算与语言（cs.CL）；人工智能（cs.AI）；编程语言（cs.PL） |
| 引用为： | arXiv:2610.17358 [cs.CL] |
| （或 arXiv:2610.17358v1 [cs.CL] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.17358 arXiv 颁发的 DOI 经由 DataCite（待注册） |
提交历史
来自：Simon Henniger [查看邮箱]
[v1]
2026年10月12日星期一 20:14:51 UTC（55 KB）
来源：arXiv cs.AI · arxiv.org