Verification issues cause failures in multi-agent proof searches

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

Computation and LanguageArtificial IntelligenceMultiagent Systems

Summary

The paper studies an automated system where multiple AI models work together to prove difficult problems. It finds that the system often fails because the verifiers disagree or fail to parse results correctly, preventing any solution from being accepted. Sometimes one verifier approves a wrong proof that others reject, showing that relying on a single verifier would cause false successes. Also, even rejected attempts yield useful information that the system extracts and reuses, but this requires careful handling to keep track of the disagreement and context. The authors highlight that such systems need better ways to handle verification errors and preserve useful disagreements to improve trust and future performance.

What this means in practice

  • For ai system engineers: Improve multi-agent AI proof systems by distinguishing error types and preserving verifier disagreement to avoid false proof acceptances.
  • For software quality teams: Use insights on verification failure modes to design better testing and logging tools for complex automated reasoning systems.

Authors

Benji Xu, Ken Zheng, Noah Han

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.
View PDFOpen arXiv