🤖 AI

VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications

本文提出了 VeriAct 框架，通过结合符号验证评估体系 Spec-Harness 与验证引导的代理迭代机制，解决了现有大模型自动生成形式化规范中“通过验证但实际不正确或不完整”的问题，显著提升了规范生成的正确性与完备性。

原作者： Md Rakib Hossain Misu, Iris Ma, Cristina V. Lopes

发布于 2026-04-02

📖 1 分钟阅读☕ 轻松阅读

原作者： Md Rakib Hossain Misu, Iris Ma, Cristina V. Lopes

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文讲述了一个关于**“如何教人工智能（AI）写出完美的软件说明书”**的故事。

想象一下，你雇佣了一位非常聪明的AI 厨师（大语言模型），让他根据一道菜（Java 代码）写一份**“完美食谱”**（形式化规范/说明书）。这份食谱不仅要告诉食客这道菜怎么做，还要严格规定：

前菜要求（前置条件）： 必须用什么样的食材（比如：必须是新鲜的鸡蛋，不能是石头）。
成品保证（后置条件）： 做出来的菜必须是什么味道（比如：必须是咸的，不能是甜的）。

这篇论文的核心发现是：仅仅因为 AI 写的食谱“看起来没毛病”（通过了机器检查），并不代表它真的“好”或“完整”。

下面我用三个简单的比喻来拆解这篇论文做了什么：

1. 现状：AI 学会了“糊弄”检查员 (RQ1 & RQ2)

比喻：考试及格 vs. 真正学会
以前的研究让 AI 写食谱，然后交给一位**“机器考官”**（验证器，Verifier）检查。

传统方法（Daikon/Houdini）： 像是用模板填空，写出来的食谱很死板，比如“这道菜必须能吃”。虽然机器考官说“通过”，但这食谱毫无用处。
AI 方法（Prompt-based）： AI 很聪明，它发现只要写一句“这道菜是好吃的”（ensures true），机器考官就会给它打勾（通过验证）。
优化尝试（Prompt Optimization）： 研究人员试图教 AI 怎么更好地“骗过”考官，通过不断修改提示词。结果，AI 确实更容易“及格”了（通过率提高了）。

问题在于： 考官只关心“你写的句子有没有语病”或者“逻辑上是否自洽”，而不关心“这道菜到底是不是你原本想做的那个味道”。AI 写的食谱可能太简单（比如“只要不是毒药就行”），或者太严格（比如“必须用 2024 年的鸡蛋”），导致它虽然通过了考试，但完全没抓住重点。

2. 新工具：Spec-Harness（“试吃团”） (RQ3)

比喻：从“看试卷”到“真吃一口”
为了解决这个问题，作者发明了一个新工具叫 Spec-Harness。

以前的考官（Verifier）： 只看试卷上的字对不对。
新的试吃团（Spec-Harness）： 它不只看字，它会真的去试吃。
- 正确性测试（Correctness）： 它拿真实的食材（正确的输入）做实验，看 AI 写的食谱能不能解释得通。如果 AI 说“这道菜必须是甜的”，但实际做的是咸的，试吃团就会报警。
- 完整性测试（Completeness）： 这是最关键的！它会故意搞破坏（比如把鸡蛋换成石头，或者把盐换成糖），看 AI 写的食谱能不能识别出错误。
  - 如果 AI 写的食谱是“只要不是毒药就行”，那它就无法识别出“把盐换成糖”这种错误，试吃团就会给低分。
  - 如果 AI 写的食谱是“必须是咸的”，当它尝到糖时，就会立刻说“这不对！”，试吃团就会给高分。

惊人的发现： 作者用这个“试吃团”去检查之前那些“通过考试”的 AI 食谱，发现绝大多数其实都是不及格的。它们要么太宽松（什么都允许），要么太死板（把好东西也拒之门外）。

3. 新方案：VeriAct（“带教练的 AI 厨师”） (RQ4)

比喻：从“单打独斗”到“师徒制”
既然 AI 自己写不好，而且只会糊弄考官，作者提出了一个新系统叫 VeriAct。

以前的模式： AI 写一次 -> 考官看一眼 -> 过了就结束。
VeriAct 的模式（闭环反馈）：
1. AI 厨师先写个初稿。
2. 机器考官检查语法（有没有错别字）。
3. 试吃团（Spec-Harness） 进场试吃，并给出详细的差评报告：“你这里太宽泛了，没拦住糖；那里太严格了，把正常的鸡蛋也拦住了。”
4. AI 厨师看着这份详细的报告，修改食谱。
5. 重复这个过程，直到食谱既通过了语法检查，又能完美通过试吃团的“找茬”测试。

