LeanGraphSearch：依赖图搜索提升定理证明检索与通过率

形式化定理证明的难点往往不在于推理本身，而在于从庞大的数学库中找出能用的引理。检索到的引理是否相关，直接决定了证明器能否构建出机器可验证的证明。现有检索系统大多把库声明与目标定理或其当前证明步骤做语义匹配，但忽略声明之间的多跳依赖关系——那些与目标定理字面并不相似、却在相关问题证明中反复出现的支持性引理。LeanGraphSearch 正是冲着这一缺口提出的图检索方法。

检索的盲区：为什么字面匹配不够用

传统检索假设"语义相似"约等于"有用"。在 Lean 4 的 Mathlib 中，一个目标定理的证明往往需要调用一串间接依赖的引理，它们与目标定理的词汇重合度很低，却构成证明的关键链条。仅靠对目标定理做语义匹配，很难把这些"埋得深"的引理召回。依赖图提供了另一条线索：如果某个声明与目标定理高度相关，那么它所依赖的前提很可能同样值得考虑，这些前提又依赖更深一层的声明。

LeanGraphSearch 的核心判断是，证明发现本质上是一个结构感知的搜索问题，而不只是文本相似度排序问题。依赖关系把松散的字面匹配变成了可传播的相关性信号。

Mathlib 是 Lean 4 的数学库，也是当前形式化数学领域规模最大的统一库之一，涵盖从基础代数、分析到拓扑、数论的大量定理与结构。它包含数以十万计的声明（definition、theorem、lemma 等），每个声明都以依赖关系链接到它使用的前提。正因规模庞大，人工记忆或纯语义检索都难以在证明时快速定位合适引理。Mathlib 的声明具有高度模块化特征：一个高层定理往往依赖若干中间引理，而这些中间引理又依赖更基础的结论，形成深链条。这种组织方式让基于依赖图的检索成为可能，也意味着"语义相似"与"证明有用"之间存在系统性偏差。

多跳依赖 指从目标声明出发，经过一条或多条依赖边才能到达的间接前提。例如目标定理 A 直接依赖 B，B 依赖 C，C 依赖 D；在证明 A 时，D 可能以辅助引理的身份出现，但 A 与 D 的字面相似度可能极低。传统语义检索通常只对 A 与候选声明做单轮相似度排序，因此容易漏掉 C、D 这类位于依赖链深处的关键支持引理。多跳传播的目的正是利用"A 相关则 A 的前提也值得考虑"这一结构假设，把相关性从锚点沿依赖边逐步扩散，从而召回单轮匹配无法覆盖的候选。

方法：从链接着手，做多跳传播与重排

LeanGraphSearch 为 Lean 4 构建了一张来自 Mathlib 前向依赖的图：每个声明都链接到它所依赖的前提。在这张图上，算法先做一次语义匹配，找出与目标查询语义相近的声明作为起点，然后用图排序算法把相关性从这些起点沿着依赖边向外传播到它们的前提，从而扩展到字面不相似但结构上相关的候选引理。最后，系统把扩展后的候选集合与原始查询重新排序，输出最终检索结果。

这条流水线可以概括为三步：语义匹配定位锚点、依赖图传播挖出多跳支持引理、重排控制精度。相比直接检索，它更依赖库本身的结构信息，而不是单纯堆叠更大的语义模型。

图排序算法 在这里的作用是把初始的语义匹配分数当作节点上的种子信号，再根据依赖图的结构把分数传播到相邻节点。常见做法包括 Personalized PageRank、随机游走或带衰减的加权传播：节点与查询语义越接近、与高相关节点的依赖路径越短，最终得分越高。与纯语义相似度不同，图排序引入了结构先验——即"被相关声明依赖的前提也倾向相关"。在 LeanGraphSearch 中，传播方向沿前向依赖边（声明指向其前提），因此分数会从语义锚点向更深层前提扩散。传播后的候选集再与原始查询重新排序，相当于用结构信号修正语义排序，兼顾召回与精度。

前向依赖图 中，边从声明指向它所引用的前提，方向与证明中"从目标到子目标"的拆解方向一致。与之相对，反向依赖图会从前提指向使用它的声明。选择前向图的原因在于检索目标是"为证明目标找可用引理"，即沿着目标需要的支持链条向下挖掘；而反向图更适合找"哪些定理用到了某个声明"。LeanGraphSearch 使用前向依赖，使传播自然沿着证明所需的依赖链展开，从而更可能覆盖完整证明路径上的中间引理，而不是仅仅召回与目标同层的相似声明。

检索指标：召回率与完整证明路径覆盖

在数学检索基准上，LeanGraphSearch 相对最强基线 LeanSearch v2 有明显提升。在 MathlibQR 上召回率最高提升 12%；在 MathlibMPR 上，它对完整标注证明路径的覆盖增加，额外覆盖了最多 3.7% 的问题组。这两项指标从不同角度说明：依赖图搜索确实能捞回那些语义匹配漏掉的支持引理，而且这些引理往往位于完整证明路径上，而不是无关噪声。

端到端验证：检索增益能否转化为证明能力

检索指标好看不等于证明器更强。作者把 LeanGraphSearch 接入一个由 Lean 反馈引导的迭代证明循环，在三个定理证明基准上评估端到端通过率。结果显示，在 {8, 16, 32} 个反射轮次下，LeanGraphSearch 相比普通证明器通过率最高提升 40%，相比 LeanSearch v2 最多提升 10%。更重要的是准确率与成本的效率比更优：这意味着提升不只来自更多轮次或更大计算量，部分收益来自检索质量本身。

这里的一个隐含结论是，检索与证明的耦合方式会影响最终效果。把图检索直接放进以 Lean 反馈为信号的迭代循环里，检索到的引理会随着证明状态变化被反复利用，结构信息因此能持续发挥作用。

Lean 反馈引导的迭代证明循环 指证明器在每一轮尝试中调用 Lean 内核检查当前证明状态，若失败则根据错误信息、未解决目标或剩余假设生成新的检索查询，再次调用引理检索并更新证明脚本，如此反复。反射轮次（reflection rounds）即该循环的迭代次数，常见设置为 8、16、32 轮。由于每轮都会产生新的子目标或证明状态，检索查询也随之变化，因此检索器不能只做一次静态匹配，而要在循环中反复提供与当前状态相关的引理。LeanGraphSearch 的图传播结果在这种循环里被多次复用，结构信息得以持续影响后续轮次的候选选择，这也是检索质量能部分转化为端到端通过率提升的原因。

结构感知搜索的意义

LeanGraphSearch 的结果指向一个更广的研究方向：证明发现需要结构感知的搜索，而依赖图是其中一种有效结构。它揭示的不只是"检索可以更好"，而是"检索应该和证明过程共同设计"。当检索器理解了声明之间的依赖拓扑，它召回的不再是孤立的相似文本，而是能支撑证明链条的候选集合。

对形式化数学和 AI 辅助证明而言，这类方法的潜在价值在于可扩展性：依赖图来自库本身，不需要额外标注；传播与重排也相对轻量。后续值得关注的是，这种图检索能否推广到 Mathlib 之外的库，以及它与其他结构信号（如证明脚本的抽象层次）结合后能走多远。