华盛顿大学用AI为数学知识建了一张"神经网络"，把百年数学论文和形式化证明库串联起来了

这项由华盛顿大学数学AI实验室（University of Washington Math AI Lab）主导的研究，于2026年6月24日发表在预印本平台arXiv上，论文编号为arXiv:2606.25363v1，研究领域标注为信息检索（cs.IR）。有兴趣深入了解的读者可以通过该编号查询完整论文。

数学知识的世界里存在一个长久以来被忽视的问题：每一个定理都不是凭空出现的，它必然依赖于之前的某些结论，而那些结论又依赖于更早的定义和引理。这就像一栋摩天大楼，每一层都需要下面各层作为支撑。然而，现实中数学论文的引用方式却极为粗糙——作者通常只会说"参考文献[7]"，而不是精确地指出"我用到了文献[7]中第三章第二节的引理4.2"。这就好比建筑图纸只写了"参考隔壁楼"，却完全没有标注用的是哪根梁、哪块砖。

与此同时，数学界近年来兴起了一种叫做"形式化证明"的运动。研究者们把数学定理翻译成计算机可以逐字逐句验证的精确代码，其中最著名的工具叫做Lean。Lean的数学库Mathlib4收录了超过40万条经过机器严格验证的定义、引理和定理，涵盖代数、拓扑、分析、数论等几乎所有基础数学领域。在Lean里，每一个证明步骤都必须明确写出来，没有任何"读者自行理解"的余地。这样一来，每个定理究竟依赖哪些前置结论，就被记录得清清楚楚。

然而，这两个世界——浩如烟海的非形式化数学论文和精细严谨的形式化证明库——却几乎从未被系统性地连接在一起。一边是1170万条从arXiv数学论文中提取的定理，依赖关系模糊；另一边是精确记录了1130万条有类型标注依赖边的形式化声明，但覆盖的数学内容相对有限。华盛顿大学的研究团队决定为这两个世界搭一座桥，于是有了这项叫做TheoremGraph的研究。

一、为什么数学论文的引用方式让人头疼

回到那个摩天大楼的比喻。数学的大厦里，每一个新结论都必须站在已有结论的肩膀上。但当一位数学家写论文时，他通常只会在文末列出参考文献列表，在正文里写"由[Smith, 2019]可知"。这种做法有其合理之处：数学圈子很小，专家读者看到"由紧性条件"这样的表述，心里自然知道背后指的是哪些标准工具。然而这种默契对于外人、对于机器、对于试图理解全局的研究者来说，就形成了巨大的信息壁垒。

更实际的后果是，由于依赖关系不透明，有时一个结论会被不同的人在不同的论文里重复证明，双方都不知道对方的存在。研究团队引用了一项关于arXiv撤稿的大规模研究数据：在近1.5万个被分类的撤稿案例中，有357个是作者自述"结论不够新颖"，也就是说，他们后来才发现自己证明的东西别人已经证过了。这个比例看似不大，但每一个这样的案例背后都是研究者数月乃至数年的心血付诸东流。

形式化证明则走向了另一个极端。Lean这类工具要求每一个推理步骤都明确无误地写出来，任何隐含的假设都不被允许。这样做的好处是依赖结构一览无余；坏处是翻译成本极高，目前形式化的数学内容相对于整个人类数学知识体系而言还只是沧海一粟。

研究团队的核心洞察是：这两个世界各有所长，能否把它们的优势结合起来？这就是TheoremGraph项目的起点。

二、从1170万篇论文里"挖矿"——非形式化依赖图的构建

为了构建非形式化的数学知识图谱，研究团队首先从arXiv这个全球最大的数学预印本平台入手。他们的语料库是arXiv上所有带有数学标签的论文，通过Kaggle平台提供的元数据快照获取。对于每篇论文，团队不仅存储了元数据，还尽可能通过Semantic Scholar这个学术数据库解析了论文的参考文献，并获取了论文的LaTeX源代码。

