Semantic Search over 9 Million Mathematical Theorems

この論文は、arXiv などの 920 万件の定理を網羅する大規模コーパスを用いて、自然言語記述による意味検索が数学者による専門的な定理検索において既存手法を大幅に上回る有効性を有することを示しています。

要約

数学の「定理」を直接探す新しい地図：900 万件の知識を巡る冒険

この論文は、「数学の定理（定理）」という、非常に専門的で小さな「真実」を、インターネット上の膨大な論文から素早く見つけるための新しい検索エンジンを作ったというお話しです。

従来の検索では「論文全体」を探すしかありませんでしたが、この研究は「論文の中の『ある特定の定理』」を直接見つける方法を確立しました。

以下に、難しい専門用語を避け、身近な例え話を使って解説します。

---

1. 従来の問題：「図書館の棚」から「本」を探す難しさ

Imagine you are looking for a specific recipe (say, "how to make the perfect soufflé") inside a massive library containing 2.4 million cookbooks (arXiv の論文).

• 今の検索（Google Scholar や arXiv）：
  検索すると、「『フランス料理大全』という本が見つかりました」という結果が返ってきます。でも、その本は 500 ページあります。あなたが知りたい「 soufflé のレシピ」が、その本の 342 ページ目にあるのか、それとも「パンの章」の 12 ページ目にあるのか、本を開いて1 ページずつめくって探す必要があります。
• AI の失敗：
  最新の AI（ChatGPT など）に「 soufflé のレシピを教えて」と聞いても、AI は「本」を推薦しますが、たまに「昔、誰かが同じレシピを書いていたのに気づかずに、新しい本を出してしまった」という**重複（撤回された論文）**を犯したり、間違ったページを指差したりすることがあります。

この研究のゴール：
「本全体」を探すのではなく、「 soufflé のレシピ」そのものを、図書館の膨大な資料から直接、瞬時に見つけることです。

---

2. 解決策：900 万件の「定理」を「短い言葉」に変える魔法

この研究チームは、arXiv（学術論文のデータベース）や他の信頼できるソースから、920 万件もの「定理（数学の重要な結論）」を抜き出しました。

しかし、数学の定理は「LaTeX」という特殊な記号（$\sum$ や $\int$ など）で書かれており、普通の検索エンジンには読めません。

そこで彼らは、**「魔法の翻訳機（AI）」**を使いました。

• 魔法の翻訳（スローガン生成）：
  複雑な数式で書かれた定理を、AI が**「短い、普通の英語の文章（スローガン）」**に書き換えます。
  • 元の定理: 「$\forall x \in \mathbb{R}, \exists y \in \mathbb{R} \dots$」のような難解な記号。
  • AI のスローガン: 「すべての実数に対して、ある条件を満たす別の実数が必ず存在する」という、誰でも読める短い要約。

これを**「920 万件の定理すべて」**に行いました。これで、数式ではなく「言葉」で検索できるようになったのです。

---

3. 検索の仕組み：「意味」でつなぐネット

彼らは、この「スローガン（要約）」と、ユーザーが検索する「質問」を、**同じ「意味の空間」**に配置しました。

• アナロジー：
  従来の検索は「キーワードの一致」でした（「リンゴ」と入力すると「リンゴ」という文字があるものを探す）。
  この新しい検索は**「意味の類似」**です。
  • ユーザーが「赤くて丸い果物」を検索すると、システムは「リンゴ」という言葉がなくても、意味が近い「リンゴ」の定理をピンポイントで見つけます。

彼らは、どの AI モデルを使えば一番うまく「意味」を捉えられるか、徹底的に実験しました。その結果、**「文脈（論文の導入部など）を一緒に教えてあげると、AI がより良い要約を作れる」**という重要な発見をしました。

---

4. 結果：プロの数学者も驚く精度

彼らは、プロの数学者に「あなたが知っている定理を言葉で説明して」と依頼し、その質問で検索テストを行いました。

