Semantic Search over 9 Million Mathematical Theorems

이 논문은 arXiv 등 920 만 개의 수학적 정리를 대상으로 자연어 설명을 활용한 대규모 의미 기반 정리 검색 시스템을 구축하고, 전문가가 작성한 평가 세트를 통해 기존 방법보다 뛰어난 검색 성능을 입증했습니다.

핵심

1. 문제: "책 전체를 뒤져야 하는 고통"

지금까지 수학자나 AI 가 새로운 정리를 찾을 때 겪는 문제는 마치 거대한 도서관에 비유할 수 있습니다.

• 현재 상황: 연구자가 "세상에서 가장 빠른 달리기 기록"이라는 특정 사실을 알고 싶다면, 도서관 사서 (구글, arXiv 등) 는 그 사실이 적힌 **'책 전체'**를 찾아서 연구자에게 건네줍니다.
• 문제점: 그 책에는 100 페이지 분량의 내용이 있는데, 정작 필요한 '기록'은 45 페이지의 한 줄에 불과합니다. 연구자는 그 책의 100 페이지를 다 읽어서 45 페이지를 찾아내야 합니다.
• AI 의 실수: 최근의 AI(챗봇 등) 도 이 책을 다 읽지 못해, "아마도 이 책에 있을 거예요"라고 말하거나, 아예 틀린 책의 페이지를 가리키는 경우가 많습니다. 실제로 AI 가 수십 년 전에 이미 증명된 정리를 "새로운 발견"이라고 착각하는 일도 벌어졌습니다.

2. 해결책: "수학의 '한 줄 요약' 카드" 만들기

이 연구팀은 920 만 개의 수학 논문에서 개별적인 '정리 (Theorem)' 하나하나를 찾아내어, 각각에 **자연어 (사람이 쓰는 말) 로 된 '한 줄 요약 카드'**를 붙였습니다.

• 비유: 도서관의 책 전체를 검색하는 대신, 책 속에 있는 각각의 중요한 문장 (진리) 을 뽑아내어 작은 카드로 만들었습니다.
• 카드의 내용: 이 카드는 복잡한 수식 ($\LaTeX$) 이 아니라, "이 정리는 무엇을 말하는가?"를 설명하는 쉬운 문장으로 되어 있습니다.
  • 예시: "원주율 $\pi$는 무리수이다"라는 복잡한 수식 대신, **"원둘레를 지름으로 나눈 값은 소수점 끝이 무한히 이어지는 수이다"**라고 적힌 카드입니다.

3. 작동 원리: "의미로 찾는 검색 엔진"

이제 이 920 만 개의 '카드'를 쌓아두고, 사용자가 질문을 하면 **의미 (Semantic)**가 비슷한 카드를 찾아줍니다.

• 기존 방식 (문자 매칭): "원주율"이라는 단어가 들어간 카드를 찾습니다. (하지만 '원주율'이 들어간 다른 불필요한 내용도 많이 나옵니다.)
• 이 연구의 방식 (의미 매칭): 사용자가 "소수점 끝이 무한히 이어지는 수"라고 검색하면, 비록 '원주율'이라는 단어가 없더라도 **의미가 똑같은 '카드'**를 찾아냅니다.
• 핵심 기술: AI 가 복잡한 수식을 읽지 않고, **수학자가 이해할 수 있는 쉬운 말 (슬로건)**로 정리된 내용을 검색합니다.

4. 왜 이것이 혁신적인가? (실험 결과)

연구팀은 전문 수학자들에게 111 개의 질문을 던져 이 시스템을 테스트했습니다.

• 기존 도구 (구글, 챗GPT 등): 정답을 찾지 못하거나, 관련 책 전체를 추천했습니다. (정답 찾기 성공률 약 20% 미만)
• 이 연구의 시스템: **45%**의 확률로 사용자가 원하는 '정리'를 정확히 찾아냈습니다.
• 의미: 수학자들이 원하는 '진리'를 책 전체를 뒤지지 않고, 직접적이고 정확하게 찾을 수 있게 된 것입니다.

5. 실제 활용: "AI 가 수학 문제를 풀 때의 조력자"

이 시스템은 AI 가 수학 문제를 풀 때 아주 유용하게 쓰입니다.