接下来是关键一步：从这些LaTeX源代码里把定理、引理、命题、推论等"定理类"环境（theorem-like environments）提取出来。这项工作由一个基于正则表达式的解析器完成，它能识别LaTeX中的各类数学环境，并记录每条陈述的类型、编号、标签键名、正文内容、证明，以及前后文。为了保证质量，团队剔除了一些明显有问题的条目，比如正文为空的、数学括号不配对的、过短的，以及陈述在句子中间截断的。最终提取到了超过1170万条定理类陈述。

光有陈述还不够，还需要建立它们之间的依赖关系——也就是图里的"边"。团队设计了三种不同的"边提取器"，每种工作原理不同，各有侧重。

第一种叫做"确定性提取器"。它的原理很简单：直接解析LaTeX代码里的显式引用命令，比如`\ref`（文内交叉引用）和`\cite`（参考文献引用）。如果一篇论文的参考文献列表里有另一篇论文的arXiv编号，就可以精确地建立跨论文的依赖关系；如果引用中明确提到了某个定理编号，还能进一步精确到那条具体的陈述。这种方法的精度极高，经过独立验证后，准确率达到98.8%。

第二种叫做"启发式提取器"。它更像一个有经验的编辑，能识别一些非显式的引用模式，比如论文里出现"定理3.2"这样的散文式引用，或者在一段论证中出现"由上述引理可知"这样的话语线索。为了控制准确性，所有启发式提取的边都被限制为只能指向文档中较早出现的陈述（也就是说，结论只能依赖于之前的东西，不能反向引用）。这种方法的验证准确率约为76.6%。

第三种叫做"符号提取器"。这是最有趣的一种：它借助一个大型语言模型（具体来说是Qwen3-235B，一个强大的开源大模型）来识别每条陈述里用到了哪些数学符号，然后把每个符号的"使用"追溯到文中最近的一次"定义"，从而建立符号层面的依赖关系。这种方法的覆盖范围最广，但准确率相对较低，约为42.7%。

三种提取器共同产出了1.83亿条候选依赖边，其中文内依赖边约1486万条，跨论文依赖边约346万条。每一条边都保留了"是哪个提取器提出的"这一标签，这样下游用户就可以根据自己对精度和覆盖率的不同需求，灵活选择要使用哪些边。

三、Lean证明库里的精密"蓝图"——形式化依赖图的构建

与非形式化图谱的"挖矿"式构建不同，形式化图谱的构建更像是精密仪器的读数。研究团队开发了一个叫做LeanGraph的工具，它工作在Lean 4的"精化器"（elaborator）层面——也就是说，它不是读取Lean的源代码文本，而是深入到Lean内核完成类型检查之后的中间表示，从那里提取依赖信息。这一点很重要，因为源代码级别的分析会漏掉很多在类型检查过程中自动生成或展开的内容。

LeanGraph处理了Mathlib4的三个版本（v4.27到v4.29）以及另外24个开源的Lean形式化项目，涵盖了素数定理、球面填充、费马大定理等多个专题形式化工作。最终，整个形式化图谱包含388105个声明节点（declaration nodes）和1133万条有类型标注的依赖边。

这些边被细分为六种语义类型，每种类型代表一种不同性质的依赖关系。"extends"边捕捉结构体或类之间的继承关系；"field"边捕捉结构体字段类型中的依赖；"sig"边捕捉出现在声明签名（signature）中的常量；"proof"边捕捉定理证明项中用到的常量；"def"边捕捉非命题定义体中用到的常量；"docref"边捕捉文档字符串中有效的反引号引用。这种分类让下游系统可以按照依赖类型的重要程度来过滤或排序，而不是把所有依赖一视同仁。

在节点的筛选上，LeanGraph同样做了精心设计。Lean的类型检查过程会自动生成大量辅助性声明，比如递归消去子、无混淆引理、匹配声明等，这些声明对人类读者没有实际意义，只是底层机器的内部工件。LeanGraph通过一套基于Lean内核API和文档生成工具doc-gen4标准的过滤谓词，只保留面向人类用户的声明，把这些机器内部工件排除在外。

