Semantic Search over 9 Million Mathematical Theorems

Cet article présente un système de recherche sémantique à grande échelle capable d'extraire des théorèmes spécifiques parmi 9,2 millions d'énoncés mathématiques issus d'arXiv et d'autres sources, démontrant une efficacité supérieure aux méthodes existantes pour répondre aux requêtes de mathématiciens professionnels.

L'essentiel

Imaginez que vous êtes un détective cherchant une information précise dans une bibliothèque gigantesque qui contient 9 millions de livres. Le problème ? Dans cette bibliothèque, les livres sont rangés par titre, mais si vous cherchez une phrase spécifique à l'intérieur d'un chapitre, vous devez ouvrir chaque livre et feuilleter manuellement des centaines de pages. C'est exactement le problème que rencontrent les mathématiciens et les intelligences artificielles aujourd'hui : ils doivent chercher des théorèmes (des résultats mathématiques précis) dans des articles entiers, ce qui est lent et inefficace.

Voici comment les auteurs de cette recherche ont résolu ce casse-tête, expliqué simplement :

1. Le Problème : Chercher une aiguille dans une botte de foin

Aujourd'hui, si vous demandez à Google ou à un chatbot : "Où se trouve le théorème qui dit que X implique Y ?", ils vous répondront souvent : "Voici un article qui parle de X et Y". Mais l'article fait 20 pages ! Vous devez lire tout le texte pour trouver la phrase exacte. C'est comme si vous cherchiez une recette de cuisine précise dans un livre entier, mais le moteur de recherche vous donnait juste le nom du livre sans vous dire à quelle page.

2. La Solution : Créer des "Étiquettes Magiques"

Les chercheurs ont construit une base de données géante contenant 9,2 millions de théorèmes extraits de milliers de documents scientifiques. Mais au lieu de stocker les formules mathématiques complexes (qui ressemblent à du code informatique illisible pour une machine), ils ont demandé à une intelligence artificielle (un "robot écrivain") de faire quelque chose de génial :

Pour chaque théorème, le robot a écrit une petite phrase simple en langage courant, comme une étiquette ou un résumé accrocheur.

• Avant : Une formule complexe de 3 lignes avec des symboles grecs.
• Après : "Si vous avez un objet géométrique spécial, il est impossible de le déformer sans le casser."

C'est comme si, au lieu de chercher un livre par son code-barres technique, vous cherchiez par son résumé sur la couverture.

