Vero：人工智能代理可以构建经过正式验证的软件存储库吗？

人工智能代理越来越多地用于编程，但不能对生成代码的正确性提供任何保证。经过验证的代码生成，其中代理生成其规范的实现和机器检查的证明，为实现值得信赖的人工智能生成的软件提供了更强有力的途径。这个方向的现有基准要么专注于单个功能，要么仅评估提供的实现的证明生成。代理是否可以在真实的多模块代码库中做出一致的实现和证明选择仍然是一个悬而未决的问题。为了弥补这一差距，我们引入了 Vero，这是第一个在存储库级别评估联合实施和证明综合的基准。 Vero 包含 43 个多模块实例，这些实例源自现实世界的存储库，涵盖 Python、Dafny、Verus 和 Coq，涵盖从加密协议到分布式系统的不同领域。每个实例都包含一个多模块 Lean 4 存储库，具有预定的 API 接口、手动策划的正式规范和参考实现，支持仅证明和代码和证明评估模式。为了提高基准测试的可靠性，Vero 还包括一个审计机制，允许代理正式证明所提供规范的不满足性或参考代码的不正确性，从而在管理过程中显示并纠正潜在的代码和规范错误。我们通过精益工具链访问来评估前沿编码代理配置。最强大的代理仅完全解决了 43 个实例中的 27 个，并且没有关闭最难存储库的规范。 Vero 提供了一个具体的测试平台，用于衡量存储库规模验证软件合成的进展，而当前的代理仍然存在不足。我们在 https://github.com/sunblaze-ucb/vero 发布了基准测试、管理流程和评估工具。