Spec-Harness：测量和改进 LLM 综合正式规范的行为充分性

正式规范在确保软件可靠性方面发挥着核心作用，但自动合成高质量规范仍然很困难，并且通常需要领域专业知识。最近的工作应用 大语言模型 生成 Java 建模语言 (JML) 规范，报告验证器通过率很高。但通过验证器仅确认实现与规范一致，而不表明规范有意义。诸如 Ensure true 之类的简单后置条件可以满足任何验证者的要求，同时对代码只字未提。那么，验证者接受的规范实际上捕获了多少行为？在这项工作中，我们首先在统一设置下比较经典和基于提示的 JML 合成方法，发现通过验证反馈进行提示优化可以提高通过率，但达到了明显的上限。然后，我们介绍 Spec-Harness，这是一个框架，使用基于霍尔三重的符号验证和输入/输出突变，沿着前置条件和后置条件的正确性和完整性四个维度来衡量规范的行为充分性。 Spec-Harness 揭示了许多验证者接受的规范（包括优化的规范）在行为上都很薄弱，以验证者看不到的方式对输入和输出进行过度或不足的约束。最后，我们展示了 Spec-Harness 作为反馈信号，帮助 编码智能体 合成具有更高行为充分性的规范，包括 Codex CLI 和 Claude Code 等通用代理，以及我们为本研究构建的 JML 专用代理 VeriAct。