TheoremGraph: 衔接形式化与非形式化数学

TL;DR TheoremGraph 构建了首个桥接非形式化 (arXiv) 与形式化 (Lean) 数学的统一语句级依赖图，通过语义嵌入和 LLM 评判实现跨语料匹配，为数学检索与推理提供新基础设施。

问题

问题背景

数学知识天然以定理为节点、以依赖关系为边构成图结构，但这一结构在不同载体中暴露得极不均匀：非正式论文仅提供文档级引用，而形式化库（如 Lean、Coq）则记录了精细的语句级依赖，但覆盖范围极窄。这导致数学信息的检索与推理长期被割裂在两个世界。

现有方法局限

• 非正式侧：传统数学检索（如 arXiv 论文搜索）依赖全文关键词或文档间引用，颗粒度粗，无法定位定理间的直接推导关系；基于 LLM 的提取虽可尝试解析依赖，但缺乏统一表示，且噪声高，难以规模化验证。
• 形式化侧：Lean 等系统的依赖图虽精确，却仅涵盖已被形式化验证的小量数学，且与自然语言表述完全解耦，形成孤岛。
• 跨侧对齐：现有工作多为单向“非正式→形式化”的翻译（如 autoformalization），或仅在封闭库内建模，缺乏一个统一图结构来同时承载两边节点及其语义链接。

为什么这个问题难且重要

技术挑战体现在三个层面：

1. 解析难度：非正式论文中定理环境多样，依赖关系常隐含在证明叙述里，没有显式“引用”标记，需用多策略提取器（正则、LLM、引用分析）综合处理 1170 万个定理环境，产生 1830 万候选边，每条边需标注可信度以供下游按需取舍。
2. 语义对齐：非正式定理的自然语言表述与形式化定义的代码符号距离极大，需通过生成自然语言 slogan 并嵌入共享语义空间，再用 LLM 评判器在余弦相似度 0.8 阈值下筛选出 4.8 万组匹配对，这一过程同时考验表示质量和评判可靠性。
3. 工程规模：构建并维护一个包含千级万节点、亿级边的知识图谱，并提供 HTTP API 与 MCP 接口，要求高效的数据管道、增量更新策略和检索性能优化。

业界关注度持续上升：自动定理证明、数学文献挖掘、检索增强推理等方向均需此类基础设施来突破“信息孤岛”瓶颈，TheoremGraph 首次将两个世界以图结构桥接，为下游任务（如前提选择、概念检索、文献溯源）提供了可复用的基础数据。

行业类比

这类似于软件工程中从代码函数调用图到文档知识图谱的融合：仅靠文档搜索无法理解函数间的真实依赖，仅靠代码分析又缺失高水平设计意图，唯有将两者链接为统一图，才能实现精准的语义级代码搜索与问答，TheoremGraph 正为数学领域完成了这一步。

核心洞察

• TheoremGraph 通过生成自然语言标语（slogan）将非正式论文的声明与形式库的条目投影到统一语义空间，实现跨模态对齐。有别于现有工作仅聚焦单侧（非正式引文网络或形式依赖图），该方案无需人工标注等价关系，仅依靠嵌入和 LLM 裁判即可建立 4.8 万对较高置信度的连接，为检索增强定理证明和自动形式化提供了可扩展的信号源。
• 在 Lean 概念检索任务中，单纯使用名称与类型签名加图结构扩展（无 LM 重排序器）即可达到 Recall@10 0.775，与 LeanSearch v2 的重排序结果（0.780）几乎持平。这表明从依赖图中提取的局部结构特征能有效弥补简单文本表征的不足，为工程中平衡检索精度与推理开销提供了新思路：结构感知的图检索可能是语义模型重排序的低成本替代方案。

方法

整体流水线：从非正式论文与形式化库到统一依赖图

输入 包含两类语料：arXiv 数学类论文（非正式数学，含定理环境等结构化文本块）与多个 Lean 4 项目（形式化数学，含声明节点与有类型依赖边）。

关键模块

1. 非形式图构建 (Informal Graph)：从 11.7M 定理式环境中利用多种提取器恢复 18.3M 条候选有向依赖，每条边标记其来源提取器，允许使用者按精度/覆盖偏好过滤。提取器可能基于引用线索、邻近语义、或数学“证明里引用”的模式，通过消歧和准入控制提升可信度。

2. 形式图构建 (Formal Graph)：发布 LeanGraph 提取器，在 Lean 4 elaborator 级别解析声明间的依赖关系，输出 388,105 个节点和 11.3M 条类型化边（如定义依赖、定理依赖等），覆盖 25 个 Lean 库。

3. 共享语义空间与桥接：为每个语句生成自然语言 slogan（一句话概括），通过嵌入模型映射到同一语义空间。使用余弦相似度（≥0.8 作为 floor）跨图链接相关陈述，再由 LLM 裁判 确认匹配质量：floor 以上 48% 被接受，≥0.9 区间接受率升至 87%，最终得到 47,952 条高质量跨图匹配。

输出 — 统一的 TheoremGraph：一个融合非形式与形式数学的语句级依赖图，提供 HTTP API 与 MCP 接口，支持数学搜索、归因及检索增强推理。

与同类方法的差异：不同于仅利用文档级引用网络或纯形式库内部依赖的工具，TheoremGraph 首次在语句粒度桥接非正式与正式数学，并引入 slogan 语义对齐 + LLM 裁判的二阶段过滤，在检索精度与链接可信度之间取得灵活平衡。

实验

实验设计

