LEVER：通过 AND/OR 图进行自适应成本感知证明搜索

数学家重视证明的不仅仅是正确性：在正确的证明中，简单性、纯度以及找到它们的计算成本差异很大。然而，LLM 驱动的定理证明者主要寻找任何正确的证明，只有在找到正确的证明后才提高其质量。我们提出了 LEVER，一种证明搜索算法，可以使正确证明的目标可编程并在搜索过程中对其进行优化。 LEVER 通过 AND/OR 证明图对部分证明进行评分，将实现的目标值与开放子目标的预测相结合，因此目标在证明完成之前指导搜索。相同的机制优化了计算成本、证明长度、主题杂质，甚至它们的加权组合，而精益内核则强制正确性。在 Lean 4 的 PutnamBench 上，在匹配的预算下，LEVER 的成本比强大的单对话代理低 34%，同时将解决率从 80% 提高到 96%。在减少局部杂质方面，即证明偏离其定理主题有多远，它比事后重构有所改进（减少了 42% 对 33%），而成本只有三分之二甚至更多 可靠；在证明长度上，度量重构是为了它而构建的，它接近重构。改变目标的权重可以描绘出质量成本权衡曲线，因此用户可以选择更好的证明的价值。总体而言，LEVER 是一种高性能、经济高效且可调的证明搜索算法，用于导航正确证明的空间。