发表机构
Columbia University; Barnard College, Columbia University; The Hong Kong University of Science and Technology（哥伦比亚大学; 哥伦比亚大学巴纳德学院; 香港科技大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对程序验证中定理证明成本高昂的问题，提出CoCo-Prover，通过两层证明图与智能体编排实现成本高效决策，在五个Lean 4基准上取得最优求解率并降低最高30.9%成本。
AI 中文摘要
程序验证通过在定理证明器中构造机器可检查的证明来确立软件的正确性。这种保证对于由大语言模型（LLMs）生成的代码尤其有价值，因为此类代码虽流畅但缺乏正确性保证。然而，几乎所有的现有证明器都仅追求通过率，不惜任何采样或搜索预算，而忽略了成功与成本之间的权衡；然而，真实软件通常包含数百个相互依赖的证明义务，因此在规模化场景下，关键不在于某个定理能否被证明，而在于能以经济的方式证明多少个定理。我们提出了CoCo-Prover，它将成本高效的程序证明形式化为成本下的元级决策，基于两层证明图：每个声明内部的AND/OR证明超图与跨声明的引理依赖图相连接；在每一步中，它回答两个问题：选择哪些开放目标，以及在这些目标上购买哪些操作。选择保持符号化，作为对证明图的拓扑遍历。操作选择通过元级决策进行智能体编排：一个智能体路由器将每个有界专家调用视为一次单独定价、尽力而为的计算，将异构专家智能体与配置相匹配，并随着证据的积累而演化路由规则。在Lean 4中的五个程序验证基准上，包括函数级CLEVER、VERINA和AlgoVeri，以及仓库级NTP4VC和Vero，我们展示了CoCo-Prover比包括前沿编码智能体和最先进的基于LLM的证明器在内的基线实现了更好的成功-成本权衡：它在每个基准上都达到了最佳求解率，并在两个基准上达到了100%。与评估中最强基线和最强LLM相比，它还将成本降低了高达30.9%。
英文摘要
Program verification establishes software correctness through machine-checkable proofs constructed in theorem provers. It's a guarantee especially valuable for code generated by large language models (LLMs), which is fluent but carries no assurance of correctness. Almost all existing provers, however, pursue pass rates alone at whatever sampling or search budget it takes, and overlook the success-vs-cost frontier; yet real software often carries hundreds of interdependent proof obligations, so what matters at scale is not whether one theorem can be proved, but how many can be proved economically. We introduce CoCo-Prover, which formalizes cost-efficient program proving as metalevel decision-making under cost, grounded on two-level proof graphs: an AND/OR proof hypergraph within each declaration is joined to a lemma-dependency graph across declarations; and at each step, it answers two questions: which open goals to select, and which actions to purchase on these goals. Selection stays symbolic as a topological pass over the proof graphs. Action choice is agent orchestration via metalevel decision-making: an agentic router treats every bounded specialist invocation as a separately priced, best-effort computation, matching heterogeneous specialist agents together with configurations, under evolved routing rules as evidence accumulates. On five program verification benchmarks in Lean 4 including function-level CLEVER, VERINA, and AlgoVeri, and repository-level NTP4VC and Vero, we show that CoCo-Prover achieves a better success-vs-cost frontier than baselines including frontier coding agents and state-of-the-art LLM-based provers: it achieves the best solve rate on every benchmark and up to 100% on two benchmarks. It also reduces cost by up to 30.9% compared to the strongest baseline with the strongest LLM in our evaluation.
