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

当Agentic证明器处理一个开放问题时，没有可以依靠的证明助手：它的验证器和引理库最终是判断模型输出的语言模型。我们端到端地检测了这样一个系统，并分析了从被拒绝的参数中提取的 $51{,}754$ 跟踪观察结果（$186$ 小时，\$$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\%$）。上下文已删除。总而言之，这些发现表明，如果没有外部验证，监督本身就是一个关键的信任边界：系统必须区分弃权和拒绝，保留有用的分歧，并在信息成为未来背景之前保留信息的来源和极性。