加州大学伯克利分校发布 Vero 基准：首个面向仓库级形式化验证的 AI 智能体评测标准

OmniTools 9月2日消息，加州大学伯克利分校等机构正式发布 Vero 基准，旨在评估 AI 智能体在真实软件开发场景中同步生成可验证代码与数学证明的能力。

Vero 被称为首个要求智能体在完整仓库粒度上同时编写实现与形式化证明的公开基准，涵盖 43 个多模块 Lean 4 实例、743 个计分 API 接口及 2705 条形式化规范。

该基准聚焦于软件工程中的高可靠性需求，强调智能体对类型系统、逻辑推理与模块化协作的综合理解能力，不依赖自然语言任务或单函数级测试。