数学家在评估证明时不仅看正确性，还关注简洁性、纯粹性以及寻找证明的计算成本。现有的基于大模型的定理证明系统往往只寻找任意正确的证明，质量提升只能在证明完成后再进行。LEVER 提出一种可编程的目标函数，在搜索过程中直接对正确证明进行优化。它在 AND/OR 证明图上为每个部分证明打分，结合已实现的目标值和对未完成子目标的预测，使得目标在完整证明出现前就能引导搜索。相同机制可用于最小化计算成本、证明长度、主题纯度以及它们的加权组合，Lean 核心保证所有证明的形式正确性。实验在 Lean 4 的 PutnamBench 上进行，预算相同的情况下，LEVER 的计算成本比强大的单轮对话代理低 34%，同时解题成功率从 80% 提升到 96%。在降低主题纯度（即证明偏离定理主题的程度）方面，LEVER 相比事后重构实现 42% 的下降（后者为 33%），且成本仅为后者的三分之二，且更可靠；在证明长度指标上，LEVER 的表现接近事后重构。通过调节目标函数的权重，可以绘制出质量‑成本的权衡曲线，用户可自行决定更好证明的价值。总体而言，LEVER 是一种高效、成本友好且可调的正确证明空间搜索算法。
点评