评测大模型将编程题自动转为精确形式规范的能力，发现顶尖模型仅能正确完成77.8%的任务。
Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
- 构建可交互的代理环境，让模型在真实Rust验证器中尝试生成可执行的形式规范。
- 用竞赛题目和对手构造的极端案例测试，发现顶尖模型正确率77.8%，但常漏关键前提或误拒合法输出。
- 提出新评估方法：用可执行规范+对抗测试，比单纯人工判断更有效，能发现26%额外错误。
AI编程代理日益用于编写真实软件，但确保其输出正确仍是根本挑战。形式化验证提供可行路径：代理生成代码及机器可验证的证明，确保代码满足形式规范。然而，形式规范本身是否符合用户意图仍无保障。本文研究规范自动形式化：大模型能否将非正式编程问题转化为忠实的形式规范。我们提出Verus-SpecBench基准，包含581个源自Codeforces题目的规范撰写任务，针对Verus（Rust验证器）；并构建Verus-SpecGym，一个代理环境，模型可与Verus、bash及文件系统交互以生成规范。核心挑战是评估：专家编写的参考规范成本高，而大模型作为评判者会遗漏细微错误。为此，我们（a）扩展Verus的exec_spec机制，使生成的规范可作为Rust代码执行；（b）在官方Codeforces测试用例及从竞赛“黑客”环节提取的对抗性边缘案例上进行测试。在Verus-SpecBench上，最强模型Gemini 3.1 Pro解决77.8%任务，其他前沿模型解决51.1%–57.8%，开源模型仅21.5%–25.5%。分析显示，模型生成的规范常遗漏输入假设、接受错误输出、拒绝合法输出。此外，大模型作为评判者会漏掉26%我们评估器捕捉的失败。整体表明，规范自动形式化对前沿代理已可实现，但在已有正确代码生成能力的问题上仍显脆弱。
原文摘要 · Abstract (English)
AI coding agents are increasingly used to write real-world software, but ensuring that their outputs are correct remains a fundamental challenge. Formal verification offers a promising path: an agent generates code together with a machine-checked proof, guaranteeing that the code satisfies a formal specification. However, there is no guarantee that the formal spec itself matches the user's intent. In this work, we study specification autoformalization: whether LLM agents can translate informal programming problems into faithful formal specifications. We introduce Verus-SpecBench, a benchmark of 581 spec-writing tasks derived from Codeforces problems targeting Verus, a verifier for Rust, and Verus-SpecGym, an agentic environment in which models interact with Verus, bash, & the filesystem to develop these specs. The central challenge is evaluation: expert-written reference specs are expensive to write, & LLM judges can miss subtle mistakes. We address this by (a) extending Verus's exec_spec mechanism so that generated specs can be executed as Rust code, & (b) testing them against official Codeforces tests & adversarial cases extracted from Codeforces "hacks", which are edge cases written by competitors to break incorrect solutions. On Verus-SpecBench, the strongest model, Gemini 3.1 Pro, solves 77.8% of tasks, other frontier models solve 51.1--57.8% & OSS models reach only 21.5--25.5%. Our analysis of failure modes shows that model-generated specs can omit important input assumptions, accept incorrect outputs, & reject valid ones. We also find that LLM-as-a-judge evaluation misses 26% of the failures our evaluator catches. Overall, our results suggest that spec autoformalization is within reach for frontier agents but remains brittle even on problems where they can already generate correct code. The code, data, & logs can be found at https://github.com/formal-verif-is-cool/verus-spec-gym
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。