Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification

📄 arXiv: 2610.09681v1 📥 PDF

作者: Shuangjie Yao, Nikolaus Holzer, Mark Paul Santolucito, Baishakhi Ray, Suman Jana, Dongdong She

分类: cs.AI, cs.LO, cs.PL, cs.SE

发布日期: 2026-10-07

💡 一句话要点

提出CoCo-Prover以实现高效的程序验证

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 程序验证 成本效率 元层决策 证明图 专家系统 自动化测试 软件正确性

📋 核心要点

  1. 现有程序验证方法通常只关注通过率，忽视了成功与成本的平衡，导致在处理复杂软件时效率低下。
  2. CoCo-Prover通过元层决策和两级证明图的结合，优化了程序证明的选择和行动，提升了成本效率。
  3. 在五个基准测试中，CoCo-Prover在每个测试中均取得最佳解决率，并在两个基准上实现了100%的成功率，同时成本降低了30.9%。

📝 摘要（中文）

程序验证通过机器可检查的证明来确保软件的正确性，尤其对于大型语言模型生成的代码至关重要。现有的证明器往往只关注通过率，而忽视了成功与成本之间的平衡。CoCo-Prover通过元层决策制定，结合两级证明图，优化了程序证明的成本效率。实验结果表明，CoCo-Prover在多个基准测试中表现优异，成功率和成本效益均优于现有方法。

🔬 方法详解

问题定义：论文旨在解决现有程序验证方法在成功率与成本之间的平衡问题，尤其是在处理复杂的证明义务时，现有方法往往效率低下。

核心思路：CoCo-Prover通过元层决策制定，将程序证明形式化为成本效率的决策过程，利用两级证明图来优化目标选择和行动决策。

技术框架：整体架构包括一个AND/OR证明超图和一个引理依赖图，选择开放目标并决定购买的行动。选择过程保持符号化，而行动选择则通过代理协调进行。

关键创新：CoCo-Prover的创新在于将每个专家调用视为单独定价的计算任务，通过演化的路由规则将异构专家代理与配置相匹配，从而实现高效的证明过程。

关键设计：在设计中，采用了符号选择和代理路由机制，确保在收集证据的过程中动态调整决策，优化了整体证明效率。具体参数设置和损失函数的设计细节在论文中有详细阐述。

🖼️ 关键图片

img_0
img_1
img_2

📊 实验亮点

CoCo-Prover在五个程序验证基准测试中均取得最佳解决率，其中两个基准测试的成功率达到100%。与最强基线相比，成本降低幅度高达30.9%，显示出显著的成本效益。

🎯 应用场景

该研究的潜在应用领域包括软件开发、自动化测试和安全验证等，能够为大型软件系统提供更高效的验证手段，确保生成代码的正确性，降低开发成本。未来，CoCo-Prover可能在智能合约和嵌入式系统等领域发挥重要作用。

📄 摘要（原文）

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.