优化 Lean 中代理定理证明器的成本 - 质量权衡

大型语言模型常用于生成 Lean 形式化证明，现有工作流通常将问题分解为引理并采样多次尝试，但计算成本高昂。本文提出一种包含数据平面与控制平面的动作路由代理：数据平面负责引理分解与证明采样；控制平面则基于失败反馈评估成功率与成本，动态决定是继续当前目标还是重启分解。在 PutnamBench 子集上的实验表明，该代理在保持性能的同时，平均降低了 25.8% 的计算成本，证明了利用失败轨迹进行成本感知资源分配的有效性。