首个代码库级形式化验证基准 Vero 发布
dawnsongtweets · x · 2026-08-23
Dawn Song 团队推出 Vero，这是首个用于联合实现和证明合成的代码库级基准，旨在评估 AI 构建经形式验证软件的能力。Vero 包含 43 个多模块 Lean 4 实例，涵盖 743 个 API 和 2705 个规范。评测显示，即使是最强的前沿代理（GPT-5.5 高推理模式）在 90 分钟内也仅完全验证了 43 个仓库中的 27 个。研究揭示了跨模块不变量所需的引理库构建是当前主要的能力短板。
所属事件:Dawn Song 团队发布首个仓库级形式化验证基准 Vero(9 条相关)→
「编程与Agent」频道最新
- Vercel 后端升级:Python 正式 GA,新增容器与 Daemons — cramforce · 2026-10-16
- Datadog 发布 Scout 1.0:专攻生产事故调查的垂直模型 — tianyin_xu · 2026-10-16
- WorldMemArena 中选 NeurIPS:存储式 Agent 记忆评估遭颠覆 — xwang_lk · 2026-10-16
- Vercel Ship 现场宣布容器部署,Go/Ruby/Java 皆可上 — edwin · 2026-10-16
- TRL 零时差支持 Muse Spark Open：64 张 H100 上 LoRA 微调 816B MoE — QGallouedec · 2026-10-16
- 工程师入职首日全靠 AI 提问，第二天就能提交有影响力的 PR — Yuchenj_UW · 2026-10-16