Spec-Harness：检验LLM合成规约的行为充分性
热点事件持续更新
Spec-Harness：检验LLM合成规约的行为充分性
1 篇报道1 个报道来源8 小时前更新
先了解这件事
AI 综述
研究者提出 Spec-Harness 框架，用于评估大语言模型合成的形式化规约是否在行为上充分，而不仅仅是通过验证器。该框架用 Hoare 三元组符号验证和输入/输出变异，从前置与后置条件的正确性和完整性四个维度打分。 研究发现，通过验证的 JML 规范中有 22.7% 完全没有后置条件，许多被验证器接受的规范存在过约束或欠约束。作者称该框架可作为反馈信号，帮助 Codex、Claude Code 及 CodeAct 风格智能体合成行为充分性更高的规范。
AI 根据报道生成 · 1 小时前更新
最新进展10月15日 12:00
Spec-Harness：评估和引导 LLM 合成的形式化规范超越可验证性报道时间线
沿着报道，了解事件的不同侧面。
10月15日
- arXiv cs.AISpec-Harness：评估和引导 LLM 合成的形式化规范超越可验证性
Spec-Harness 框架通过 Hoare 三元组符号验证和输入/输出变异，从前置与后置条件的正确性和完整性四个维度衡量规范的行为充分性。研究发现，22.7% 通过验证的 JML 规范完全没有后置条件，许多被验证器接受的规范在行为上存在过约束或欠约束。该框架可作为反馈信号，帮助 Codex、Claude Code 及 CodeAct 风格智能体合成行为充分性更高的规范。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。