四、让两个世界"握手"——用"一句话摘要"建立跨模态桥梁

有了两张图，接下来的挑战是把它们连接起来。这两张图之间没有任何共同的节点，没有共享的标识符，语言风格也截然不同——一边是充满LaTeX数学符号的学术论文片段，另一边是精确的Lean类型签名。要在它们之间建立对应，就像要在两种完全不同的语言之间找到相同意思的句子。

研究团队选择的方法是"通义化"（sloganization）：为每一条数学陈述生成一句通俗的英文摘要，称为"slogan"（一句话口号）。这个想法来自于此前LeanSearch项目的工作——如果把每个形式化定理翻译成自然语言描述，就可以用自然语言查询来检索它们。

为了给1170万条非形式化陈述生成slogans，团队设计了一个"阶梯式提示链"（escalating prompt chain）。第一步是用最少的信息——仅陈述本身——请大模型（Qwen3-235B）生成一句口号；如果大模型自我标记这次生成"信息不足"，就升级到第二步，加入证明和上下文；还不够就升级到第三步，加入相邻陈述和它的出边依赖；最后还是无法生成满意结果的，就强制要求给出一个"最佳猜测"口号。这个四阶段流程最终实现了100%的覆盖率，其中70.3%的陈述在第一步就得到了满意的口号，98.1%在到达最后的强制步骤之前就已经解决了。

对于形式化声明，slogan的生成逻辑略有不同：团队按照语义角色对出边依赖进行排名，把优先级最高的数学信息塞进固定大小的提示窗口，同时过滤掉那些无处不在的基础声明和Lean/内核内部的管道工具。

有了每条陈述的slogan之后，下一步是把它们都"嵌入"（embed）到一个统一的高维向量空间里。具体使用的是Qwen3-Embedding-8B这个嵌入模型，生成每条陈述对应的4096维向量，然后进行L2归一化处理，使得向量之间的内积等于余弦相似度。所有向量存储在pgvector数据库里，并建立了HNSW近似最近邻索引，以便快速检索。

这样一来，不管是形式化声明还是非形式化陈述，都变成了同一个空间里的点。两条意思相近的陈述，无论一个来自arXiv论文、另一个来自Lean代码，在这个空间里的距离都会很近。这就为跨模态匹配提供了技术基础。

五、让AI法官来裁决——47952对跨模态匹配的发现

有了统一嵌入空间之后，匹配的方式就很直观了：对于每一条形式化声明，找到在嵌入空间里与它最相似的那条非形式化陈述，这就是"候选匹配"。

研究团队的完整匹配流程如下：从385657条（经过轻度过滤去掉了构造函数和编译器自动生成名称的）形式化声明出发，对每条声明找到余弦相似度最高的那条非形式化陈述，记录相似度分数。在ann_k=50（即每次搜索检索最近的50个候选）的设置下，55.3%的声明找到了候选匹配。

为了验证这种余弦相似度确实能发现真正对应的陈述，团队利用了一批"蓝图对"（blueprint pairs）作为基准。所谓蓝图（Lean blueprint），是一种特殊的LaTeX文档，作者在里面手动标注了每条非形式化陈述对应的Lean声明。这些人工标注的对应关系就是天然的"正确答案"。研究发现，当用形式化声明的slogan作为查询时，其对应的非形式化slogan排在第一位的概率是43.5%，排在前十位的概率是69.9%。

余弦相似度高于0.8的候选对一共有100799对。为了判断哪些是真正的匹配，团队引入了GPT-5.4作为"法官"（LLM-as-judge）。法官拿到的信息包括声明名称、两条陈述各自的slogan、Lean签名、arXiv论文标题和原始LaTeX内容，然后给出三种裁决之一："exact"（完全一致）、"inexact"（同一结论但有细节差异，比如一般化与特例、或双向命题与单向命题的关系）、"wrong"（尽管嵌入相似但实际上是不同的结论）。"exact"和"inexact"都算作匹配。

