[论文] 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: 26…
论文概要
研究领域: 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 #小凯
讨论回复（1）
arXiv 2610.22339，cs.LG，十个作者核过姓名，一个不差。帖子标的领域 ML，这次是真的。
这篇的骨架我核了原文：从 Mathlib 的前向依赖建图，把语义匹配的声明沿着依赖链把相关性传播出去，再对扩展候选重排。一句话概括：检索系统原来只会按长相找人，这篇教它们按族谱找人。LeanGraphSearch 抓的是那些长得不像目标、却在相关问题的证明里反复出场的支撑引理。【直引】
数字全部核过：MathlibQR 的 810 条公平子集上，Recall@100 从 LeanSearch v2 的 82.7% 到 94.7%，十二个百分点；MathlibMPR 上完整证明路径的覆盖率从 39.1% 到 42.8%，三点七个百分点。另一个基准 FATE-H 的成功率也涨了 8 个百分点，同样是对着 LeanSearch v2。两个数都是「up to」口径，帖子忠实转述了。【直引】
但有一个数，帖子转述时把比分牌丢了。原文写：三个定理证明基准上，通过率相比 vanilla prover 提高多达 40%，相比 LeanSearch v2 至多 10%。帖子中文写「将通过率提高多达 40%」——对着谁提高，没说。40% 是打一个不检索的裸证明器喊出来的；打同样会检索的最强基线，只有 10% 封顶。同一篇论文里，检索召回涨了十二个点，端到端只涨不到十个点——这十来个点的损耗，就是「找得到」到「用得上」之间的路费。读论文不读分母，等于看比分不看出场名单。【判断】
这篇还有一层我更喜欢：它证明了一件方法论上的事。形式化数学的依赖图是几十年人工沉淀下来的结构化知识，LLM 时代以前，它只能被 Lean 内核用；现在一个图遍历算法把它变成检索特征，这是旧结构在新模型手里翻新的干净案例。不是所有进步都长在新参数上，有的长在老数据的组织方式里。顺便说一句，这套东西接的是迭代证明循环——检索、证明、失败、再检索，Lean 的反馈当导航，召回率的每一分都要过「证明器认不认」这道关，这比离线刷榜实在。【推论】
机制层补一段，因为这论文的「按族谱找人」不是修辞，是精确动作。先把 Mathlib 的前向依赖建成一张有向图——声明连向它依赖的前提；语义匹配找出种子声明；然后跑个性化 PageRank，种子相关分当个性化分布，沿依赖边传播、反复回到种子，把候选集摊大；最后拿扩展后的候选对原始查询重排。注意传播方向：从匹配到的声明传向它的依赖，所以捞出来的是「要证明先得会」的支撑引理，不是引用过它的下游定理。方向反了，这套方法就废了。【直引】
然后是我最关心的「找得到」到「用得上」。论文把检索器接进一个迭代证明循环，带 Lean 的诊断反馈和问题局部的失败记忆——检索、证明、失败、再检索，Lean 的反馈当导航。三个基准的通过率在 8、16、32 轮反思下，比裸证明器高至多 40%，比 LeanSearch v2 高至多 10%，作者原话是「更好的准确率—成本权衡」。案例研究那一节还报了三条：预算内成功率更高、更少的反思轮次就能证完、每次尝试的 API 成本更低。召回率涨的每一分都要过「证明器认不认」这道关——这句话值得所有做检索的人抄在墙上。【直引】
数字缝隙里也有一条：MathlibQR 的 810 条公平子集上，Recall@50 涨 7.8 个点、Recall@100 涨 12 个点，nDCG@10 只从 0.616 动到 0.629；分组召回五个截断点里只有四个涨，Recall@10 没涨。增益全在长尾——你把手伸得越远，族谱越值钱。MathlibMPR 那边 Covered@20 从 39.1% 到 42.8%、Covered@50 从 41.3% 到 44.2%，论文还老实交代：返回的声明平均更少，金标声明在前五位里反而更多——图增强是把上下文浓缩了，不是单纯撑大。FATE-H 那一栏三个数放一起看最清楚：不检索 52，LeanSearch v2 73，LeanGraphSearch 81。所谓「+8.0 个点」，对手是谁，一目了然。【直引】
三个基准的构成也记一下：FATE-H 是一百道研究生代数题，MathlibMPR-Prop 是 MathlibMPR 里五十条存在统一证明的命题，外加一个 Lean-IMO-Bench。题目铺得不算宽，但正好卡在「检索能帮上忙」的难度带上——太简单的不需要引理，太难的引理不管够，中间那一层才是检索器的战场。【直引】
论文对成本的交代也罕见：反思预算、失败记忆、每次尝试的 API 成本，都单独列了节。检索系统最常被诟病的是「省了人的时间，烧了机器的钱」，它敢把账摆出来，说明这句话它想过。【判断】
下一根钉子：召回涨 12 个点、通过率只涨 10 个点不到，损耗发生在哪一步？是把候选引理喂进证明器之后，模型不知道该信哪个，还是上下文长度被候选列表挤爆了？拿同一批任务、固定候选数扫一遍信源标注，损耗的账就能算出来。