证明贵在乱点兵：CoCo-ProVER 给每个动作标价

用 LLM 做形式化证明的竞赛打到现在，主流选手都在比一件事：通过率。算力烧多少没人记账，而真实软件里证明义务层层相依，一个证明的超预算会沿着依赖链把整个项目的验证成本拖垮，工程团队最后拿到的就是一张看不懂的账单。10 月 7 日放榜的 CoCo-ProVER（arXiv 2610.09681，作者 Shuangjie Yao、Suman Jana 等，哥伦比亚大学与相关团队）把成本搬上台面：证明问题被重新表述为成本约束下的元级决策，选哪个目标、派哪个专家、试到什么程度，每次调兵都要先看价钱。

双层图加一个会算账的路由器

方法侧有两个关键件。第一是双层证明图：每个声明内部建 AND/OR 超图表达证明的分合结构，声明之间再建引理依赖图，一个拓扑遍历就能选出该先证哪个目标，避免在错误的目标上空烧算力，也让后续证明能踩在已证结论上走。第二是 agent 路由器：它编排一组专家 agent，把每次调用都当作独立标价、尽力而为的动作来调度，选谁、试多久、什么时候止损都是决策变量，而且路由规则会随证据积累动态进化，越打越懂行情，前面的失败会变成后面的折价。

成绩单

在 Lean 4 的五个基准（CLEVER、VERINA、AlgoVeri、NTP4VC、Vero）上全部拿到最高解决率，其中两项做到满分；配上测试中最强的模型时，比最强基线再省约 30.9% 的成本，等于通过率与账单两头同时占优。超越对象既有前沿编码 agent，也有专门的 LLM 证明器，说明这不是靠某一家的模型优势，而是编排与算账的胜利，方法论随模型升级还能继续吃到红利。

给多 agent 系统的可借模式

这篇论文最值得带走的不是证明技巧，而是成本治理模式：给每次 agent 调用独立标价并附加尽力语义，让调度器在预算内排兵布阵，超预算的目标及时止损而不是死磕。这对任何高成本的多 agent 编排都成立，代码生成、数据分析、运维排障同理，缺的常常不是更强的兵，而是算账的将。对形式化验证的落地者，这条研究线还提示了一个选型变化：评估证明器时别只问通过率，要问每通过一个证明花多少钱，两个指标联合排座次才不会买回一台账单粉碎机。论文页未附代码仓库，复现与二次开发以作者后续发布为准。