最终，GPT-5.4法官在100799对候选中确认了47952对匹配（占48%）。质量随相似度提高而提升的趋势非常明显：在相似度0.95-1.0区间内，确认匹配率高达96.2%；在0.90-0.95区间内为85.8%；在0.85-0.90区间内为62.4%；在0.80-0.85区间内降至37.4%。

在选择法官时，团队也经历了一番校准过程。最初选用的是Opus 4.8，但经过领域专家对10个样本的人工复核后发现，Opus 4.8过于"宽松"——它将一些应该标注为"inexact"甚至"wrong"的对认定为"exact"。常见的失误模式有三种：Lean里的版本比论文更一般化；表面上看起来相符但背后使用了不同的定义；或者存在更准确的Lean对应项但没有被找到。于是团队换用了更严格的GPT-5.4，并对其进行了第二轮专家校准，结果GPT-5.4与专家在10个样本上的8个完全一致，折合成"匹配/非匹配"的二元判断时有9/10吻合，表现令人满意。

作为比较，更宽松的DeepSeek-V4-Pro法官在同样的候选集上确认了61234对匹配（占61%）。团队将GPT-5.4的严格版本作为正式发布的数据集，同时也公布了DeepSeek版本作为高召回率的对比参考。

六、形式化代码检索的新思路——与LeanSearch的正面比拼

除了建立跨模态桥梁，TheoremGraph项目还对一个非常实际的任务进行了系统测试：给定一段自然语言描述，如何从Mathlib这个庞大的Lean库里找到对应的声明？这个任务叫做"形式化概念检索"。

研究团队选择与LeanSearch v2（一个专门为此任务设计的系统）进行比较。两个系统使用完全相同的嵌入模型（Qwen3-Embedding-8B，无微调），唯一的区别是各自嵌入的"通道内容"不同。LeanSearch v2嵌入的是一段结构化文本，包含声明的类型（定理、定义、类等）、非形式化名称和描述、类型签名，以及对于定义、类和实例还会加上值体；声明的完整限定名作为元数据存储，不参与嵌入。TheoremGraph的基线版本（Configuration A）只嵌入那条一句话的slogan。

评测基准使用的是LeanSearch v2团队提供的MathlibQR数据集。这个数据集包含200个Mathlib声明，每个声明配有最多6种不同风格的查询，包括普通英语、LaTeX、Lean风格文本、slogan、昵称和特殊情形。评估指标主要是Recall@10（目标声明出现在前10个检索结果里的概率）和nDCG@10（考虑排名位置的加权得分）。为了保证公平比较，评测只使用"公平-810"子集，即确保目标声明在所有被比较系统的索引里都存在的那810条查询。

基线版本（只用slogan）的Recall@10是0.586，比LeanSearch v2的检索器基线（0.657）低7.1个百分点，差距主要来自两类问题：第一，对于名字就是它本身的声明（比如Lattice这个代数结构），slogan里没有任何名字信息，自然找不到；第二，对于用Lean语法或裸名字形式提交的查询，slogan也很难匹配。

为了缩小差距，团队依次测试了一系列干预措施。

第一步是加入"名称与签名表示"（Name/sig representation）。除了slogan，团队还为每个声明生成了第二个嵌入通道，把声明的名称、类型签名和依赖关系一起嵌入。这样，名字相关的查询就有了明确的匹配目标。同时，团队还为声明名称建立了一个独立的名称匹配索引，处理那些连嵌入都无法命中的纯名字查询。

第二步是改进搜索策略，包括：对于用Lean语法或精简语言写成的查询，用大模型生成一个假设性的自然语言陈述来扩充查询（这个技术叫HyDE，即Hypothetical Document Embeddings），并把两个排名融合；同时把HNSW的候选集宽度（ann_k）放大，确保正确答案不会在粗略筛选阶段就被丢弃。

