arXiv cs.AI· Aditya Vempaty, Himaneesh Sompalle, Manan Tayal, Mowafak Allaham, Prasenjit Dey, Ashish Jagmohan, Ravi Kokku·· 2 小时前AI 评分44
LLM 验证式代码生成研究：验证通过也可能是空洞的——三个失败面分析
Verified but Vacuous: Three Failure Surfaces of LLM-Driven Verified Code Generation
AI 导读
一篇 arXiv 论文指出，评估 LLM 生成代码的“验证”指标混杂了三个不同属性：验证器接受（Surface A）、语法层面规范绑定（Surface B）与语义层面规范保真（Surface C）。
正文 · 原文
Abstract:What should ``verified'' mean when evaluating LLM-generated code? Many existing pipelines report a single verification number. We argue this collapses three distinct properties measured in a conditional audit sequence: verifier acceptance (Surface A), \emph{syntactic specification binding (Surface B: does the proof obligation bind to the spec?), and \emph{semantic specification fidelity} (Surface C: does the spec capture the informal requirement?). Two empirical demonstrations show the surfaces separate. \textbf{First ($A \neq B$), via Li@Opus (a same-model reproduction of \citet{li2025dafny}'s Dafny-as-intermediate-representation (IR) pipeline under Claude Opus 4.7) on three Python benchmarks}: it reaches \textbf{99.1\% verifier acceptance} on HumanEval while only \textbf{1.9\%} carry a certificate binding to a spec-defined predicate or function. \textbf{Second ($B \neq C$), via VCG on two Rust benchmarks}: we use VCG (which is our own in-house Dafny-as-intermediate pipeline) on Rust because the Rust target lets us enforce fully-verifiable output (every component ships as a Dafny certificate, ensures-binding gate passing by construction). Even inside that construction, \textbf{11.48\% (MBPP-Rust) and 14.82\% (VeriContest LC slice) of structurally-verified samples still fail hidden tests}. On the LC slice of VeriContest, \textbf{VCG's reported End2End rate is 7.79\% (535/6870).} The cited external rates are 5.51\% (GPT-5.5) and 1.88\% (single-shot Opus 4.7). These give descriptive differences of 2.3 percentage points and 4.14$\times$, respectively; task-budget, repair and harness differences prevent a matched-performance claim.
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2611.05590 [cs.AI] |
| (or arXiv:2611.05590v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2611.05590 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Aditya Vempaty [view email]
[v1]
Tue, 3 Nov 2026 20:20:57 UTC (164 KB)
来源：arXiv cs.AI · arxiv.org