[论文] Lean Graph Search for Formal Theorem Proving

论文概要

研究领域: ML
作者: Yihan Xu, Jia-Chen Gu, Junyi Zhang, Di Wu, Haikang Deng, Po-Nien Kung, Kai-Wei Chang, Amit Sahai, Wei Wang, Nanyun Peng
发布时间: 2026-10-15
arXiv: 2610.22339

中文摘要

检索相关引理对形式化定理证明至关重要。最近的检索系统对声明间多跳依赖的利用有限。我们提出 LeanGraphSearch，这是一个用于 Lean 4 的基于图的检索方法，从 Mathlib 的前向依赖构建图并遍历它以通过多跳依赖链发现支撑引理。LeanGraphSearch 将每个声明链接到它依赖的前提，使用基于图的排序算法将相关性从语义匹配的声明传播到其依赖，并对扩展的候选重新排序。在两个数学检索基准上，LeanGraphSearch 在 MathlibQR 上比最强基线提高召回率达 12%，在 MathlibMPR 上覆盖了多达 3.7% 的额外证明路径组。将 LeanGraphSearch 集成到迭代证明循环中，在三个定理证明基准上将通过率提高多达 40%。

原文摘要

Retrieving relevant lemmas is crucial for formal theorem proving, enabling provers to build machine-checkable proofs from established mathematical results. Recent retrieval systems match library declarations to a target theorem or its intermediate proof steps, but make limited use of multi-hop dependencies among declarations. These dependencies can reveal supporting lemmas that are not necessarily lexically similar to the target theorem but recur in proofs of related problems. To this end, we propose LeanGraphSearch, a graph-based retrieval method for Lean 4 that constructs a graph from Mathlib's forward dependencies and traverses it to uncover supporting lemmas through multi-hop dependency chains. Specifically, LeanGraphSearch links each declaration to the premises it depends on, uses a g...

自动采集于 2026-10-17

#论文 #arXiv #ML #小凯