华盛顿大学用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的世界里，每一步证明都必须写得清清楚楚，没有“读者自行理解”这回事。这样一来，每个定理到底依赖哪些前置结论，就被记录得明明白白。

然而，这两个世界——一边是浩如烟海、依赖关系模糊的非形式化数学论文，另一边是精细严谨、但覆盖范围有限的形式化证明库——几乎从未被系统地连接过。华盛顿大学的研究团队决定，要在这两个世界之间搭一座桥。于是，就有了TheoremGraph。

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

回到那个摩天大楼的比喻。数学大厦里，每一个新结论都必须站在已有结论的肩上。但数学家写论文时，通常只在文末列个参考文献列表，正文里写一句“由[Smith, 2019]可知”。这种做法其实有它的道理：圈子很小，专家读者看到“由紧性条件”这类表述，自然知道背后指的是哪些标准工具。但这种默契，对圈外人、对机器、对试图理解全局的研究者来说，就成了一堵厚重的信息墙。

更实际的后果是，由于依赖关系不透明，同一个结论经常被不同的人在不同的论文里反复证明，双方都不知道对方的存在。研究团队引用了一项针对arXiv撤稿的大规模研究数据：在近1.5万个撤稿案例中，有357个的作者自述是“结论不够新颖”——说白了，就是后来才发现自己证明的东西，别人早就证过了。这个比例看着不算大，但每一个案例背后，都是研究者数月甚至数年的心血打了水漂。

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

研究团队的核心洞察其实很简单：这两个世界各有所长，为什么不把它们的优势结合起来？这就是TheoremGraph的起点。

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

要构建非形式化的数学知识图谱，首先得有一个足够大的语料库。团队盯上了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个开源的形式化项目，涵盖了素数定理、球面填充、费马大定理等多个专题。最终，整个形式化图谱包含388,105个声明节点，和1133万条有类型标注的依赖边。

这些边被细分为六种语义类型，每种代表一种不同性质的依赖关系：“extends”边捕捉结构体或类之间的继承关系；“field”边捕捉结构体字段类型中的依赖；“sig”边捕捉出现在声明签名中的常量；“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之后，下一步就是把它们都“嵌入”到一个统一的高维向量空间里。具体用的是Qwen3-Embedding-8B这个嵌入模型，生成每条陈述对应的4096维向量，然后进行L2归一化处理，使得向量之间的内积等于余弦相似度。所有向量都存储在pgvector数据库里，并建立了HNSW近似最近邻索引，方便快速检索。

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

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

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

完整的匹配流程是这样的：从385,657条（已过滤掉构造函数和编译器自动生成的名称）形式化声明出发，对每条声明找到余弦相似度最高的那条非形式化陈述，并记录相似度分数。在ann_k=50的设置下，55.3%的声明找到了候选匹配。

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

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

最终，GPT-5.4法官在100,799对候选中，确认了47,952对匹配（占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法官，在同样的候选集上确认了61,234对匹配（占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”子集，确保目标声明在所有被比较系统的索引里都存在。

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

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

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

第二步是改进搜索策略，包括：对于用Lean语法或精简语言写成的查询，用大模型生成一个假设性的自然语言陈述来扩充查询（这个技术叫HyDE），并把两个排名融合；同时把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）。

从分声明类型的分析来看，这些干预措施主要帮助了那些“名字就是它本身”的声明类型——结构体、类、定义和归纳类型都有显著提升，而定理和实例本来就有描述性的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只消耗了14,000个输出token和68次工具调用，而RAG+Library消耗了37,000个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。