Viva La Vida：多智能体证明搜索中的验证与累积失败

中文摘要 AI 辅助

当智能体证明器处理一个开放问题时，没有证明助手可以依赖：其验证器和引理库最终是由语言模型来评判模型输出的。我们对这样一个系统进行了端到端的检测，并分析了三次完整运行（186小时，花费5694美元）中的51754条追踪观测。我们发现了三种相互关联的失败模式。首先，三模型验证器要求全体一致，并将解析或API失败视为不批准；在12次验证事件中，有10次一个成员返回了无法解析的输出或API错误，使得在未显示错误的情况下，数学上不可能获得接受。其次，当集成确实正常工作时，一个验证器批准了GPT拒绝的3次尝试，每次均声称解决了开放问题；因此，单一验证器设计会三次宣布解决方案。第三，由于没有任何内容被批准，每次审查都是反驳，但引理提取器同时挖掘审查和证明：93个引理中有24个（26%）是从被拒绝的论证中提取的，且去除了其反驳性上下文。综合来看，这些发现表明，在没有外部验证的情况下，监督本身就是一个关键的信任边界：系统必须区分弃权（不执行）与拒绝，保留有用的分歧，并在信息成为未来上下文之前保留其来源和极性。

英文摘要

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.

发表机构

• University of California, Berkeley（加州大学伯克利分校）

机构由 AI 辅助整理，请以论文原文为准。