Vero 揭差距：agent 不建可复用引理库，74% 证明行靠辅助引理
dawnsongtweets · x · 2026-08-23
Vero 结果揭示了能力差距所在：最强 agent 能通过 87% 的单条规约，但留下 16 个仓库未完成——剩余规约编码了跨模块不变式，需要可复用的引理库，而 agent 很少主动构建。在 82 次完整求解中，约 74% 的证明行位于跨规约共享的辅助引理里。agent 有时还会绕开难验证的参考算法，自己写满足同样规约的更简单实现。
所属事件:Dawn Song 团队发布首个代码库级形式化验证基准 Vero(8 条相关)→
「研究」频道最新
- Prompt Injection 损失极小？攻击成本降低或带来新风险 — joshua_saxe · 2026-08-23
- 硬核移植：将 Ninfer 移植至 CMP 170HX，Qwen 性能翻倍 — ubrtnk · 2026-08-23
- Claude 与 Codex 闯关 Cayley 666 难题：为何越来越难 — AndLukyane · 2026-08-23
- 研究：错误配置的 Admin 提示可击穿安全层 — Simple_Passion_7741 · 2026-08-23
- 7500 行代码教你从零训练现代语言模型 — tom_doerr · 2026-08-23
- ProteinDPO 用偏好对齐解决蛋白模型对齐问题 — bravo_abad · 2026-08-23