3. Comment ça marche ? (L'analogie du traducteur)

Imaginez que vous voulez trouver un théorème. Vous tapez votre question en français simple, par exemple : "Comment prouver que ce cercle est rond ?".

1. Le Traducteur : Le système prend votre question et la transforme en une "empreinte digitale" numérique.
2. La Recherche : Il compare cette empreinte avec les "étiquettes magiques" (les résumés simples) de ses 9 millions de théorèmes.
3. Le Match : Au lieu de chercher des mots-clés exacts, il cherche des idées similaires. Si votre question ressemble sémantiquement (par le sens) à l'étiquette d'un théorème, il vous le propose, même si vous n'avez pas utilisé les mêmes mots.

4. Les Résultats : Une révolution

Les chercheurs ont testé ce système avec de vrais mathématiciens professionnels. Les résultats sont impressionnants :

• Google et les anciens outils trouvaient le bon article seulement 37 % du temps.
• Leur nouveau système trouve le bon théorème précis (pas juste l'article) dans 45 % des cas, et l'article contenant ce théorème dans 56 % des cas.

C'est comme passer d'une recherche où vous deviez fouiller dans des cartons entiers à une recherche où vous appuyez sur un bouton et le bon document s'ouvre directement à la bonne page.

5. Pourquoi c'est important pour l'avenir ?

Cela aide les humains à ne pas réinventer la roue (en découvrant qu'un résultat existe déjà) et aide les robots (les IA) à faire des preuves mathématiques sans se tromper. C'est un peu comme donner une boussole à un explorateur qui se perdait dans une forêt de documents.

En résumé :
Les auteurs ont pris une forêt de 9 millions de documents mathématiques, ont demandé à une IA de résumer chaque résultat important en une phrase simple, et ont créé un moteur de recherche capable de comprendre le sens de vos questions pour vous donner la réponse exacte, instantanément. C'est un outil puissant pour rendre les mathématiques plus accessibles et pour aider les intelligences artificielles à "penser" plus juste.

Résumé technique

Voici un résumé technique détaillé de l'article « Semantic Search over 9 Million Mathematical Theorems » en français.

1. Problématique

La recherche d'informations mathématiques souffre d'un décalage fondamental : la connaissance mathématique est structurée autour de résultats discrets (théorèmes, lemmes, propositions), mais les outils de recherche existants (Google Scholar, arXiv, et même les LLMs avec accès au web) opèrent au niveau du document entier.

• Limites actuelles : Les chercheurs et les agents d'IA doivent parcourir manuellement des articles entiers pour trouver une affirmation spécifique. Cela conduit à des erreurs, comme la publication de résultats déjà établis (2,5 % des prépublications retirées sur arXiv sont dues à cela) ou à des échecs des agents d'IA qui "résolvent" des problèmes déjà prouvés.
• Défi technique : Le corpus mathématique est hautement technique, utilisant une notation symbolique (LaTeX) qui est difficile à interpréter sémantiquement par les modèles d'embedding standards.

2. Méthodologie

Les auteurs proposent un pipeline complet pour la recherche sémantique à l'échelle web, reposant sur trois piliers principaux :

A. Construction du Corpus

• Échelle : Un corpus unifié de 9,2 millions d'énoncés de théorèmes, extrait de sources variées : arXiv (99,5 %), ProofWiki, Stacks Project, et cinq autres sources open-source.
• Parsing : Trois stratégies de parsing LaTeX sont utilisées pour extraire les noms et corps des théorèmes :
  1. Recherche de nœuds via plasTeX (méthode principale).
  2. Journalisation TeX personnalisée (fallback).
  3. Parsing par expressions régulières (fallback ultime).
• Nettoyage : Filtrage heuristique pour éliminer les extraits tronqués ou corrompus.

B. Représentation Sémantique (Le "Slogan")

Au lieu d'encoder directement le code LaTeX (peu efficace pour la recherche sémantique), chaque théorème est transformé en une description naturelle courte (un "slogan") générée par un Grand Modèle de Langage (LLM).

• Génération : Utilisation du modèle DeepSeek V3 pour générer une description déclarative en anglais, évitant la notation symbolique et les détails de preuve.
• Stratégies de contexte : L'étude compare trois approches d'entrée pour le LLM :
  1. Corps du théorème uniquement.
  2. Corps + Résumé (Abstract).
  3. Corps + Introduction (première section).
• Résultat clé : L'inclusion de l'introduction du papier améliore significativement la qualité de la recherche, car elle fournit le contexte nécessaire pour comprendre l'énoncé isolé.

C. Moteur de Recherche et Embedding

• Modèle d'Embedding : Utilisation du modèle Qwen3-Embedding-8B pour mapper les slogans et les requêtes utilisateurs dans un espace vectoriel partagé.
• Architecture de recherche :
  • Stockage dans une base de données PostgreSQL avec l'extension pgvector.
  • Indexation via un graphe HNSW (Hierarchical Navigable Small World) avec quantification binaire pour une recherche rapide des plus proches voisins.
  • Reranking : Une étape de ré-ranking utilisant un modèle croisé (cross-encoder, Qwen3-Reranker-0.6B) sur les 100 meilleurs candidats pour affiner la précision.
• Interface : Un outil de recherche web, une API REST et un serveur MCP (Model Context Protocol) permettant aux agents IA d'utiliser ce moteur.

3. Contributions Clés

1. Le plus grand corpus de théorèmes : Une collection de 9,2 millions d'énoncés mathématiques de niveau recherche, la plus grande jamais publiée.
2. Preuve de concept "Slogan" : Démonstration que l'encodage de théorèmes via des descriptions en langage naturel (générées par LLM) surpasse largement l'encodage direct des formulations LaTeX brutes.
3. Analyse systématique : Une étude ablation détaillée montrant l'impact critique du contexte (Introduction > Abstract > Corps seul), du choix du LLM générateur (Claude Opus 4.5 et Gemini 3 Pro surpassent les modèles open-source comme DeepSeek pour la génération de slogans), et du modèle d'embedding.
4. Outils ouverts : Mise à disposition du jeu de données, de l'API, du serveur MCP et de l'interface de recherche.

4. Résultats

L'évaluation a été réalisée sur un ensemble de 111 requêtes rédigées par des mathématiciens professionnels, couvrant 14 catégories d'arXiv.

• Performance au niveau Théorème :
  • La méthode proposée (Qwen3 8B + Reranker) atteint un Hit@20 de 45,0 %.
  • Cela surpasse significativement les bases de comparaison : ChatGPT 5.2 avec recherche (19,8 %) et Gemini 3 Pro (27,0 %).
  • Google Search et arXiv ne peuvent pas retourner de théorèmes spécifiques, leur performance est donc mesurée au niveau du papier (Hit@20 de 37,8 % pour Google), ce qui reste inférieur à la performance de l'approche proposée au niveau papier (56,8 %).
• Robustesse : Le système réussit à retrouver des lemmes techniques profonds dans un article, là où les moteurs basés sur les métadonnées (titre/résumé) échouent.
• RAG (Retrieval-Augmented Generation) : Une expérience montre que l'ajout de ce moteur de recherche corrige les hallucinations d'un LLM (Claude) sur une question mathématique de recherche avancée, lui permettant de fournir la réponse correcte avec des références précises.

5. Signification et Impact

Ce travail démontre que la recherche sémantique de théorèmes est réalisable à l'échelle du web.

• Pour les chercheurs : Il permet de vérifier l'existence de résultats spécifiques sans parcourir des centaines de pages, réduisant le risque de redondance dans la publication.
• Pour l'IA : Il fournit une infrastructure critique pour les agents d'IA effectuant des preuves formelles ou des raisonnements mathématiques, en leur permettant de récupérer des prémisses pertinentes (lemmes) avec une précision inédite.
• Futur : L'approche ouvre la voie à une intégration plus profonde entre la littérature mathématique informelle et les systèmes de preuve automatisés, transformant les théorèmes en objets de recherche de première classe.

L'ensemble du projet est accessible via theoremsearch.com.