超越类型检查：对正式规范生成的整体评估

生成可验证代码时，自然语言要求会使用 LLM 和 agentic 工作流程映射到机器检查的代码。该管道的一个关键组成部分是规范生成 (SpecGen)，它生成正式合同，代理可以根据该合同证明实施的正确性。证明生成可以从定理证明者获得确定性反馈，但 SpecGen 缺乏对生成的规范是否捕获用户意图的明确检查。因此，经过检查的证明可以针对歪曲预期行为的规范确定正确性。我们向整体 SpecGen 评估迈出了一步，使用由 350 美元的现有精益任务（包括来自 VERINA 的 189 美元和来自 CLEVER 的 161 美元）组装而成的统一数据集，以及涵盖形式有效性、参考相似性和等效性以及行为充分性的框架。我们区分接受所需输入、接受有效输出和拒绝无效输出，同时明确每个指标的证据范围。在四种 SpecGen 配置中，限制 广义树编辑距离 (GTED) 比较（一种参考相似性度量）与 32 美元联合可测量的 VERINA 任务将 VERINA 配置的平均相似度位置从第二位更改为第四位，显示了测量覆盖范围的重要性。在编写的控件中，规范在接受 $0\%$ 所需输入的同时实现了 $100\%$ 正测试召回和负测试拒绝。这表明完美的后置条件分数可能会错过不可用的输入契约，从而激发对输入覆盖和输出约束的单独反馈。