11月5日发布在 arXiv 上的一篇论文，探讨了大语言模型生成的代码究竟在何种意义上算是“经过验证”。论文将检查分为三个方面：验证器是否接受代码、证明是否与规范绑定，以及该规范是否反映了原始需求。
作者报告称，在一项测试中，HumanEval 上有 99.1% 的代码通过验证器检查，但只有 1.9% 的样本带有与规范所定义谓词或函数绑定的证书。在另一套旨在确保这种绑定关系的 Rust 流程中，经过结构验证的 MBPP-Rust 样本仍有 11.48% 未通过隐藏测试；VeriContest 子集上的这一比例为 14.82%。
为什么重要
对于使用证明检查来评估生成代码的团队而言，这些结果表明，仅凭验证器接受代码，未必能证明代码与需求存在有意义的联系，也无法保证其能通过隐藏测试。