TheoremGraph 构建两步：先从 arXiv 非正式论文中解析 11.7M 定理环境，恢复 18.3M 候选依赖边（由多个提取器标注来源）；再以 LeanGraph 抽取 388k 声明节点 与 11.3M 类型边 构建正式图。二者通过为每个定理生成自然语言「标语」嵌入共享语义空间，实现跨语料对齐。桥接评估中，设定余弦阈值，用 LLM 裁判 裁定匹配质量，统计各区间接受率。概念检索实验在 Mathlib 基准上对比 LeanSearch v2，仅使用名称+签名+图扩展表示（无 LM 重排序），并测试在 MathlibMPR 上的迁移性。附加消融探究图扩展与引用链对召回的影响。

关键发现

跨模态桥梁在 余弦 0.8 以上捕获 47,952 对匹配，裁判接受率从基线的 48% 显著跃升至 ≥0.9 区间的 87%，证实语义空间有效连接非正式/正式数学。正式检索中，纯表示+图扩展方案达到 Recall@10 0.775，与 LeanSearch v2 重排序结果（0.780）仅差 0.5pp，无需额外 LM 重排器即可接近最优。此外，引用图扩展能找回嵌入搜索遗漏的依赖，提升命题选择质量。

与基线对比解读

TheoremGraph 的核心突破在于 统一图与跨领域连接，这是 LeanSearch v2 等纯形式库引擎所不具备的。虽然检索指标略低 0.5pp，但省略 LM 重排器大幅简化流水线、降低推理开销，且差距可能通过更精细的图算法弥补。其真正优势在于桥接能力：允许非正式论文中的定理直接检索对应的形式化版本，为自动形式化与文献溯源打开新路径。这一工作将数学知识从文档级引用提升到语句级依赖图，为新一代数学 AI 基础设施提供了标准化数据与 API。

行业影响

落地场景

TheoremGraph 提供的统一数学依赖图可嵌入多种知识密集型产品：

• 智能 IDE 与定理证明助手：如 Lean 4 环境可直接集成 LeanGraph，在编辑器内实现语义级定理推荐、反例搜索与依赖可视化。
• 学术搜索与文献管理工具：在 Semantic Scholar、Zotero 等平台中，用图谱增强引用导航：从粗粒度文档引文升级到语句级依赖，帮助研究者快速定位关键引理与变体。
• 数学教育平台：为习题推荐系统提供知识图谱，动态生成知识点链路与个性化练习。
• LLM 驱动的数学搜索引擎：利用自然语言 slogan 检索形式化定理，支持用户用口语化查询直接定位可复用的形式化代码。

商业价值

• 降本增效：自动化抽取 11.7M 定理级依赖，省去人工标注高成本；LeanGraph 的边缘直接来源于 elaborator，无需额外推理，可显著降低知识库维护成本。
• 提升体验与增收：在数学问答、论文写作工具中集成该图谱，可提供更精准的参考和引用建议，提高用户粘性；对需要严谨数学推理的垂直领域（如加密、金融建模）可构建高壁垒服务。
• 差异化竞争优势：目前大多数通用搜索和 RAG 系统仅捕捉文档或段落级关联，TheoremGraph 深入到陈述级并桥接形式与非形式数学，为需要高可信度的领域提供独特价值。

与现有产品/工作流的接口

• HTTP API 与 MCP 接口：已发布的标准接口使任何支持 REST 或流式工具调用的系统（如 ChatGPT 插件、Copilot 扩展）可直接查询图谱。
• 检索增强生成（RAG）：可将图谱节点作为向量数据库中的元数据，或在检索阶段用图扩展（graph expansion）召回相关定理，补强现有文本检索；实验显示图扩展可将 Recall@10 提升至 0.775，逼近带重排的专有系统。
• 形式化项目 CI/CD：在 Lean 项目的 CI 管线中集成 LeanGraph，自动检测声明变更的影响范围，生成依赖报告。

具体用例

1. 企业级数学建模平台（如金融定价模型验证）： 量化团队用自然语言查询“Black-Scholes 公式的扩展形式”，API 返回 Lean 中已形式化的声明及非形式化论文片段。可直接将形式化代码嵌入可信验证流程，减少人工校对成本，并确保模型无逻辑漏洞。
2. 在线教育自适应学习： 智能习题平台根据学生当前掌握的定义/定理节点，用图扩展推荐下一步需要学习的引理。例如，学生在“线性子空间”上卡住时，系统沿依赖边反查建议“向量空间公理”回顾，提升学习路径合理性。

局限

• 数据提取和依赖关系的精度: 从 arXiv 提取的非形式化定理陈述和依赖关系依赖于多个提取器, 每个提取器具有不同的精度和覆盖率。论文为每个候选边标记了提取器, 允许下游用户进行权衡, 但这意味着图结构本身包含噪声。对于某些依赖关系, 提取可能是错误或缺失的, 从而影响依赖图的完整性和准确性, 特别是在需要高精度关系的应用(如前提选择)中可能不可靠。
• LLM 评判的局限性: 跨形式化与非形式化语句的匹配依赖 LLM 评判器, 其评判标准可能带有内在偏差, 且评判准确性受提示设计和模型选择影响。在 0.8 余弦阈值下, 评判接受率仅 48%, 表明候选匹配中仍有大量低质量对齐。提高阈值可提升接受率至 87%, 但会严重降低召回率, 限制了大规模自动挖掘的对齐数量。此外, LLM 评判可能无法处理复杂的数学定义等价性, 导致漏判。
• 与现有检索系统的比较: 尽管在 Lean 形式化概念检索上, 带有图扩展的 name-and-signature 表示达到了接近 LeanSearch v2 的 Recall@10 (0.775 vs 0.780), 但没有 LM 重排序的情况下并未超越现有系统。图扩展方法可能引入额外计算开销, 且尚未在更大规模或跨学科场景中进行验证。对于非 arXiv 来源的数学文献, 提取性能下降(附录 D 中提到定义准确率受作者风格影响), 限制了该方法的通用性。