🤖 machine learning

VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

本文介绍了 VERITAS，这是一个通过两阶段的 Best-of-N 和批判者引导的 MCTS 协议，将丰富的验证器信号反馈回搜索过程，从而增强形式化定理证明的零样本框架，在 miniF2F 和一个新的组合数学数据集等基准测试上实现了最先进的性能。

原作者： Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

发布于 2026-06-19

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

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

想象一下你正在尝试解决一个非常困难的谜题，比如一道复杂的数学题，但你是带着一个 AI 助手团队来完成的。通常情况下，当这些 AI 助手尝试解决问题时，它们会猜一个答案，检查是否奏效，如果失败了，它们只会得到一个简单的“不，再试一次”的信号。它们会丢弃关于失败原因的所有细节。

VERITAS 是一个改变游戏规则的新系统。它不再仅仅说“不”，而是倾听证明失败的具体原因，并利用这些原因来引导下一次尝试。这就像一位侦探，不仅会说“嫌疑人是清白的”，还会说“嫌疑人是清白的，因为他在下午 5 点在商店里，所以让我们去找另一个也在商店里的人”。

以下是 VERITAS 的工作原理，分为几个简单的部分：

1. 四位专家组成的团队

VERITAS 并不依赖于单一的 AI 大脑。它使用四个专门的“智能体（agent）”进行对话：

策略家 (The Strategist)： 在尝试解决问题之前，这个智能体决定高层级的计划（例如，“让我们尝试通过分类讨论来拆解这个问题”或“让我们尝试用反证法来证明”）。它通过缩小搜索范围来确保团队不会在错误的想法上浪费时间。
检索者 (The Retriever)： 这个智能体就像一位图书管理员。它能快速找到可能有助于解决当前步骤的参考书籍（数学规则和引理）。
战术家 (The Tactician)： 这是主要的工作者。它尝试编写实际的证明步骤。至关重要的一点是，它会查看早期失败尝试的失败记录列表。如果之前的尝试因为使用了错误的规则名称而失败，战术家会被告知：“不要再使用那个名字了；这是错误信息。”
评论家 (The Critic)： 这个智能体扮演教练的角色。它观察进度，并根据计算机检查数学结果的反馈给出评价，例如：“你离目标越来越近了，”或者“你正在走向死胡同。”

2. 两阶段游戏计划

该系统分两个不同的轮次进行游戏，以提高效率：

第一阶段：“快速扫射” (Best-of-N)
团队进行 5 次快速、独立的解题尝试。如果其中一个成功了，太棒了！他们立即停止。这很快，可以处理“简单”的问题。
第二阶段：“深度挖掘” (Critic-Guided Search)
如果快速扫射失败，系统就会切换到更谨慎的模式。它会将第一阶段所有的错误提取出来，并将这些信息作为“负面示例”反馈给战术家。
- 类比： 想象你在尝试打开一扇锁着的门。在第一阶段，你快速尝试了 5 把不同的钥匙。没有一把能用。在第二阶段，你不再是随机尝试钥匙，而是观察那 5 把卡住锁的钥匙，记录下它们是如何卡住的，并利用这些信息来打造一把符合锁孔特定形状的新钥匙。

3. 为什么这很重要：“组合数学”问题

论文在两类数学问题上测试了该系统。

标准数学问题： VERITAS 解决这些问题的数量超过了以往的方法（40.6% 对比 36.9%）。
组合数学（计数问题）： 这是 VERITAS 真正大放异彩的地方。在这些问题中，你通常需要使用非常具体且精确的数学规则名称。
- 问题所在： 标准的 AI 猜测经常会“幻觉”（编造）不存在的规则名称。如果 AI 猜了一个虚假的规则名，标准系统只会说“失败”然后继续下一步。
- VERITAS 的解决方法： 因为 VERITAS 会阅读具体的错误信息（例如“未知常量 'X'”），它能在实时过程中意识到“X”并不存在。它会迭代地修正名称，直到找到真实的名称。
- 结果： 在这些困难的计数问题上，标准的猜测方法随着尝试次数的增加反而变得更糟（因为它不断编造虚假的名称）；而 VERITAS 则变得越来越好，因为它能从错误中学习。

