Spec-Harness：评估LLM形式化规约的行为充分性

Md Rakib Hossain Misu 等作者发布论文，提出 Spec-Harness 框架，通过 Hoare 三元组符号验证和输入/输出变异，从前置与后置条件四个维度衡量 LLM 合成的 JML 规范的行为充分性。研究发现，22.7% 通过验证的规范完全没有后置条件，许多被验证器接受的规范在行为上仍然薄弱。该框架可作为反馈信号，帮助 Codex、Claude Code 及 CodeAct 风格智能体合成行为充分性更高的规范。

AI 根据报道生成 · 2 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。