900万件の数学定理に対する意味検索
Semantic Search over 9 Million Mathematical Theorems
February 5, 2026
著者: Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Giovanni Inchiostro, Vasily Ilin
cs.AI
要旨
数学的成果の検索は依然として困難な課題である。既存のツールの多くは論文全体を検索するが、数学者や定理証明エージェントが求めているのは、クエリに答える特定の定理、補題、命題であることが多い。意味検索は急速に進歩しているものの、研究レベルの数学定理のような大規模で高度に専門的なコーパスにおけるその挙動は十分に理解されていない。本研究では、arXivおよびその他7つの情報源から抽出した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}.