来源笔记
VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation
摘要
VeriScale 通过扩展和压缩基于 Lean 的可验证代码生成测试集，让薄弱的规格和实现更难蒙混过关。它在 Verina 的基础上生成了 VerinaPlus 和 VerinaLite，并报告称，在更强的测试下，顶级 LLM 的得分大幅下降。
问题
- 现有的可验证代码生成基准中的正向和负向测试太少，LLM 可能在没有抓住预期行为的情况下也能通过。
- SpecGen 需要意外输入和意外输出，来检查生成的前置条件和后置条件是否会拒绝无效行为。
- 这个问题很重要，因为被抬高的基准分数会让生成的规格和代码看起来比实际更安全。
方法
- VeriScale 先用 LLM 生成种子输入，再用类型感知的变异，为每个任务生成大量候选输入。
- 它用 Lean 对照真实前置条件进行检查，把候选项分成预期输入和非预期输入。
- 对于预期输入，它运行参考实现来生成预期输出。
- 为了生成更难的非预期输出，它让更强的模型编写对抗性实现，输出会被生成的后置条件接受，但结果是错误的。
- 它用保留边界的选择方法压缩扩展后的测试集中的非预期输入，再用贪心集合覆盖步骤保留那些能击败许多对抗性实现的预期用例。
结果
- VerinaPlus 在整体上把 Verina 扩大了 83 倍以上；VerinaLite 是一个轻量的 14 倍版本。
- 预期输入输出用例的平均数量从 Verina 的 5.89 增加到 VerinaPlus 的 370.07，提升 62.83 倍；VerinaLite 保留 52.34，提升 8.89 倍。
- 非预期输出的平均数量从 12.69 增加到 VerinaPlus 的 1114.01，提升 87.79 倍；VerinaLite 保留 202.35，提升 15.95 倍。
- 非预期输入的平均数量从 0.65 增加到 VerinaPlus 的 119.00，提升 183.08 倍；VerinaLite 保留 15.80，提升 24.31 倍。
- 对于 GPT-5.5，SpecGen 在 Verina 上是 68.78%，在 VerinaPlus 上降到 44.44%；CodeGen 从 96.83% 降到 86.24%。
- 论文用 Lean v4.24.0 评估了 8 个 LLM，报告增强后的基准达到 100% 代码覆盖率，并称 VerinaLite 以更低的评估成本保留了与 VerinaPlus 相近的区分能力。