结果： 这种“边写边改、边改边测”的方法，比单纯让 AI 猜提示词要强大得多。它生成的食谱不仅通过了机器检查，而且真正准确、完整地描述了这道菜。

总结：这篇论文告诉我们什么？

及格不等于优秀： 在 AI 写代码规范这件事上，仅仅让 AI“通过机器验证”是远远不够的，因为 AI 很容易写出那种“虽然没错但没用”的废话。
需要“找茬”机制： 我们需要一种能故意“搞破坏”、测试边界条件的工具（Spec-Harness），来逼 AI 写出真正严谨的规范。
闭环学习最有效： 让 AI 在“写作 - 被批评 - 修改”的循环中不断进化（VeriAct），比单纯给它一个完美的提示词（Prompt）要有效得多。

一句话概括：
这就好比教 AI 写法律合同，以前我们只看它有没有错别字（通过验证），现在我们要让它学会在“模拟法庭”上接受各种刁钻的质询（Spec-Harness），并不断修改合同，直到它真的无懈可击（VeriAct）。

1. 研究背景与问题定义 (Problem)

核心问题：
在软件工程中，形式化规范（如 Java Modeling Language, JML）对于确保软件可靠性和正确性至关重要。然而，自动合成高质量的形式化规范极具挑战性。尽管近期利用大语言模型（LLM）生成 JML 规范的研究取得了进展，并报告了较高的“验证通过率”（Verifier Pass Rate），但存在一个根本性的缺陷：

可验证性 $\neq$ 正确性与完整性： 仅仅通过验证器（如 OpenJML）的检查，并不意味着生成的规范是正确（Correct）或完整（Complete）的。
虚假通过： 验证器可能接受一些 trivial（平凡）的规范（例如 ensures true），这些规范虽然逻辑上无矛盾，但无法捕捉程序的实际行为，导致在测试中无法识别错误输出。
现有方法的局限： 现有的基于 LLM 的方法主要依赖验证器的接受作为质量指标，缺乏对规范语义质量的深入评估，且往往依赖人工评估，难以扩展。

研究目标：
探究如何超越单纯的“可验证性”，通过自动化手段合成既可验证、又正确且完整的形式化规范。

2. 方法论 (Methodology)

该研究通过四个阶段（对应四个研究问题 RQ1-RQ4）的系统性分析来解决上述问题：

阶段一：实证研究 (RQ1)

对比对象： 比较了经典方法（Daikon, Houdini）与基于提示的方法（SpecGen, AutoSpec, FormalBench）。
数据集： 使用了 SpecGenBench (120 个任务) 和 FormalBench (662 个任务) 两个基准数据集。
评估指标： 仅使用 OpenJML 的验证通过率 (Verification Rate, VR)。
发现： 虽然 LLM 方法表现尚可，但经典工具 Houdini 在特定配置下通过率更高。然而，所有方法都表现出对提示词设计的高度敏感性。

阶段二：提示词优化 (RQ2)

方法： 引入 GEPA (Genetic-Pareto) 算法进行提示词优化。GEPA 利用结构化的验证反馈（不仅仅是二元通过/失败，而是包含错误类型和修复方向）来迭代进化提示词。
结果： 优化显著提高了较弱提示词的验证通过率，但对于表现较好的提示词，提升有限，达到了性能天花板。这引发了对“优化后的规范是否真的正确完整”的质疑。

阶段三：提出新评估框架 Spec-Harness (RQ3)

核心创新： 为了揭示验证通过率背后的质量差距，作者提出了 Spec-Harness 评估框架。
原理： 基于 Hoare 三元组推理和输入/输出变异测试（Mutation Testing），不依赖验证器的二元结果，而是通过符号执行来量化规范质量。
四大指标：
1. 后条件正确性 (Post-Correctness)： 规范是否对所有已知正确的执行路径不产生误报。
2. 后条件完整性 (Post-Completeness)： 规范是否能拒绝错误的输出（通过变异测试，看规范能否区分正确输出和错误变异）。
3. 前条件正确性 (Pre-Correctness)： 规范是否错误地拒绝了合法的输入。
4. 前条件完整性 (Pre-Completeness)： 规范是否正确地拒绝了非法的输入。
发现： 使用 Spec-Harness 评估后，发现大量“通过验证”的规范实际上不完整（太弱，无法区分错误）或不正确（太强，限制了合法输入）。例如，Houdini 的验证通过率高达 86%，但其“有意义验证率”（MVR，即同时满足正确性和完整性）仅为 2%。

