arXiv：cs.AI· Nihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang, Suman Jana·· 4 小时前
LEVER：在 AND/OR 图上进行自适应成本感知的证明搜索
LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs
AI 导读
LEVER 是一种证明搜索算法，将正确证明的目标（如计算成本、证明长度、主题纯度）设为可编程目标并在搜索过程中优化，由 Lean kernel 保证正确性。在 Lean 4 的 PutnamBench 上，相同预算下 LEVER 成本比强单轮对话智能体低 34%，求解率从 80% 提升至 96%。
正文
Abstract: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.
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.11862 [cs.AI] |
| (or arXiv:2610.11862v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.11862 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Nihal Jain [view email]
[v1]
Thu, 8 Oct 2026 12:40:14 UTC (109 KB)
来源：arXiv：cs.AI · arxiv.org