LeanSearch v2：精益 4 定理证明的全局前提检索

在 Lean 4 中证明定理通常需要识别一组分散的库引理，这些引理的联合使用可以实现简洁的证明——我们称之为全局前提检索的任务。现有工具解决相邻问题：语义搜索引擎找到与查询匹配的单独声明，而前提选择系统一次预测一个策略步骤中有用的引理。两者都无法恢复整个定理所需的完整前提集。我们推出了 LeanSearch v2，这是一个用于此任务的两种模式检索系统。其标准模式应用带有嵌入重排序管道的层次结构非正式化 Mathlib 语料库，无需特定领域的 微调 即可实现最先进的单查询检索（nDCG@10 为 0.62，而次优系统为 0.53）。其推理模式以标准模式为检索基础，通过迭代草图-检索-反思循环来针对全局前提检索。在研究级 Mathlib 定理的 69 个查询基准上，推理模式在 10 个检索到的候选中恢复了 46.1% 的 真值 前提组，在相同基准上优于强推理检索系统 (38.0%) 和前提选择基线 (9.3%)。在具有固定证明者循环的受控下游评估中，用 LeanSearch v2 替换替代 检索器 会产生最高的证明成功率（次优系统为 20%，而没有检索则为 4%），从而确认检索质量传播到证明生成。我们开源了所有代码、数据和基准。代码和数据：https://github.com/frenzymath/LeanSearch-v2。标准模式可通过 API 访问公开获取：https://leansearch.net/。