Vero 揭差距：agent 不建可复用引理库，74% 证明行靠辅助引理
dawnsongtweets · x · 2026-08-23
Vero 结果揭示了能力差距所在：最强 agent 能通过 87% 的单条规约，但留下 16 个仓库未完成——剩余规约编码了跨模块不变式，需要可复用的引理库，而 agent 很少主动构建。在 82 次完整求解中，约 74% 的证明行位于跨规约共享的辅助引理里。agent 有时还会绕开难验证的参考算法，自己写满足同样规约的更简单实现。
所属事件:Dawn Song 团队发布首个仓库级形式化验证基准 Vero(9 条相关)→
「研究」频道最新
- SubQ 开源 Decision LCR:72K-115K 长文决策基准,自研模型领先 — ryanallred · 2026-10-16
- 「特征不是神经网络基本单位」：可解释性范式之争再升温 — MoonL88537 · 2026-10-16
- FOMO-Dex 力控遥操作：机器人学会拿薄卡片、拧螺丝 — HaozhiQ · 2026-10-16
- 机制可解释性新假设：神经网络从训练第一步就开始泛化 — burny_tech · 2026-10-16
- 普林斯顿 AI 实验室启动新研究计划：确保自主系统符合人类意图 — LakeBrenden · 2026-10-16
- UbiComp 2026 论文 OrganicHAR：让传感器「发现」活动而非识别预设标签 — mynkgoel · 2026-10-16