华盛顿大学用AI为数学知识建了一张"神经网络"

由华盛顿大学数学AI实验室（University of Washington Math AI Lab）主导的华盛研究成果，已于2026年6月24日上传至预印本平台arXiv（论文编号：arXiv:2606.25363v1，学用学知分类：cs.IR）。为数该研究旨在解决数学领域中非形式化论文与形式化证明库之间的识建割裂问题，通过构建名为TheoremGraph的张神知识图谱，实现了两大数学世界的经网系统性连接。

一、华盛 核心痛点：数学知识的学用学知“黑箱”与“孤岛”

数学大厦的构建依赖于严密的逻辑链条，但现实中的为数知识管理存在两大断层：

1. 非形式化论文的引用模糊：传统数学论文通常仅列出参考文献编号（如“参见[7]”），缺乏对具体引理、识建章节或定理的张神精确指向。这种“黑箱”式引用导致依赖关系不透明，经网甚至造成重复劳动。华盛据arXiv撤稿数据显示，学用学知约357例撤稿源于作者事后发现结论已被他人证明，为数凸显了依赖关系缺失带来的效率损耗。
2. 形式化证明的覆盖局限：以Lean及其数学库Mathlib4为代表的形式化证明运动，虽然实现了40万+条经过机器验证的定理和清晰的依赖记录，但其内容仅占人类数学知识的极小部分，且翻译成本极高。

TheoremGraph项目的核心目标，正是搭建一座桥梁，将1170万条非形式化定理陈述与1130万条形式化声明进行语义对齐。

二、 非形式化依赖图构建：从海量论文中“挖矿”

研究团队从arXiv数学标签论文出发，通过解析LaTeX源代码，提取出超过1170万条定理类陈述（定理、引理、命题等），并设计了三种提取器构建依赖边：

• 确定性提取器（Deterministic Extractor）：直接解析LaTeX中的\ref和\cite命令。精度极高，经验证准确率达98.8%，能精确建立跨论文及文档内的依赖关系。
• 启发式提取器（Heuristic Extractor）：识别“定理3.2”、“由上述引理可知”等非显式文本模式。为保证逻辑方向性（结论不依赖未来内容），限制其仅指向较早出现的陈述。验证准确率约为76.6%。
• 符号提取器（Symbolic Extractor）：利用大模型（Qwen3-235B）识别数学符号的使用与定义追溯。覆盖范围最广，但准确率较低，约为42.7%。

三种提取器共同生成了1.83亿条候选依赖边（含1486万条文内边和346万条跨论文边），并保留提取器标签供用户按需筛选。

三、 形式化依赖图构建：LeanGraph的精密解析

不同于非形式化图谱的“挖掘”，形式化图谱通过LeanGraph工具进行精密提取。该工具深入Lean 4内核的类型检查中间表示（而非源代码文本），处理了Mathlib4（v4.27-v4.29）及24个开源项目。

• 节点筛选：通过过滤谓词剔除递归消去子、无混淆引理等机器内部工件，仅保留面向人类的声明，最终获得388,105个声明节点。
• 六类依赖边：将依赖细分为extends（继承）、field（字段类型）、sig（签名常量）、proof（证明常量）、def（定义常量）和docref（文档引用）。这种分类允许下游系统根据依赖性质进行加权或过滤。
• 规模：最终形成包含1133万条有类型标注依赖边的形式化图谱。

四、 跨模态桥梁：基于“Slogan”的语义嵌入

由于非形式化陈述与形式化声明在标识符和语言风格上完全不同，团队采用“通义化”（Sloganization）策略建立映射：

1. 生成Slogan：为每条陈述生成一句通俗英文摘要。
2. 非形式化：采用“阶梯式提示链”，由Qwen3-235B模型逐步增加上下文（证明、相邻陈述、依赖边），最终实现100%覆盖率。
3. 形式化：基于语义角色排名，提取关键数学信息生成Slogan。
4. 向量化嵌入：使用Qwen3-Embedding-8B模型将Slogan转化为4096维向量，并进行L2归一化。向量存储于pgvector数据库，建立HNSW索引以支持快速检索。
5. 统一空间：在此高维空间中，语义相近的陈述（无论来源）距离更近，为跨模态匹配奠定基础。

五、 AI裁决下的跨模态匹配发现

研究团队利用余弦相似度进行初步匹配，并引入GPT-5.4作为“AI法官”进行最终裁决：

• 初步筛选：在ann_k=50的设置下，55.3%的形式化声明找到候选匹配。
• 基准验证：利用人工标注的“蓝图对”（Blueprint Pairs）验证，形式化Slogan查询对应非形式化Slogan的Top-1命中率为43.5%，Top-10为69.9%。
• AI裁决结果：在相似度>0.8的100,799对候选中，GPT-5.4确认47,952对为有效匹配（含完全一致和部分一致）。
• 质量趋势：相似度越高，匹配准确率越高（0.95-1.0区间达96.2%）。
• 模型校准：相比过于宽松的Opus 4.8，GPT-5.4在专家校准中表现出更高的一致性（9/10吻合）。作为对比，DeepSeek-V4-Pro确认了61,234对匹配（高召回率参考）。

六、 形式化概念检索：挑战LeanSearch v2

TheoremGraph在“形式化概念检索”任务上与专用系统LeanSearch v2进行了对比。测试基于MathlibQR数据集（公平-810子集），指标为Recall@10和nDCG@10。

