Les LLMs et la recherche mathématique

Découverte, Formalisation et Raisonnement dans 4 Papiers Récents

François-David Collin
francois-david.collin@umontpellier.fr

CNRS

IMAG, Montpellier

24 novembre 2025

L’IA et les Mathématiques

  • 🧠 L’IA ne sert plus seulement à calculer, mais à raisonner et découvrir.
  • 📚 Quatre papiers récents (2025) illustrent cette tendance :
    1. 🔍 Découverte : Trouver de nouveaux objets mathématiques.
    2. 🗣️ Traduction : Passer du langage naturel au langage formel.
    3. ✅ Preuve : Raisonner rigoureusement pour démontrer.
    4. 📉 Frugalité : Raisonner avec de petits modèles.

Pas « juste un chatbot »

  • 💬 Ici, on ne fait pas juste poser un problème à un chatbot généraliste.
  • 🧪 Il s’agit de recherche en mathématiques :
    • nouveaux algorithmes,
    • nouveaux objets,
    • nouvelles preuves.
  • 🧱 On conçoit des systèmes complets : modèles, moteurs de recherche, vérificateurs formels.

Les 4 Papiers à l’étude

  1. 🧬 AlphaEvolve (Nov. 2025) : Exploration et découverte à grande échelle (Georgiev et al. 2025). (Google)
  2. 🌉 ProofBridge (Oct. 2025) : Auto-formalisation de preuves (Jana et al. 2025). (Georgia Institute of Technology)
  3. 🤖 Kimina-Prover (Avr. 2025) : Raisonnement formel par renforcement (Wang et al. 2025). (Project Numina)
  4. 🐜 VibeThinker (Nov. 2025) : Petit modèle spécialisé (Xu et al. 2025). (Weibo)

Note : une recherche « utilitariste »

Ingénierie avant tout

  • 🧮 Très peu de mathématiques (au sens traditionnel) dans ces recherches
  • 🎯 L’accent sur les méthodes d’IA pour la recherche mathématique, pas sur les résultats mathématiques eux-mêmes.

Contexte : Le Tournant du Raisonnement (2025)

Le « Moment AlphaGo » du LLM

  • 🧠 Système 1 (Réflexe) : ChatGPT classique. Répond vite, prédit le mot suivant.
  • 🐢 Système 2 (Réflexion) : Modèles de Raisonnement (open ai o1, DeepSeek R1), génère des « traces de raisonnement ».
  • 🔑 La Clé : Transposer l’exploration stratégique d’AlphaGo (Jeux) vers le Raisonnement (Maths/Code).

L’Exemple DeepSeek R1

  • ♟️ AlphaGo : Explore l’arbre des coups possibles pour gagner.
  • 🗣️ DeepSeek R1 : Explore l’arbre des pensées possibles pour résoudre.
  • 🔄 Reinforcement Learning :
    • Le modèle génère une trace de raisonnement (<think>).
    • Si la réponse finale est bonne, tout le chemin est renforcé.
    • Il apprend à “réfléchir” par essai-erreur.

Comparaison avec/sans Raisonnement

Sur un (très) petit modèle (350M paramètres)

Prompt : Lily is three times older than her son. In 15 years, she will be twice as old as him. How old is she now?

Avec Raisonnement

Let’s use algebra to solve this problem.

Let Lily’s age be L and her son’s age be S.

According to the first statement, we have: L = 3S

According to the second statement, in 15 years L will be twice as old as his son. So: L + 15 = 2(S + 15)

Now we can substitute the first equation into the second one: 3S + 15 = 2(S + 15)

Now let’s solve for S. First, distribute the 2 on the right side: 3S + 15 = 2S + 30

Next, subtract 2S from both sides: 3S - 2S = 30 - 15

This simplifies to: S = 15

Now that we know his age, we can find Lily’s age: L = 3S L = 3 * 15 L = 45

So Lily is currently 45 years old.

Sans Raisonnement

Lily’s current age is 20 years.

Partie 1 : La recherche exploratoire

AlphaEvolve

Le Problème de la Découverte

  • 💎 En mathématiques, on cherche souvent des “objets” rares :
    • Un graphe avec des propriétés spécifiques.
    • Une constante optimale dans une inégalité.
  • 🌾 Optimisation dans un immense espace de solutions pour trouver ces objets rares.
  • 🎲 Méthodes classiques (recherche aléatoire) peu adaptées

La Lignée Alpha : Search + Learning

  • 💡 Paradigme : Deep Learning/LLM (~Intuition) + Recherche (~Raisonnement).
  • ♟️ AlphaGo / AlphaZero :
    • Intuition : Prédit le meilleur coup.
    • Recherche : Explore les prochains « coups » possibles (MCTS1).
  • 📐 AlphaProof : Adaptation aux maths formelles (Lean).

AlphaEvolve

  • 🧬 Nouveauté : Remplace la recherche arborescente par une évolution de programmes.
  • 🔄 Cycle : génération du code \(\Rightarrow\) exécution \(\Rightarrow\) apprentissage.
  • 🏗️ But : En plus de prouver : inventer et construire.

