Semantic Search over 9 Million Mathematical Theorems

Diese Arbeit stellt ein skalierbares semantisches Suchsystem für über 9 Millionen mathematische Theoreme vor, das durch die Verwendung natürlicher Sprachbeschreibungen und optimierter Embeddings die präzise Wiederauffindung spezifischer Sätze in großen Forschungsdatenbeständen im Vergleich zu herkömmlichen Methoden deutlich verbessert.

Das Wesentliche

Mathematik-Googeln neu erfunden: Wie man die 9 Millionen Sätze der Welt findet

Stellen Sie sich die Welt der Mathematik als eine riesige, unendliche Bibliothek vor. In dieser Bibliothek gibt es nicht nur Bücher (die wissenschaftlichen Artikel), sondern Millionen von einzelnen, winzigen Schätzen: die Theoreme. Ein Theorem ist wie ein einzelner, perfekter Diamant in einem riesigen Berg aus Sand.

Das Problem bisher? Wenn Sie in dieser Bibliothek nach einem bestimmten Diamanten suchen wollten, mussten Sie sich durch ganze Bücher wühlen. Die Suchmaschinen (wie Google Scholar oder arXiv) waren wie Bibliothekare, die Ihnen nur sagten: „Hier ist das Buch, in dem der Diamant vielleicht liegt." Sie mussten dann das Buch selbst öffnen, die Seiten blättern und hoffen, den Diamanten zu finden. Das ist mühsam, besonders wenn Sie nur den Diamanten brauchen, nicht das ganze Buch.

Die Lösung: Ein neuer Suchroboter namens „Theorem Search"

Die Autoren dieses Papers haben einen neuen Suchroboter gebaut, der über 9,2 Millionen dieser mathematischen Diamanten wacht. Sie nennen es „Semantic Theorem Search". Hier ist, wie er funktioniert, einfach erklärt:

