900万数学定理的语义搜索 Semantic Search over 9 Million Mathematical Theorems
构建920万数学定理语料库并实现语义检索系统，在专业数学查询上显著优于现有工具。
前置知识
密集段落检索（Dense Passage Retrieval）
密集段落检索是一种基于深度学习的信息检索方法，使用双编码器架构将查询和文档映射到相同的向量空间中。与传统的稀疏检索方法（如BM25）不同，密集检索通过语义相似度而非关键词匹配来检索相关文档。典型代表包括DPR（Dense Passage Retrieval）和Sentence-BERT，它们使用预训练语言模型将文本编码为固定维度的向量，然后通过余弦相似度或点积计算相关性。
本文的核心方法就是基于密集检索，但需要将其扩展到数学定理这一特殊领域，理解密集检索的基本原理对于把握本文的技术路线至关重要。
向量嵌入（Vector Embedding）
向量嵌入是将文本、图像等非结构化数据转换为固定维度数值向量的技术。在自然语言处理中，词嵌入（如Word2Vec）和句子嵌入（如Sentence-BERT）将语义信息编码到向量空间中，使得语义相似的文本在向量空间中距离较近。现代嵌入模型如E5、Qwen3-Embedding等能够将整个段落甚至文档编码为向量，支持高效的语义相似度计算。常见的相似度度量包括余弦相似度：$\cos(\mathbf{a}, \mathbf{b}) = ?rac{\mathbf{a} \cdot \mathbf{b}}{\|\mathbf{a}\| \|\mathbf{b}\|}$和点积相似度：$ ext{sim}(\mathbf{a}, \mathbf{b}) = \mathbf{a} \cdot \mathbf{b}$。
本文的关键创新之一是研究不同嵌入模型对数学定理检索的影响，理解向量嵌入的工作原理有助于理解为什么某些嵌入模型在数学领域表现更好。
数学信息检索（Mathematical Information Retrieval）
数学信息检索（MathIR）是专门针对数学内容的信息检索领域，需要处理数学符号、公式、定理等特殊内容。传统MathIR方法主要关注公式级别的检索，使用符号匹配或结构相似度。然而，语义理解数学定理的含义比匹配公式结构更具挑战性，因为数学表达式通常包含复杂的逻辑关系和领域特定的符号约定。
本文的核心挑战就是如何将MathIR从公式级检索扩展到定理级语义检索，理解MathIR的传统方法和局限性有助于把握本文的创新点。
层次可导航小世界图（HNSW）索引
HNSW（Hierarchical Navigable Small World）是一种用于近似最近邻搜索的索引结构，特别适合高维向量空间。它通过构建多层次的图结构，在不同粒度上组织向量数据，使得搜索时能够快速跳转到相关区域。HNSW结合二进制量化可以进一步压缩向量表示，在保持检索质量的同时显著提升搜索速度。
本文使用HNSW索引来管理920万条定理的向量表示，理解HNSW的工作原理有助于理解系统的可扩展性和检索效率。
检索增强生成（Retrieval-Augmented Generation）
检索增强生成（RAG）是一种结合检索和生成的技术范式，通过检索相关文档来增强大语言模型的生成质量。在数学领域，RAG可以帮助LLM获取相关的定理和引理，避免生成不准确或幻觉的数学内容。典型的RAG系统包括检索器（负责找到相关文档）和生成器（基于检索结果生成回答）两个组件。
本文展示了定理检索作为RAG工具的应用案例，证明了高质量的数学定理检索能够显著提升LLM在数学推理任务上的表现。
研究动机
现有的数学文献检索工具存在严重的粒度不匹配问题。数学知识的核心组织单位是离散的定理、引理、命题和推论，但现有的检索工具——包括Google Scholar、arXiv搜索，甚至配备网络搜索的ChatGPT和Gemini——都只能在论文级别进行检索。当数学家或自动定理证明系统需要查找特定的定理陈述时，他们被迫手动扫描整篇论文来定位相关结果。这种不匹配导致了严重的效率损失：arXiv托管着超过240万篇论文，其中数学领域超过69万篇。一项对超过14000篇撤回的arXiv预印本的研究发现，有2.5%是因为作者的结果已存在于先前文献中而被撤回。更具体地，Popescu-Pampu（2007）、Zhang（2012）和Shahryari（2020）都是在发现其主要结果已被先前建立后才撤回的。AI系统也面临同样的问题：Erdős Problems Project记录了AI工具“解决”了几十年前已建立的公开问题的案例。这些案例凸显了定理级别检索的迫切需求。
本文的目标是本文的具体目标是构建一个大规模的数学定理语料库，并研究如何实现有效的语义定理检索。具体来说，作者要创建包含超过900万条定理陈述的统一语料库，这是迄今为止最大的人类撰写的、研究级数学定理集合。在此基础上，他们要系统性地分析表示上下文、语言模型选择、嵌入模型和提示策略如何影响检索质量。最终目标是实现一个实用的定理检索系统，能够在专业数学家撰写的查询上达到至少45%的Hit@20（定理级别）和56%的Hit@20（论文级别），显著优于现有的基线方法。
与已有工作不同的是，本文的独特切入角度在于将定理陈述视为一等公民进行检索对象，而不是论文的附属品。与现有工作不同，作者不是简单地改进论文级别的检索，而是专注于定理级别的语义理解。他们发现了一个关键洞察：数学家通常用自然语言查询来描述他们要找的定理，但定理本身通常以LaTeX公式形式存在。这种不对称性意味着直接嵌入LaTeX公式效果很差，而将定理转换为自然语言描述（称为“标语”）可以显著改善检索性能。这种“标语化”策略将检索任务从对称搜索（正式符号查询正式符号）转换为非对称任务（非正式查询检索正式化内容），这与Wang等人（2022）提出的嵌入方法论一致。
核心方法
本文的方法可以类比为为数学知识建立一个“语义索引系统”。就像图书馆为每本书创建主题标签和摘要一样，作者为每个数学定理创建了一个自然语言描述（称为“标语”），然后将这些描述转换为向量表示存储在数据库中。技术路线分为四个主要阶段：首先是从arXiv和其他七个来源解析定理陈述，构建包含920万条定理的大规模语料库；其次使用大语言模型为每个定理生成简洁的自然语言描述；然后使用嵌入模型将这些描述转换为向量表示；最后构建支持高效近似最近邻搜索的数据库系统。整个流程的关键创新在于将符号化的数学定理转换为语义丰富的自然语言表示，从而支持语义检索。
本文最核心的创新点是将数学定理从LaTeX公式转换为自然语言“标语”进行检索，这与直接嵌入LaTeX公式的方法有本质区别。实验表明，直接嵌入LaTeX公式的Gemma 0.3B模型在定理级别只达到2.7%的Hit@1，而使用标语后提升到8.1%。更强大的Qwen3 8B模型使用标语后达到17.1%的Hit@1，比ChatGPT 5.2的11.7%高出5.4个百分点。这种“标语化”策略的成功源于两个关键洞察：第一，数学家通常用自然语言查询，而定理以符号形式存在，标语桥接了这种语义鸿沟；第二，现代嵌入模型在自然语言上的表现远优于处理符号密集的数学符号。标语化将检索任务从对称搜索转换为非对称任务，其中非正式查询检索正式化内容，这与文本嵌入研究中的最佳实践一致。
方法步骤详情
方法分为四个主要步骤：第一步是定理解析，使用三种策略从arXiv论文中提取定理：首先是使用plasTeX库将LaTeX转换为结构化节点树，成功解析42.2万篇论文，提取约690万条定理；其次是TeX日志方法，通过注入自定义LaTeX包记录定理数据，解析13.7万篇论文，提取约180万条定理；最后是正则表达式解析作为后备方案，解析3万篇论文，提取约54.2万条定理。第二步是标语生成，使用DeepSeek V3模型为每个定理生成简洁的自然语言描述，评估三种上下文策略：仅定理主体、定理主体+摘要、定理主体+引言。第三步是向量嵌入，使用Qwen3-Embedding-8B模型将标语和查询映射到4096维向量空间。第四步是检索系统构建，使用PostgreSQL数据库配合pgvector扩展，采用HNSW索引和二进制量化支持快速近似最近邻搜索，检索时先通过汉明距离获取候选池，再用余弦相似度重排序。
技术新颖性
本文的技术新颖性体现在三个方面：首先是大规模定理语料库的构建，包含920万条定理，覆盖arXiv的数学、统计、计算机科学等多个领域，以及ProofWiki、Stacks Project等七个其他来源，这是迄今为止最大的统一数学定理集合。其次是系统性的表示学习研究，作者首次系统分析了上下文窗口、LLM选择、嵌入模型和提示策略对数学定理检索的影响，发现标语生成时包含论文引言可以显著提升检索质量。最后是实际可部署的检索系统，作者不仅提供了研究结果，还部署了公开的搜索工具、REST API和MCP服务器，使得其他研究者和AI系统可以直接使用这一能力。与现有工作相比，本文不是简单地改进公式检索，而是首次实现了定理级别的语义检索，填补了数学信息检索领域的重要空白。
实验结果
本文的实验结果表明，语义定理检索在大规模数学语料库上是可行且有效的。在包含111个专业数学家撰写查询的验证集上，最佳配置（Qwen3 8B嵌入模型+重排序器）在定理级别达到45.0%的Hit@20和27.0%的MRR@20，在论文级别达到63.1%的Hit@20和41.6%的MRR@20。这里Hit@k衡量的是正确结果是否出现在前k个结果中：$ ext{Hit@k} = ?rac{1}{|Q|} \sum_{i=1}^{|Q|} \max_{1 \leq j \leq k} I(r_{i,j})$，其中$是查询集合，{i,j}$是第$个查询的第$个结果，(r_{i,j})$在{i,j}$精确匹配时为1。MRR@k则是第一个相关结果的倒数排名的平均值：$ ext{MRR@k} = ?rac{1}{|Q|} \sum_{i=1}^{|Q|} ?rac{1}{ ext{rank}_i}$。这些结果显著优于现有基线：ChatGPT 5.2（带搜索）在定理级别只达到19.8%的Hit@20，Gemini 3 Pro达到27.0%，Google搜索在论文级别达到37.8%。特别值得注意的是，直接嵌入LaTeX公式的Gemma 0.3B模型在定理级别只达到9.0%的Hit@20，而使用标语后提升到25.2%，证明了标语化策略的有效性。消融研究显示，上下文窗口对检索质量有显著影响：仅使用定理主体时Hit@20为73.7%，加入摘要后保持73.7%，但加入论文引言后提升到76.3%。LLM选择也很重要，Claude Opus 4.5生成的标语使Hit@20达到84.2%，而DeepSeek V3.1达到73.7%。任务指令的影响因模型而异：Qwen嵌入模型在提供数学检索指令时表现更好，而Gemma模型在无指令时表现更好。嵌入空间分析显示，Qwen3 8B产生的聚类比Gemma 0.3B更紧密、分离度更好，这与检索性能差距一致。一个有趣的发现是，重复短查询（如“Landau equation Landau equation”）可以显著改善检索质量，这表明嵌入模型对输入长度敏感。系统端到端延迟约为3秒，比ChatGPT和Gemini的60+秒快得多，后者需要执行多次网络搜索和文档解析。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 定理级别检索 | Hit@20 | 45.0%（Qwen3 8B + 重排序器） | ChatGPT 5.2: 19.8%, Gemini 3 Pro: 27.0% | 比ChatGPT提升25.2个百分点，比Gemini提升18.0个百分点 |
| 论文级别检索 | Hit@20 | 63.1%（Qwen3 8B + 重排序器） | Google搜索: 37.8%, arXiv搜索: 2.7% | 比Google搜索提升25.3个百分点，比arXiv搜索提升60.4个百分点 |
| 定理级别检索 | MRR@20 | 27.0%（Qwen3 8B + 重排序器） | ChatGPT 5.2: 13.9%, Gemini 3 Pro: 19.6% | 比ChatGPT提升13.1个百分点，比Gemini提升7.4个百分点 |
| 论文级别检索 | MRR@20 | 41.6%（Qwen3 8B + 重排序器） | Google搜索: 23.7%, arXiv搜索: 1.1% | 比Google搜索提升17.9个百分点，比arXiv搜索提升40.5个百分点 |
局限与改进
尽管本文取得了显著成果，但仍存在一些局限性。首先，验证集规模较小，只有111个查询，虽然这是数学信息检索领域的典型规模（LeanSearch的查询集为50个，ARQMath-3为78个），但可能无法完全代表真实使用场景的多样性。其次，验证集主要集中在代数几何、分析和偏微分方程领域，覆盖了32个arXiv数学标签中的12个，对其他数学领域的泛化能力有待验证。第三，定理解析存在质量损失，plasTeX偶尔会截断定理主体，特别是当论文依赖未知LaTeX包时，虽然作者使用了启发式过滤（如过滤短于8个字符或以“and”或“let”结尾的定理），但仍可能包含格式错误的结果。第四，标语生成依赖大语言模型，引入了额外的成本和潜在偏差：构建整个语料库花费了约6000美元（4000美元用于LLM API调用，2000美元用于计算和存储），且不同LLM生成的标语质量差异显著。第五，系统对短查询的处理存在缺陷，嵌入模型对输入长度敏感，短关键词查询（如“Landau equation”）可能被填充或通用上下文主导，需要重复查询来增强关键术语的信号。最后，论文没有深入探讨多语言支持，虽然嵌入模型是多语言的，但标语生成和查询处理主要针对英语。
独立分析的弱点
本文的弱点主要体现在以下几个方面：首先，验证集的选择存在潜在偏差，111个查询由三位熟悉相关工作的研究数学家撰写，虽然他们是在没有访问语料库或标语的情况下凭记忆撰写查询，但查询可能偏向他们熟悉的特定领域和作者，这可能导致检索性能被高估。改进方向是构建更大规模、更多样化的验证集，包括不同数学领域、不同难度级别和不同查询风格。其次，标语生成策略虽然有效，但增加了系统复杂性和成本，每个定理都需要调用LLM生成标语，且标语质量依赖于LLM的数学理解能力。未来可以探索更高效的标语生成方法，如使用小型专门训练的模型，或者开发直接处理LaTeX公式的嵌入模型。第三，检索系统虽然实现了3秒的延迟，但没有与现有的论文级检索系统（如Google Scholar）进行公平的延迟比较，因为后者需要执行网络搜索和文档解析。可以考虑优化嵌入模型推理速度，或使用更高效的向量数据库。第四，系统缺乏用户反馈的持续学习机制，虽然论文提到有轻量级反馈系统，但没有描述如何利用这些反馈改进检索质量。可以引入在线学习或强化学习机制，根据用户点击和评分调整检索策略。
未来方向
基于本文的工作，有几个有前景的研究方向：首先，扩展定理语料库到更多来源，如nLab和其他开源教科书，作者已经计划了这一扩展，这将进一步提高系统的覆盖范围。其次，开发专门为数学内容设计的嵌入模型，当前使用通用嵌入模型处理数学内容，一个在数学语料库上专门训练的嵌入模型可能显著提升性能。第三，将定理检索与自动定理证明系统集成，作者展示了RAG增强的LLM推理案例，但可以更深入地研究检索结果如何指导证明搜索和引理选择。第四，支持多语言数学检索，当前系统主要处理英语内容，但数学文献包含大量其他语言的重要工作。第五，开发交互式检索界面，允许用户通过对话逐步细化查询，而不是一次性提供完整查询。最后，研究定理之间的关系网络，如引用关系、依赖关系和推广关系，这可以支持更智能的文献综述和知识发现。
复现评估
本文在可复现性方面表现良好，作者提供了完整的开源实现。数据集已在Hugging Face上公开发布（uw-math-ai/theorem-search-dataset），仅包含使用宽松许可证（CC BY和CC0）的arXiv论文定理。搜索工具、REST API和MCP服务器都在theoremsearch.com上公开可用。代码用于预处理、清理和标记数据在GitHub仓库中提供。复现整个系统需要：1）访问LLM API生成标语，成本约4000美元；2）计算资源用于嵌入生成和数据库构建，约2000美元；3）PostgreSQL数据库配合pgvector扩展；4）Qwen3-Embedding-8B模型进行向量嵌入。对于大多数研究团队来说，直接使用作者提供的预计算嵌入和数据库是更可行的选择，而不是从头开始构建整个系统。论文详细描述了所有技术细节，包括提示模板、嵌入模型配置和索引参数，使得有足够资源的团队能够复现结果。
论文图表
该表格展示了用于嵌入模型的任务指令。定理侧的指令为：“Represent the given math statement for retrieving related statement by natural language query.”用户查询侧的指令为：“Given a math search query, retrieve theorems mathematically equivalent to the query.”
这个表格展示了系统的关键实现细节，说明了如何通过任务指令引导嵌入模型理解数学检索任务。
该表格展示了三种上下文窗口对应的提示模板。所有模板都要求LLM生成准确、不超过四句话的ASCII摘要，避免LaTeX和数学符号，不引用“本定理”，不包含证明步骤、动机或背景讨论。主要区别在于是否包含论文摘要或引言作为上下文。
这个表格展示了标语生成的关键实现细节，说明了如何通过精心设计的提示模板引导LLM生成高质量的定理描述。
该表格展示了用于ChatGPT 5.2和Gemini 3 Pro基线的检索提示。提示要求模型返回包含定理陈述、arXiv ID和相关来源的JSON格式结果。这些提示旨在模拟用户使用LLM进行数学文献检索的典型方式。
这个表格展示了基线方法的实现细节，帮助读者理解如何公平比较本文方法与现有LLM检索工具。