[论文] Vero: Can AI Agents Build Formally Verified Software Repositories?

论文概要

研究领域: ML
作者: Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song
发布时间: 2026-08-13
arXiv: 2608.13522

中文摘要

AI智能体越来越多地用于编程，但不对生成代码的正确性提供任何保证。经过验证的代码生成（智能体同时生成实现和其规范的机器检查证明）为可信AI生成软件提供了一条更强路径。现有基准要么聚焦单个函数，要么仅评估提供实现后的证明生成。智能体能否在真实的多模块代码库中做出一致的实现和证明选择仍是一个开放问题。为弥合这一差距，我们引入Vero，首个在仓库级别评估联合实现和证明合成的基准。Vero包含43个来自真实仓库的多模块实例，涵盖Python、Dafny、Verus和Coq，覆盖从加密协议到分布式系统的多样领域。每个实例包含一个具有预定API接口、手动策划形式规范和参考实现的多模块Lean 4仓库，支持仅证明和代码加证明两种评估模式。为提高基准可靠性，Vero还包括审计机制，允许智能体形式化证明所提供规范的不可满足性或参考代码的不正确性，从而在策划过程中发现和纠正潜在的代码和规范错误。我们评估了具有Lean工具链访问权限的前沿编码智能体配置。最强的智能体仅完全解决了43个实例中的27个，在最困难的仓库上没有关闭任何规范。Vero为衡量向仓库规模验证软件合成进展提供了具体测试平台，当前智能体仍有不足。我们在https://github.com/sunblaze-ucb/vero发布基准、策划流程和评估工具。

原文摘要

AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a stronger path toward trustworthy AI-generated software. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark可靠性, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.

自动采集于 2026-08-15

#论文 #arXiv #ML #小凯