1. Der Übersetzer (Die „Slogan"-Erfindung)

Mathematiker schreiben ihre Theoreme oft in einer sehr strengen, fast fremdsprachlichen Sprache (LaTeX), voller Symbole wie $\sum$, $\int$ und griechischer Buchstaben. Ein normaler Suchroboter versteht das nicht gut.

Stellen Sie sich vor, jeder Diamant wäre in einen verschlossenen, komplizierten Safe eingeschlossen. Die Forscher haben einen KI-Übersetzer (eine große Sprach-KI) beauftragt, für jeden dieser Safes einen kurzen, einfachen Slogan zu schreiben.

• Statt: „Theorem 3.1: $\forall x \in \mathbb{R}, \exists y \in \mathbb{R} \dots$"
• Schreibt die KI: „Jede reelle Zahl hat eine Wurzel, die größer ist als null."

Jetzt kann der Suchroboter nicht mehr nur nach Symbolen suchen, sondern versteht die Bedeutung hinter den Symbolen, genau wie ein Mensch.

2. Die riesige Datenbank

Sie haben diese 9,2 Millionen Slogans gesammelt und in eine riesige Datenbank gepackt. Das ist die größte Sammlung ihrer Art, die es je gab. Sie stammt aus den wichtigsten Quellen der Welt: arXiv (wo Wissenschaftler ihre neuesten Ideen posten), ProofWiki und anderen großen Projekten.

3. Die Suche: Wie ein Detektiv

Wenn Sie nun etwas suchen, sagen Sie dem Roboter einfach in normaler Sprache, was Sie brauchen.

• Ihre Frage: „Ich suche einen Satz, der besagt, dass eine bestimmte Art von Oberfläche sich in einen Kreis verwandeln lässt."
• Der Roboter: Er wandelt Ihre Frage in einen „Gedanken" um, vergleicht ihn mit den Millionen Slogans in seiner Datenbank und findet sofort den perfekten Diamanten.

Was haben sie herausgefunden? (Die Ergebnisse)

Die Forscher haben ihren Roboter gegen die alten Methoden getestet (Google, ChatGPT, arXiv-Suche). Das Ergebnis war überwältigend:

• Besser als Google: Google findet oft das richtige Buch, aber verpasst den Diamanten darin. Der neue Roboter findet den Diamanten direkt.
• Besser als KI-Chats: Wenn Sie ChatGPT oder Gemini fragen, halluzinieren sie oft oder finden den falschen Satz. Der neue Roboter ist viel präziser.
• Der Trick mit dem Kontext: Sie haben herausgefunden, dass der Übersetzer (die KI) den Slogan viel besser schreibt, wenn er nicht nur den Satz selbst liest, sondern auch die Einleitung des Artikels dazu. Das ist wie wenn Sie jemanden bitten, einen Film zu beschreiben: Wenn er nur die letzte Szene sieht, versteht er den Film nicht. Wenn er aber den Anfang kennt, versteht er die Pointe.

Warum ist das wichtig?

Stellen Sie sich vor, Sie sind ein Mathematiker oder ein KI-Agent, der Beweise schreibt. Sie brauchen einen kleinen, spezifischen Baustein für Ihr großes Puzzle.

• Früher: Sie haben Stunden damit verbracht, PDFs durchzusehen.
• Jetzt: Sie tippen Ihren Wunsch ein, und in 3 Sekunden (statt 60 Sekunden) haben Sie den exakten Satz mit dem richtigen Autor und der richtigen Nummer.

Das ist wie der Unterschied zwischen dem Suchen nach einem Buch in einer Bibliothek und dem Suchen nach einer einzigen, spezifischen Zeile in einem Buch, die Sie sofort auf einem Bildschirm angezeigt bekommen.

Fazit:
Dieses Projekt macht die riesige Welt der Mathematik endlich durchsuchbar. Es verwandelt eine undurchdringliche Mauer aus Symbolen in eine klare, verständliche Bibliothek, in der jeder – ob Mensch oder Maschine – genau das findet, was er sucht. Die Datenbank und das Suchwerkzeug sind jetzt öffentlich verfügbar, damit jeder diesen neuen Weg der Entdeckung nutzen kann.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „Semantic Search over 9 Million Mathematical Theorems" auf Deutsch:

1. Problemstellung

Die Suche nach mathematischen Ergebnissen ist nach wie vor eine große Herausforderung. Bestehende Werkzeuge wie Google Scholar, arXiv oder auch moderne Large Language Models (LLMs) mit Webzugriff operieren primär auf der Ebene ganzer Dokumente (Papers). Mathematiker und Theorembeweis-Agenten benötigen jedoch oft Zugriff auf spezifische Sätze, Lemmata oder Propositionen, die eine Frage beantworten.

• Die Lücke: Wenn Forscher einen spezifischen Satz suchen, müssen sie manuell ganze Papers durchsuchen. Dies führt zu Ineffizienz und Fehlern.
• Folgen: Studien zeigen, dass ein signifikanter Teil zurückgezogener arXiv-Papers (ca. 2,5 %) darauf zurückzuführen ist, dass die Ergebnisse bereits in der Literatur existierten. Auch KI-Systeme „lösen" manchmal Probleme, die seit Jahrzehnten gelöst sind, da sie keine semantische Suche auf Satzebene durchführen können.

2. Methodik

Das Paper stellt einen skalierbaren Ansatz zur semantischen Suche über Theoreme vor, der folgende Schritte umfasst:

• Datenerstellung (Corpus):

  • Es wurde ein einheitliches Korpus von 9,2 Millionen Theoremaussagen erstellt.
  • Quellen: 99,5 % stammen aus arXiv (Mathematik, Statistik, Informatik, Physik etc.), der Rest aus Quellen wie dem Stacks Project, ProofWiki, dem Open Logic Project und anderen Open-Source-Repositorien.
  • Parsing: Um die Theoreme aus LaTeX-Quellen zu extrahieren, wurden drei Strategien kombiniert:
    1. Node Search (plasTeX): Konvertierung in einen Node-Baum zur Strukturierung (ca. 6,9 Mio. Theoreme).
    2. TeX Logging: Ein benutzerdefiniertes LaTeX-Paket protokolliert Theoremdaten beim Kompilieren (ca. 1,8 Mio. Theoreme).
    3. Regex-Parsing: Fallback für verbleibende Fälle (ca. 0,5 Mio. Theoreme).
  • Das Korpus enthält Metadaten wie Titel, Autoren, Zitationszahlen und arXiv-Kategorien.

• Repräsentation (Slogan-Generierung):

  • Da direkte Einbettung von rohem LaTeX für Embedding-Modelle schwierig ist (wegen symbolischer Notation), wird jedes Theorem durch einen kurzen, natürlichen Sprach-Slogan repräsentiert.
  • Ein LLM (DeepSeek V3) generiert diese Slogans basierend auf dem Theoremtyp und dem Kontext.
  • Kontext-Strategien: Es wurde untersucht, ob nur der Theoremkörper, der Körper plus Abstract oder der Körper plus Einleitung des Papers für die Generierung verwendet werden sollte.

• Embedding und Retrieval:

  • Die Slogans und Benutzerabfragen werden in einen gemeinsamen semantischen Raum eingebettet.
  • Modell: Das Qwen3-Embedding-8B Modell wurde als Embedder gewählt.
  • Datenbank: Die Vektoren werden in einer PostgreSQL-Datenbank mit der pgvector-Erweiterung und einem HNSW-Index (Hierarchical Navigable Small World) gespeichert, der eine schnelle Approximate Nearest Neighbor (ANN)-Suche ermöglicht.
  • Suchprozess: Zuerst wird eine grobe Suche über Hamming-Distanz (nach Binärquantisierung) durchgeführt, gefolgt von einer Neuzuordnung (Reranking) mittels Cosine-Similarität und optional einem Cross-Encoder-Reranker (Qwen3-Reranker-0.6B).

3. Wichtige Beiträge

1. Das größte Korpus informeller mathematischer Theoreme: Ein öffentlich zugängliches Dataset von über 9 Millionen Theoremen mit reichhaltigen Metadaten.
2. Systematische Analyse der Repräsentation: Die Autoren zeigen, dass die Einbettung von natürlichen Sprach-Slogans die Einbettung von rohem LaTeX bei weitem übertrifft. Zudem verbessert die Einbeziehung des Kontexts (insbesondere der Einleitung des Papers) die Qualität der Slogans und damit das Retrieval.
3. State-of-the-Art Retrieval: Demonstration, dass semantische Theoremsuche im Web-Scale möglich und effektiv ist.
4. Open Source: Bereitstellung des Datensatzes, der Such-Engine, einer REST-API und eines MCP-Servers (Model Context Protocol) für KI-Agenten.

4. Ergebnisse

Die Leistung wurde an einem kuratierten Testset von 111 Suchanfragen bewertet, die von professionellen Mathematikern erstellt wurden (blind, ohne Zugriff auf das Korpus).

• Vergleich mit Baselines: Das System wurde gegen Google Search, arXiv-Suche, ChatGPT 5.2 (mit Suche) und Gemini 3 Pro getestet.
• Metriken (Hit@20):
  • Auf Theoremebene: Das beste Modell (Qwen3 8B) erreicht 45,0 % Hit@20. Zum Vergleich: ChatGPT 5.2 erreicht 19,8 %, Gemini 3 Pro 27,0 %.
  • Auf Paperebene: Das System erreicht 56,8 % Hit@20, während Google Search nur 37,8 % erreicht.
• Ablationsstudien:
  • Kontext: Slogans, die mit dem Abstract und der Einleitung des Papers generiert wurden, performten besser als nur mit dem Theoremkörper.
  • LLM-Wahl: Proprietäre Modelle wie Claude Opus 4.5 und Gemini 3 Pro generierten bessere Slogans als DeepSeek-V3, aber Qwen3 8B als Embedder zeigte die beste Gesamtleistung.
  • Embedding: Qwen3 8B als Embedder war deutlich überlegen gegenüber Gemma 0.3B oder Qwen3 0.6B.
• RAG-Experiment: Ein Experiment mit Claude (Opus 4.5) zeigte, dass das System ohne Retrieval eine falsche, aber plausibel klingende Antwort auf eine komplexe Frage zur KSBA-Kompaktifizierung gab. Mit Zugriff auf das Theorem-Korpus (RAG) fand Claude die korrekte Antwort und zitierte spezifische Theoremnummern.

5. Bedeutung und Ausblick

• Paradigmenwechsel: Das Paper etabliert Theoreme als „First-Class-Objekte" für die Informationssuche, anstatt nur nach Dokumenten zu suchen.
• Anwendbarkeit:
  • Für Mathematiker: Effizientere Literaturrecherche, Vermeidung von Doppelarbeit und schnellerer Zugriff auf technische Lemmata, die tief in Papers versteckt sind.
  • Für KI-Agenten: Verbesserte Premissenauswahl für formale Beweissysteme (z. B. in Lean) und Reduktion von Halluzinationen in mathematischen Argumentationen durch Retrieval-Augmented Generation (RAG).
• Verfügbarkeit: Die Tools sind unter theoremsearch.com sowie über Hugging Face und eine API verfügbar.

Zusammenfassend demonstriert diese Arbeit, dass die Kombination aus großskaliger Datenerfassung, natürlicher Sprachzusammenfassung (Slogans) und moderner Embedding-Technologie die semantische Suche nach mathematischen Ergebnissen revolutionieren kann und dabei bestehende Werkzeuge signifikant übertrifft.