论文揭示大语言模型形式化验证代码生成的三类失效维度

研究表明大语言模型形式化验证代码生成存在验证器接受、语法规约绑定与语义规约保真度三层相互脱节的失效维度，单一验证通过率无法证明代码真正正确。基于 Claude Opus 4.7 的实验显示，其在 HumanEval 上的验证器接受率达 99.1%，但仅 1.9% 绑定了规约定义的谓词；在 Rust 基准测试中，通过结构验证的代码仍有 11.48% 至 14.82% 未能通过隐藏测试。