arXiv cs.AI· Nihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang, Suman Jana·· 9 天前AI 评分27
LEVER：面向 AND/OR 图的自适应成本感知证明搜索
LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs
AI 导读
LEVER 是一种在搜索过程中直接优化证明目标的证明搜索算法，通过在 AND/OR 证明图上为部分证明打分，结合已实现目标值与未完成子目标的预测，让目标在证明完成前就引导搜索。
正文 · AI 翻译
摘要：数学家看重证明，不仅在于其正确性：在正确的证明中，简洁性、纯粹性以及找到它们所需的计算成本差异很大。然而，由 LLM 驱动的定理证明器大多只寻找任意一个正确的证明，并且只在找到之后才改进其质量。我们提出 LEVER，一种证明搜索算法，它使针对正确证明的目标可编程，并在搜索过程中对其进行优化。LEVER 在 AND/OR 证明图上对部分证明进行评分，将已实现的目标值与对未完成子目标的预测相结合，因此目标在证明完成之前就能引导搜索。同一机制可优化计算成本、证明长度、主题不纯度，甚至它们的加权组合，同时由 Lean 内核保证正确性。在 Lean 4 的 PutnamBench 上，在相同预算下，LEVER 的成本比一个强大的单轮对话智能体低 34%，同时将求解率从 80% 提高到 96%。在降低主题不纯度（即证明偏离其定理主题的程度）方面，它优于事后重构（降低 42% 对 33%），成本仅为三分之二且更可靠；在证明长度这一重构所针对的指标上，它接近重构的效果。改变目标的权重可以描绘出一条质量—成本权衡曲线，因此用户可以选择更好的证明值多少代价。总体而言，LEVER 是一种高性能、高成本效益且可调的证明搜索算法，用于在正确证明的空间中导航。
| 学科： | 人工智能（cs.AI） |
| 引用为： | arXiv:2610.11862 [cs.AI] |
| （或 arXiv:2610.11862v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.11862 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
来自：Nihal Jain [查看电子邮件]
[v1]
2026年10月8日星期四 12:40:14 UTC（109 KB）
来源：arXiv cs.AI · arxiv.org