arXiv cs.AI· Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, Yuangang Li, Shuvendu Lahiri·· 3 天前AI 评分22
Spec-Harness：评估与引导 LLM 合成的形式化规范超越可验证性
Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability
AI 导读
研究对比经典与基于提示词的 JML 规范合成，发现 22.7% 通过验证的规范完全没有后置条件，且提示词优化无法超越最佳手写规范。为此提出 Spec-Harness 框架，从前置与后置条件的正确性和完整性四个维度衡量规范的行为充分性，结合 Hoare 三元组符号验证与输入/输出变异。
正文 · AI 翻译
摘要：形式化规范在确保软件可靠性方面起着核心作用，但自动合成高质量规范仍然困难，且往往需要领域专业知识。近期工作已将大语言模型应用于生成 Java 建模语言（JML）规范，并报告了较高的验证器通过率。但通过验证器只能确认实现与规范一致，并不能说明规范本身有意义：诸如 ensures true 这样的平凡后置条件能满足任何验证器，却对代码没有任何说明。基于变异的完备性评分更进一步，但它只返回一个数字，无法告诉生成器应该修复哪个子句。在本工作中，我们首先在统一设置下比较经典 JML 合成与基于提示的 JML 合成，发现 22.7% 通过验证的规范完全没有后置条件，并且通过验证反馈进行提示优化可以修复弱提示，但无法超越最佳人工编写的提示。随后我们提出 Spec-Harness，一个通过在系统构建的测试套件上进行基于 Hoare 三元组的符号验证和输入/输出变异，从前置条件和后置条件的正确性与完备性四个维度衡量规范行为充分性的框架。Spec-Harness 揭示，许多被验证器接受的规范在行为上很弱，以验证器无法察觉的方式对输入和输出过度约束或约束不足。最后，我们表明 Spec-Harness 可作为一种反馈信号，帮助编码智能体在留出测试上合成具有更高行为充分性的规范。这适用于通用智能体 Codex 和 Claude Code，也适用于我们构建的、将验证器和 Spec-Harness 用作反馈的 CodeAct 风格 JML 合成智能体。
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI） |
| 引用为： | arXiv:2604.00280 [cs.SE] |
| （或使用 arXiv:2604.00280v3 [cs.SE] 查看此版本） | |
| https://doi.org/10.48550/arXiv.2604.00280 由 DataCite 颁发的 arXiv DOI |
提交历史
发件人：Md Rakib Hossain Misu [查看电子邮件]
[v1]
2026年3月31日星期二 22:12:15 UTC（260 KB）
[v2]
2026年9月8日星期二 22:53:51 UTC（768 KB）
[v3]
2026年10月9日星期五 23:37:19 UTC（376 KB）
来源：arXiv cs.AI · arxiv.org