一句话总结

由华盛顿大学数学人工智能实验室提出的统一陈述级依赖图 TheoremGraph，从 arXiv 中解析出 $11.7\mathrm{M}$11.7M 个类定理环境，并从 $25$25 个 Lean 项目中提取出 Lean-Graph 的 $388,105$388,105 个声明节点和 $11.3\mathrm{M}$11.3M 条带类型边，通过嵌入式自然语言标语和 LLM 评判器将它们桥接起来，产生 $47,952$47,952 个余弦相似度高于 $0.8$0.8 的匹配（在 $\geq 0.9$≥0.9 的层级接受率上升至 $87\%$87%），并利用名称与签名表示及图扩展实现形式概念检索，在未使用语言模型重排器的情况下，$Recall@10$Recall@10 比 LeanSearch v2 的重排结果低 $0.5\mathrm{pp}$0.5pp 以内（$0.775$0.775 vs. $0.780$0.780），从而支持数学搜索与检索增强推理。

核心贡献

• TheoremGraph 将来自数学 arXiv 的 1170 万个类定理环境和 1830 万条候选有向依赖与 Lean-Graph 相结合。Lean-Graph 这一提取器能够捕获 25 个 Lean 项目中 388,105 个声明节点和 1130 万条带类型边，构成横跨非形式化与形式化数学的统一陈述级依赖图。
• 将生成的自然语言标语嵌入到共享语义空间，桥接了非形式化图与形式化图，产生 47,952 个由 LLM 评判器确认的、余弦相似度下限为 0.8 的匹配，评判器接受率从该下限的 48% 上升到相似度 ≥ 0.9 的配对的 87%。
• 采用带有基于图扩展的名称与签名表示，在形式概念检索上达到 0.775 的 Recall@10，比 LeanSearch v2 重排后的 0.780 低 0.5 个百分点以内，无需语言模型重排器；数据集、提取器、API 和 MCP 接口作为开放基础设施发布。

引言

数学本质上是一个由相互依赖的陈述构成的网络，但在实践中，研究者引用的是论文而非他们使用的具体引理或定理。这种粗糙处理模糊了归属关系，遮蔽了重复内容，并使得在陈述层面浏览文献变得困难。形式化证明助手（如 Lean）能够捕获精确的依赖结构，但其库仅覆盖现有数学的一小部分，并且没有统一的图能跨越非形式化和形式化两个世界。

先前的工作只解决了部分问题：数学信息检索处理符号公式，文献计量学对论文级引用进行建模，神经网络工具则面向定理证明或自动形式化。然而，这些方法并未在非形式化研究文章和形式化验证库之间连接细粒度依赖，从而限制了跨形式化检索和大规模依赖分析。

作者通过构建 TheoremGraph 来填补这一空白。它是一个陈述级依赖图，连接了来自 arXiv 的 1170 万个非形式化陈述（1830 万条边）与来自 Lean 及 25 个形式化项目的 388,105 个声明（1130 万条带类型边）。作者使用标语化的陈述表示在共享嵌入空间中对齐两个语料库，并由 LLM 评判器验证，产生超过 47,000 个高置信度的跨形式化匹配。这一统一资源改进了检索增强的自动形式化，其性能在无需重排器的情况下与专用重排器仅相差 0.5 个百分点，并以公开数据集、API 和 MCP 接口的形式发布。

数据集

作者构建了三个相互关联的数据集，将非形式化数学文本与形式化证明助手连接起来，为神经定理证明器和自动形式化系统提供资源。

• 非形式化图（arXiv 数学论文） 来源： arXiv Kaggle 元数据快照，筛选出标记为数学的论文及其 LaTeX 源码。 规模： 1170 万个类定理陈述和 1830 万条有向依赖边（涵盖论文内部和跨论文）。 提取与过滤： 基于正则表达式的解析器识别定理环境，并记录每个陈述的类型、引用编号、\label 键、正文、证明和局部上下文。剔除正文为空、数学分隔符不平衡、内容过短或子句截断的陈述。 边类型： 边被打上了提出该边的提取器标签：确定性（通过 arXiv ID 或标题匹配解析 \ref/\cite，并解析引用到陈述级别）、启发式（向后文档序引用、话语线索、散文中出现的定理名称）和记法（LLM 识别的记法定义与使用，链接到最近的先前定义）。每条边保留其提取器标签，让用户可以在覆盖率和精确度之间进行权衡；确定性边的验证精确度达到 98.8%。