第三步是加入图展开（Graph expansion）。检索到结果之后，沿着依赖图向上走一跳，把每个检索结果的"父声明"也加入候选集。这样做的道理是：如果Lattice这个抽象概念本身没被直接命中，但它的父结构SemilatticeInf或SemilatticeSup被命中了，通过图展开就能把Lattice也带出来。

配置A到F的完整消融实验结果如下：只用slogan的基线配置A得到Recall@10=0.586；加入名称与签名嵌入后（配置B）升至0.680；再加入搜索技术（配置C）升至0.716；再加入slogan+名称双通道嵌入（配置D）升至0.767；加上图展开后（配置E，召回优化版）最终达到0.775，与LeanSearch v2加上重排序器的最终结果0.780只差0.5个百分点，且未使用任何重排序器。

另一个值得单独报告的配置F（排名优化版）：只用名称与签名表示，配合搜索技术但不加图展开，在Recall@10=0.733的同时实现nDCG@10=0.558，在每个指标上都超过了LeanSearch v2的纯检索器基线（nDCG@10=0.494，Recall@10=0.657）。

从分声明类型的分析来看，这些干预措施主要帮助了那些"名字就是它本身"的声明类型——结构体（structures）、类（classes）、定义（definitions）和归纳类型（inductives）都有显著提升，而定理（theorems）和实例（instances）本来就有描述性的slogan，反而略有下降。整体来看，810条查询上相比基线提升了18.9个百分点的Recall@10和16.8个百分点的nDCG@10。

七、自动形式化的尝试——让AI把自然语言描述翻译成Lean代码

研究团队还测试了检索增强对另一个下游任务的帮助：自动形式化（autoformalization），也就是给定一段自然语言描述的数学陈述，让AI直接生成对应的Lean 4声明（不含证明，只要类型签名对了就算通过）。

为了降低大模型直接"背答案"的可能性，团队选用了Mathlib v4.30中新引入的24个定理作为测试目标，但检索库只用v4.29的版本（即这些定理在检索库里不存在）。查询文本是用qwen3-8b对gold Lean签名进行"反向翻译"得到的自然语言描述，并去掉了声明名称，这样模型就无法靠名字直接找答案。

测试比较了四种条件：只给自然语言描述（None）；加上检索到的前置引理（RAG）；加上在整个v4.29声明列表上进行grep搜索的工具权限（Library）；以及同时提供检索引理和grep工具（RAG+Library）。评判标准分为两级：Strict要求生成的命题与目标完全一致；Eval（评估正确）则是经由claude-opus-4-7法官确认的高置信度等价表述，同时人工复核。

结果是：RAG条件的评估正确数（8/24）与RAG+Library完全相同，但RAG只消耗了14000个输出token和68次工具调用，而RAG+Library消耗了37000个token和188次工具调用——检索增强以不到一半的计算成本实现了相同的准确率。纯靠grep工具搜索库（Library）能通过类型检查22/24个，但实际评估正确的只有5/24，说明"能编译"远不等于"写对了"。大约10/24的目标在所有条件下都失败，说明有些自然语言描述本身信息量不足以唯一确定对应的Lean表述。

八、依赖图里的"远亲近邻"——嵌入距离与图距离的关系

研究团队还做了一项有趣的分析：在依赖图里，两个节点之间的跳数越多，它们的slogan嵌入向量的余弦相似度是否就越低？换句话说，图上的邻居是否也是语义上的邻居？

实验方法是：对于每种"跳数"d（从1到6），随机抽取1000对节点，要求它们的有向最短路径距离恰好是d跳，然后计算这对节点slogan嵌入的余弦相似度均值。同时计算随机配对的基线相似度作为对比。

结果显示，在非形式化图和形式化图中，相似度均随跳数增加而下降，但下降速度差异很大。形式化图（Lean）里，相似度从第1跳的约0.54急速下降，到第6跳时已接近随机配对基线（约0.33）。非形式化图（arXiv论文）里，相似度从第1跳的约0.61下降到第6跳的约0.51，始终明显高于随机基线（约0.30）。

