arXiv cs.AI· Srijith Nair, Aditya Vempaty, Jia Liu, Ashish Jagmohan·· 9 天前AI 评分24
超越类型检查：面向形式化规范生成的整体评估
Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation
AI 导读
研究提出面向 SpecGen 的整体评估框架，整合 VERINA 与 CLEVER 共 350 个 Lean 任务，覆盖形式有效性、参考相似度与等价性、行为充分性。
正文 · AI 翻译
摘要：在生成可验证代码时，自然语言需求通过 LLM 和智能体工作流映射为机器可检查的代码。该流程的一个关键组成部分是规范生成（SpecGen），它生成一份形式化契约，智能体可据此证明实现的正确性。证明生成可以从定理证明器获得确定性反馈，但 SpecGen 缺乏一种确定性检查来验证生成的规范是否捕捉到了用户意图。因此，一个通过检查的证明可能只是针对一个错误表述了预期行为的规范确立了正确性。我们朝着整体 SpecGen 评估迈出了一步，构建了一个统一数据集，由 $350$ 个现有 Lean 任务汇编而成，其中包括来自 VERINA 的 $189$ 个和来自 CLEVER 的 $161$ 个，并提出了一个涵盖形式有效性、参考相似性与等价性以及行为充分性的框架。我们区分了对必需输入的接受与对有效输出的接受及对无效输出的拒绝，同时明确每个指标的证据范围。在四种 SpecGen 配置中，将广义树编辑距离（GTED）比较——一种参考相似性度量——限制在 $32$ 个可联合测量的 VERINA 任务上，会使 VERINA 配置在平均相似性上的排名从第二变为第四，这表明了测量覆盖范围的重要性。在一项作者设计的对照中，一个规范实现了 $100\%$ 的正测试召回率和负测试拒绝率，同时接受了 $0\%$ 的必需输入。这表明完美的后置条件得分可能掩盖一个不可用的输入契约，从而促使对输入覆盖和输出约束分别给出反馈。
| 评论： | 已被 NeurIPS 2026 可验证编码人工智能研讨会接收（20 页，7 幅图） |
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI） |
| 引用为： | arXiv:2610.10604 [cs.SE] |
| （或使用 arXiv:2610.10604v1 [cs.SE] 引用此版本） | |
| https://doi.org/10.48550/arXiv.2610.10604 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
发件人：Srijith Nair [查看电子邮件]
[v1]
2026 年 10 月 7 日星期三 02:11:30 UTC（306 KB）
来源：arXiv cs.AI · arxiv.org