• 形式化图（Lean 4 项目） 来源： 已编译的 Lean 4 项目，包括 Mathlib 版本 4.27–4.29 以及 24 个其他库。 规模： 388,105 个声明节点和 11,335,708 条带类型边（仅 Mathlib 内部就有 930 万条）。 提取： LeanGraph 作为 Lean 4 阐述器在核心 Environment API 上运行，从已阐述、类型检查的声明中提取依赖。只有通过结构谓词筛选的节点才会被包含，该谓词移除内核生成的工件（辅助递归器、匹配器声明等），保留面向用户的声明。匿名实例和策略对象保留元数据。 边类型： 六种语义类别：extends（继承）、field（结构体字段依赖）、sig（签名常量）、proof（证明项常量）、def（非 Prop 定义体）和 docref（文档字符串引用）。这种分类将结构性、类型级别、值级别和文档依赖区分开来。

• 桥接图（通用图） 构建： 将形式化声明标语和非形式化陈述标语嵌入到共享向量空间。对 385,657 个形式化声明中的每一个，通过余弦相似度检索最相似的非形式化标语（ann_k=50）。作者编写的蓝图配对作为真实标准：有标注的非形式化对象排名第一的概率为 43.5%，排进前 10 的概率为 69.9%，并且在相似度 ≥0.85 的顶级候选中，GPT-5.4 评判器确认 65% 为有效匹配（精确或非精确重述）。 精选匹配： 所有余弦相似度 ≥0.8 的候选均由 GPT-5.4 评判。在 100,799 个候选中，47,952 个（48%）被确认为匹配；确认率随相似度急剧上升（≥0.9 层级为 87%）。每条桥接边存储相似度分数、评判器的精确/非精确/错误标签以及确定性图上下文，从而实现高精度的跨模态链接。 预期用途： 桥接后的图为神经定理证明器和自动形式化系统提供了支架，将形式化声明所依赖的内容与使用或描述这些概念的非形式化数学连接起来。

方法

作者先基于 arXiv 论文构建非形式化图，再将其与 Lean 声明的形式化图桥接，从而构建全面的数学知识图。

对于非形式化图，作者解析了来自数学 arXiv 论文的 1170 万个类定理陈述。他们采用基于正则表达式的解析器识别类定理环境，捕获元数据、引用和 LaTeX 源码。依赖边通过三种方法提取：确定性提取器解析引用和引文，启发式提取器从附近引用和话语线索中添加边，以及记法提取器使用 LLM 将记法使用链接到先前定义。

为了统一非形式化与形式化图，作者将每条陈述映射到一个共享语义空间。它们为每条陈述生成一条标语，即由 LLM 生成的简洁自然语言摘要。对于非形式化陈述，采用递增提示链不断添加上下文，直到生成足够的摘要。随后，这些标语被嵌入 $\mathbb{R}^{4096}$R4096 空间，使用 Qwen3-Embedding-8B 进行嵌入并进行 $\ell_2$ℓ2​ 归一化。向量存储在带 HNSW 的索引中以支持高效检索。

为了桥接形式化和非形式化语料，作者实现了一条匹配流水线，以寻找表达相同数学结论的陈述对。

如下图所示：

流水线首先将 Lean 声明和 LaTeX 陈述标语化为普通英语描述。这些标语被嵌入到一个共享索引中。对每条形式化声明，系统通过排名第一的余弦相似度搜索检索最相似的非形式化标语，给出候选匹配。

为了验证这些匹配，使用 LLM 作为评判器（GPT-5.4）评估余弦相似度为 0.8 或更高的每个候选。评判器将配对标注为精确、非精确（泛化或特例）或错误。作者设定相似度下限为 0.8，以在保持精确度的同时捕获更广泛的非精确匹配，因为低于该阈值的产出率会急剧下降。

不同相似度区间的判断结果分布展示了这一方法的有效性。

如下图所示：

图表显示，随着余弦相似度增加，精确和非精确匹配的比例显著上升，而错误匹配减少。采用更严格的 GPT-5.4 评判器作为记录，以优先保证精确度，但同时也报告了更宽松的评判器用于高召回率比较。这种基于嵌入的匹配使形式化陈述能够通过相似度直接与非形式化对应物配对，无需共享词汇。

实验