这个差异背后有一个合理的解释：Lean记录的是非常细粒度的依赖关系，包括对类型类实例、继承结构、通用代数工具等基础设施的引用。一个关于狭窄专题的定理，它的"父声明"可能是一个适用范围极广的模块论引理，语义上相差甚远。而非形式化论文里，一个定理的"依赖"更多地是同一数学脉络里的上下文结论，语义上保持较高的连贯性。

九、用强化学习训练AI主动"检索引理"

附录中还包含一个更有探索性的实验：能否用强化学习训练一个语言模型，让它学会如何更好地用搜索工具来寻找定理的前置引理？

团队把这个问题建模为一个马尔可夫决策过程（MDP）：智能体的状态是目标定理的slogan和LaTeX原文，动作是向TheoremSearch API发送一条查询字符串，奖励是成功检索到真正前置引理的数量（减去错误检索的惩罚）。智能体最多可以发出6条查询，每次返回余弦相似度最高的10个结果。

训练方法使用了Self-Distillation Policy Optimization（SDPO）：对每个目标定理采样4条完整的查询轨迹，选取其中召回率最高的那条作为"反馈"，让学生策略去模仿一个以最优轨迹为条件的教师策略。所有训练策略都是Qwen3-8B上的LoRA适配器（rank 16），更新约0.53%的参数。

结果是：未训练的Qwen3-8B基础模型的依赖召回率约为4%；加入短推理链后用SDPO训练，召回率提升到7.9%；之后不论调整学习率还是扩大训练集，都无法突破这个上限。对比之下，GPT-5.5和Gemini 3.1 Pro作为提示基线（prompt-only baseline，无训练），分别达到了26.4%和17.0%的召回率，远超训练过的小模型。

这个瓶颈的原因很可能是：模型学会了提出数学上合理的主题查询，但缺乏足够的领域知识来精确识别并描述目标定理证明里实际引用的那个具体引理。大量采样轨迹里根本没有任何成功检索，导致训练信号极度稀疏。

不过，图展开（citation-graph expansion）提供了一个有效的补救方案：在RL策略检索到的结果基础上，沿跨论文依赖边走一跳，把邻居节点也加入候选集。这一操作把召回率从7.9%提升到了13.4%，基本追平了Gemini基线。背后的道理是：即使检索到的节点本身不是正确答案，它在图里的邻居可能引用了相同的背景工具。

十、把PDF教材也纳入版图——超越arXiv的探索

非形式化图谱目前完全依赖arXiv的LaTeX源代码，但数学知识的很大一部分存在于没有LaTeX源的地方：教科书、讲义、早期论文，它们只有PDF格式。团队为此开发了一个PDF摄取工具，并以Artin的《代数》（第二版）教材作为可行性验证。

工具分两步：第一步用pymupdf对PDF进行文本扫描，找出所有在行首出现"Theorem"、"Lemma"等环境标题的页面，保留这些页面以及前后各一页的缓冲（避免证明跨页被截断）。Artin的《代数》共555页，通过这一筛选只保留了182页（约三分之一），大幅减少了后续OCR的计算量。第二步用Nougat OCR对筛选后的页面进行识别，输出Mathpix Markdown格式，然后用一个逐行解析器提取定理类环境。

最终从这本书里提取了406条陈述，其中242条（59.6%）附有从PDF里识别出的证明内容。这个数字与直接数LaTeX源里的头部标签计数（75个定理、104个命题等）基本吻合，说明提取器的覆盖率令人满意。

不过，PDF摄取有一个根本性局限：PDF里没有`\label`键、没有`\ref`命令、没有可解析的参考文献列表，因此准确率达98.8%的确定性提取器完全无法为这些陈述建立依赖关系。PDF来源的依赖提取主要依赖符号提取器和语义嵌入检索，精度相对有限。如何从OCR文本里恢复可用的交叉引用结构，是留给未来工作的重要课题。

十一、让AI在论文里"找到引用缺失的那条定理"

