Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification

Shuangjie Yao; Nikolaus Holzer; Mark Paul Santolucito; Baishakhi Ray; Suman Jana; Dongdong She

cs.AIOct 7, 2026

Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification

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

Organizations: Columbia University · The Hong Kong University of Science and Technology · Barnard College, Columbia University

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: The difference between math proving and code proving; and the difference between goals within one code proving task. ( 1(a) ) A theorem in math proving (theorem from PutnamBench [ 46 ] , proof from GoedelArchitect [ 9 ] ) is stated and proved in the vocabulary of an existing library and strongly dependent on lemma decompostion, whereas a theorem in code proving (theorem from Vero [ 53 ] ) is stated over definitions the task itself introduces so the proof follows program syntax rather than library priors. ( 1(b) ) Obligations of a single Vero task need different strategies and reasoning efforts: one goal closes under rule-based automation with no model call, two need formal proofs at different reasoning efforts (simple arithmetic versus strong induction), and a recurring fact is better stated as a shared helper lemma.

Figure 2: The two-level proof graph. Left : the lemma-dependency DAG

\mathcal{D}=(L,E_{\mathcal{D}})

, with an edge

u\rightarrow v

when the proof or plan of

v

uses helper lemma

u

, the targets

L_{\star}\subseteq L

as roots, and each lemma stable, provisional, or discarded. Right : within one declaration, the AND/OR hypergraph

\mathcal{H}_{\ell}=(A_{\ell},O_{\ell},E_{\ell})

over goal states (AND nodes

A_{\ell}

) and proof steps (OR nodes

O_{\ell}

), where an executed step attaches a verified hyperedge in

E_{\ell}

over the subgoals Lean returns.

Figure 3: Thw workflow of CoCo-Prover. Left : the scheduler gathers open AND nodes from the proof graphs and hands the router every dependency-ready goal, grouping none of them. Middle : the agentic router clusters the frontier it receives, then reasons about one group and routes it to one of four specialist agents together with the configuration. The routing rules are revised by the router itself as evidence packets accumulate. The agents alone interact with Lean checker, lemma retrieval, and shared memory. Right : every agent writes back to the two-level graphs.

Solve-Rate Comparison Across 2 Repository-Level Benchmarks
	GPT-5.6-Terra		Gemini-3.5-Flash		DeepSeek-V4-Flash
Method	NTP4VC	Vero	NTP4VC	Vero	NTP4VC	Vero
Coding Agent	85.3%	2.3%	79.7%	7.0%	39.0%	0%
CoCo-Prover	89.3%	53.5%	94.7%	60.5%	95.0%	14.0%

Table 1: Solve rates across function- and repository-level benchmarks. A task counts as solved only when Lean accepts the root declaration and no generated axioms are used.

Solve-Cost on CLEVER Benchmark (Total 161 Problems)
	GPT-5.6-Terra			Gemini-3.5-Flash			DeepSeek-V4-Flash
Method	# Commonly Solved	Cost in USD (Baseline)	Cost in USD (CoCo-Prover)	# Commonly Solved	Cost in USD (Baseline)	Cost in USD (CoCo-Prover)	# Commonly Solved	Cost in USD (Baseline)	Cost in USD (CoCo-Prover)
Ax-Prover-Base	144	69.9	63.0 $\blacktriangledown\,9.8\%$	138	364.6	140.3 $\blacktriangledown\,61.5\%$	115	53.7	14.3 $\blacktriangledown\,73.4\%$
Humanize	157	136.6	94.4 $\blacktriangledown\,30.9\%$	157	271.9	199.6 $\blacktriangledown\,26.6\%$	143	64.9	29.0 $\blacktriangledown\,55.3\%$
Coding Agent	148	90.4	72.5 $\blacktriangledown\,19.8\%$	152	258.7	176.4 $\blacktriangledown\,31.8\%$	124	56.9	24.1 $\blacktriangledown\,57.7\%$
CoCo-Prover	161	–	100.2	161	–	235.6	156	–	38.7

Table 2: Cost comparison on commonly solved problems. For each baseline, we compare expenditure only on the intersection of problems solved successfully by both CoCo-Prover and that baseline, yielding a like-for-like comparison of the cost of valid proofs.

