💬 NLP

Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean

本文介绍了一种具有数据面和控制面的动作路由智能体，该智能体通过根据失败信号动态决定是继续还是重启证明尝试，优化了 Lean 智能定理证明中的成本-质量权衡，在保持性能的同时，在 PutnamBench 上实现了 25.8% 的计算成本降低。

原作者： Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck, Martin Vechev

发布于 2026-06-04

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck, Martin Vechev

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

想象一下你正在尝试解决一个非常困难的数学谜题，比如在著名的普特南数学竞赛（Putnam competition）中发现的那种。在过去，使用人工智能（AI）通过一种被称为 Lean 的严格计算机可读语言来解决这些谜题，就像雇佣了一支被告知无论如何都要尝试相同次数的工人团队。

如果 AI 在一个无法解决的问题上卡住了，它会一直尝试直到达到预设的限制（例如 64 次尝试），从而浪费大量的资金和计算资源。如果问题实际上很简单，它可能在第一次尝试时就解决了，但系统仍会强制它尝试直到达到上限以确保万无一失。这种“一刀切”的方法极其昂贵。

这篇论文介绍了一种更聪明、更灵活的 AI 智能体，它不像僵化的机器人，而更像是一位睿智的项目经理。以下是它的工作原理，分为几个简单的概念：

1. 问题所在：“盲目”的工人

把旧的 AI 系统想象成一个被告知：“尝试修理这个损坏的引擎正好 50 次。如果 50 次尝试后还没修好，就放弃。” 的工人。

浪费： 如果引擎缺少一个根本不存在的零件（一个不可能解决的问题），工人会白白浪费 50 次尝试。
成本： 每次“尝试”都会消耗金钱（计算能力）。在一个坏掉的引擎上进行 50 次尝试是巨大的资源浪费。

2. 解决方案：“聪明”的经理

论文中描述的新系统将工作分为两个部分：工人（尝试解决数学问题）和经理（决定何时停止）。

工人（数据平面）

这部分将大的数学问题分解成较小的、易于处理的步骤（引理/lemmas）。它尝试证明每一个步骤。如果失败了，它会再次尝试。它是实际进行重体力劳动的部分。

经理（控制平面）

这是这项新发明。经理不再让工人盲目地尝试 50 次，而是观察工人的尝试过程。它观察失败的历史并询问两个问题：

这花了我们多少钱？（我们消耗了多少个计算机“Token”？）
还有希望吗？（根据目前为止犯下的错误，工人是在接近解决方案，还是仅仅在原地打转？）

3. “红绿灯”系统

经理使用一个简单的规则来决定下一步该做什么：

绿灯（继续前进）： 如果工人正在取得进展且成本较低，经理会说：“做得好，再试一次！”
红灯（停止并重启）： 如果工人不断犯同样的错误，或者成本过高而成功机会微乎其微，经理会说：“停！这条路是死胡同。让我们放弃这个计划，尝试一种完全不同的拆解问题的方法。”

4. 结果：在不损失胜率的情况下节省资金

研究人员在 85 个困难的数学问题上测试了这个“聪明经理”。

旧方法： 为了解决一定比例的问题，旧系统花费了大量的资金。
新方法： 新的智能体解决了几乎相同数量的问题，但平均节省了 25.8% 的资金。
权衡： 如果他们想要花费与旧系统相同的金额，新的智能体实际上能多解决 7.8% 的问题。

5. 经理是如何“知道”的？

经理并非拥有魔法；它像侦探观察犯罪现场一样，寻找失败尝试中的特定线索：

重复性错误： 如果工人不断犯完全相同的错误，这表明他们陷入了循环。
混乱： 如果工人尝试着完全不同、随机且不合逻辑的方法，这表明这个问题对于当前的计划来说可能太难了。

核心结论

这篇论文表明，在 AI 数学证明的世界里，知道何时放弃与知道如何工作同样重要。 通过添加一个观察成本和尝试质量的“经理”，我们可以节省四分之一的计算预算，而不会牺牲解决难题的能力。它将一种浪费性的、蛮力尝试的方法转变为一种聪明、高效的策略。

技术摘要：优化 Lean 中智能定理证明器的成本-质量权衡

问题陈述

大型语言模型（LLMs）通过采用智能工作流（agentic workflows），在 Lean 形式化证明辅助工具的自动化定理证明领域取得了显著进展。这些工作流通常将复杂问题分解为较小的引理，生成大量的证明尝试，并利用编译器反馈来引导搜索。虽然这种方法在 PutnamBench 等具有挑战性的基准测试上取得了高性能，但其计算成本极高。目前的系统通常为每个问题分配固定的、预先指定的分解和证明生成预算，而不考虑问题的难度。这种“固定步数”策略导致了严重的浪费，因为智能体经常在不可行的题目或极不可能成功的误形式化语句上耗费大量计算资源。核心挑战在于现有智能体缺乏动态的成本感知能力，无法优化计算支出与证明成功率之间的权衡。

方法论

