对超过900万条数学定理进行语义搜索

摘要

数学成果检索依然面临挑战：现有工具大多返回整篇论文，而数学工作者与定理证明智能体通常需要定位能解答查询的特定定理、引理或命题。尽管语义搜索技术发展迅速，但其在大型高专业性语料（如研究级数学定理）中的表现仍鲜为人知。本研究基于从arXiv等八个来源提取的920万条定理陈述构建统一语料库——这是目前最大的公开研究级人工撰写定理库，首次系统性地开展大规模语义定理检索研究。我们采用简短自然语言描述作为定理的检索表征，系统分析了表征语境、语言模型选择、嵌入模型及提示策略对检索质量的影响。在由专业数学家编写的定理搜索评估集上，本方法在定理级和论文级检索效果上均显著超越现有基线，证明语义定理搜索在互联网规模下具有可行性和有效性。定理搜索工具详见https://huggingface.co/spaces/uw-math-ai/theorem-search，数据集详见https://huggingface.co/datasets/uw-math-ai/TheoremSearch。

English

Searching for mathematical results remains difficult: most existing tools retrieve entire papers, while mathematicians and theorem-proving agents often seek a specific theorem, lemma, or proposition that answers a query. While semantic search has seen rapid progress, its behavior on large, highly technical corpora such as research-level mathematical theorems remains poorly understood. In this work, we introduce and study semantic theorem retrieval at scale over a unified corpus of 9.2 million theorem statements extracted from arXiv and seven other sources, representing the largest publicly available corpus of human-authored, research-level theorems. We represent each theorem with a short natural-language description as a retrieval representation and systematically analyze how representation context, language model choice, embedding model, and prompting strategy affect retrieval quality. On a curated evaluation set of theorem-search queries written by professional mathematicians, our approach substantially improves both theorem-level and paper-level retrieval compared to existing baselines, demonstrating that semantic theorem search is feasible and effective at web scale. The theorem search tool is available at https://huggingface.co/spaces/uw-math-ai/theorem-search{this link}, and the dataset is available at https://huggingface.co/datasets/uw-math-ai/TheoremSearch{this link}.

对超过900万条数学定理进行语义搜索

Semantic Search over 9 Million Mathematical Theorems

摘要

Support