CoCo-Prover：通过Agent编排降低程序验证的定理证明成本

程序验证通过在定理证明器中构建的机器可检查证明来确定软件的正确性。对于由大型语言模型 (LLM) 生成的代码来说，这是一种特别有价值的保证，这些代码很流畅，但不能保证正确性。然而，几乎所有现有的证明者在任何采样或搜索预算下都只追求通过率，而忽略了成功与成本的边界；然而，真正的软件通常承担数百个相互依赖的证明义务，因此在规模上重要的不是是否可以证明一个定理，而是可以经济地证明多少个定理。我们引入了 CoCo-Prover，它将具有成本效益的程序证明形式化为成本下的元级决策，基于两级证明图：每个声明中的 AND/OR 证明超图连接到跨声明的引理依赖图；在每一步中，它都会回答两个问题：选择哪些开放目标，以及为这些目标购买哪些行动。选择仍然具有象征意义，就像对证明图的拓扑传递一样。动作选择是通过元级决策进行Agent编排：Agentic 路由器将每个有界专家调用视为单独定价、尽力而为的计算，根据随着证据积累而演变的路由规则，将异构专家Agent与配置相匹配。在 Lean 4 中的五个程序验证基准（包括功能级 CLEVER、VERINA 和 AlgoVeri，以及存储库级 NTP4VC 和 Vero）上，我们表明 CoCo-Prover 比包括前沿编码Agent和最先进的基于 LLM 的证明器在内的基准实现了更好的成功与成本前沿：它在每个基准上实现了最佳解决率，在两个基准上达到了 100%。与我们评估中最强的 LLM 的最强基线相比，它还可将成本降低高达 30.9%。