超越类型检查：形式化规范生成的全面评估
原标题：Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation
AI 摘要
该论文针对LLM与智能体工作流中形式化规范生成（SpecGen）缺乏验证用户意图机制的问题，提出统一评估框架。作者整合了VERINA（189个）和CLEVER（161个）共350个Lean任务，构建覆盖形式有效性、参考相似性与等价性、行为充分性的数据集与指标。实验发现，将广义树编辑距离（GTED）比较限制在32个可联合测量的VERINA任务后，某配置的平均相似度排名从第二降至第四，说明测量覆盖范围影响结论；同时一个规范可在后置条件测试上表现完美却接受不可用的输入契约，表明需分别反馈输入覆盖与输出约束。
正文节选
Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation Abstract When generating verifiable code, natural language requirements are mapped to machine checked code using LLMs and agentic workflows. A crucial component of this pipeline is specification generation (SpecGen), which produces a formal contract against which an agent can prove implementation correctness. Proof generation can obtain deterministic feedback from a theorem prover, but SpecGen lacks a definitive