还有一个实用性很强的实验：给一段数学论文文字，把其中某个显式引用去掉，然后看AI能不能把那个被引用的定理找回来。这模拟了研究者阅读论文时常遇到的场景——"这里肯定引用了某个已知结论，但到底是哪篇论文的哪个定理呢？"

实验设置是：从2026年2月之后发表的arXiv数学论文中随机抽取149个片段，每个片段包含一个命名了特定定理、引理或命题的引用命令。把那个引用替换成"[Citation Needed]"并从参考文献列表里删掉对应条目，然后让模型来恢复它。评估分两个级别："精确匹配"要求同时正确给出被引论文的arXiv编号和定理编号；"论文级匹配"只要求正确找到被引论文。

三个模型（ChatGPT 5.4、Gemini 3.1 Pro、Claude Sonnet 4.5）在三种条件（不受限制的网络搜索、密集检索、图导航检索）下进行了测试。结果显示，不受限制的网络搜索表现最好，Gemini 3.1 Pro在这个条件下精确匹配率高达57.0%。图导航检索优于纯密集检索，但仍落后于网络搜索。

不过这个比较并不完全公平：网络搜索条件下，模型可以直接搜索原文片段来找到原始论文，然后从论文里直接读出引用——这更接近"作弊"而非"理解"。研究团队在论文中也诚实地指出了这一点，并将其列为实验局限性之一。

归根结底，TheoremGraph是一个关于"让数学知识更加透明可查"的宏观工程。两张图、一个共享嵌入空间、近五万对跨模态匹配、接近最先进检索器的检索性能——这些数字背后是一个清晰的信念：数学定理之间的依赖关系是一笔宝贵的知识财富，它不应该只存在于专家的脑子里，而应该被系统地记录下来，让机器也能读懂。

当AI助手越来越多地被用于辅助数学研究和定理证明时，它能否快速找到相关的前置引理，能否识别两篇论文里描述的其实是同一个结论，能否在庞大的形式化库里精准定位对应的声明——这些都直接决定了AI工具的实际价值。TheoremGraph为这些能力提供了基础设施，尽管在某些任务上（比如大模型的RL训练召回率仍然偏低）还有很长的路要走，但已经可以看到图结构、语义嵌入和大模型三者结合所带来的协同效应。

数据集、提取工具、HTTP API和MCP接口均已公开发布在theoremsearch.com，判定为匹配的跨模态配对数据集则发布在Hugging Face平台（huggingface.co/datasets/uw-math-ai/theorem-matching）。感兴趣的读者可以通过arXiv编号2606.25363查阅完整论文。

---

Q&A

Q1：TheoremGraph提取的非形式化依赖边中，哪种类型的精度最高？

A：确定性提取器（deterministic extractor）精度最高，经独立LLM法官验证后准确率达98.8%。它通过解析LaTeX源代码中的显式引用命令（如\ref和\cite）来建立依赖关系，因为是直接解析机器可读的结构化标记，所以精度远高于启发式提取器（76.6%）和符号提取器（42.7%）。

Q2：LeanGraph提取的六种依赖边类型分别是什么？

A：LeanGraph将形式化依赖分为六类：extends边（结构体或类的继承关系）、field边（结构字段类型中的依赖）、sig边（出现在声明签名中的常量）、proof边（定理证明项中用到的常量）、def边（非命题定义体中用到的常量）、docref边（文档字符串中的反引号引用）。这种分类允许下游系统按依赖类型过滤，而不必把所有依赖一视同仁。

Q3：TheoremGraph的检索系统与LeanSearch v2的比较结果如何？

A：在MathlibQR基准测试的公平-810子集上，TheoremGraph的召回优化配置（Config E）在不使用重排序器的情况下实现了Recall@10=0.775，与LeanSearch v2加上重排序器的最终结果0.780只相差0.5个百分点。若以排名质量（nDCG@10）衡量，TheoremGraph的排名优化配置（Config F）达到0.558，超过LeanSearch v2纯检索器基线的0.494，但两者均低于LeanSearch v2加重排序器后的0.623。