4. “单调性”保证

作者确保了 VERITAS 永远不会丢失已经找到的解。

保证： 如果“快速扫射”（第一阶段）解决了问题，VERITAS 会保留该解并且不再触碰它。“深度挖掘”（第二阶段）仅针对第一阶段无法解决的问题进行工作。
意义： 这证明了 VERITAS 所取得的任何额外成功，都完全来自于这种智能的、基于反馈的搜索，而不是仅仅通过尝试更多的随机猜测。

5. “批处理”技巧

论文中一个聪明的工程技巧是关于如何检查答案的。

旧方法： 检查一个猜测，等待计算机说“不”，再检查下一个，等待，再检查下一个……这很慢。
VERITAS 方法： 他们将 6 个猜测打包进一个单一文件中，并要求计算机一次性检查所有猜测。这使得系统速度提高了约 10 到 20 倍，节省了大量的时间和成本。

总结

VERITAS 是一个将计算机错误信息视为地图而非“停止标志”的系统。通过阅读证明失败的具体原因（语法错误、类型错误、缺失步骤）并将这些信息反馈到 AI 的下一次尝试中，它能够解决其他系统会放弃的困难数学问题。它结合了快速的“尝试并观察”方法与智能的“从失败中学习”方法，以获得最佳结果。

技术摘要：VERITAS：用于零样本形式化定理证明的验证器引导型证明搜索

问题陈述

当前的基于大语言模型（LLM）的形式化定理证明器通常会将来自形式化验证器（如 Lean 4）的丰富、结构化信号坍缩为二元的通过/失败结果。验证器提供细粒度的反馈，包括语法错误、类型不匹配、部分目标进展以及证明完成状态。然而，标准的流水线会丢弃这些中间产物，将其总结为标量奖励或直接丢弃。这迫使搜索算法去“重新学习”验证器已经明确提供的已知信息，这种局限性在需要依赖链式策略（即每一步的正确性都取决于前一步对目标的效应）的证明中成本尤为高昂。

方法论：VERITAS 框架

VERITAS 是一个零样本框架，旨在将每一个验证器信号路由回证明生成过程。它采用了一个由共享证明状态协调的四智能体架构和两阶段搜索协议。

1. 四个专业智能体

所有智能体都在一个共享的 ProofState 上运行，该状态包含定理、当前目标、假设、策略历史以及来自 Lean 的四个结构化信号：

策略家 (Strategist)： 将证明状态映射到六种高层策略之一（直接、归纳、矛盾、分类、重写、应用引理），并估计深度，从而将搜索限制在相关的子空间内。
检索器 (Retriever)： 通过计算关键词与目标标记（tokens）、引理名称及签名的重叠度，提取相关的 Mathlib 前件。
批判者 (Critic)： 一个轻量级模型，用于对部分证明状态进行评分，建议下一步策略并提供剪枝建议。它利用集成了 Lean 四向反馈的价值估计来取代 MCTS 中的随机采样。
战术家 (Tactician)： 生成以策略、检索到的前件、批判者指导以及——至关重要的是——包含之前失败策略及其特定 Lean 错误信息的负面示例为条件的 $K$ 个候选战术。

2. 具有单调性保证的两阶段协议

该框架使用一种保守的两阶段协议，以确保收益可归因于反馈驱动的搜索：

第一阶段 (Best-of-N)： 标准的 Best-of-N 扫描（例如 $N=5$ ）生成战术批次。如果其中任何一个成功，则立即解决定理。
第二阶段 (Critic-Guided MCTS)： 仅在第一阶段失败时激活。第一阶段的失败集合（战术及其错误）会被注入到战术家的系统提示词中作为负面示例。批判者引导蒙特卡洛树搜索 (MCTS)：
- 选择 (Selection)： 使用结合了批判者价值和策略一致性的扩展 UCB 公式。
- 扩展 (Expansion)： 智能体顺序运行；候选者通过批量 Lean 验证进行校验。
- 模拟 (Simulation)： 用由结构化信号（ $\sigma_A$ 语法、 $\sigma_B$ 类型、 $\sigma_C$ 进展、 $\sigma_D$ 完成）增强的批判者价值取代随机采样。
- 反向传播 (Backpropagation)： 将结构化信号向上层传递，而非坍缩为二元的胜/负，从而保留对部分进展的信用分配。

