优化精益中代理定理证明者的成本质量权衡

大语言模型 (LLM) 越来越多地用于在精益中生成正式证明的工作流程。这些工作流程通常将问题分解为更小的引理，对许多证明尝试进行采样，并使用编译器反馈来指导搜索。然而，它们可能非常昂贵，通常会在最终失败的尝试上花费大量计算。在这项工作中，我们使用由数据平面和控制平面组成的动作路由代理来解决这个问题。数据平面生成自然语言引理分解，以 Lean 形式化它们，并对所得定理和引理目标进行样本证明尝试。控制平面观察之前失败的精益尝试，估计成功的可能性和另一次尝试的成本，并决定是继续证明当前目标还是从新的故障重新开始。在 PutnamBench 的一个子集上，我们的代理平均比固定步长基线降低了 28.9% 的成本，在保持性能的同时使用更少的计算。这些结果表明，失败的精益轨迹为代理定理证明中的成本感知资源分配提供了可操作的信号。