• 상황: AI 가 어려운 수학 문제를 풀려고 할 때, 필요한 '도구 (정리)'를 모르면 엉뚱한 답을 만들어냅니다 (환각 현상).
• 해결: AI 가 이 '카드 검색 시스템'을 연결하면, "이 문제를 풀려면 이 정리가 필요해!"라고 정확한 도구를 찾아서 가져옵니다.
• 결과: AI 가 틀린 답을 지어내는 대신, 실제 수학 논문 속에 있는 정확한 정리를 인용하여 올바른 논리를 전개할 수 있게 됩니다.

6. 결론: "수학 지식의 민주화"

이 연구는 단순히 검색 속도를 높인 것이 아니라, 수학 지식을 '책'이라는 단위가 아닌 '진리'라는 단위로 분해했습니다.

마치 레고 블록을 쌓아 올린 건물을 해체하여, 필요한 '특정 블록' 하나하나를 바로 꺼낼 수 있게 만든 것과 같습니다. 이제 수학자나 AI 는 거대한 책 더미 속에서 헤매지 않고, 정확히 필요한 '진리의 조각'을 손쉽게 찾아내어 새로운 발견을 할 수 있게 되었습니다.

이 프로젝트는 theoremsearch.com에서 누구나 무료로 사용해 볼 수 있습니다.

기술 요약

1. 문제 정의 (Problem)

기존의 수학 지식 검색 도구 (Google Scholar, arXiv, 최신 LLM 등) 는 전체 문서 (Paper) 수준에서 검색을 수행합니다. 그러나 수학자와 자동 증명 에이전트는 특정 정리 (Theorem), 보조정리 (Lemma), 명제 (Proposition) 와 같은 구체적인 수학적 결과를 찾고자 할 때가 많습니다.

• 현황: 연구자가 새로운 결과를 증명하기 전에 기존 문헌에 해당 명제가 존재하는지 확인해야 하며, AI 에이전트 또한 증명 과정에서 관련 보조정리를 검색해야 합니다.
• 한계: 현재 도구들은 논문 전체를 반환하므로, 사용자는 원하는 특정 명제를 찾기 위해 논문을 수동으로 스캔해야 합니다. 이는 arXiv 에 240 만 개 이상의 논문 (수학만 69 만 개 이상) 이 존재하는 환경에서 비효율적이며, AI 가 이미 증명된 문제를 다시 "해결"했다고 잘못 주장하는 등의 오류를 유발합니다.

2. 방법론 (Methodology)

저자들은 920 만 개의 정리 문장을 포함하는 대규모 코퍼스를 구축하고, 이를 자연어 기반의 의미 검색 (Semantic Search) 으로 변환하는 파이프라인을 개발했습니다.

A. 데이터 수집 및 파싱 (Data Collection & Parsing)

• 소스: arXiv(수학, 통계, 컴퓨터 과학, 물리 등 7 개 분야), Stacks Project, ProofWiki 등 총 8 개 출처에서 920 만 개의 정리 문장을 추출했습니다.
• 파싱 전략: LaTeX 문서의 다양한 정의 방식으로 인해 3 단계 파싱 전략을 사용했습니다.
  1. plasTeX: LaTeX 소스를 노드 트리로 변환하여 정리 환경을 식별 (약 690 만 개 정리 추출).
  2. TeX Logging: 커스텀 LaTeX 패키지를 주입하여 컴파일 시 정리 데이터를 기록 (약 180 만 개).
  3. Regex 기반: 정규 표현식을 사용하여 \begin{...} 등 구분자 기반 추출 (약 54 만 개).
• 데이터 정제: 8 자 미만의 짧은 정리나 "and", "let"으로 끝나는 malformed 데이터는 휴리스틱으로 제거했습니다.

B. 정리 표현 (Theorem Representation)

• 핵심 아이디어: 원본 LaTeX 수식 그대로를 임베딩하는 대신, LLM 이 생성한 자연어 "슬로건 (Slogan)" 을 검색 표현으로 사용합니다.
• 생성 과정: DeepSeek V3 모델을 사용하여 각 정리의 본문을 바탕으로 간결한 영어 설명 (최대 4 문장) 을 생성합니다.
  • 제약: 수학적 기호나 증명 세부 사항, 문서 구조 참조를 배제하고 결과만 서술하도록 프롬프트를 설계했습니다.