• 基线表现：仅使用Slogan嵌入的TheoremGraph基线（Config A）Recall@10为0.586，低于LeanSearch v2基线（0.657）。
• 优化迭代：
• 加入名称/签名嵌入：Recall@10升至0.680。
• 改进搜索策略：引入HyDE（假设文档嵌入）融合排名，Recall@10升至0.716。
• 双通道嵌入：Slogan+名称联合嵌入，Recall@10升至0.767。
• 图展开（Graph Expansion）：沿依赖图向上检索父声明，Recall@10达到0.775，仅比LeanSearch v2加重排序器（0.780）低0.5个百分点，且无需重排序器。
• 排名优化：Config F（仅名称/签名+搜索技术）在nDCG@10（0.558）上超越LeanSearch v2纯检索器（0.494）。

七、 自动形式化辅助：检索增强生成（RAG）

团队测试了TheoremGraph在自动形式化（将自然语言描述转为Lean类型签名）中的辅助作用。

• 实验设置：使用Mathlib v4.30新定理作为目标，检索库仅限v4.29，防止模型“背答案”。
• 结果：
• RAG（仅检索前置引理）：评估正确率8/24，消耗14,000 token。
• RAG+Library（检索+全库Grep）：评估正确率8/24，消耗37,000 token。
• 结论：RAG以不到一半的计算成本实现了与更复杂方法相同的准确率。纯Grep搜索虽能通过类型检查（22/24），但实际语义正确率仅5/24，证明“能编译”不等于“写对”。

八、 嵌入距离与图距离的相关性分析

研究发现，非形式化图谱中节点间的语义相似度随图距离（跳数）增加下降缓慢（第6跳仍显著高于随机基线），而形式化图谱中相似度下降迅速（第6跳接近随机水平）。

• 原因：Lean记录的是细粒度的基础设施依赖（如类型类实例、通用代数工具），导致语义跨度大；而非形式化论文中的依赖更多是同一脉络下的上下文结论，语义连贯性更强。

九、 强化学习训练AI检索策略

团队尝试用SDPO（自蒸馏策略优化）训练Qwen3-8B模型，使其学会主动检索前置引理。

• 瓶颈：未训练模型召回率仅4%，训练后提升至7.9%，但难以突破。相比之下，GPT-5.5和Gemini 3.1 Pro作为提示基线分别达到26.4%和17.0%。
• 原因：小模型缺乏领域知识以精确描述具体引理，导致训练信号稀疏。
• 补救：结合图展开技术，将检索结果的邻居节点纳入候选，召回率提升至13.4%，基本追平Gemini基线。

十、 扩展至PDF教材：超越arXiv的局限

为覆盖教科书等非LaTeX资源，团队开发了PDF摄取工具，以Artin《代数》为例：

• 流程：pymupdf筛选含定理标题的页面 -> Nougat OCR识别 -> 逐行解析提取陈述。
• 成果：提取406条陈述，59.6%包含证明内容，覆盖率与LaTeX头部标签计数吻合。
• 局限：PDF缺乏\label和\ref等结构化标记，无法使用高精度确定性提取器，依赖关系构建主要靠符号提取和语义检索，精度有限。恢复OCR文本中的交叉引用结构是未来方向。

十一、 引用恢复实验：AI能否“补全”缺失的引用？

模拟读者在阅读论文时遇到缺失引用的场景，测试AI恢复被删引理的能力。

• 设置：从2026年2月后arXiv论文中抽取149个片段，移除引用命令和参考文献条目。
• 结果：
• Gemini 3.1 Pro在开放网络搜索条件下表现最佳，精确匹配率达57.0%。
• 图导航检索优于纯密集检索，但仍逊于直接搜索原文。
• 局限性：该实验存在“作弊”嫌疑（模型可直接搜索原文片段），团队已将其列为局限。

结语

TheoremGraph项目通过整合非形式化论文与形式化证明，构建了包含近5万对跨模态匹配的知识基础设施。尽管在自动形式化和强化学习检索方面仍有提升空间，但其展现出的图结构+语义嵌入+大模型的协同效应，为AI辅助数学研究提供了关键支撑。

资源发布：
* 数据集、提取工具、HTTP API及MCP接口：theoremsearch.com
* 跨模态匹配数据集：Hugging Face
* 完整论文：arXiv:2606.25363v1

Q&A

Q1：TheoremGraph提取的非形式化依赖边中，哪种类型的精度最高？
A：确定性提取器（Deterministic Extractor）精度最高。它通过解析LaTeX源代码中的显式引用命令（如\ref和\cite）建立依赖关系，经独立LLM法官验证，准确率达98.8%。相比之下，启发式提取器准确率为76.6%，符号提取器为42.7%。

Q2：LeanGraph提取的六种依赖边类型分别是什么？
A：LeanGraph将形式化依赖细分为以下六类，以支持下游系统按性质过滤：
1. extends：结构体或类的继承关系。
2. field：结构体字段类型中的依赖。
3. sig：出现在声明签名（Signature）中的常量。
4. proof：定理证明项中用到的常量。
5. def：非命题定义体中用到的常量。
6. docref：文档字符串中有效的反引号引用。

Q3：TheoremGraph的检索系统与LeanSearch v2的比较结果如何？
A：在MathlibQR基准测试（公平-810子集）中：
* 召回率（Recall@10）：TheoremGraph的召回优化配置（Config E，含图展开）达到0.775，仅比LeanSearch v2加重排序器（0.780）低0.5个百分点，且无需重排序器。
* 排名质量（nDCG@10）：TheoremGraph的排名优化配置（Config F）达到0.558，优于LeanSearch v2纯检索器基线（0.494），但低于LeanSearch v2加重排序器后的结果（0.623）。
* 总体：TheoremGraph在无需重排序的情况下，性能已接近最先进系统。

本文地址：https://www.xyaji.com/html/021a80399175.html