LeanGraphSearch
一种面向形式化定理证明的依赖图检索方法，通过语义匹配定位锚点并沿前向依赖图做多跳相关性传播，再重排候选引理，以提升引理检索召回率与证明通过率
时间轴 (近 90 天)
LeanGraphSearch 是一种针对 Lean 4 形式化定理证明的图检索方法，通过构建来自 Mathlib 前向依赖的图，先做语义匹配定位锚点，再用图排序算法沿依赖边传播相关性，最后重排候选集。
在 MathlibQR 基准上，LeanGraphSearch 相对最强基线 LeanSearch v2 的召回率最高提升 12%。
在 MathlibMPR 基准上，LeanGraphSearch 对完整标注证明路径的覆盖额外增加了最多 3.7% 的问题组。
在 {8, 16, 32} 个反射轮次下进行端到端评估，LeanGraphSearch 相比普通证明器通过率最高提升 40%，相比 LeanSearch v2 最多提升 10%。
LeanGraphSearch 使用前向依赖图（边从声明指向其引用的前提），传播方向沿证明中从目标到子目标的拆解方向一致，以便覆盖完整证明路径上的中间引理。
LeanGraphSearch 的核心判断是：证明发现本质上是一个结构感知的搜索问题，而不仅是文本相似度排序问题。
LeanGraphSearch 的图排序算法可使用 Personalized PageRank、随机游走或带衰减的加权传播等方法，将语义匹配分数作为种子信号沿前向依赖边传播。
LeanGraphSearch 的依赖图来自 Mathlib 本身，不需要额外标注，传播与重排相对轻量，因此具有可扩展性潜力。
LeanGraphSearch 在端到端评估中准确率与成本的效率比更优，表明通过率提升不只是来自更多轮次或更大计算量，部分收益来自检索质量本身。
全部知识事实 (9)
LeanGraphSearch 是一种针对 Lean 4 形式化定理证明的图检索方法，通过构建来自 Mathlib 前向依赖的图，先做语义匹配定位锚点，再用图排序算法沿依赖边传播相关性，最后重排候选集。
50%待验证在 MathlibQR 基准上，LeanGraphSearch 相对最强基线 LeanSearch v2 的召回率最高提升 12%。
50%待验证在 MathlibMPR 基准上，LeanGraphSearch 对完整标注证明路径的覆盖额外增加了最多 3.7% 的问题组。
50%待验证在 {8, 16, 32} 个反射轮次下进行端到端评估，LeanGraphSearch 相比普通证明器通过率最高提升 40%，相比 LeanSearch v2 最多提升 10%。
50%待验证LeanGraphSearch 使用前向依赖图（边从声明指向其引用的前提），传播方向沿证明中从目标到子目标的拆解方向一致，以便覆盖完整证明路径上的中间引理。
50%待验证LeanGraphSearch 的核心判断是：证明发现本质上是一个结构感知的搜索问题，而不仅是文本相似度排序问题。
50%待验证LeanGraphSearch 的图排序算法可使用 Personalized PageRank、随机游走或带衰减的加权传播等方法，将语义匹配分数作为种子信号沿前向依赖边传播。
50%待验证LeanGraphSearch 的依赖图来自 Mathlib 本身，不需要额外标注，传播与重排相对轻量，因此具有可扩展性潜力。
50%待验证LeanGraphSearch 在端到端评估中准确率与成本的效率比更优，表明通过率提升不只是来自更多轮次或更大计算量，部分收益来自检索质量本身。
50%