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 三元组符号验证与输入/输出变异。
正文 · 原文
Abstract:Formal specifications play a central role in ensuring software reliability, yet automatically synthesizing high-quality specifications remains difficult and often requires domain expertise. Recent work has applied large language models to generate specifications in the Java Modeling Language (JML), reporting high verifier pass rates. But passing a verifier only confirms that an implementation is consistent with a specification, not that the specification is meaningful: a trivial postcondition such as ensures true satisfies any verifier while saying nothing about the code. Mutation-based completeness scores go further, but they return a single number and cannot tell a generator which clause to fix. In this work, we first compare classical and prompt-based JML synthesis under a unified setup, and find that 22.7% of the verified specifications have no postcondition at all, and that prompt optimization through verification feedback repairs weak prompts but does not go beyond the best hand-written one. We then introduce Spec-Harness, a framework that measures the behavioral adequacy of a specification along four dimensions of precondition and postcondition correctness and completeness, using Hoare-triple based symbolic verification and input/output mutation on systematically built test suites. Spec-Harness reveals that many verifier-accepted specifications are behaviorally weak, over- or under-constraining inputs and outputs in ways the verifier cannot see. Finally, we show that Spec-Harness works as a feedback signal that helps coding agents synthesize specifications with higher behavioral adequacy on held-out tests. This holds for the general-purpose agents Codex and Claude Code and for a CodeAct-style JML synthesis agent that we built to use the verifier and Spec-Harness as feedback.
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2604.00280 [cs.SE] |
| (or arXiv:2604.00280v3 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2604.00280 arXiv-issued DOI via DataCite |
Submission history
From: Md Rakib Hossain Misu [view email]
[v1]
Tue, 31 Mar 2026 22:12:15 UTC (260 KB)
[v2]
Tue, 8 Sep 2026 22:53:51 UTC (768 KB)
[v3]
Fri, 9 Oct 2026 23:37:19 UTC (376 KB)
来源：arXiv cs.AI · arxiv.org