🤖 AI

Pessimistic Verification for Open Ended Math Questions

本文介绍了“悲观验证”（pessimistic verification），这是一种如果任何并行验证器检测到错误就会拒绝数学解法的智能体工作流，以及其增强型的“渐进式”（progressive）变体，该变体通过细粒度的证明分解，在具有挑战性的开放式数学问题上显著提升了现有方法的准确率和 Token 效率，同时揭示了由于标注错误，当前的基准测试可能会低估强模型的表现。

原作者： Yanxing Huang, Zihan Tang, Zejin Lin, Peng Li, Yang Liu

发布于 2026-06-23

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Yanxing Huang, Zihan Tang, Zejin Lin, Peng Li, Yang Liu

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你是一名正在批改一叠数学试卷的老师。你的目标不仅仅是看最终答案是否正确，还要检查学生的逻辑是否严密。如果学生在第三步犯了一个错误，那么即使他们最后神奇地得到了正确的数字，整个证明过程也是错误的。

这篇论文介绍了一种让 AI 扮演这种老师角色的新方法。作者称之为**“悲观验证”（Pessimistic Verification）**。

以下是他们想法的简单拆解，使用了日常类比：

1. 问题所在：“乐观型”AI

目前的 AI 在尝试检查数学证明时，往往表现得像一个乐观的朋友。它读完整个证明后，心想：“嗯，看起来大体上没问题，”然后给出一个及格的分数。

缺陷： AI 很难发现隐藏的错误。它经常会漏掉微小的错误，因为它试图表现得“友善”，或者因为它被冗长、复杂的论证搞得应接不暇。
代价： 为了保险起见，目前的系统会尝试检查这个证明数十次。这就像请 64 个不同的朋友来读同一篇论文。这行得通，但极其昂贵且缓慢（就像为了请这些朋友喝咖啡而烧掉了大量的钱）。

2. 解决方案：“悲观型”AI

作者提出了一种**悲观（Pessimistic）**的方法。想象一个严厉、多疑的银行保安。

规则： “只要任何人发现哪怕一个瑕疵，整个东西就会立即被拒绝。”
运作方式： 你不是要求 AI 写一篇长文来论证为什么这个证明是好的，而是问它：“这里有错误吗？”
魔力所在： 寻找错误比证明某件事是完美的要容易得多。通过专注于寻找错误，AI 变得更加敏锐。如果它发现了错误，它会停下来并说：“错误（False）”。如果它尝试了几次后仍未发现错误，它才会说：“正确（True）”。

3. 三种变体（工具）

论文测试了三种应用这种“悲观”思维的方式：

简单悲观法（“重复”法）：
- 类比： 你要求同一个保安连续读 10 遍整个证明。
- 结果： 比读一次要好，但仍然有点浪费，因为保安每次都要重新阅读整个内容。
垂直悲观法（“缩放”法）：
- 类比： 与其读整本书，不如把证明切成小段落。你要求保安只看第 1 段，然后只看第 2 段。
- 结果： 这有助于发现那些在长篇阅读中容易被忽略的微小拼写或逻辑错误。但如果切分的段落过于细碎，速度会变慢。
渐进悲观法（“聪明侦探”法）：
- 类比： 这是赢家。侦探首先快速扫描整个证明。如果他们没看到明显的重大错误，就会放大到特定的段落。如果他们仍然没看到，就会进一步放大到单个句子。
- 为何获胜： 它非常高效。它不会在那些显然没问题的部分浪费时间。它只在怀疑有问题的环节进行深度挖掘。它比其他方法能更快地发现错误，并且消耗更少的计算资源。

4. 大惊喜：“标准答案”竟然错了

论文中最有趣的发现之一是关于用于测试这些 AI 系统的“标准答案”的问题。

发现： 研究人员发现，测试数据集中的“正确”答案实际上是错误的。
类比： 想象一位老师的标准答案说某个学生的证明是“A+”。但新的“悲观型 AI”看了之后却说：“等等，这里的数学计算有误！”
结果： 研究人员进行了人工核查，发现 AI 是正确的。人类评分员（以及标准答案）确实漏掉了这些错误。
启示： 目前测试 AI 数学能力的测试集实际上低估了最聪明 AI 的水平，因为测试本身就包含错误。

5. 终极测试：解决真正的奥林匹克难题

作者不仅停留在评分阶段；他们还让他们的 AI 尝试去解决世界上最难的数学问题（如国际数学奥林匹克竞赛题）。

他们使用这种“渐进悲观法”在 AI 解决问题的过程中对其工作进行检查。
结果： 与之前的方法相比，该 AI 能够更正确地解决更多问题，并且使用的计算资源（token）更少。这就像拥有一支能比其他人更快、更廉价地破解谜团的侦探团队。

总结

论文认为，要验证数学，我们不应该试图追求完美，而应该学会怀疑。通过教 AI 积极地搜寻错误，并将证明拆解成更小、更易处理的块，我们可以让它们变得更聪明、更快、更可靠。在此过程中，他们还发现许多我们现有的“正确”数学答案其实并不正确。

技术摘要：针对开放式数学问题的悲观验证法

1. 问题陈述

自动验证是构建数学求解智能体（Agents）和大型语言模型（LLMs）强化学习系统的关键瓶颈。虽然基于规则的验证效率很高，但它仅限于具有确定性答案的问题，无法处理需要证明评估的开放式数学问题。相反，基于 LLM 的自动验证存在三个主要局限性：

