LLM代码生成存在三种验证失效面

该论文指出评估 LLM 生成代码时，单一的验证通过率指标掩盖了三个独立的失效表面：验证器接受度、语法规范绑定以及语义规范保真度。作者通过实证证明这三个层面并不等价，高验证率可能仅意味着通过了形式化检查，而非解决了实际需求。 在第一个实验中，使用 Claude Opus 4.7 复现 Li@Opus 的 Dafny 管道，在 HumanEval 基准上达到了 99.1% 的验证器接受度，但仅有 1.9% 的代码证书真正绑定到规范定义的谓词或函数。第二个实验针对 Rust 基准，即使构建了强制所有组件都附带 Dafny 证书的 VCG 管道，仍有 11.48% 的 MBPP-Rust 样本和 14.82% 的 VeriContest LC 切片样本在隐藏测试中失败；VCG 报告的端到端成功率为 7.79%，而外部引用的 GPT-5.5 为 5.51%，单次 Shot 的 Opus 4.7 仅为 1.88%。 事实层面显示当前验证流程存在严重的“虚假安全”现象，推断表明单纯追求验证通过率会误导工程实践，猜测认为未来需要建立包含语义保真度的多维评估体系。这些差异受任务预算、修复机制和测试套件的差异影响，无法直接进行性能匹配比较。