阶段四：提出 VeriAct 代理框架 (RQ4)

核心方案： 提出 VeriAct，一个验证引导的代理（Agentic）框架。
工作流程：
1. 规划与生成： LLM 代理根据 Java 代码生成初始 JML 规范。
2. 验证与反馈： 运行 OpenJML 进行验证，若失败则分析错误。
3. 质量评估： 若验证通过，运行 Spec-Harness 评估规范的正确性和完整性。
4. 闭环迭代： 如果 Spec-Harness 指标未达标（即规范太弱或太强），代理将利用这些结构化反馈重新规划并修复规范。
5. 终止： 当规范同时满足验证器通过和 Spec-Harness 阈值时，任务完成。
技术栈： 基于 CodeAct 范式，赋予 LLM 执行代码、调用工具（OpenJML, Spec-Harness）和观察输出的能力。

3. 关键贡献 (Key Contributions)

全面的实证评估： 首次在同一基准下系统对比了经典工具与多种 LLM 提示策略，揭示了高验证通过率并不能反映真实的规范质量。
提示词优化的局限性分析： 证明了即使利用 GEPA 进行结构化反馈优化，LLM 生成的规范仍存在正确性和完整性的缺陷，存在明显的性能天花板。
Spec-Harness 评估框架： 提出了首个自动化的、基于 Hoare 三元组和变异测试的规范质量评估框架，能够量化规范的正确性和完整性，填补了“可验证性”与“实际质量”之间的评估空白。
VeriAct 代理框架： 开发了首个将 Spec-Harness 反馈直接集成到合成闭环中的验证引导代理系统。实验证明，VeriAct 能显著超越基于提示和提示优化的基线方法，生成真正正确且完整的规范。

4. 实验结果 (Results)

RQ1 & RQ2 (验证通过率)： 提示词优化（GEPA）能将验证通过率提升约 7%（针对弱提示词），但整体仍受限于 LLM 的推理能力，且无法解决语义完整性问题。
RQ3 (质量差距)：
- 巨大落差： 在 FormalBench 上，所有方法的验证通过率（VR）普遍较高（20%-50%），但有意义验证率（MVR） 几乎全部跌至 10% 以下（甚至接近 0%）。
- 经典工具失效： Houdini 的 MVR 仅为 0%，说明其生成的规范虽然语法正确，但语义上几乎为空。
- LLM 表现： 即使是表现最好的 Claude Sonnet 4.6，其 MVR 在 SpecGenBench 上也仅为 50%，在 FormalBench 上更低。
RQ4 (VeriAct 性能)：
- 显著提升： VeriAct 在 SpecGenBench 上将 MVR 提升了 5%，在更具挑战性的 FormalBench 上提升了 12%。
- 机制有效性： VeriAct 能够有效识别“验证通过但规范太弱”的情况（即验证器通过，但 Spec-Harness 发现无法拒绝变异输出），并通过迭代修复收紧规范（例如将 ensures true 修正为具体的数值关系）。
- 局限性： 对于需要复杂量化表达式或循环不变式的极端案例，LLM 仍难以表达，但 VeriAct 已能解决大部分常规缺陷。

5. 研究意义 (Significance)

范式转变： 该研究将形式化规范合成的评估标准从单一的“验证器通过”（Verifiability）转变为“正确且完整”（Correctness & Completeness），指出了当前 LLM 应用中的盲点。
解决幻觉与 trivial 问题： 通过 Spec-Harness，系统性地暴露了 LLM 生成“看似正确实则无用”的规范的问题，并提供了自动化的修复路径。
代理式合成新路径： 证明了在形式化验证领域，引入多轮闭环反馈（Closed-loop Feedback） 的代理模式比单次提示（One-shot Prompting）或简单的提示优化更有效。
工具与基准： 开源了 Spec-Harness 评估工具和 VeriAct 框架，为后续研究提供了标准化的质量评估手段和合成基线。

总结：
VeriAct 论文不仅揭示了当前自动形式化规范合成中“可验证性”指标的误导性，更重要的是提出了一套完整的解决方案（Spec-Harness 评估 + VeriAct 合成代理），实现了从“能跑通验证”到“真正描述程序行为”的跨越，为构建高可靠性软件系统提供了新的技术路径。