如何全面评估形式规范生成而不止于类型检查

研究动机与问题所在

在利用大语言模型和代理工作流把自然语言需求转换为可机器验证的代码时，形式规范（SpecGen）扮演着中介的角色：它为后续的证明过程提供一个可以被定理检查器验证的正式契约。虽然证明步骤能够得到定理证明器的确定性反馈，但目前缺乏一种直接的手段来判断生成的规范是否真的捕捉了用户的原始意图。这样一来，即使证明过程返回“正确”，也可能是针对一个实际上偏离预期行为的规范成立的正确性。因此，需要一种更为全面的评估方式，既要考察规范的形式正确性，又要衡量其在输入输出约束上的行为表现。

数据集的构建方式

作者们从已经公开的 Lean 任务中抽取了总计 350 个样本作为统一评估基准。其中 189 条来自 VERINA 基准集，剩余的 161 条来源于 CLEVER 集合。这样做的目的在于让不同来源的任务在同一套度量下可以进行比较，避免单一数据集的偏倚。在这 350 个任务中，进一步挑选出 32 个在 VERINA 中可以同时度量的子集，用于后续对广义树编辑距离（GTED）的受限比较。这一步骤突显了度量覆盖面对结果排名的影响：当只在这 32 个共同可测的任务上计算 GTED 时，原来在 VERINA 上排名第二的配置会下降到第四位，说明如果度量未能涵盖足够多的任务，容易得到误导性的结论。

评估框架的四个维度

提出的评估框架覆盖了以下几个方面：

1. 形式有效性：检查生成的规范是否符合 Lean 的语法和类型系统，能否被定理检查器接受为合法的正式契约。
2. 参考相似度与等价性：利用 GTED 等树编辑距离度量生成规范与人工标注参考规范之间的结构相似度，进一步探讨两者在语义上是否可互换。
3. 行为适配性：分别测量规范对必需输入的接受程度、对合法输出的接受程度以及对非法输出的拒绝程度。这一步把输入覆盖和输出约束分开来看，避免只看后置条件而忽略前置条件的问题。
4. 综合反馈：将上述三类指标的证据范围作明确区分，便于定位是哪一环节出现偏差。

在实验中，作者对四种不同的 SpecGen 配置进行了对比。除了上述提到的 GTED 受限比较导致排名变化之外，还观察到在某些配置下，尽管后置条件（postcondition）得分可以达到满分，但在输入覆盖方面却表现为零。具体来说，他们构造了一个对照实验：生成的规范能够在正向测试中捕获全部的预期输出（阳性测试召回率 100%），在负向测试中也能够正确地拒绝所有非法输出（阴性测试拒绝率 100%），然而它对必需输入的接受率却为 0%。这一现象说明，仅凭后置条件的优秀表现无法保证规范在实际使用中的可用性，必须同时关注输入端的约束质量。

关键发现与启示

• 度量覆盖不可忽视：当只使用部分任务来计算相似度时，配置的相对优势会发生变化。完整的 350 任务基准提供了更稳定的评估视角。
• 输入与输出需要分别反馈：传统的后置条件验证只能保证输出端的正确性，却可能遗漏对输入范围的限制。因此，评估体系应当提供独立的输入覆盖指标，以防止产生看似正确却不可用的规范。
• 形式正确性只是基础：即使一个规范能够通过定理检查器的语法验证，也不代表它与用户意图一致；行为适配性才是衡量其实用价值的关键。
• 统一基准促进可比性：把 VERINA 和 CLEVER 的任务合并，并在同一框架下测量形式有效性、相似度和行为适配性，有助于不同研究团队之间的结果对照和方法改进。

结语

这项工作提出了一套从形式有效性、参考相似度到行为适配性的多维评估途径，并通过具体的实验表明，仅依赖类型检查或后置条件得分是不足以判断规范质量的。未来在设计 SpecGen 系统时，除了追求证明端的确定性反馈之外，还应当在这四个维度上进行平衡优化，以确保生成的正式契约不仅能通过验证，而且真正能够指导代理在实际任务中产生正确的行为。希望这些思路能够为后续的形式方法与机器学习结合研究提供参考。