Semantic Search over 9 Million Mathematical Theorems

De auteurs introduceren een schaalbaar semantisch zoeksysteem voor wiskundige stellingen dat op een corpus van 9,2 miljoen stellingen is getraind en door middel van geoptimaliseerde representaties en zoekstrategieën een aanzienlijke verbetering biedt ten opzichte van bestaande methoden voor het vinden van specifieke wiskundige resultaten.

De kern

Stel je voor dat wiskunde een gigantische, eeuwenoude bibliotheek is. Maar in plaats van boeken die je gewoon kunt openen en lezen, zit deze bibliotheek vol met miljoenen losse, ingewikkelde zinnen: stellingen, lemma's en bewijzen.

Vroeger was het zoeken naar één specifieke zin in deze bibliotheek een nachtmerrie. Als je een wiskundige vraag had, moest je hele boeken doorbladeren (zoals Google Scholar of arXiv doen) om te zien of het antwoord ergens in zat. Het was alsof je een specifiek woord zocht in een heel boek, maar de zoekmachine je alleen het hele boek gaf.

Dit nieuwe onderzoek is als het bouwen van een superkrachtige "Google" voor losse wiskundige feiten.

Hier is hoe het werkt, vertaald in alledaagse termen:

1. Het probleem: De "Boek"-vs.-"Zin"-dilemma

Stel je voor dat je op zoek bent naar een specifieke recept voor een taart (een stelling). De oude zoekmachines gaven je een lijst met kookboeken. Je moest dan zelf bladeren door de inhoudsopgave en de pagina's om te zien of het recept erin stond.

