arXiv Artificial Intelligence· Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, Yuangang Li, Shuvendu Lahiri·· 19 小时前AI 评分26
Spec-Harness：评估和引导 LLM 合成的形式化规范超越可验证性
Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability
AI 导读
研究对比经典与基于提示词的 JML 规范合成后发现，22.7% 通过验证的规范完全没有后置条件，且提示优化无法超越最佳手写规范。为此提出 Spec-Harness 框架，基于 Hoare 三元组符号验证和输入/输出变异，从前后置条件的正确性与完整性四个维度衡量规范的行为充分性。
来源：arXiv Artificial Intelligence · arxiv.org