Viva La Vida: Verification and Accumulation Failures in Multi-Agent Proof Search

Benji Xu; Ken Zheng; Noah Han

cs.CLOct 4, 2026

Viva La Vida: Verification and Accumulation Failures in Multi-Agent Proof Search

Authors: Benji Xu, Ken Zheng, Noah Han

Organizations: University of California, Berkeley

Abstract

When an agentic prover works on an open problem, there is no proof assistant to fall back on: its verifier and lemma library are ultimately language models judging model outputs. We instrumented such a system end to end and analyzed $51{,}754$ traced observations across three full runs ( $186$ hours, $ $5{,}694$ ). We find three connected failure modes. First, the three-model verifier requires unanimity and treats parse or API failure as non-approval; in $10$ of $12$ verification events, one member returned no parseable output or an API error, making acceptance arithmetically impossible without surfacing an error. Second, when the ensemble did function, one verifier approved $3$ attempts that GPT rejected, each claiming to resolve the open problem; a single-verifier design would therefore have announced a solution three times. Third, because nothing could be approved, every review was a refutation, yet the lemma extractor mines reviews as well as proofs: $24$ of $93$ lemmas ( $26\%$ ) were extracted from rejected arguments with their refutational context removed. Taken together, these findings show that without external verification, supervision is itself a critical trust boundary: systems must distinguish abstention from rejection, preserve useful disagreement, and preserve the provenance and polarity of information before it becomes future context.

Figures & tables

Figure 1: Viva La Vida . The spine is one iteration: a stateful prover with recursive ( fork , spawn_sub_prover ) and non-recursive tools emits a proof attempt; a coordinator triages whether it claims completion; if so, a three-model ensemble must approve unanimously. Above the spine is the intake path: proof attempts and reviews are both mined for lemmas by a conservative extractor, curated, and embedded for retrieval by later provers. All three gates scrutinize the prover. The red edge is the channel none of them was designed for.

Prover backbone	Hours	Cost	Generations	Iters	Verified	fork	spawn
GPT-5.4	91.3	$3,517	11,743	10	0	404	689
Gemini 3.1 Pro	81.4	$1,947	4,929	12	10	366	30
Claude Opus 4.7	13.9	$229	881	15	2	17	40
Total	186.6	$5,694	17,553	37	12	787	759

Table 1: The three full runs. “Iters” counts coordinator judgements; “Verified” counts attempts reaching the ensemble.

Channel	Source artifacts	Candidates extracted	Lemmas added	Share
Proof attempts	37	98	69	74%
Reviews (critiques)	36	38	24	26%
Total	73	136	93

Table 2: Lemma intake by channel across the three runs. Every review in the corpus is a critique of a rejected attempt, so the entire review channel is refutation-derived.

Appendix figures & tables3 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 3: Proof attempt from the Gemini 3.1 Pro prover claiming $\alpha^{\star}=3/5$ . (The root span’s displayed total ($1,258.61) is Langfuse’s own aggregate; summing the per-generation costs over the same trace gives the $1,947 reported in Table 1 .) — Figure 3: Proof attempt from the Gemini 3.1 Pro prover claiming $\alpha^{\star}=3/5$ . (The root span’s displayed total ( $1,258.61) is Langfuse’s own aggregate; summing the per-generation costs over the same trace gives the$ 1,947 reported in Table 1 .)

Figure 4: The Gemini verifier returning approved: false on the attempt in Figure 3 . The Claude verifier’s approved: false in the same event was an API Error , not a judgement.

Figure 5: Library intake following the rejection. The lemma-integrator runs under verifier-oai-injector , so the lemmas being embedded are extracted from the verifier’s critique instead of from the proof attempt.

LLM Agent Verification

LLM agent verification checks whether agents’ actions, evidence, policies, and completion claims satisfy explicit requirements.

See all 145 papers

VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks
Oct 1, 2026Caiqi Zhang, Rujun Han, Zifeng Wang +4LLM Agent Verification Long-Horizon LLM Agents
University of Cambridge · Google Cloud AI Research
Maestro: Agentic Formal Proof Development by Coordination
Oct 19, 2026Haoyu Li, Zeren Shui, Yuhao Zhang +4Large Language Model-Guided Theorem Proving Lean Theorem Proving
University of Illinois Urbana-Champaign · AWS AI Labs · Georgia Institute of Technology
AgentProofBench: Benchmarking Reusable Verifiers for Web Agents
Oct 25, 2026Jingjie Ning, Xueqi Li, Yi Lu +1LLM Agent Verification Web Agent Benchmarks

Oct 1, 2026J/K move · Enter open · S save

VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks

Caiqi Zhang, Rujun Han, Zifeng Wang, Zoey CuiZhu+3

University of Cambridge · Google Cloud AI Research

LLM Agent Verification Long-Horizon LLM Agents LLM Agent Harnesses

Open paper AskPDF arXiv

As LLM agents undertake increasingly complex, long-horizon tasks, verifying their outputs becomes increasingly challenging. We study how verification capability can be strengthened with a fixed base model, without access to reference answers or grading rubrics at test time. Repeated sampling yields multiple rollouts that can contain complementary correct claims, but we need a reliable verification mechanism to determine which claims to trust. We first find that disagreement often exposes correct alternatives, while consensus can conceal errors. These observations motivate VeriHarness, which turns the underlying LLM a generator uses into an agentic verifier by giving it a workspace, evidence tools, and reusable verification skills. A disagreement resolver checks competing claims against environmental evidence, while a consensus challenger tests shared claims and searches for omitted requirements. Their findings guide the selection and revision of the final artifact. Across five long-horizon workspace benchmarks and two frontier models, VeriHarness achieves the highest selection scores among the evaluated baselines. Evidence-backed revision further improves average performance, bringing gains over a single rollout to 6.2 points with Gemini 3.5 Flash and 6.4 points with Claude Opus 4.8. We further show that verification skills can self-improve from failure feedback, demonstrating VeriHarness as a novel and critical approach for scaling long-horizon agentic verification. We release the full pool of approximately 26,000 rollouts across all five benchmarks and both models, produced at a cost of over $100,000, to support future research on agentic verification.

Abstract

LLM Agent Verification

Explore similar work

VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks

Maestro: Agentic Formal Proof Development by Coordination

AgentProofBench: Benchmarking Reusable Verifiers for Web Agents