• Het risico: Wiskundigen (en nu ook AI's) vinden vaak dat ze iets nieuws hebben bedacht, terwijl het al 50 jaar geleden in een boek staat. Het is alsof je een nieuwe taart uitvinden, terwijl iemand anders die al lang geleden heeft bedacht, maar je hebt het boek niet gevonden.

2. De oplossing: De "Slogan"-truc

De onderzoekers hebben een database gemaakt van 9,2 miljoen losse wiskundige stellingen. Maar wiskundige taal is vaak vol met vreemde symbolen (zoals $\int$ of $\sum$) die computers moeilijk begrijpen als ze in "mensentaal" zoeken.

Om dit op te lossen, hebben ze een slimme truc gebruikt:

• Ze hebben een slimme AI (een "robot-schrijver") gevraagd om voor elke complexe wiskundige stelling een korte, begrijpelijke slogan te schrijven.
• Voorbeeld: In plaats van een zin vol met formules, zegt de AI: "Als je een bepaalde vorm hebt, is deze vorm altijd rond."
• Nu kunnen mensen zoeken met gewone woorden, en de computer zoekt naar die simpele slogans in plaats van de ingewikkelde formules.

3. De zoekmachine: Een slimme bibliothecaris

Deze nieuwe zoekmachine werkt als een super-snelle bibliothecaris die:

1. Luistert naar je vraag (bijvoorbeeld: "Is er een manier om een bolvormige ruimte te beschrijven?").
2. Kijkt naar de "slogans" van de 9,2 miljoen stellingen.
3. Je direct de juiste zin geeft, niet het hele boek.

Wat is het resultaat?

• Sneller: Het vindt het antwoord in 3 seconden. Oude methoden (zoals ChatGPT of Google) duren vaak minuten of geven het verkeerde antwoord.
• Beter: De onderzoekers hebben het getest met echte wiskundigen. Hun systeem vond het juiste antwoord in 45% van de gevallen (binnen de top 20 resultaten), terwijl de beste concurrenten (zoals Google en ChatGPT) maar rond de 20% haalden.
• Dieper: Het kan ook kleine, onbelangrijke regels vinden die diep in een boek staan, die een gewone zoekmachine nooit zou vinden omdat ze niet in de samenvatting staan.

4. Waarom is dit belangrijk?

• Voor mensen: Wiskundigen hoeven niet meer uren te zoeken in PDF-bestanden. Ze kunnen direct zien of hun idee al bestaat.
• Voor AI: Als robots (AI's) wiskundige bewijzen moeten maken, kunnen ze nu direct de juiste "recepten" (stellingen) ophalen om hun redenering op te bouwen, in plaats van te gissen.

Kortom:
De onderzoekers hebben een gigantische database gebouwd van 9 miljoen wiskundige feiten, ze vertaald naar simpele menselijke zinnen, en een zoekmachine gemaakt die precies weet wat je zoekt. Het is alsof je van een bibliotheek waar je alleen de boekenkast mag zien, overschakelt naar een bibliotheek waar je direct de juiste zin op een kaartje krijgt.

Je kunt deze zoekmachine nu zelf proberen op theoremsearch.com.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "Semantic Search over 9 Million Mathematical Theorems" in het Nederlands.

Titel: Semantische Zoeking over 9 Miljoen Wiskundige Stellingen

1. Het Probleem

Huidige zoektools voor wiskundige kennis (zoals Google Scholar, arXiv en zelfs geavanceerde LLMs met webtoegang) opereren voornamelijk op documentniveau. Ze zoeken naar volledige papers, terwijl wiskundigen en AI-agenten die bewijzen vaak op zoek zijn naar specifieke stellingen, lemma's, proposities of gevolgtrekkingen binnen die papers.

• De Gaping: Wiskundige kennis is georganiseerd rond discrete resultaten. Zoekmachines dwingen gebruikers echter om handmatig papers te scannen om een specifieke stelling te vinden.
• Gevolgen: Dit leidt tot herhaling van werk (retracties omdat resultaten al eerder waren gepubliceerd) en fouten in AI-systemen die "oplossingen" vinden voor problemen die decennia eerder al waren opgelost.
• Technische Uitdaging: Bestaande methoden voor semantische zoekopdrachten presteren slecht op grote, technisch complexe corpora zoals wiskundige theorieën, vooral vanwege de zware afhankelijkheid van symbolische notatie (LaTeX) die moeilijk te vertalen is naar natuurlijke taal voor zoekopdrachten.

2. Methodologie

De auteurs hebben een geautomatiseerde pipeline ontwikkeld om een unificerend corpus te bouwen en semantische zoekopdrachten mogelijk te maken.

• Data Collectie & Parsing:

  • Een corpus van 9,2 miljoen stellingen is samengesteld uit arXiv (99,5% van de dataset) en zeven andere bronnen (waaronder Stacks Project, ProofWiki, en HoTT Book).
  • Drie strategieën worden gebruikt om LaTeX-documenten te parseren:
    1. Node Search (plasTeX): Converteert LaTeX naar een gestructureerde boom; succesvol voor ~6,9 miljoen stellingen.
    2. TeX Logging: Een aangepast LaTeX-pakket logt stellingdata tijdens het compileren (fallback voor ~1,8 miljoen).
    3. Regex-based Parsing: Gebruikt reguliere expressies voor delimiters (voor ~542.000 stellingen).
  • Metadata (auteur, categorie, URL) wordt zorgvuldig behouden.

• Representatie (Slogan-Generatie):

  • In plaats van ruwe LaTeX direct te embedden, genereren de auteurs een korte, natuurlijke taalbeschrijving (een "slogan") voor elke stelling met behulp van een Large Language Model (LLM), specifiek DeepSeek V3.
  • Prompt-strategie: De prompt instrueert het model om de hoofdstelling in maximaal vier zinnen te beschrijven, zonder symbolen, bewijsdetails of verwijzingen naar de documentstructuur.
  • Context-studies: Er wordt onderzocht of het toevoegen van de abstract of de inleiding van de paper de kwaliteit van de slogan verbetert.

• Embedding & Zoekarchitectuur:

  • De gegenereerde slogans en gebruikersquery's worden geëmbed in een gedeelde semantische ruimte met het Qwen3-Embedding-8B model.
  • De embeddings worden opgeslagen in een PostgreSQL-database met de pgvector extensie, gebruikmakend van een HNSW-index (Hierarchical Navigable Small World) voor snelle benadering van de dichtstbijzijnde buren.
  • Zoekproces: Een tweestapsproces: eerst een initiële selectie op basis van Hamming-afstand (na binair kwantisatie), gevolgd door een herordening (reranking) op basis van cosinus-ähnelijkheid of een cross-encoder (Qwen3-Reranker).

3. Belangrijkste Bijdragen

1. Grootste Corpus: De release van het grootste publiek beschikbare corpus van menselijk geschreven, onderzoeksgerichte wiskundige stellingen (9,2 miljoen items) met rijke metadata.
2. Systematische Analyse: Een grondig onderzoek naar de invloed van representatiekeuzes. De kernbevinding is dat het embedden van natuurlijke taal-slogans aanzienlijk beter presteert dan het embedden van ruwe LaTeX-formules.
3. State-of-the-art Prestaties: Het demonstreren van een werkend semantisch zoeksysteem op web-schaal dat de huidige bestaande tools (Google, arXiv, ChatGPT, Gemini) overtreft.
4. Openbare Tools: De beschikbaarstelling van een zoekinterface, REST API, MCP-server (voor AI-agenten) en de dataset zelf.

4. Resultaten

Het systeem werd geëvalueerd op een handmatig samengestelde set van 111 zoekopdrachten geschreven door professionele wiskundigen.

• Stelling-niveau Zoekopdrachten:
  • Het beste model (Qwen3 8B + Reranker) bereikte een Hit@20 van 45,0%.
  • Dit is een aanzienlijke verbetering ten opzichte van ChatGPT 5.2 met zoekfunctie (19,8%) en Gemini 3 Pro (27,0%).
• Document-niveau Zoekopdrachten:
  • Hit@20 van 56,8% voor het vinden van het juiste paper, vergeleken met 37,8% voor Google Search.
• Ablatie Studies:
  • Context: Slogans gegenereerd met de volledige inleiding van de paper presteerden beter dan alleen de stelling of alleen de abstract.
  • LLM Keuze: Propriëtaire modellen (zoals Claude Opus 4.5) genereren soms betere slogans dan open-source modellen, maar Qwen3 8B bleek de beste all-round embedder.
  • Embedding: Het gebruik van natuurlijke taal (slogans) is cruciaal; directe embedding van LaTeX leverde zeer slechte resultaten op.
• RAG Experiment: In een experiment met Claude (Opus 4.5) kon het model zonder zoekhulp een foutief wiskundig antwoord geven. Met toegang tot het theorema-database als RAG-tool (Retrieval-Augmented Generation) vond het model de juiste stellingen en gaf het een correct, onderbouwd antwoord.

5. Betekenis en Impact

• Toegang tot Wiskundige Kennis: Het systeem behandelt stellingen als "eersteklas zoekobjecten", waardoor onderzoekers en AI-agenten specifieke resultaten kunnen vinden zonder volledige papers te hoeven scannen.
• AI en Bewijsvoering: Het biedt een essentiële tool voor AI-agenten die formele bewijzen genereren, door hen te helpen relevante lemma's te vinden en hallucinaties te voorkomen.
• Schaalbaarheid: Het bewijst dat semantische zoekopdrachten op schaal van miljoenen technische documenten haalbaar en effectief zijn, mits de juiste vertaalslag van formele notatie naar natuurlijke taal wordt gemaakt.
• Toekomstige Toepassingen: De dataset en API kunnen worden gebruikt voor literatuuroverzichten, het trainen van gespecialiseerde wiskundige modellen, en het verbeteren van automatische stellingbewijzers.

De projectpagina, zoektool, dataset en API zijn beschikbaar via theoremsearch.com.