L’Approche AlphaEvolve

  • 🔑 Idée clé : Générer le programme qui construit l’objet, pas l’objet lui-même.
  • 🛠️ Outils :
    • LLM : Écrit et modifie du code (Python).
    • Algo Évolutif : Sélectionne et “mute” les meilleurs programmes.
  • 🚀 Méta-recherche : Optimisation de la stratégie de recherche.

Résultats d’AlphaEvolve

  • 🧪 Testé sur 67 problèmes difficiles (analyse, combinatoire, géométrie).
  • 🏆 Succès :
    • Redécouverte des meilleures solutions connues.
    • Amélioration des solutions pour plusieurs problèmes ouverts.
  • 🔭 Impact : L’IA comme outil d’exploration pour fournir des constructions explicites.

Exemple : Graphes Extrémaux

Problème : Trouver un graphe à 50 sommets, sans triangles ni cycles de longueur 4, avec le plus d’arêtes possible.

  • 🧑‍💻 Approche classique : Chercher directement le graphe optimal (espace énorme \(2^{1225}\)).
  • 🧬 AlphaEvolve :
    1. Fait évoluer un programme Python qui cherche de bons graphes.
    2. Le programme s’exécute et peut retrouver le graphe de Hoffman–Singleton (ou mieux).
    3. On obtient une recette explicite plutôt qu’un simple résultat brut.

Limites et Nuances (AlphaEvolve)

  • 🪄 N’a pas battu l’état de l’art partout.
  • 🎯 Conçu pour l’optimisation constructive, pas la théorie abstraite.
  • ⚖️ Certaines solutions accessibles par méthodes classiques.

Note

Les algorithmes évolutionnaires sont anciens, mais avec les LLMs, ils gagnent en expressivité et adaptabilité.

Le Cadre Formel

Introduction à Lean

Lean et Curry-Howard

  • 🛡️ Lean 4 : Assistant de preuve utilisé par ces papiers.
  • 🤝 Correspondance de Curry-Howard :
    • Proposition \(\leftrightarrow\) Type
    • Preuve \(\leftrightarrow\) Programme

Conséquences

  • 🧩 Prouver \(A \Rightarrow B\) = Écrire une fonction \(A \to B\).
  • ✅ Vérifier une preuve = Vérifier que le code compile.
  • 🛡️ Offre un cadre strict et vérifiable pour l’IA.

Note

Lean possède une vaste bibliothèque mathématique (mathlib), facilitant la formalisation.

Exemple : Preuve \(\leftrightarrow\) Programme

Théorème (Modus Ponens) : Si \(P\) implique \(Q\), et que \(P\) est vrai, alors \(Q\) est vrai.

-- 1. L'Énoncé (Le Type)
theorem modus_ponens (P Q : Prop) : (P → Q) → P → Q :=

-- 2. La Preuve (Le Programme)
  fun (implication : P → Q) (hypothese_p : P) =>
    implication hypothese_p
  • 🧩 Structure :
    • theorem définit le Type (la proposition à prouver).
    • := sépare l’énoncé de la preuve.
    • La Preuve est une simple fonction qui “applique” l’implication à l’hypothèse.

La Traduction

ProofBridge

La distance linguistique

  • 🗣️ Langage Naturel (NL) : Ambigu, concis et lisible.
  • 💻 Langage Formel (FL) : Strict, vérifiable, mais peu lisible.
  • 🚧 Défi : Traduire automatiquement une preuve en langage naturel en code vérifiable

Astuce

L’inverse (code formel → explication en langage naturel) est plus simple et déjà bien maîtrisé.

L’apporche ProofBridge

  • 🔗 Approche Unifiée : Traduit Théorème ET Preuve.
  • 🌌 Joint Embeddings1 : Espace sémantique partagé NL/FL.
  • 📍 Si deux preuves (Anglais / Lean) disent la même chose, elles sont proches.

Fonctionnement de ProofBridge

  1. 🔍 Retrieval (RAG) : Cherche des preuves Lean similaires.
  2. ✍️ Traduction Guidée : Utilise ces exemples pour guider le LLM.
  3. 🔧 Réparation Itérative : Vérifie la compilation ET le sens (via juge LLM).
  • 📈 Résultat : Meilleure formalisation de preuves complexes.

Limites et Nuances (ProofBridge)

  • 📉 Manque de Données : Exemples alignés (Texte \(\leftrightarrow\) Code Lean) rares.
  • 🤖 Dépendance au Juge : La vérification sémantique repose elle-même sur un LLM.

La Preuve

Kimina-Prover

Le Défi du Raisonnement Formel

  • 🦜 LLMs classiques : Bons pour “parler”, mauvais pour la rigueur.
  • 😵‍💫 Hallucinations : Inventent des étapes de preuve fausses.
  • 🌳 Recherche classique : Algorithmes externes (MCTS/BFS), exploration de l’arbre des preuves (coûteux et peu scalables).

L’Approche Kimina-Prover

  • 🏋️ Reinforcement Learning (RL)1
  • 🧠 Formal Reasoning Pattern : Fournit des « chaînes de pensée » (CoT) avant de répondre.
  • 📝 Blocs <think> : Mélange intuition informelle et code formel.

