arXiv cs.AI· Aditya Vempaty, Himaneesh Sompalle, Manan Tayal, Mowafak Allaham, Prasenjit Dey, Ashish Jagmohan, Ravi Kokku·· 10 小时前AI 评分42
LLM 驱动的已验证代码生成存在三重失效面：验证通过不等于规格正确
Verified but Vacuous: Three Failure Surfaces of LLM-Driven Verified Code Generation
AI 导读
一项条件审计指出，LLM 生成代码的“验证通过”混淆了验证器接受、语法规格绑定与语义规格保真三个层面。Li@Opus 在 Claude Opus 4.7 上复现 Dafny-as-IR 流程，HumanEval 验证器接受率达 99.1%，但仅 1.9% 的样本带有绑定到规格谓词或函数的证书。
正文 · AI 翻译
摘要：在评估 LLM 生成的代码时，“已验证”应当意味着什么？许多现有流程只报告一个单一的验证数字。我们认为，这抹平了在条件审计序列中测量的三个不同属性：验证器接受（Surface A）、\emph{语法规范绑定（Surface B：证明义务是否绑定到规范？）以及 \emph{语义规范保真度}（Surface C：规范是否捕捉到了非正式需求？）。两项实证演示表明这些层面是彼此分离的。\textbf{第一（$A \neq B$），通过 Li@Opus（在 Claude Opus 4.7 下对 \citet{li2025dafny} 的 Dafny 作为中间表示（IR）流程的同模型复现）在三个 Python 基准上}：它在 HumanEval 上达到 \textbf{99.1\% 的验证器接受率}，而只有 \textbf{1.9\%} 携带绑定到规范定义的谓词或函数的证书。\textbf{第二（$B \neq C$），通过 VCG 在两个 Rust 基准上}：我们在 Rust 上使用 VCG（这是我们自研的 Dafny 作为中间表示流程），因为 Rust 目标让我们能够强制实现完全可验证的输出（每个组件都以 Dafny 证书形式交付，ensures 绑定门在构造上即通过）。即使在该构造内部，\textbf{11.48\%（MBPP-Rust）和 14.82\%（VeriContest LC 切片）的结构化验证样本仍然未通过隐藏测试}。在 VeriContest 的 LC 切片上，\textbf{VCG 报告的 End2End 率为 7.79\%（535/6870）。}所引用的外部比率为 5.51\%（GPT-5.5）和 1.88\%（单次 Opus 4.7）。这分别给出 2.3 个百分点和 4.14$\times$ 的描述性差异；任务预算、修复和测试框架的差异使得无法声称性能匹配。
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2611.05590 [cs.AI] |
| （或 arXiv:2611.05590v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2611.05590 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Aditya Vempaty [查看电子邮件]
[v1]
2026年11月3日星期二 20:20:57 UTC（164 KB）
来源：arXiv cs.AI · arxiv.org