准确性不足： 当前的模型缺乏足够的自我验证能力，通常需要人类专家的指导。
计算成本高昂： 现有的工作流（例如 DeepSeekMath-V2, DeepSeek-V3.2）通常生成大量的候选证明，并对其进行大规模并行验证（例如 64 轮），每个问题都会消耗数千次 API 调用。
基准测试可靠性： 本文认为，现有的基准测试由于存在固有的标注错误（即人类标注者忽略了证明中微妙或关键的错误），可能会低估更强模型的实际能力。

本文的核心观点是，自动验证的主要局限性不在于生成解题过程，而在于检测证明中错误的能力。

2. 方法论

作者提出了**悲观验证（Pessimistic Verification）**范式，即如果多个并行验证器中的任何一个识别出缺陷，则拒绝该解法。这种方法优先考虑错误检测而非共识。论文介绍了该方法的三个变体：

2.1 简单悲观验证

该变体在并行状态下重复标准的验证过程 $n$ 次。如果 $n$ 个独立的检查中有任何一个发现了错误，则将该证明标记为错误。这作为代表当前主流方法的基准，但缺乏结构化优化。

2.2 垂直悲观验证

该方法不再重复审查整个证明，而是将证明划分为固定长度 $k$ 的块（chunks）。它采用了一种特定的提示策略（如图 2 所示），指示 LLM 在保留完整证明作为上下文的同时，专门专注于特定的块。这使得对特定部分进行更深入、细粒度的检查成为可能。虽然它比单次通过验证提高了错误检测能力，但由于固定粒度的问题，会产生高昂的成本，可能会在易于验证的部分浪费 Token。

2.3 渐进式悲观验证

这是核心贡献，结合了简单法和垂直法的机制。它采用了多尺度验证策略：

迭代分解： 过程始于对完整证明的验证。如果没有发现错误，则对证明进行细分（例如减半），并分别验证每个部分。
剪枝： 检测到错误的证明会被立即过滤掉。验证仅在剩余的证明上继续进行。
参数： 该方法使用 $n$ 来控制最大迭代次数，使用 $k$ 来设置分割大小的下限，以防止过度分割。
效率： 这种动态方法允许系统在宏观层面快速过滤掉明显的错误，然后在必要时才深入到详细步骤，与固定粒度的方法相比，显著降低了 Token 消耗。

3. 核心贡献

识别成本低效问题： 研究强调了当前数学推理工作流中普遍存在的成本低效问题，并提供了一个以“错误为中心”的验证新视角。
创新的验证变体： 提出了三种悲观验证方法（简单、垂直、渐进），这些方法在提升 LLM 验证能力的同时，比扩展长思维链（CoT）具有更高的效率。
实证验证与基准分析： 在验证基准（IMO-GradingBench, Hard2Verify）和解题任务（IMO 2025, MathArena Apex 2025）上进行了全面的实验。至关重要的是，作者证明了现有基准测试通常包含标注错误，从而低估了强模型的验证能力。

4. 实验结果

实验在三个数据集上进行：IMO-GradingBench（人类评分的 IMO 解法）、Hard2Verify（带有人类标注的竞赛题目）以及 QiuZhen-Bench（由 GPT-5 标注的本科水平题目）。

性能指标： 主要指标为真阴性率（TNR）、真阳性率（TPR）和平衡 F1 分数。
扩展效率： 渐进式悲观验证在所有模型（范围从 Qwen3-1.7B 到 GPT-5 和 Gemini 3 Pro）中始终实现了最高的性能和 Token 效率。它在准确性和成本方面都优于标准长 CoT 和简单的并行验证。
错误检测 vs. 共识： 结果证实，错误检测（TNR）是强验证器与弱验证器之间的关键区别，而 TPR 在不同模型间保持相对稳定。
关于标注错误的案例研究： 对假阴性（FN）案例的详细分析显示，最先进的模型（如 GPT-5, Gemini 3 Pro）经常能识别出在原始标注中被人类标注者误判为正确（7/7 分）的证明中的关键错误。这表明，对于顶尖模型而言，当前的基准测试是不可靠的，观察到的“TPR 损失”往往是由于错误的地面真值（ground truth）导致的，而非模型本身的失败。
问题求解： 在 IMO 2025 和 MathArena Apex 2025 的智能体工作流中，渐进式悲观验证工作流显著提高了最终准确率和效率（以等效输出 Token 衡量），优于直接求解或朴素的并行验证。例如，在 IMO 2025 数据集上，该渐进式方法实现了 22/42 的总分，而直接求解仅为 13/42，且 Token 使用量低于简单的悲观验证基准。

5. 意义与主张

论文声称，渐进式悲观验证在形式化定理证明器（计算成本高昂且需要复杂的自动形式化）的严格严谨性与非形式化验证的局限性之间，提供了一个可行的折中方案。

以错误为中心的哲学： 本研究强调，识别出错误的验证结果具有更高的信息含量，值得优先处理。这种哲学促进了算法剪枝，从而提升了效率。
分段审查： 该方法认为，有效的验证需要对过程中的微小细节进行细致检查，而不是对整体进行重复且肤浅的审查。
实际影响： 作者认为，一旦非形式化验证达到足够的性能，它可以满足数学研究和软件工程（例如在不执行测试用例的情况下调试代码）中大多数实际应用的需求。
未来潜力： 该方法被视为推动最先进模型能力边界的一种方式，可以作为训练流水线的一个组成部分，以提高 LLM 的严密推理和验证能力。

作者总结道，他们的方法为当前验证工作流提供了一个可扩展、具有成本效益的替代方案，能够处理研究级数学问题的复杂性，同时揭示了现有基于人类标注的基准测试的局限性。