Verus-SpecGym: 一个用于评估规范自动形式化的智能体环境

TL;DR 提出 Verus-SpecBench 与 Verus-SpecGym，评估 LLM 将非正式问题转化为形式规范的能力；发现前沿模型虽达 77.8% 准确率，但仍易漏约束、误判输出，且 LLM 评判漏检 26% 错误。

问题

问题背景

随着 AI coding agents（如 Copilot、Devin）逐步融入日常软件开发，生成代码的正确性保障从“人工审查”转向“形式验证”已成为趋势。形式验证要求代码附带机器可检查的形式规范（formal spec）及证明，确保实现与规范一致。然而，规范本身是否准确反映非形式化的用户意图，正成为新的瓶颈。

现有方法局限

传统规范编写完全依赖专家手工完成，成本高、迭代慢，无法跟上 AI 生成代码的节奏。近年来出现的 specification autoformalization 尝试让 LLM 自动将自然语言或半形式化问题翻译为形式规范，但评估手段严重滞后：

• 人工标注参考规范：昂贵、扩展性差，且对复杂问题难以穷举所有边界情况。
• LLM-as-a-judge 评估：容易漏掉细微的错误，例如遗漏输入假设、允许错误输出却仍通过验证。
• 测试不充分：现有 benchmark 多依赖静态符号检查，无法动态执行规范，导致无法捕捉运行时才暴露的“忠实性”偏差。

为什么这个问题难/重要

规范自动形式化要求模型同时理解问题的显式约束与隐性假设，并将其转化为严格的形式逻辑。一个微小的表达偏差（如漏掉“数组非空”前提）就会导致“证明上正确，实际上错误”的代码进入生产环境。在金融、自动驾驶、基础设施软件等安全攸关领域，这种“规范漂移”可能引发严重后果。业界核心挑战在于：如何用可扩展的方式，可信地判定 LLM 生成的规范是否真正忠于人类意图。

行业类比

这一问题与自动驾驶系统的 safety specification 生成高度相似：如果行为规范漏写了“行人闯入车道时必须减速”，那么即使控制算法被形式验证为完美实现该规范，车辆依然不安全。规范自动形式化须确保“规范即意图”。

核心洞察

• 规范自动形式化的可靠评估必须结合可执行规范与对抗性测试用例，仅靠符号验证或 LLM-as-a-judge 会遗漏 26% 以上的意图偏离失败。与以往依赖专家参考规范或 LLM 判断的工作不同，本研究通过 exec_spec 将规范转换为可运行 Rust 代码，并直接利用 Codeforces 官方测试和竞争性 hack 案例，揭露了符号检查通过但实际与意图不符的错误规范。这种基于执行和对抗样本的评估机制更贴近真实部署场景，为构建可信形式验证代理提供了缺失的验证闭环。
• 前沿模型能在 77.8% 的任务上生成合法规范，但即使在它们已可正确生成代码的问题上，规范生成仍频繁失败（如遗漏输入假设或接受错误输出），表明代码生成能力与约束形式化能力之间存在显著断层。现有工作多孤立评估代码或证明生成，而本研究首次在相同问题上系统对比代码与规范的生成难度，揭示了模型在非形式化需求转形式化规范时的深层推理瓶颈，对依赖代理自动生成安全关键代码的工程实践具有警示意义。

方法

从非形式化问题到可执行形式化规约的 Agent 流程

输入：Codeforces 竞赛平台的非形式化编程问题描述，包含自然语言陈述、输入/输出样例和约束条件。这些任务原本用于评估算法实现，现被重新定义为形式化规约写作任务。

关键模块：

1. Agent 交互环境 (Verus-SpecGym)
   提供与 Verus 验证器（针对 Rust 的 deductive verifier）、bash 和文件系统的交互。Agent（LLM）在循环中生成形式化规约代码（Verus 要求的 Rust 子集），每次调用 Verus 检查语法错误、类型错误和证明义务。反馈（如验证失败的具体位置）被用于下一轮修改，直至规约通过验证或达到步数上限。

2. 可执行规约评估机制 (exec_spec)
   传统的评估依赖专家编写的参考规约或 LLM-as-a-judge，成本高且容易漏掉细微错误。本工作采用双重测试驱动评估：

   • 官方测试用例：通过 exec_spec 将形式化规约自动翻译为可执行的 Rust 代码，直接在 Codeforces 提供的标准测试集上运行。
   • 对抗性测试用例：从 Codeforces “hacks” 中提取的边界用例，由参赛者专门设计用于攻破错误解法。这些用例能有效暴露规约中遗漏的输入假设、错误接受的输出、或错误拒绝的有效解。 规约必须同时通过两类测试才能被判定为正确。

3. 迭代修正与反馈闭环
   Agent 根据测试失败信息（例如某个用例被错误拒绝或接受）修改规约，重新进入验证-测试循环，模拟真实开发中的“规约-测试-修正”流程。

输出：通过 Verus 验证且通过全部测试用例的形式化规约，以及完整的交互日志。任务成功率是最终指标，前沿模型（如 Gemini 3.1 Pro）可达 77.8%，而开源模型仅 21.5–25.5%。

与同类差异：现有工作多依赖 LLM 直接评分或静态参考规约比对，Verus-SpecGym 首次将可执行规范与对抗性测试结合，用真实执行结果客观衡量规约的忠实度，显著降低了误判率（LLM-as-a-judge 漏报 26% 的错误）。

实验

实验设计

