Семантический поиск по 9 миллионам математических теорем
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
Аннотация
Поиск математических результатов остается сложной задачей: большинство существующих инструментов извлекают целые статьи, в то время как математики и системы доказательства теорем часто ищут конкретную теорему, лемму или утверждение, отвечающее на запрос. Хотя семантический поиск быстро развивается, его поведение на больших, высокотехничных корпусах, таких как теоремы уровня научных исследований, остается малоизученным. В данной работе мы представляем и исследуем семантический поиск теорем в крупном масштабе на едином корпусе из 9,2 миллионов формулировок теорем, извлеченных из arXiv и семи других источников, что представляет собой крупнейший общедоступный корпус теорем уровня исследований, созданных человеком. Мы представляем каждую теорему кратким описанием на естественном языке в качестве представления для поиска и систематически анализируем, как контекст представления, выбор языковой модели, модель эмбеддингов и стратегия промптинга влияют на качество поиска. На курируемом наборе для оценки поисковых запросов по теоремам, составленном профессиональными математиками, наш подход значительно улучшает как поиск на уровне теорем, так и на уровне статей по сравнению с существующими базовыми методами, демонстрируя, что семантический поиск теорем осуществим и эффективен в масштабах веба. Инструмент поиска теорем доступен по ссылке 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}.