• 맥락 실험: 슬로건 생성 시 본문만, 본문 + 초록, 본문 + 서론 중 어떤 맥락이 검색 성능에 영향을 미치는지 분석했습니다.

C. 검색 및 임베딩 (Retrieval & Embedding)

• 임베딩 모델: Qwen3-Embedding-8B 모델을 사용하여 자연어 슬로건과 사용자 쿼리를 공유된 의미 공간 (Vector Space) 에 매핑합니다.
• 인덱싱: PostgreSQL 의 pgvector 확장 기능을 사용하며, HNSW (Hierarchical Navigable Small World) 인덱스와 이진 양자화 (Binary Quantization) 를 결합하여 빠른 근접 이웃 검색을 수행합니다.
• 재랭킹 (Reranking): 초기 검색 결과 (Top-100) 를 Qwen3-Reranker-0.6B 를 사용하여 정밀하게 재순위화합니다.

3. 주요 기여 (Key Contributions)

1. 대규모 정리 코퍼스: 인간이 작성한 연구 수준의 정리를 다룬 최대 규모의 공개 데이터셋 (920 만 개) 을 구축하고 공개했습니다.
2. 표현 방식의 체계적 분석:
   • 원본 LaTeX 임베딩보다 자연어 슬로건 임베딩이 검색 성능을 획기적으로 향상시킵니다.
   • 슬로건 생성 시 논문 서론 (Introduction) 을 포함하는 것이 본문만 사용하는 것보다 성능이 우수함을 증명했습니다.
   • 임베딩 모델 (Qwen3 8B) 과 생성 모델 (Claude Opus 4.5 등) 의 선택이 성능에 결정적임을 밝혔습니다.
3. 최신 성능 달성 (SOTA): 전문가가 작성한 111 개 쿼리 세트를 기준으로 기존 도구들을 압도하는 성능을 달성했습니다.

4. 실험 결과 (Results)

전문 수학자가 작성한 111 개 쿼리에 대한 평가 결과 (Hit@20 기준):

모델/방법	정리 수준 (Theorem-level) Hit@20	논문 수준 (Paper-level) Hit@20
본 연구 (Qwen3 8B + Reranker)	45.0%	56.8%
ChatGPT 5.2 (Search)	19.8%	-
Gemini 3 Pro	27.0%	-
Google Search	-	37.8%
arXiv Search	2.7%	2.7%

• 의미: 제안된 방법은 기존 검색 엔진이나 LLM 보다 정리 수준에서 2 배 이상, 논문 수준에서도 1.5 배 이상 우수한 성능을 보입니다.
• 특이점: Google Search 나 일반 LLM 은 논문 제목이나 초록에 의존하여 논문의 후반부에 있는 보조정리 (Lemma) 를 찾기 어렵지만, 본 시스템은 모든 정리를 독립적으로 인덱싱하여 이러한 "깊은 위치"의 결과도 효과적으로 찾습니다.
• RAG 효과: Claude(Opus 4.5) 를 사용하여 본 데이터베이스를 RAG(검색 증강 생성) 도구로 연결했을 때, 수학적으로 잘못된 추론을 수정하고 정확한 정리를 인용하는 능력을 입증했습니다.

5. 의의 및 결론 (Significance)

• 수학 지식 접근의 혁신: 수학적 지식을 "문서" 단위가 아닌 "정리" 단위로 접근할 수 있게 하여, 연구자와 AI 에이전트의 작업 효율을 극대화합니다.
• AI 안전성 및 정확성: AI 가 기존에 증명된 결과를 모르고 중복하여 "발견"하는 것을 방지하고, 정확한 문헌 기반 증명을 가능하게 합니다.
• 실용적 도구: theoremsearch.com 을 통해 검색 도구, REST API, MCP 서버, 데이터셋을 공개하여 연구 커뮤니티와 AI 개발자가 즉시 활용할 수 있도록 했습니다.

이 연구는 대규모 수학 텍스트에 대한 의미 검색이 웹 규모에서도 실현 가능하고 효과적임을 입증하며, 향후 자동 수학 증명 및 수학 지식 관리 시스템의 새로운 표준을 제시합니다.