• Google 検索や ChatGPT：
  正解を見つける確率は 20〜30% 程度でした。
• この新しいツール：
  正解を見つける確率は45% 以上に跳ね上がりました。
  さらに、「論文レベル」で探せば、**56%**の確率で正解の論文にたどり着けます。

これは、「論文のタイトルや抄録（要約）」だけでなく、論文の「中身（定理）」そのものを検索できることを意味します。論文の 50 ページ目に隠れている小さな補題（Lemma）でも、タイトルに書かれていなければ見つけられなかったものが、今では一発で見つかるようになりました。

---

5. なぜこれが重要なのか？

• 数学者にとって：
  「この結果は昔からあるんじゃないか？」と確認する作業が、数時間から数秒に短縮されます。重複した研究（撤回される論文）を防ぐことができます。
• AI にとって：
  AI が数学の証明をする際、必要な「定理」を正しく引き出せるようになり、間違った答え（ハルシネーション）を減らすことができます。
  （実験では、AI がこのツールを使わないと間違った答えを出しましたが、ツールを使わせると、正しい定理を引用して正解を導き出しました。）

まとめ

この研究は、「数学という巨大な図書館」を、本単位ではなく「定理（真実）」単位で検索できる、世界最大の辞書を作ったものです。

AI が複雑な数式を「人間の言葉」に翻訳し、意味でつなぐことで、数学者も AI も、必要な知識を瞬時に引き出せるようになりました。これは、数学の発見と共有のあり方を大きく変える一歩です。

プロジェクト名： Theorem Search
場所： theoremsearch.com（誰でも試せます！）

技術概要

900 万の数学定理を対象とした意味検索に関する論文の技術的サマリー

本論文は、数学研究における「定理レベル」の検索課題を解決し、920 万個の定理ステートメントからなる大規模コーパスを構築・評価した研究です。既存の検索ツールが論文全体を返すのに対し、数学者や定理証明エージェントが特定の定理・補題・命題を直接検索できる環境を提供することを目的としています。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細にまとめます。

1. 問題定義 (Problem)

数学知識は「定理」「補題」「命題」「系」といった離散的な結果を中心に構成されています。しかし、現在の検索環境には以下の重大な課題があります。

• ドキュメントレベルの限界: Google Scholar や arXiv などの既存ツールは、論文全体を検索対象としており、特定の定理を直接見つけることが困難です。ユーザーは論文を人手でスキャンする必要があります。
• AI エージェントの課題: 形式証明を生成する AI や、新しい結果を証明する研究者は、既存の文献にその定理がすでに存在するかどうかを確認する必要があります。しかし、現在の LLM（Web 検索機能付き）や検索エンジンは、特定の定理を正確に特定できず、誤った参照や「ハルシネーション（もっともらしいが誤った主張）」を引き起こすことがあります。
• 重複と撤回: arXiv の撤回論文の約 2.5% は、結果が既存文献にすでに存在していたことが原因であり、定理レベルの検索の重要性を示しています。

2. 手法とアプローチ (Methodology)

本研究は、自然言語による意味検索（Semantic Search）を数学定理に適用するためのパイプラインを構築しました。

2.1 データ収集とコーパス構築

• 規模: arXiv（数学、統計、CS、物理など 7 分野）および Stacks Project、ProofWiki などの 7 つのソースから、920 万件の定理ステートメントを抽出しました。これは現在、公開されている人間が執筆した研究レベルの定理の最大の集合です。
• 解析: LaTeX ソースから定理を抽出するために、plasTeX、カスタム TeX ロギング、正規表現によるパースの 3 段階の戦略を採用し、定理名、参照番号、注記、および本文（Body）を抽出しました。

2.2 定理の表現（スローガン生成）

LaTeX 形式のまま埋め込むのではなく、LLM を用いて各定理を**自然言語の「スローガン（短い記述）」**に変換するアプローチを採用しました。

