LEVER：在 AND/OR 图上做自适应成本感知的证明搜索

LEVER 是一种可在搜索过程中优化证明目标的证明搜索算法，它在 AND/OR 证明图上为部分证明打分，结合已实现的目标值与未完成子目标的预测，让目标在证明完成前就引导搜索。在 Lean 4 的 PutnamBench 上，相同预算下 LEVER 成本比强单轮对话智能体低 34%，求解率从 80% 提升到 96%；在降低主题杂质上，它以三分之二成本实现 42% 的降幅，优于事后重构的 33%。