发表机构
Columbia University（哥伦比亚大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
LEVER是一种基于与/或图的自适应成本感知证明搜索算法，可在搜索中优化计算成本等多目标，在Lean 4的PutnamBench上成本降低34%、解决率提升至96%，还能优化证明质量与成本的权衡。
AI 中文摘要
数学家重视证明的价值不止于正确性：在所有正确的证明中，其简洁性、纯粹性以及寻找它们的计算成本存在巨大差异。然而，基于大语言模型（LLM）的定理证明器大多只搜索任意正确的证明，且仅在找到证明后才提升其质量。我们提出LEVER，一种可对正确证明的目标进行编程并在搜索过程中优化的证明搜索算法。LEVER在与/或证明图上对部分证明进行评分，结合已实现的目标值与开放子目标的预测值，因此目标能在证明完成前就引导搜索。该机制可优化计算成本、证明长度、主题不纯性，甚至它们的加权组合，同时Lean内核会强制执行正确性。在Lean 4的PutnamBench上，在匹配的预算下，LEVER的成本比强大的单对话智能体低34%，同时将解决率从80%提升至96%；在降低主题不纯性（即证明偏离其定理主题的程度）方面，它比事后重构（减少42% vs 33%）成本仅为其三分之二且更可靠；在证明长度（重构所针对的指标）上，它接近重构的效果。改变目标的权重可绘制出质量-成本权衡曲线，因此用户可选择更好的证明值得付出多少代价。总体而言，LEVER是一种用于探索正确证明空间的高性能、成本高效且可调整的证明搜索算法。
英文摘要
Mathematicians value proofs for more than correctness: among correct proofs, simplicity, purity and the computational cost of finding them vary widely. Yet LLM-powered theorem provers largely search for any correct proof, and improve its quality only after it is found. We propose LEVER, a proof search algorithm that makes the objective over correct proofs programmable and optimizes it during search. LEVER scores partial proofs over an AND/OR proof graph, combining realized objective values with predictions for open subgoals, so the objective guides search before a proof is complete. The same mechanism optimizes computational cost, proof length, topical impurity, and even their weighted combinations, while the Lean kernel enforces correctness. On PutnamBench in Lean 4, under matched budgets, LEVER costs 34% less than a strong single-conversation agent while raising the solve rate from 80% to 96%. On reducing topical impurity, i.e., how far a proof strays from its theorem's subject, it improves over post-hoc refactoring (42% reduction against 33%) at two-thirds of the cost and more reliably; on proof length, the metric refactoring is built for, it approaches refactoring. Varying the objective's weights traces a quality-cost trade-off curve, so the user can choose how much a better proof is worth. Overall, LEVER is a performant, cost-efficient and tunable proof search algorithm for navigating the space of correct proofs.