检索增强形式化实验表明，添加基于标语的检索改善了 LLM 将非形式化数学重述为 Lean 的能力，在提高评估正确性的同时，使用的 token 和工具调用远比全库 grep 少，尽管仅凭类型检查是一个误导性的成功信号。与 LeanSearch‑v2 检索器的比较显示，仅嵌入标语的表现低于基线，但添加名称与签名表示、查询重写和名称匹配索引后，差距被弥合，在无需重排器的情况下达到更高的召回率和 nDCG。这些干预主要提升了标语表现不佳的声明类型（结构、类）的检索，而对定理的检索略有损失，且同样的调优配置不能迁移到链式前提检索，表明存在任务特定的权衡。

从描述性标语切换到名称与签名表示显著改善了检索排序，而保留标语或通过依赖图扩展则在排序代价较小的情况下带来了小幅召回率提升。这些变化主要惠及标语最薄弱的结构和定义等类别，对定理和实例检索影响甚微。使用名称与签名嵌入（配置 F）将 nDCG@10 从 0.494 提升至 0.558，Recall@10 从 0.657 提升至 0.733，在所有报告指标上均超过仅含检索器的基线。表示本身是排序提升的原因，因为配置 B 和 F 采用完全相同的搜索技术，唯一的区别在于嵌入的内容。混合回标语（配置 D）并添加图扩展（配置 E）将 Recall@10 提升至 0.775，但 nDCG@10 降至 0.548，接近重排后 0.780 的召回率而不使用重排器。图扩展在所有手段中贡献最小：从 D 到 E 时，Recall@10 增加了 +0.8 个百分点，而 nDCG@10 损失了 –0.2 个百分点。按声明类型来看，结构、类、定义和归纳类型从干预中获益最多，而定理和实例检索则略有下降，因为它们已经拥有较强的标语。

三个提取器贡献了重叠的非形式化依赖边集，记法提取器产生的边总数最多，且全部在同一篇论文内部。确定性提取器识别出最多的外部边，其中一部分指向具名定理。去重后，合并集包含 1832 万条边，以论文内部边为主。记法提取器产生最多边（788 万条），且全部为论文内部边。确定性提取捕获的外部边（192 万条）多于启发式提取（170 万条），其中 7.9 万条指向特定的定理。去重后，论文内部边（1486 万条）超过外部边（346 万条）四倍多。

一个基于 LLM 的评判器评估了从 500 篇 arXiv 论文提取的依赖边。确定性提取器几乎达到完美精确度（98.8% 验证通过），而启发式和记法提取器的精确度依次降低。合并去重后的整体精确度为 68.1%，但大量的依赖（6,372 条）仅被评判器发现，导致总体 F1 为 0.642。确定性提取最为可靠，其 98.8% 的边得到评判器确认，在重视精确度时可为用户提供高置信标签。提取器共同遗漏了 6,372 条评判器识别的边，表明在召回率上存在相当差距，仍有改进空间。

递增提示链为全部 1175 万条非形式化陈述生成了标语，多数在极少的上下文下即可解决。仅 1.9% 的陈述需要最终的强制回退，而 70.3% 仅凭陈述正文即已足够。这一增量策略仅在前一阶段自我标记为不足时才添加上下文，在不浪费计算的情况下确保覆盖。仅使用陈述正文时，70.3% 的标语生成已足够。标语充足率在强制回退前达到 98.1%，仅有 1.9% 需要最佳猜测补全。

当通过嵌入相似度将形式化 Lean 声明匹配到非形式化陈述时，只有极小部分达到了 0.90 以上的高余弦相似度。大多数成功匹配集中在 0.50 至 0.80 的中等区间，而超过 44% 的声明在默认检索深度下未找到邻居。更深入的检索显示，这些缺失的匹配通常反映的是确实不存在接近的非形式化对应物，而非检索范围的限制。极少一部分形式化声明获得了极高相似度的非形式化匹配，而大多数匹配落在 0.50–0.80 的中等区间，且有大量声明完全没有匹配。使用更大的候选列表进行更深探测后，大多数先前未匹配的声明得以恢复候选，但几乎没有超过 0.85 相似度的，这证实了缺失匹配指示的是非形式化覆盖的真实缺口，而非浅层检索。

评估分析了用名称与签名嵌入替代标语带来的检索改进、用于生成标语的递增提示链的有效性，以及从非形式化数学中提取依赖边的情况。名称与签名表示带来了最强的排序提升，尤其是在标语薄弱的类别上，而混合回标语或添加图扩展则在轻微排序代价下提供了适度的召回收益。提示链在强制回退前实现了 98.1% 的标语充足率，确定性边提取达到接近完美的精确度，但遗漏了许多边，表明存在召回缺口。将形式化声明与非形式化陈述匹配时，超过 44% 缺乏接近的对应物，证实了真实的覆盖缺口而非搜索局限。