作者提出了一种全新的**动作路由智能体（Action Routing Agent）**架构，旨在用动态的、数据驱动的路由决策取代静态策略。该系统在概念上分为两个平面：

1. 数据平面（证明生成）

受先前工作（如 Chen et al., 2025c; Varambally et al., 2025）的启发，数据平面负责实际的证明生成。它通过四个模块运行：

分解模块（Breakdown Module）： 一个通用模型（GPT-OSS-20B）将原始问题分解为自然语言形式的引理和证明草图。
形式化模块（Formalizer）： 智能体使用 GOEDEL-FORMALIZER-V2-8B 将这些引理形式化为 Lean 代码，并选择能够通过语法或类型检查的最佳候选方案。
形式化分解证明器（Formal Breakdown Prover）： 系统尝试将这些形式化的引理作为公理，并在自然语言草图的指导下证明顶层定理。
引理证明器（Lemma Prover）： 一旦分解过程被证明，智能体会递归地尝试证明证明过程中所需的各个引理，并将新的依赖项压入栈中。

2. 控制平面（成本-质量路由）

控制平面观察失败尝试的轨迹，并决定是继续尝试当前目标，还是终止当前轨迹以重新开始新的分解。它利用一个基于成本-质量权衡的轻量级路由策略：

状态 ( $s$ )： 总结失败尝试的历史记录，包括证明尝试、编译结果、错误信息和输出长度。
动作空间： $\{ \text{尝试 (ATTEMPT)}, \text{终止 (TERMINATE)} \}$ 。智能体要么为当前目标采样另一个证明，要么丢弃当前的分解。
效用函数： 路由器计算效用得分 $\tau(s) = \hat{q}(s) - \lambda\hat{c}(s)$ $τ (s) = \overset{q}{^} (s) - λ \overset{c}{^} (s)$ ，其中：
- $\hat{q}(s)$ 是下一次尝试成功的预测概率（质量）。
- $\hat{c}(s)$ 是下一次尝试的预测成本（以 LLM 生成的 token 数/SFLOPs 衡量）。
- $\lambda$ 是控制计算成本惩罚项的超参数。
决策规则： 如果 $\tau(s) > 0$ ，则继续；否则，终止当前轨迹。

估计器：

成本估计器： 假设尝试成本是独立同分布的，使用轨迹中先前尝试的平均成本。
质量估计器： 一个逻辑回归模型，根据轨迹特征预测成功概率，具体特征包括：
- 证明相似度（Proof Similarity）： 归一化证明的平均成对模糊字符串比例（低相似度意味着逻辑混乱）。
- 错误多样性（Error Diversity）： 唯一编译错误与总错误数的比例（低多样性意味着存在持续性的失败模式）。
- 尝试次数（Attempt Count）： 之前尝试的次数。

核心贡献

识别低效性： 本文指出，Lean 智能体中的固定步数缩放效率极低，减少不必要的尝试对于实现更好的成本-质量权衡至关重要。
创新架构： 开发了一种具备在线、自适应成本-质量路由器的引理式 Lean 证明器，该路由器能动态评估额外计算的边际价值。
实证验证： 证明了所提出的路由器在保持竞争力的准确度的同时，显著降低了计算浪费，证明了失败的轨迹包含用于资源分配的可行信号。

实验结果

系统在 PutnamBench 的 85 个问题子集上进行了评估，将动态路由智能体与固定步数基线以及拥有地面真值成功概率的“先知（oracle）”智能体进行了对比。

成本降低： 在准确度持平的情况下，与固定步数基线相比，所提出的智能体平均减少了 25.8% 的所需预算。
准确度提升： 在成本持平的情况下，该智能体实现了 7.8% 的求解率提升。
特定权衡：
- 为了达到 ~43.6% 的求解率，固定步数基线需要 31.6 M SFLOPs，而路由智能体仅需 22.6 M SFLOPs（成本降低 28.4%）。
- 在中等预算阶段（~41.6% 求解率），该智能体降低了 29.6% 的成本（17.5 M vs. 24.9 M SFLOPs）。
消融研究：
- 特征重要性： “错误多样性”被发现是质量估计中最关键的特征。
- 数据平面影响： 引理式分解架构本身相比于全证明生成方法，在相同 8B 模型下使求解率提升了近 100%，接近 32B 模型的性能。
- 先知差距： 虽然路由智能体显著优于固定基线，但与实现 59.9% 成本降低的先知智能体之间仍存在差距，这表明在特征工程和估计器架构方面仍有改进空间。

重要性与主张

本文主张，失败的 Lean 轨迹为成本感知的资源分配提供了可行的信号。通过从静态的固定步数策略转向动态路由，智能体可以在不牺牲性能的前提下显著减少计算浪费。作者将这项工作定位为形式化数学证明中“成本感知控制”的基础性步骤，并指出未来的智能体应当根据观察到的进度和失败模式来动态分配计算，而不是静态地分配推理预算。结果表明，固定步数策略在效率提升方面仍有巨大的改进空间，且路由策略可以有效地缓解不必要的成本。