Panel of Figure 4 — Figure 4: Success–cost frontier on the 3 benchmarks. Each curve gives the number of problems a method solves when every problem is capped at the per-problem budget on the horizontal axis, total 427 problems summed over CLEVER, VERINA, and AlgoVeri.

Appendix figures & tables14 assets

Supplementary material from the paper’s appendix.

Appendix

Model	Provider	Input	Cache hits	Cache write	Output
GPT-5.6-Terra	OpenAI	2.50	0.250	3.125	15.00
Gemini-3.5-Flash	Google Vertex AI	1.50	0.150	–	9.00
DeepSeek-V4-Flash	DeepSeek	0.44	0.014	–	1.32

Appendix

Table 4: Official model prices , in US dollars per million tokens. Input applies to uncached input tokens, Cache hits to input tokens read from the provider’s prompt cache, and Output to output tokens, including reasoning tokens. Sources: OpenAI, https://developers.openai.com/api/docs/pricing , and Google, https://ai.google.dev/gemini-api/docs/pricing , both fetched with standard tier on July 19, 2026; DeepSeek, https://api-docs.deepseek.com/quick_start/pricing/ with peak-hour rates, fetched on August 17, 2026.

Benchmark	License	Repository
CLEVER [ 43 ]	MIT	github.com/trishullab/clever
VERINA [ 54 ]	Apache-2.0	github.com/sunblaze-ucb/verina
AlgoVeri [ 57 ]	Apache-2.0	github.com/haoyuzhao123/algoveri
NTP4VC [ 51 ]	Mixed ‡	github.com/xqyww123/NTP4VC
Vero [ 53 ]	Apache-2.0 †	github.com/sunblaze-ucb/vero

Appendix

Table 5: Benchmark licenses. ‡ NTP4VC’s tooling is released under MIT; its verification conditions keep the licenses of their upstream C projects, which include GPL-2.0, GPL-3.0, LGPL-2.1, BSD-3-Clause, and MIT. † Vero’s pipeline, specifications, and permissively licensed tasks are released under Apache-2.0; tasks derived from copyleft upstream projects keep their upstream licenses: flocq and portion (LGPL-3.0-or-later) and huffman (LGPL-2.1-or-later).

Baseline	Backbone	Package / GitHub repository	Version
Codex	GPT-5.6-Terra	@openai/codex	0.146.0
Gemini CLI	Gemini-3.5-Flash	@google/gemini-cli	0.55.1
DeepSeek Harness	DeepSeek-V4-Flash	@deepseek-ai/dsh	0.1.2-alpha.2
Humanize	all three	humanfia/putnambench	8e21ff2
Ax-Prover-Base	all three	Axiomatic-AI/ax-prover-base	06dfadc

Appendix

Table 6: Baseline versions. Coding agents are pinned by npm release; Humanize and Ax-Prover-Base by Git commit, abbreviated to seven characters (each entry links to the full commit). Full commit hashes: Humanize 8e21ff211daa731fa826c491e1f12ed284135c0d ; Ax-Prover-Base 06dfadc9ab439755af5efcfe0add95bfef2733c7 .

Panel of Figure 5 — Figure 5: Per-problem cost and wall-clock time of every solved problem in CLEVER benchmark, for CoCo-Prover and each coding agent. Each point is one problem solved and plotted at its wall-clock time and monetary cost. Triangles on the axes mark each system’s mean cost ( $\blacktriangleleft$ ) and mean time ( $\blacktriangledown$ ) over its own solved set.

Backbone	CLEVER Cost (USD)	VERINA Cost (USD)	AlgoVeri Cost (USD)
GPT-5.6-Terra	17.85 $\pm$ 0.80 (4.5%)	30.32 $\pm$ 2.54 (8.4%)	15.47 $\pm$ 5.29 (34.2%)
Gemini-3.5-Flash	28.64 $\pm$ 1.61 (5.6%)	43.49 $\pm$ 1.06 (2.4%)	38.82 $\pm$ 3.22 (8.3%)
DeepSeek-V4-Flash	4.22 $\pm$ 0.93 (22.0%)	7.66 $\pm$ 0.91 (11.9%)	3.00 $\pm$ 0.23 (7.7%)

Appendix

Table 7: Run-to-run variance of CoCo-Prover. We run the complete system three times with each backbone on the 30 ablation problems (10 each from CLEVER, VERINA, and AlgoVeri) and report the mean

