Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
作者: Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck, Martin Vechev
分类: cs.CL, cs.LO
发布日期: 2026-06-03
💡 一句话要点
提出行动路由代理以优化Lean中的成本-质量权衡
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式证明 自动定理证明 成本优化 机器学习 Lean 资源分配 智能决策
📋 核心要点
- 现有的形式证明工作流在生成证明时往往面临高昂的计算成本，许多尝试最终失败，导致资源浪费。
- 本文提出了一种包含数据平面和控制平面的行动路由代理，通过智能决策来优化证明过程中的成本和质量。
- 在实验中，该代理在PutnamBench的子集上平均降低了25.8%的计算成本，同时保持了良好的性能表现。
📝 摘要（中文）
大型语言模型（LLMs）在生成Lean中的形式证明工作流中越来越多地被使用。这些工作流通常将问题分解为较小的引理，进行多次证明尝试，并利用编译器反馈来指导搜索。然而，这些方法往往成本高昂，许多尝试最终失败。本文提出了一种行动路由代理，包含数据平面和控制平面。数据平面生成自然语言引理分解，形式化为Lean，并对生成的定理和引理目标进行证明尝试。控制平面观察之前失败的Lean尝试，估计成功的可能性和再次尝试的成本，并决定是继续证明当前目标还是从新的分解开始。在PutnamBench的一个子集上，我们的代理平均降低了25.8%的成本，同时保持性能，显著减少了计算资源的使用。这些结果表明，失败的Lean轨迹为成本意识的资源分配提供了可操作的信号。
🔬 方法详解
问题定义：本文旨在解决在Lean中生成形式证明时的高计算成本问题，现有方法在多次尝试中常常导致资源浪费，尤其是在失败的尝试上。
核心思路：提出的行动路由代理通过数据平面和控制平面的协同工作，智能地选择是否继续当前证明或重新开始，从而优化成本与成功率的平衡。
技术框架：整体架构分为两个主要模块：数据平面负责生成引理分解和进行证明尝试，控制平面则根据历史失败尝试的反馈来评估成功概率和成本，做出决策。
关键创新：最重要的创新在于利用失败的尝试数据作为反馈信号，指导后续的证明尝试，从而实现更高效的资源分配，与传统方法相比，显著降低了不必要的计算开销。
关键设计：在设计中，控制平面通过机器学习模型来估计成功概率和成本，结合历史数据进行决策，确保在不同情况下都能做出最优选择。
🖼️ 关键图片
📊 实验亮点
实验结果显示，提出的行动路由代理在PutnamBench的子集上平均降低了25.8%的计算成本，相较于固定步骤基线，保持了相似的性能表现，展现了显著的资源利用效率提升。
🎯 应用场景
该研究的潜在应用领域包括自动定理证明、形式化验证和智能合约等。通过优化证明过程中的成本与质量权衡，可以在资源有限的情况下提高自动化证明系统的效率，推动相关领域的进一步发展。
📄 摘要（原文）
Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proof attempts, and use compiler feedback to guide search. However, they can be prohibitively expensive, often spending substantial compute on attempts that ultimately fail. In this work, we address this problem with an action routing agent that consists of a data plane and a control plane. The data plane generates natural-language lemma decompositions, formalizes them in Lean, and samples proof attempts for the resulting theorem and lemma targets. The control plane observes previous failed Lean attempts, estimates both the likelihood of success and cost of another attempt, and decides whether to continue proving the current target or restart from a new breakdown. On a subset of PutnamBench, our agent decreases the cost by $25.8\%$ over a fixed-step baseline on average, preserving performance while using substantially less compute. These results suggest that failed Lean trajectories provide actionable signals for cost-aware resource allocation in agentic theorem proving.