# Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification arXiv: https://arxiv.org/abs/2610.09681 ยท HTML: https://mlsanity.com/paper/2610.09681/ ## Key facts - No citing papers in the map yet (data through 7 Oct 2026). - Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use. - Builds on 30 of its 59 references that are in the map. - First posted on arXiv 7 Oct 2026. ## Placed in - LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/) ## Builds on (most cited first, 30 of 30) - [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021) - [FrugalGPT: How to Use Large Language Models While Reducing Cost and Improving Performance](https://mlsanity.com/paper/2305.05176/) (2023) - [RouteLLM: Learning to Route LLMs with Preference Data](https://mlsanity.com/paper/2406.18665/) (2024) - [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025) - [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025) - [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025) - [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025) - [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024) - [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023) - [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025) - [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026) - [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025) - [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025) - [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026) - [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026) - [Spend Less, Reason Better: Budget-Aware Value Tree Search for LLM Agents](https://mlsanity.com/paper/2603.12634/) (2026) - [Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification](https://mlsanity.com/paper/2603.19329/) (2026) - [Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement](https://mlsanity.com/paper/2606.06468/) (2026) - [VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean](https://mlsanity.com/paper/2602.18307/) (2026) - [OProver: A Unified Framework for Agentic Formal Theorem Proving](https://mlsanity.com/paper/2605.17283/) (2026) - [Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory](https://mlsanity.com/paper/2607.06447/) (2026) - [WybeCoder: Verified Imperative Code Generation](https://mlsanity.com/paper/2603.29088/) (2026) - [DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent](https://mlsanity.com/paper/2604.26311/) (2026) - [Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs](https://mlsanity.com/paper/2606.17981/) (2026) - [Agentic Proving for Program Verification](https://mlsanity.com/paper/2605.23772/) (2026) - [Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean](https://mlsanity.com/paper/2606.04883/) (2026) - [Automated Lemma Discovery in Agentic Program Verification](https://mlsanity.com/paper/2603.22114/) (2026) - [Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models](https://mlsanity.com/paper/2602.10538/) (2026) - [P3: Joint Program-and-Proof Planning for Verified Code Generation](https://mlsanity.com/paper/2608.09277/) (2026) - [Vero: Can AI Agents Build Formally Verified Software Repositories?](https://mlsanity.com/paper/2608.13522/) (2026) ## Abstract (arXiv) 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.