\pm

standard deviation of total cost in USD. Parenthesized percentages are coefficients of variation (standard deviation divided by the mean). Every run solves all 30 problems. The Gemini-3.5-Flash means are the complete-system figures used in Table 3 .

	CoCo-Prover	Codex	Humanize	Ax-Prover-Base
Outcome	proved	proved	proved	failed ( sorry )
Total cost (USD)	2.36	8.67 ( $3.7\times$ )	10.74 ( $4.5\times$ )	5.48
Wall-clock time (s)	2,816	2,550	4,538	6,893
Uncached input tokens	425,737	408,271	1,000,932	452,135
Cache-read tokens	2,115,584	26,675,200	23,777,280	77,568
Total prompt tokens	2.54M	27.08M	24.78M	0.53M

Appendix

Table 8: CLEVER prob_15 under identical LLM, prices, and caps. Ax-Prover-Base’s 288,669 output tokens include 228,209 reasoning tokens. Codex and Humanize find proofs of similar size and structure to ours; most of their extra cost is cache reads from re-sending an ever-growing context at every step. Ax-Prover-Base keeps its context small but spends $4.33 on output, mostly reasoning, re-deriving a monolithic proof each iteration, and never compiles a complete proof.

Iter.	Open goal(s) at start	New helper lemmas proposed	Closed by Proof Writer	Cost ($)
1	correctness	implementation_splitOn	both conjuncts of the spec	0.263
2	implementation_splitOn	round-trip (#4) + no-space (#3)	implementation_splitOn	0.262
3	#3, #4	toList / splitOn bridges (#5, #6)	#4 ( calc chain); #3	0.453
4	#5, #6	private worker (#7) + predicate split (#8)	#5, #6	0.266
5	#7, #8	byte-scanner agreement (#9)	#7 (induction generalizing acc ); #8	0.263
6	#9	UTF-8 offset lemma (#10)	#9 (25 calls, $0.325: hardest step)	0.612

Appendix

Table 9: Iteration timeline (declaration numbers from Table 10 ). Each iteration pushes the open gap exactly one layer down: from the specification, to the string API, to character lists, to the byte scanner. Deterministic Automation opened iteration 1 by producing the five-tactic skeleton of correctness at zero model cost; on the eight lower-level goals it failed fast (heartbeat timeout, no progress, or a partial script below the quality threshold) and the controller moved on without spending model budget there.

Figure 6: Lemma-dependency graph of the final proof of CLEVER prob_15 . The root is the specification-level correctness theorem; every edge points from a helper lemma to the declaration whose proof consumes it. Depth corresponds to the layer of abstraction each iteration reached: implementation_splitOn instantiates the specification to the implementation, the round-trip and no-space lemmas work at the string API, the toList and splitOn bridges move to character lists (including the private accumulator worker), and the lowest branch descends through the byte-level scanner agreement to UTF-8 offset arithmetic. Each declaration was proposed with a sorry body, checked for counterexamples, and proved exactly once ( Table 10 ).

#	Lemma/Theorem	Proposed	Counterexample check	Lines
1	correctness	target theorem	—	14
2	implementation_splitOn	iter. 1	no counterexample	9
3	nat_repr_toList_no_space	iter. 2	no counterexample	9
4	string_splitOn_space_intercalate	iter. 2	inconclusive (timeout)	28
5	string_toList_intercalate	iter. 3	no counterexample	9
6	string_splitOn_singleton	iter. 3	no counterexample	5

Appendix

Table 10: Every declaration in the final proof. Each lemma was proposed with a sorry body and a structured header ( @description , @lib_depends_on , @used_in , and @depends_on once it has generated dependencies), tested for counterexamples before acceptance, and proved exactly once, in the iteration after it was proposed.

Round	Cost	Worker’s stated blocker (from the run log)
1	$0.83	“ String.splitOn ’s irreducible positional scanner; the needed semantic bridge is absent”
2	$0.98	“ String.splitOn ’s irreducible UTF-8 scanner; no applicable semantic split/intercalate lemma”
3	$2.77	established the splitOn " " $\leftrightarrow$ character-splitting bridge, but “the remaining obstacle is … the opaque/internal String.intercalate implementation”
4	$0.99	“the recursive join helper is inaccessible for induction”
5	$0.79	“the required semantic bridge … is not exported; List.splitOn_intercalate cannot be applied”
6	$0.99	“the unresolved piece is a public recursive lemma for this Lean version’s private String.intercalate helper”

Appendix

Table 11: Humanize’s nine rounds. The eight failed rounds name the same two obstacles that our lemmas #7–#10 dissolve.

	CoCo-Prover (GPT-5.6-Terra)	Coding-agent baseline (GPT-5.6-Terra)
Targets proved	56 / 56	5 / 56
Full file checks in Lean	yes	no

Appendix

Table 12: Vero prob_14 outcome. The final 2,471-line proof file passes the checker: all 56 targets proved with no sorry and no axioms beyond Lean’s standard ones, and all 56 target statements identical to the originals (no restated targets).

	Closed by Automation	Closed by an LLM script (no new lemma)	Closed using lemmas or earlier targets
56 target theorems	8	2	46
55 helper lemmas	12	20	23

Appendix

Table 13: How each declaration was closed. The 8 targets closed by Deterministic Automation alone are local facts, including overlaps symmetry, self-overlap, disjointness, merge_nil , merge_singleton , chop_removes , and chop_append_coverage ; everything else is built through lemmas, and 7 of the 46 lemma-built targets are themselves reused as lemmas by later targets.

Figure 7: Lemma-dependency graph of prove_chop_canonical_merge_fixpoint , the deepest target in the Vero intervaltree run; edges point from a helper lemma to the declaration whose proof consumes it. Below the target, chop_merge_fixpoint_unfolded bridges to the unfolded goal shape left by the automation prefix and chop_merge_fixpoint_public restates it over the public definitions; the proof then splits into the two halves of the library, merging a canonical list is the identity (left) and chopping preserves canonicity (right). Two forms of reuse are visible. prove_chop_canonical_preserves_canonical (bold) is another benchmark target that this proof consumes as a lemma, and disjointSortedNonempty_pairwise_gap is a single node feeding both halves rather than a fact re-derived in each.

Declaration	Kind	Direct users	Targets depending on it (transitively)
prove_merge_coverage	target	15	18
disjointSortedNonempty_pairwise_gap	lemma	11	24
prove_merge_disjoint_strict	target	11	18
sortByLo_pairwise_lo	lemma	7	31
sortByLo_output_nonempty	lemma	7	28
prove_chop_pointwise	target	5	6

Appendix

Table 14: The most reused declarations. A handful of layer lemmas (sortedness, nonemptiness, the strict-gap conversion) feed more than half of the 56 targets, and seven proved targets are themselves reused as lemmas—this is why decomposing into lemmas scales here: each hard induction is done once and then reused.

Explore similar work

Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
Jun 3, 2026Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck +1Theorem Proving Trade-Off
1ETH Zurich, Switzerland.
Harnessing Code Agents for Automatic Software Verification
Jul 7, 2026Shuangxiang Kan, Shuanglong Kan, Sebastian ErtelFormal Verification Theorem Proving
Singapore Management University · Singapore · Barkhausen Institut +1
AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
Jul 17, 2026Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang +4Theorem Proving Proof
Nanyang Technological University · Singapore · Imperial College London +5

Jun 3, 2026, cs.CLJ/K move · Enter open · S save

Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean

Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck, Martin Vechev

1ETH Zurich, Switzerland.

Theorem Proving Trade-Off

Open paper AskPDF arXiv

Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proof attempts, and use compiler feedback to guide search. However, they can be prohibitively expensive, often spending substantial compute on attempts that ultimately fail. In this work, we address this problem with an action routing agent that consists of a data plane and a control plane. The data plane generates natural-language lemma decompositions, formalizes them in Lean, and samples proof attempts for the resulting theorem and lemma targets. The control plane observes previous failed Lean attempts, estimates both the likelihood of success and the cost of another attempt, and decides whether to continue proving the current target or restart from a new breakdown. On a subset of PutnamBench, our agent decreases the cost by 28.9% over a fixed-step baseline on average, preserving performance while using substantially less compute. These results suggest that failed Lean trajectories provide actionable signals for cost-aware resource allocation in agentic theorem proving.

Abstract

Explore similar work

Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean

Harnessing Code Agents for Automatic Software Verification

AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language