用智能代理优化证明生成的算力消耗，省钱不降效
Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
- 分两层控制：一层生成证明思路，一层判断是否继续试错
- 在PutnamBench上降低28.9%算力开销，效果不变
- 适合关注效率的自动化定理证明研究者
大型语言模型（LLMs）正被用于生成Lean形式化证明。这些工作通常将问题拆解为小引理，多次采样证明尝试，并利用编译器反馈引导搜索。但过程常因大量失败尝试而代价高昂。本文提出一种动作路由代理，包含数据平面与控制平面：数据平面生成自然语言引理分解，形式化为Lean代码并采样证明；控制平面观察历史失败记录，估算成功概率与后续成本，决定继续当前目标或重新分解。在PutnamBench子集上，该方法相比固定步数基线平均降低28.9%成本，性能保持不变。结果表明，失败的证明轨迹可作为成本敏感资源分配的有效信号。
原文摘要 · Abstract (English)
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 the 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 28.9% 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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。