Verus-SpecGym：评估规范自动形式化的代理环境

AI 编码智能体 越来越多地用于编写现实世界的软件，但确保其输出正确仍然是一个基本挑战。形式验证提供了一条有希望的途径：代理生成代码以及机器检查的证明，保证代码满足形式规范。但是，不能保证正式规范本身符合用户的意图。在这项工作中，我们研究规范自动形式化：LLM 代理是否可以将非正式编程问题转化为忠实的形式规范。我们引入了 Verus-SpecBench，它是 581 个规范编写任务的基准，源自针对 Verus（Rust 验证器）的 Codeforces 问题，以及 Verus-SpecGym，这是一个代理环境，模型在其中与 Verus、bash 和文件系统交互以开发这些规范。核心挑战是评估：专家编写的参考规范的编写成本很高，而且 LLM 评委可能会错过细微的错误。我们通过以下方式解决这个问题：(a) 扩展 Verus 的 exec_spec 机制，以便生成的规范可以作为 Rust 代码执行，以及 (b) 根据官方 Codeforces 测试和从 Codeforces“黑客”中提取的对抗性案例进行测试，这些案例是竞争对手为打破不正确的解决方案而编写的边缘案例。在 Verus-SpecBench 上，最强模型 Gemini 3.1 Pro 解决了 77.8% 的任务，其他前沿模型解决了 51.1--57.8%，OSS 模型仅达到 21.5--25.5%。我们对故障模式的分析表明，模型生成的规范可以忽略重要的输入假设、接受不正确的输出并拒绝有效的输出。我们还发现，LLM 作为法官的评估遗漏了评估器捕获的 26% 的失败。总的来说，我们的结果表明，规范自动形式化对于前沿代理来说是可以实现的，但即使在他们已经可以生成正确代码的问题上仍然很脆弱。代码、数据和日志可以在 https://github.com/formal-verif-is-cool/verus-spec-gym 找到