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}.