TheoremGraph：桥接形式化与非形式化数学 TheoremGraph: Bridging Formal and Informal Mathematics
构建统一数学陈述级依赖图，连接arXiv非形式化论文与Lean形式化定理库
前置知识
Proof Assistant
证明助手如Lean、Coq是软件系统，允许数学家用形式化语言表达定义、定理和证明，并由可信内核验证逻辑正确性。Lean基于构造演算，通过类型系统编码逻辑，证明是构造特定类型的程序。形式化要求明确指定每个逻辑依赖，揭示了数学论证的细粒度依赖结构，但与人类数学写作相比过程繁琐且覆盖范围有限。截至2026年，Lean的数学库mathlib4包含超过40万个形式化定义、引理、定理和证明，覆盖代数、拓扑、分析和数论等领域。这种形式化库虽然增长迅速，但仍然比非形式化数学知识体小得多且不那么全面。在形式化证明中，必须指定每个逻辑依赖和足够的中间结构以被内核类型检查，公式表示为 P 推出 Q 的形式。
本文的核心是连接非形式化数学写作与形式化证明库，需要理解形式化系统如何组织数学知识以及与非形式化表示的差异。LeanGraph从Lean4精化后的声明提取依赖，这是论文形式化图部分的基础，理解证明助手的工作原理对于理解论文的技术路线至关重要。
Dependency Graph
依赖图是有向图，节点表示数学陈述（定理、引理、定义），边表示依赖关系（定理A引用定理B）。在形式化数学中，依赖关系显式记录在证明中，而在非形式化论文中则通过引用、隐含知识等方式呈现。依赖图结构可用于分析数学文献的影响传播、知识演化，并为定理证明系统提供前提选择的基础。本文的非形式化图边陈述比约为1.56，而形式化图约为29.2，反映了形式化数学的细粒度依赖记录。这种密度差异揭示了两种表示方式的本质区别，形式化系统记录了所有逻辑步骤，而非形式化写作则省略了专家读者可以补全的背景知识。图的距离可以表示为 d(u,v)，表示从节点u到节点v的最短路径长度。
本文的核心贡献就是构建数学陈述级依赖图，跨越形式化和非形式化两个领域。理解依赖图是评估其规模、密度和应用价值的基础。论文分析了1170万非形式化陈述和1830万依赖边，以及38.8万形式化声明和1130万类型边，这些规模前所未有。
Dense Retrieval
稠密检索通过将文本编码为连续向量，然后使用向量相似度如余弦相似度进行匹配，相比传统关键词检索能捕捉语义相关性。在数学领域，因为数学符号和公式无法用关键词充分表达，稠密检索尤为重要。本文使用Qwen3-Embedding-8B将数学陈述的slogan编码为R4096维向量并L2归一化，然后使用HNSW索引进行快速候选生成。向量存储在pgvector中，并使用二值量化投影进行快速候选生成。余弦相似度计算公式为 sim(u,v) 等于 u点积v除以u的范数乘以v的范数。这种方法使得跨模态匹配成为可能，因为形式化和非形式化陈述可以在同一向量空间中比较。
论文使用稠密检索连接形式化和非形式化陈述，通过向量相似度发现语义等价的数学陈述。理解稠密检索是理解论文匹配pipeline的关键。论文将两种图嵌入到同一空间，使跨模态匹配成为最近邻查询，这是论文技术创新的核心。
Statement Slogan
Slogan是对一个数学陈述的简洁、独立、自然语言摘要。论文使用LLM如Qwen3-235B-A22B-Instruct-2507为每个定理生成slogan，将形式化的Lean声明和非形式化的LaTeX定理都转化为统一的自然语言表示。非形式化slogan使用渐进式提示链生成，仅在先前尝试被自标记为不足时添加上下文，添加顺序包括陈述正文、证明和本地上下文、邻近陈述和出边依赖、最后强制最佳猜测slogan。形式化slogan通过语义角色排名出边依赖并打包最高优先级的数学信息上下文。Slogan损失了细节但保留了核心语义，使得跨模态匹配成为可能。生成过程可以表示为 s 等于 SloganGen(c,theta)，其中c是陈述内容，theta是模型参数。
Slogan是论文跨模态匹配的基础，将不同表示的数学陈述统一到同一嵌入空间中。理解slogan的生成过程和权衡是理解论文方法的关键。口号化的有损特性是论文局限性的来源之一，但通过渐进式生成确保了高质量覆盖。
研究动机
数学知识结构以陈述及其依赖关系为核心，但在现有文献中这种结构暴露不充分。非形式化论文主要在文档级别引用，而形式化库记录细粒度依赖但覆盖范围小。作者引用论文而非具体引理、定义或定理，部分原因是因为专家读者被期望提供相关背景。这种实践避免了显式依赖注释的负担，但使数学知识结构变得粗糙，归属可能模糊或不精确，相关工作可能被重复。在一项被撤回arXiv提交的大规模研究中，百分之2.4的被分类撤回是作者自我标识为不新颖的案例，反映出工作后来被判断为重复或缺乏相对于现有结果的原创性。证明助手已成为使数学验证更严格和明确的重要工具，这些系统允许数学家用形式化语言表达定义、定理和证明，其正确性可由可信内核验证。与非形式化证明相比，其中对先前结果的引用和常规中间论证往往被隐含，形式化证明必须指定每个逻辑依赖和足够的中间结构以被内核类型检查。因此，形式化揭示了数学论证底层的细粒度依赖结构。Lean是最突出的现代证明助手之一，基于构造演算，并由活跃的开源生态系统支持。Lean的数学库mathlib4包含超过40万个形式化定义、引理、定理和证明，由社区在代数、拓扑、分析和数论等数学领域贡献。尽管这种快速增长，形式化数学仍然比非形式化数学知识体小得多且不那么全面。
本文的目标是构建一个统一的陈述级依赖图，跨越非形式化和形式化数学。从非形式化侧，解析arXiv数学论文中的1170万个类定理环境，恢复1830万个候选有向依赖边，每个边都由提出它的提取器标记，以便下游用户可以在覆盖和精度之间权衡。从形式化侧，发布LeanGraph，一个Lean4精化级提取器，产生38.8万个声明节点和1130万个类型边，跨越25个Lean项目。通过将生成的自然语言口号嵌入到共享语义空间中，连接跨论文和跨非形式化形式化界限的相关陈述。大语言模型评判器在0.8余弦阈值以上确认47952个此类匹配，确认率从阈值处的百分之48上升到大于等于0.9层级的百分之87。在形式化概念检索上，名称和签名表示结合图扩展在Recall@10上达到0.775，与LeanSearch v2的重排序Recall@10（0.780）相差0.5个百分点。
与已有工作不同的是，本文的独特切入角度是构建陈述级而非文档级的依赖图，并且同时覆盖非形式化和形式化数学两个领域。现有工作要么关注非形式化数学的信息检索，要么关注形式化库的依赖提取，但很少有人尝试将两者统一起来。TheoremKB和AutoMathKG在较小规模上为非形式化源构建了定理级图，一些工作将基于图的分析应用于Mathlib依赖结构，但这些工作没有跨模态桥接。本文通过共享slogan嵌入空间和大语言模型评判器，实现了跨模态的陈述匹配，这是前所未有的规模和质量（47952个评判确认的匹配）。论文还系统分析了两种图的结构属性及其在数学搜索、导航和推理中的应用，为后续研究提供了基础设施。此外，论文在自动形式化和前提选择任务上评估了检索系统的实用性，展示了其实际价值。这种跨模态桥接不仅连接了两个异构的数学表示，还为自动定理证明和数学推理提供了新的基础设施和思路。
核心方法
方法分为三个核心部分，非形式化图提取、形式化图提取和跨模态匹配。非形式化图从arXiv LaTeX源码解析定理类环境，使用确定性、启发式和符号三种提取器恢复依赖边。形式化图LeanGraph从Lean4精化后的声明提取六种类型的依赖边。两者通过slogan嵌入和大语言模型评判器连接。整体思路是将非形式化和形式化数学都映射到统一的语义空间，然后在其中寻找匹配，类似将两个异构数据库通过共同字段连接起来。技术路线包括陈述提取和slogan生成、依赖边提取、向量嵌入和索引构建、跨模态候选检索、大语言模型评判器验证。这种设计允许用户根据提取器标签选择精度覆盖权衡，并为下游应用提供灵活的接口。输入是arXiv论文和Lean项目，输出是两个依赖图和一个匹配集，中间过程包括解析、提取、嵌入、检索和评判五个步骤。整个pipeline可以表示为从两个图到匹配对集合的映射，其中图表示图结构，匹配对表示匹配对集合。
核心创新点在于共享slogan嵌入空间和陈述级依赖图的结合。论文不是简单地连接论文或声明，而是在数学陈述级别进行细粒度匹配，这比文档级别的连接更有价值。另一创新是使用三层渐进式slogan生成确保高质量覆盖，百分之70.3在最小阶段解析，百分之98.1在最终回退前解析，避免了slogan生成的覆盖缺失问题。此外，论文使用严格的大语言模型评判器进行验证，在独立样本上达到百分之93.2一致性（kappa等于0.86），比更宽松的DeepSeek模型提供更精确的匹配集。论文还引入六种类型边将依赖分类，允许下游系统按角色过滤边。最后，论文将依赖图用于图扩展，在检索时跳转到依赖的父声明，解决了同名冲突，提高了概念检索的召回率。这些技术的结合使得论文能够在没有重排序器的情况下接近LeanSearch v2的性能，达到了0.775 vs 0.780的Recall@10。
方法步骤详情
非形式化图提取分为四个步骤。第一步是语料库和陈述提取，从arXiv Kaggle元数据快照筛选数学类论文，对于每篇论文，存储元数据、通过Semantic Scholar解析的引用和论文的LaTeX源码。基于正则的解析器识别定理类环境，记录每个陈述的类型、引用编号、标签键、正文、证明和本地上下文，丢弃格式错误或不可信的陈述。第二步是依赖提取，使用三种提取器恢复依赖边。确定性提取器解析论文内的引用类命令和论文引用列表中的引用键，使用arXiv ID或标题匹配。启发式提取器添加来自附近引用、向后话语提示和散文引用的边。符号提取器使用大语言模型识别每个陈述定义和使用的符号。第三步是验证，在500篇抽样论文上使用独立大语言模型评判器评估提取器管道。第四步是边标记，每个发布的边都保留其提取器标签，允许用户选择自己的精度覆盖权衡。形式化图提取LeanGraph在Lean4内核环境应用程序接口上运行，从精化、类型检查后的声明提取依赖，发出六种边类别。跨模态匹配通过口号嵌入和大语言模型评判器完成，相似度计算使用余弦相似度公式。
技术新颖性
技术新颖性体现在多个方面。首先是规模前所未有，非形式化图包含1170万陈述和1830万边，形式化图包含38.8万声明和1130万边，这是最大的数学陈述级依赖图之一，跨越非形式化和形式化两个领域。其次是跨模态匹配pipeline，将非形式化和形式化数学嵌入到同一空间，使匹配成为最近邻查询，无需共享词汇或表面重叠，这是前所未有的跨模态数学陈述匹配。第三是三层渐进式slogan生成确保高质量覆盖，避免了slogan生成的覆盖缺失问题，70.3%在最小阶段解析，98.1%在最终回退前解析。第四是六种类型边将依赖分类为结构继承、字段依赖、签名依赖、证明依赖、定义依赖和文档引用，允许下游系统按角色过滤边。第五是图扩展技术在检索时跳转到依赖的父声明，解决了同名冲突，提高了概念检索的召回率。第六是严格的大语言模型评判器提供质量保证，在独立样本上达到93.2%一致性（kappa等于0.86）。最后是在没有重排序器的情况下接近LeanSearch v2的性能，Recall@10达到0.775 vs 0.780，仅差0.5个百分点。
实验结果
非形式化依赖提取评估在500篇arXiv论文上进行，使用独立大语言模型评判器。确定性提取器达到百分之98.8的评判验证精度（4989除以5051），启发式提取器百分之76.6（3535除以4616），符号提取器百分之42.7（2665除以6241），综合提取器百分之68.1（9855除以14481）。评判器还识别了6372条仅评判器发现的边，F1分数为0.642。这显示了不同提取器的互补性，确定性提取器精度高，启发式提取器覆盖广，符号提取器捕捉符号依赖但误报率高。在蓝图对上的开放池检索验证显示，形式化到非形式化方向命中率1为百分之43.5，命中率10为百分之69.9，平均倒数排名为百分之52.5。非形式化到形式化方向命中率1为百分之42.6，命中率10为百分之71.7，平均倒数排名为百分之53.1。两者都显著优于BM25基线（命中率10百分之61.0）。百分之61.2的蓝图对被至少一个方向恢复，百分之22.3是相互排名1。跨模态匹配方面，在100612个大于等于0.8余弦相似度的候选中，大语言模型评判器确认47952个为匹配（百分之47.7），DeepSeek确认61234个（百分之60.7）。质量集中在高相似度端：大于等于0.9层级单独给出6353个匹配（其候选的百分之87），大于等于0.85层级给出24687个匹配（其候选的百分之71.5）。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 非形式化依赖提取精度 | Judge-Verified Precision | 98.8% (Deterministic), 76.6% (Heuristic), 42.7% (Notation) | N/A | 高精度可信赖提取器 |
| 蓝图对开放池检索Hit@10 | Hit@10 | 69.9% (f到i), 71.7% (i到f) | 61.0% (BM25) | +8.9pp / +10.7pp |
| 蓝图对开放池检索MRR | MRR | 52.5% (f到i), 53.1% (i到f) | 41.0% (BM25) | +11.5pp / +12.1pp |
| 跨模态匹配质量大于等于0.9 | Match Rate | 87.0% (GPT-5.4), 98.4% (DeepSeek) | N/A | 严格评判器确保质量 |
| 跨模态匹配质量大于等于0.8 | Match Rate | 47.7% (GPT-5.4), 60.7% (DeepSeek) | N/A | 严格评判器确保质量 |
| 检索增强自动形式化 | Evaluated Correctness | 8/24 (RAG) | 5/24 (None) | +60% |
| MathlibQR概念检索Recall@10 | Recall@10 | 0.775 (Config E) | 0.780 (LSv2 reranked) | -0.5pp (但无需重排序器) |
| MathlibQR概念检索nDCG@10 | nDCG@10 | 0.558 (Config F) | 0.494 (LSv2 retriever) | +13.0% |
局限与改进
作者承认的主要局限性包括TheoremGraph基于arXiv LaTeX源码构建，这是一个大型结构化语料库，但不覆盖所有数学写作如教科书、讲义、较旧的论文仅以PDF形式存在。非形式化依赖提取必然是近似的，所以发布的图保留每个提取器的标签，让用户选择自己的精度覆盖权衡。跨形式化桥梁依赖于大语言模型生成的slogan和Qwen3嵌入模型，而slogan化是有损的。匹配评判器从有限上下文的slogan工作，专家校准仅覆盖十对，所以并非每个评判确认的匹配都是基本事实。匹配仅获取最近候选，当arXiv语料库中不存在对应部分时，知名结果可能不匹配。下游评估集中在有金标签的设置，但相同的配置不转移到链式前提检索。独立观察到的额外局限性包括slogan化丢失精度，口号将复杂的数学陈述压缩为一行自然语言，丢失了关键假设、定义和上下文，可能导致看似相似但数学上不同的陈述被误判为匹配。形式化图的过度连通可能记录了一些基础设施依赖，这些依赖在高层语义上与目标陈述不直接相关。
独立分析的弱点
独立分析的弱点包括slogan化损失精度，口号将复杂的数学陈述压缩为一行自然语言，丢失了关键假设、定义和上下文，可能导致看似相似但数学上不同的陈述被误判为匹配。改进方向是开发多粒度表示，同时保留slogan的简洁性和详细上下文，或在评判器中提供更多上下文如源论文全文。匹配范围受限，匹配仅在arXiv语料库内进行，知名结果在其对应部分不在arXiv中时可能不匹配，导致桥梁不完整。改进方向是扩展语料库到教科书、讲义和经典论文，通过PDF摄取和与现有数据库集成。跨模态迁移性差，在MathlibQR上调优的配置在链式前提检索上表现更差（Recall@10从0.224降至0.165），表明概念检索和链式前提检索需要不同的信号。改进方向是研究任务特定的检索策略和表示，或学习多任务表示。评判器校准有限，专家校准仅覆盖十对，无法完全捕捉不同数学领域的细微差别。改进方向是扩大校准数据集，覆盖更多领域和匹配类型。
未来方向
作者提出的未来方向包括给评判器更多上下文，如源论文，以及评估替代slogan生成器、嵌入模型、重排序器和更广泛的评判者小组。由于匹配仅获取最近候选，研究召回率优化技术，如更大搜索窗口或重排序。将跨项目双候选通过大语言模型评判器确认，扩大跨项目匹配范围，目前有446对在余弦大于等于0.85。学习图扩展，控制扩展候选的预算，以及训练决策哪些检索陈述值得扩展的策略。基于成果可延伸的额外方向包括开发多粒度表示，同时保留slogan的简洁性和详细上下文。为不同数学领域训练领域特定的嵌入模型和评判器，不同领域的slogan风格和依赖模式可能不同。开发交互式匹配，允许用户提供反馈以改进匹配质量。追踪非形式化和形式化数学之间依赖结构的时间演化，研究新结果如何被形式化和引用。将桥接扩展到其他语言的数学文献，扩大覆盖范围。
复现评估
开源情况良好。论文发布TheoremGraph数据集、LeanGraph和非形式化提取器、超文本传输协议应用程序接口和模型控制协议接口作为基础设施，可在theoremsearch.com和huggingface.co获取。评判的形式化非形式化匹配在huggingface.co数据集上发布。然而，由于arXiv的默认许可证不授予第三方再分发权，公开发布限制为携带开放可再分发许可证的陈述。作者自己的贡献如slogan、评判和元数据根据知识共享许可协议。复现难度中等到较高。数据规模大，需要相当的存储和计算资源。slogan生成和嵌入需要大规模语言模型和图形处理器资源。匹配评判需要访问大语言模型，成本较高（评判100612个候选）。PDF摄取工具依赖光学字符识别，需要额外设置。评估需要特定数据集。然而，论文提供了详细的实现描述和附录，包括提取器配置、评判器提示、参数设置和消融研究，有利于复现。
论文图表