本工作构建 Verus-SpecBench，一个包含 581 个规范写作任务的基准，任务源自 Codeforces 编程竞赛问题，目标验证器为 Verus（Rust 形式验证工具）。同时设计 Verus-SpecGym 智能体环境，使 LLM 代理能直接与 Verus、bash 及文件系统交互，迭代生成形式规范。评估核心挑战在于缺少高质量参考规范——专家编写昂贵，而 LLM 评判易遗漏微妙错误。为此，团队扩展 Verus 的 exec_spec 机制：将生成的规范编译为可执行 Rust 代码，并采用两类测试套件进行验证：(a) 官方 Codeforces 测试用例；(b) 从 Codeforces “hacks” 提取的对抗性用例（由参赛者构造的边缘情况，用于攻破错误解法）。这一设计同时保证了评估的可扩展性与严格性。

关键发现

• 顶尖模型已接近可用门槛：Gemini 3.1 Pro 在 581 项任务上解决率达到 77.8%，表明规范自动形式化对于前沿智能体已非遥不可及。
• 能力断层显著：其他前沿模型解决率仅为 51.1–57.8%，而开源模型（如 DeepSeek、Qwen 等）仅为 21.5–25.5%，暴露出封闭源与开源方案在严谨形式推理上的巨大差距。
• 脆弱性普遍存在：即使模型已能生成正确代码的问题，其生成的规范仍易遗漏必要的输入假设、接受错误输出或拒绝合法解。典型失败模式包括忽略数据类型约束、边界条件等。
• 执行式评估不可替代：流行的 LLM-as-a-judge 范式漏掉了 26% 的真实规范错误，而 exec_spec 与对抗性测试的组合能可靠捕获这些微妙缺陷，证明白盒执行验证的必要性。

基线对比解读

相较于依赖人类专家撰写黄金规范或纯语言模型评判的传统方法，Verus-SpecGym 的创新在于将评估完全自动化且更为严格。 exec_spec 将规范转化为可执行代码，结合对抗性样本，使评估不仅覆盖常规流程，还能探测模型在极端输入下的表现。 Gemini 3.1 Pro 虽以 77.8% 领先，但考虑到问题本身来自其可能已见过的 Codeforces 竞赛，该数字离完全可信赖仍有差距。尤其在一些代码生成易解的问题上，规范生成却意外失败，凸显出当前智能体在「理解意图」与「严谨形式化」之间的鸿沟。这一结果提示，单纯扩大模型规模或依赖更强大的基础模型并非银弹，需引入结构化推理、迭代修正及更丰富的外部验证信号才能实质性推进规范自动形式化走向实用。

行业影响

落地场景

形式化规范自动生成可直接融入安全关键软件(金融交易系统、自动驾驶控制、医疗设备固件、区块链智能合约)的开发流程。例如，智能合约审计平台可将 Solidity 或 Rust 合约的语义自动转换为形式化规范，再由验证器检查是否存在重入、溢出等漏洞；车企可将控制算法的非正式需求文档转化为机器可 check 的规范，保证车辆行为符合安全约束。在 AI 代码生成工具(如 Copilot、CodeWhisperer)中，规范自动生成能提供“带证明的代码”，辅助开发者编写更可靠的实现。

商业价值

人工编写形式化规范成本极高，需要同时掌握领域逻辑与证明系统(如 Coq、Verus)。自动化可降低形式化验证的准入门槛与人力成本，使中小型团队也能在关键模块引入机器证明。以金融领域为例，错误交易逻辑可能造成数百万美元损失，自动形式化+验证可将这类风险前置到开发阶段，减少事后审计与赔偿。对于提供形式化验证服务的公司，该技术能提升吞吐，将工程师从重复性规范写作中解放，变计费模式为工具订阅，扩大市场规模。

与现有产品 / 工作流的接口

• CI/CD 集成：将规范自动生成作为 pre-commit 或 pull request 检查步骤，对提交的代码片段生成规范并验证，不通过则阻断合并。
• 编程助手增强：在 IDE 中，当用户编写关键函数时，后台调起智能体生成规范与证明，若成功则高亮显示“已验证”，否则给出反例。可基于 Language Server Protocol 实现，与现有工具链(如 Rust Analyzer)兼容。
• 审计平台插件：安全审计公司可将该环境嵌入内部审计流，对众包或合约代码批量自动形式化，筛出高风险点供专家复核。

具体用例

1. 去中心化金融协议开发：项目方使用内置 Verus-SpecGym 的 CI 管道，对 Uniswap V4 hook 合约的 Rust 实现自动生成并验证池平衡不变式，避免流动性抽取漏洞。
2. 自动驾驶规划模块验证：车企把路径规划算法的非正式需求(如“车辆不得越过实线”)输入智能体，生成形式化规范，配合仿真测试和形式化证明，确保模型在所有边缘场景下满足安全准则，加速功能安全认证(如 ISO 26262)。

局限

• **基准的领域与评估局限**：Verus-SpecBench 全部来自 Codeforces 算法竞赛题，规模较小且风格单一，难以代表实际软件工程中的规格自动形式化需求。评估仅依赖官方测试用例和对抗“hacks”，仍可能遗漏语义偏差；`exec_spec` 执行检查只能验证输入输出行为，无法保证规格完整捕获了用户意图。研究仅针对 Verus/Rust，对其他验证器或编程语言的泛化性未验证。
• **模型能力的根本脆弱性**：前沿模型在代码生成成功的问题上，规格生成仍频繁出错，常见遗漏输入约束、接受错误输出或拒绝合法输出等失败模式。LLM-as-a-judge 评估漏检 26% 的失败案例，表明纯语言模型尚不能可靠判断规格忠实度，制约了自动化迭代与大规模应用的可行性。
• **实验设置的简化**：Verus-SpecGym 环境为 agent 提供了交互能力，但实验主要测试单轮生成，未充分探索多轮反馈、增量式规格开发等更符合真实场景的策略。agent 架构和提示策略的消融也较有限，未能揭示环境交互对性能提升的深度影响。