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

Jun 3, 2026cs.CL

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

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.

Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck +1

1ETH Zurich, Switzerland.

Theorem Proving Trade-Off

Ask PDF

Jul 7, 2026cs.FL

Harnessing Code Agents for Automatic Software Verification

Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it (retrieving premises and predicting tactics one step at a time, or splitting goals by divide-and-conquer), and still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary and limiting. Handing the whole lemma to a general LLM code agent (for example, Claude Code), free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving full coverage: every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs under feedback and hard constraints from the harness that keep each one sound (accepted only when the prover's kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent tactics). We evaluate this harness plus code agent along three dimensions. (1) Core logic: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior provers manage barely one in eight, Aria proves all 318. (3) Generality: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. A state-of-the-art model (Claude Opus 4.7) can write proofs for verified software development fully and automatically.

Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel

Singapore Management University · Singapore · Barkhausen Institut +1

Formal Verification Theorem Proving Coding Agents

Ask PDF

Jul 17, 2026cs.SE

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

Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to a shared root: current agents operate on serialized concrete syntax, emitting proofs as source text and recovering proof states through separate, line-number-based queries, so every edit shifts later lines and forces repeated relocation of errors and states. This same dependence on concrete syntax also blocks adoption of Minilang, a recent proof language that reaches SOTA on LLM-based proving but is too new for LLMs' training corpora. We address both problems by lifting the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST -- native to tool-calling LLMs -- and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree. We realize this design in \emph{Agent over AST} (AoA). Against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3--4.7x (normalized input-cache accounting), uses 2.9--6.9x fewer tokens and 3.9--8.9x fewer tool calls, and finishes 1.4--2.0x faster -- while also solving far more problems on the harder verification benchmark.

Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang +4

Nanyang Technological University · Singapore · Imperial College London +5

Theorem Proving Proof Syntax Zero-Knowledge Proofs Agent2Agent

Ask PDF