• 変換プロセス: 抽出された定理本文を DeepSeek V3 などの LLM に提示し、数式記号や証明の詳細を避け、定理の主要な結果を簡潔な英語の文で記述させるプロンプトを設計しました。
• コンテキストの影響: 定理本文のみ、本文＋抄録、本文＋論文導入部（第 1 章）の 3 つのコンテキスト設定を比較実験しました。

2.3 埋め込みと検索アーキテクチャ

• 埋め込みモデル: 生成されたスローガンとユーザーの検索クエリを、Qwen3-Embedding-8B モデルを用いて固定次元のベクトル空間に埋め込みました。
• 検索エンジン: PostgreSQL の pgvector 拡張機能と HNSW（階層的ナビゲ可能小世界）インデックスを使用し、近似最近傍探索（ANN）を高速化しました。
• 再ランク付け: 初期検索結果（Top-100）を、クロスエンコーダー（Qwen3-Reranker-0.6B）を用いて再ランク付けし、精度を向上させました。

3. 主要な貢献 (Key Contributions)

1. 大規模定理コーパスの公開: 920 万件の定理を含む、メタデータ付きの最大規模の数学定理データセットと、そのデータシートを公開しました。
2. 表現選択の体系的な研究: 定理の表現方法（生 LaTeX vs 自然言語スローガン）、コンテキスト（本文のみ vs 導入部込み）、LLM の選択、プロンプト戦略が検索品質に与える影響を体系的に分析しました。
   • 重要な発見: 生 LaTeX 形式を直接埋め込むよりも、自然言語のスローガンに変換して埋め込む方が検索性能が劇的に向上しました。
3. 最先端の検索性能の実証: 専門数学者によって作成された 111 のクエリに対する評価において、既存のツールを大幅に上回る性能を達成しました。

4. 実験結果 (Results)

専門数学者が作成した 111 のクエリを用いた評価セット（Validation Set）での結果は以下の通りです。

• 定理レベル検索 (Theorem-level Retrieval):
  • 提案手法（Qwen3 8B + リランク）は Hit@20 で 45.0% を達成。
  • 比較対象: ChatGPT 5.2 (19.8%)、Gemini 3 Pro (27.0%)、Google Search (定理レベルでは評価不可/論文レベルのみ)。
  • 提案手法は、正しい定理をトップ 20 以内で見つける確率が他モデルを大きく上回りました。
• 論文レベル検索 (Paper-level Retrieval):
  • 提案手法は Hit@20 で 56.8% を達成。
  • 比較対象: Google Search (37.8%)。
• コンテキストの影響: 定理本文だけでなく、論文の「導入部（Introduction）」を含めてスローガンを生成すると、検索精度が最も高くなりました（導入部には結果の文脈や既存研究との関係が書かれているため）。
• LLM による推論の改善: RAG（検索拡張生成）として本システムを利用した Claude (Opus 4.5) は、検索なしでは誤った結論を導き出していた数学的問題に対し、検索結果に基づき正しい答えと論理的な証明チェーンを導き出しました。

5. 意義と応用 (Significance)

• 数学研究の効率化: 研究者は特定の定理を直接検索でき、文献レビューや結果の重複確認が大幅に効率化されます。
• AI 定理証明の支援: 形式証明システム（Lean など）や AI エージェントが、証明の過程で必要な補題や定理を正確に検索・取得できるようになり、推論の信頼性が向上します。
• 技術的示唆: 専門性の高い技術文書（数学など）における検索では、生形式（LaTeX）よりも、LLM による自然言語要約（スローガン）への変換が、意味的類似性の捕捉において極めて有効であることが示されました。

本研究は、数学知識へのアクセスを「論文単位」から「定理単位」へとシフトさせ、Web スケールで実用的な意味検索を実現した画期的な成果です。検索ツール、データセット、API は theoremsearch.com で公開されています。