Exemple : La Trace de Raisonnement

Problème : Montrer que pour tout \(n\), \(n\) divise \(n^2\).

Sortie du Modèle :

<think>
Pour montrer que n | n^2, je dois trouver un entier k tel que n^2 = n * k.
Intuitivement, k = n.
Je vais utiliser la définition de la divisibilité (Dvd.dvd).
En Lean, `use n` devrait marcher, puis `ring` pour l'égalité.
</think>
theorem n_divides_n_sq (n : ℕ) : n ∣ n^2 := by
  use n
  ring

Résultats et passage à l’échelle

  • 🥇 Performance : Nouvel état de l’art sur miniF2F1 (80.7%).
  • 📈 Échelle : La performance augmente avec la taille du modèle (Nouveau !).
  • 💡 Émergence : Le raisonnement « profond » naît du RL.

Limites et Nuances (Kimina)

  • 💰 Coût : Dépend du nombre d’essais (sampling budget).
  • 🤖 Données Synthétiques : Risque de bruit via l’auto-formalisation.
  • 🚧 Expérimental : différent de l’intuition humaine

Petit Modèle, Grande Logique

  • 📉 Frugalité : Rendre le raisonnement mathématique accessible grâce à des modèles plus petits et moins coûteux.

VibeThinker-1.5B

Bigger is Not Always Better

  • 🏗️ Idée reçue : Pour raisonner, il faut des modèles géants (> 100B paramètres).
  • 🦖 Exemples : DeepSeek R1 (671B), Kimi K2 (>1T).
  • 🚧 Problème : Coût prohibitif, recherche réservée aux géants de la Tech.
  • ❓ Question : Un “petit” modèle (1.5B) peut-il rivaliser ?

L’Approche VibeThinker

  • 🌈 Spectrum-to-Signal Principle (SSP) :
    1. SFT (Spectrum) : Maximiser la diversité des solutions (Pass@K). Ne pas chercher juste la bonne réponse, mais toutes les approches.
    2. RL (Signal) : Amplifier le signal correct parmi cette diversité (MGPO).

Résultats Étonnants

  • 🐜 VibeThinker-1.5B vs 🦖 DeepSeek R1 (671B).
  • 🏆 Maths : Bat DeepSeek sur AIME24, AIME25, HMMT251
  • 💸 Coût : Entraîné pour seulement 7 800 $2.
  • 📉 Conclusion : La logique n’est pas (que) une question de taille, mais de méthode d’entraînement.

Limites et Nuances (VibeThinker)

  • 🧠 Spécialisation : performant en maths/code, peut-être moins “généraliste” qu’un gros modèle.
  • 📚 Données : Dépend de la qualité de la distillation (“Teacher models”).
  • 🔬 Empirique : Ingénierie ad hoc (comme la majorité des approches actuelles).

Conclusion

Synthèse

Une chaîne complète et accessible :

  1. 🔭 Exploration (AlphaEvolve).
  2. 🗣️ Traduction (ProofBridge).
  3. ✅ Preuve (Kimina-Prover).
  4. 📉 Frugalité - Accessibilité (VibeThinker).

Où en est-on vraiment ?

  • 🧮 Benchmarks dominants : surtout des maths de lycée / début de licence
    (olympiades type AMC/AIME/IMO, AIME24/25, HMMT25, miniF2F…).
  • 🧱 Au-delà :
    • preuves plus avancées possibles, mais
    • fortement décomposées, guidées, appuyées sur des bibliothèques comme mathlib.
  • 🎯 Image honnête :
    • très bons sur des problèmes d’exercices bien posés,
    • contributions ponctuelles en recherche,
    • loin encore d’un « doctorant automatique » en maths.

Références

Georgiev, Bogdan, Javier Gómez-Serrano, Terence Tao, et Adam Zsolt Wagner. 2025. « Mathematical exploration and discovery at scale ». arXiv preprint arXiv:2511.02864.
Jana, Prithwish, Kaan Kale, Ahmet Ege Tanriverdi, Cruise Song, Sriram Vishwanath, et Vijay Ganesh. 2025. « ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings ». arXiv preprint arXiv:2510.15681.
Wang, Haiming, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, et al. 2025. « Kimina-prover preview: Towards large formal reasoning models with reinforcement learning ». arXiv preprint arXiv:2504.11354.
Xu, Sen, Yi Zhou, Wei Wang, Jixin Min, Zhibin Yin, Yingwei Dai, Shixi Liu, Lianyu Pang, Yirong Chen, et Junlin Zhang. 2025. « Tiny Model, Big Logic: Diversity-Driven Optimization Elicits Large-Model Reasoning Ability in VibeThinker-1.5 B ». arXiv preprint arXiv:2511.06221.

Liens Démos et sites

  • 🧬 AlphaEvolve : https://github.com/algorithmicsuperintelligence/openevolve
  • 🤖 Kimina-Prover : https://demo.projectnumina.ai/
  • 🐜 VibeThinker : https://huggingface.co/WeiboAI/VibeThinker-1.5B et @chatgpt-imag sur mattermost