批量 Lean 验证： 为了避免在每次扩展时调用 $K$ 次 Lean，候选者被编译成单个 .lean 文件作为私有定理，并在一次调用中完成验证。这使验证成本从 $O(K)$ 降低到 $O(1)$ ，实现了约 $10\times$ 的加速。

单调性： 该协议保证最终解决的定理集是仅靠第一阶段解决定理集的超集 ( $S \supseteq S_1$ )。这隔离了第二阶段的贡献，确保任何额外的解决案例都严格归功于验证器引导的 MCTS。

核心贡献

零样本四智能体框架： 一个将 Lean 结构化反馈（语法、类型、进展、完成）路由到每一次生成决策中的系统，无需痕迹微调。
两阶段协议： 一种 Best-of-N $\to$ Critic-MCTS 的设计，具有内部单调性保证，允许对搜索贡献进行清晰的归因。
效率优化： 批量 Lean 验证技巧将验证开销降低了约 $10\times$ 。
VERITAS-CombiBench： 一个包含 55 个经作者验证的、困难组合数学定理的 Lean 4 新基准测试，旨在揭示无引导采样的局限性。
归因分析： 实证表明，11 个 miniF2F 定理是仅由 MCTS 阶段唯一解决的，而平铺采样无法达到这些题目。

实验结果

实验在 miniF2F (244 个定理) 和 VERITAS-CombiBench (55 个定理) 上进行。

miniF2F 表现： VERITAS 达到了 40.6% 的解决率 (99/244)，优于独立的 Best-of-5 基准 (36.9%) 和手工设计的组合集 (Portfolio, 26.2%)。
- 第二阶段贡献了 11 个平铺采样无法实现的独特解题，主要集中在需要 2–4 个依赖战术的问题上。
- 在“困难”非 sorry 问题上，VERITAS 达到 28.9%，对比 Best-of-5 的 25.9%。
VERITAS-CombiBench 表现： 该基准凸显了无引导采样的失败。Best-of-5 仅实现了 1.8%，低于组合集 (3.6%)，因为 LLM 会幻觉出错误的 Mathlib 引理名称。VERITAS 通过利用 Lean 错误反馈迭代修正这些名称，达到了 7.3%。
效率： VERITAS 在推理侧方法中占据帕累托前沿，以每个定理约 27 次 Lean 调用实现 40.6% 的解决率，API 成本约为每次扫描 $150 美元。
失败模式： 分析显示，32% 的失败源于语法层面（幻觉名称），17% 是类型正确但逻辑错误，10% 是“接近成功”（部分目标进展）的情况，在这些情况下批判者可以提供高价值指导。

意义与主张

论文提出了一个通用设计原则：当确定性验证器发出结构化中间信号时，将这些信号折回生成过程比单纯增加采样次数能更大幅度地增强 LLM 的能力。

VERITAS 证明了：

验证器信号即状态： 确定性的验证器信号可以作为推理时的状态，而不不仅仅是最终检查。
组件协同： 将验证器与生成过程紧密耦合，比孤立地扩展 LLM 或搜索组件更为有效。
迭代修正： 对于需要精确引理检索的领域（如组合数学），利用验证器错误进行迭代修正优于平铺采样，后者往往会产生词法错误的名称。

作者得出结论，虽然 VERITAS 并非解决 IMO 级创造力或交互延迟的良药，但其主要贡献在于路由：即高效地收集第一阶段的简单证明，并仅在第二阶段将计算预算投入到验证器失败可以引导下一步战术的地方。未来的工作方向被确定为改进检索、创建更廉价的批判者，以及将第二阶段的痕迹蒸馏出来，以将这一原则扩展到剩余的困难问题领域。