用于形式化定理证明的Lean图搜索
Lean Graph Search for Formal Theorem Proving
AI总结：
针对形式化定理证明中多跳依赖利用不足的问题，提出LeanGraphSearch方法，通过构建Mathlib依赖图并结合图排序与重排序，在检索基准和端到端定理证明任务中均实现了性能提升。
摘要：
检索相关引理对于形式化定理证明至关重要，它能让证明器基于已有的数学结果构建可被机器验证的证明。近期的检索系统会将库声明与目标定理或其中间证明步骤进行匹配，但对声明间的多跳依赖关系利用有限。这些依赖关系能揭示出与目标定理在词汇上未必相似、却在相关问题的证明中反复出现的支撑引理。为此，我们提出LeanGraphSearch，这是一种针对Lean 4的基于图的检索方法，它从Mathlib的前向依赖关系构建图，并通过多跳依赖链遍历图以挖掘支撑引理。具体而言，LeanGraphSearch将每个声明与其依赖的前提关联，使用基于图的排序算法将相关性从语义匹配的声明传播到其依赖项，并对扩展后的候选与原始查询进行重新排序。在两个数学检索基准测试中，LeanGraphSearch在MathlibQR上的召回率比最强基线LeanSearch v2提升了12%，在MathlibMPR上增加了完整带注释证明路径的覆盖范围，覆盖了多达3.7%的额外组。更重要的是，我们通过将LeanGraphSearch集成到由Lean反馈引导的迭代证明循环中，评估这些检索增益是否能转化为端到端定理证明的提升。在三个定理证明基准测试中，LeanGraphSearch在{8,16,32}次反思轮次下的通过率比普通证明器提升了多达40%，比LeanSearch v2最多提升了10%，展现出更高的准确率-成本效率。这些发现凸显了依赖图搜索对定理证明的价值，并为基于结构的证明发现搜索的进一步研究提供了动力。
英文摘要：
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 graph-based ranking algorithm to propagate relevance from semantically matched declarations to their dependencies, and reranks the expanded candidates against the original query. Across two mathematical retrieval benchmarks, LeanGraphSearch improves recall by up to 12% over the strongest baseline, LeanSearch v2, on MathlibQR and increases coverage of complete annotated proof routes on MathlibMPR, covering up to 3.7% of extra groups. More importantly, we evaluate whether these retrieval gains translate into improved end-to-end theorem proving by integrating LeanGraphSearch into an iterative proving loop guided by Lean feedback. Across three theorem proving benchmarks, LeanGraphSearch improves pass rate at {8, 16, 32} reflection turns by as much as 40% compared to vanilla prover and at most 10% compared to LeanSearch v2, showing higher accuracy-cost efficiency. These findings highlight the value of dependency graph search for theorem proving and motivate further research on structure-aware search for proof discovery.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
