Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

Cet article présente la boucle conjecture-preuve (CPL), un pipeline qui exploite l'apprentissage en contexte en alimentant itérativement un LLM avec ses propres théorèmes et preuves formellement vérifiés en Lean 4, afin d'améliorer considérablement le taux de découverte et le succès de conjectures mathématiques nouvelles et difficiles à démontrer.

L'essentiel

Imaginez que vous essayez d'enseigner à un robot très intelligent, mais légèrement oublieux, comment résoudre des énigmes mathématiques complexes. Le robot est un Modèle de Langage à Grande Échelle (LLM), et les énigmes sont des preuves mathématiques formelles écrites dans un langage informatique strict appelé Lean.

L'article présente une nouvelle méthode pour enseigner à ce robot, appelée la Boucle de Conjecture-Preuve (CPL). Voici comment elle fonctionne, expliquée par le biais d'analogies simples :

Le Problème : Le Piège du « Deviner-et-Vérifier »

Habituellement, lorsque l'on tente de faire faire des mathématiques à une IA, on lui demande de deviner une énigme et de la résoudre en une seule fois.

• L'Analogie : Imaginez demander à un élève de « Rédiger un problème de mathématiques et le résoudre immédiatement ».
• Le Problème : L'élève devient paresseux. Il rédige des problèmes faciles (comme « 2 + 2 = 4 ») car ils sont simples à résoudre. Il évite les problèmes difficiles car il sait qu'il risque d'échouer. L'IA finit par générer des milliers de preuves faciles et ennuyeuses, manquant ainsi les problèmes difficiles et intéressants.

La Solution : La « Danse en Deux Temps » (CPL)

Les auteurs divisent le processus en deux rôles distincts : un Conjecteur (le Générateur d'Idées) et un Preuveur (le Résolveur).

1. Le Conjecteur (L'Architecte) : Cette partie de l'IA examine une bibliothèque de règles mathématiques existantes et élabore de nouvelles idées (conjectures). Elle ne tente pas encore de les résoudre ; elle se contente de les écrire.
2. Le Preuveur (Le Bâtisseur) : Cette partie prend les idées et tente de construire une preuve pour elles. Si elle échoue, elle réessaie. Elle continue d'essayer jusqu'à ce qu'elle réussisse ou qu'elle épuise ses tentatives.
3. La Bibliothèque (La Mémoire) : Chaque fois que le Preuveur construit avec succès une preuve, cette preuve est ajoutée à la bibliothèque.

L'Ingrédient Magique : L'Apprentissage en Contexte
Voici la partie ingénieuse : le Preuveur ne se contente pas d'examiner les règles mathématiques originales. Il examine la bibliothèque de preuves qu'il a déjà construites avec succès au cours de la session en cours.

• L'Analogie : Imaginez un élève passant un examen. À l'ancienne, il devait se fier uniquement à ce qu'il avait mémorisé avant le début de l'examen. Dans cette nouvelle méthode, chaque fois que l'élève résout correctement un problème, il a le droit de relire sa propre solution avant d'attaquer le problème suivant. Il apprend les « astuces » et les « stratégies » de ses propres succès récents.

Ce Qu'ils Ont Découvert

Les chercheurs ont testé cela sur des concepts topologiques délicats (une branche des mathématiques traitant des formes et des espaces) que l'IA ne maîtrisait pas encore bien.

• Quantité vs Qualité : L'ancienne méthode (deviner et résoudre en une fois) a généré plus de théorèmes au total, mais ils étaient pour la plupart courts et faciles. La nouvelle méthode (CPL) a généré moins de théorèmes au total, mais ils étaient beaucoup plus difficiles et plus longs.
• La Grande Victoire : La nouvelle méthode a découvert avec succès un théorème spécifique et difficile concernant les « ensembles alpha-ouverts » que l'ancienne méthode n'a jamais trouvé, même après 20 tentatives.
• Apprendre du Succès : Lorsque l'IA a reçu la bibliothèque de ses propres preuves précédentes comme « aide-mémoire » (contexte), elle a pu prouver des théorèmes difficiles qu'elle n'aurait pas pu résoudre sans ce contexte. Même lorsque l'IA ne pouvait pas prouver le théorème en anglais courant, elle a pu le prouver en code Lean une fois qu'elle avait vu des preuves réussies similaires.

La Conclusion

L'article affirme qu'en séparant la « génération d'idées » de la « résolution de preuves » et en permettant à l'IA d'apprendre de ses propres succès vérifiés en temps réel, nous pouvons l'amener à découvrir des vérités mathématiques plus difficiles et plus complexes qu'elle manquerait autrement. C'est comme donner à l'IA un élan en lui permettant d'étudier ses propres devoirs avant de passer l'examen final.

Note : L'article se concentre strictement sur cette méthode pour générer et vérifier des théorèmes mathématiques. Il ne prétend pas que cette méthode fonctionne pour le diagnostic médical, les prévisions financières ou d'autres applications réelles en dehors des mathématiques formelles.

Résumé technique

Résumé technique : Découverte de nouveaux théorèmes via des LLM avec apprentissage de preuves en contexte dans Lean

Énoncé du problème
Les grands modèles de langage (LLM) ont montré des promesses dans la preuve de théorèmes formels, mais font face à des défis majeurs : ils peuvent halluciner, et la génération simultanée d'une conjecture mathématique et de sa preuve conduit souvent à une convergence vers des théorèmes triviaux ou faciles. Les approches existantes reposent généralement sur un ajustement fin supervisé (SFT) ou un apprentissage par renforcement avec récompenses vérifiées (RLVR), qui nécessitent d'importantes quantités de données d'entraînement et sont difficiles à appliquer aux modèles à source fermée. De plus, les méthodes actuelles peinent souvent à découvrir des théorèmes « difficiles à prouver » car la probabilité de générer un théorème est fortement pondérée par le taux de réussite immédiat de sa preuve, ce qui provoque l'effondrement de la recherche vers des preuves simples et courtes.

Méthodologie : La boucle conjecture-preuve (CPL)
Les auteurs proposent la boucle conjecture-preuve (CPL), un pipeline conçu pour générer automatiquement des conjectures mathématiques et les vérifier dans Lean 4. Le cadre sépare la génération des conjectures de la génération des preuves, en utilisant une bibliothèque de théorèmes précédemment vérifiés comme contexte pour les deux étapes.

Le pipeline fonctionne via quatre composants principaux : un Conjecteur (agent LLM), un Prouveur (agent LLM), un Serveur Lean et une Bibliothèque (données de code Lean).

1. Phase de conjecture : Le Conjecteur génère de nouvelles affirmations mathématiques au format Lean 4 basées sur la bibliothèque actuelle. Il interroge le Serveur Lean pour garantir la validité syntaxique et la nouveauté (en vérifiant que l'affirmation n'est pas déjà prouvable par les théorèmes existants dans Mathlib4 ou la bibliothèque actuelle).
2. Phase de preuve : Pour chaque conjecture valide, le Prouveur tente de construire une preuve formelle. Crucialement, le Prouveur reçoit la bibliothèque (contenant les théorèmes et preuves précédemment vérifiés) comme contexte. Cela permet au LLM d'apprendre des stratégies de preuve via l'apprentissage en contexte sans réentraînement du modèle. Le Prouveur itère jusqu'à un nombre maximal d'essais (fixé à 16 dans les expériences), utilisant les messages d'erreur du Serveur Lean pour affiner ses tentatives.
3. Itération : Les paires vérifiées de conjectures et de preuves sont ajoutées à la bibliothèque, qui sert ensuite de contexte pour les itérations suivantes.

Cette séparation permet au système d'allouer des ressources de recherche en fonction de la difficulté de la preuve. Contrairement à une boucle simple (SL) où une affirmation et une preuve sont générées simultanément, la CPL tente plusieurs preuves pour une seule affirmation avant de l'abandonner. Cela déplace la distribution des théorèmes générés vers ceux qui sont prouvables mais difficiles, plutôt que vers ceux qui sont simplement faciles à prouver.

Contributions clés

1. Proposition de pipeline : L'introduction de la CPL, un cadre qui découple la génération de conjectures de la génération de preuves, permettant la découverte de preuves plus longues et plus complexes.
2. Apprentissage en contexte pour les modèles à source fermée : La démonstration que les LLM à source fermée (spécifiquement ChatGPT-o3) peuvent améliorer leurs capacités de preuve grâce à l'apprentissage en contexte à partir de leurs propres sorties précédemment vérifiées, éliminant ainsi le besoin de mises à jour de paramètres ou d'ajustement fin.
3. Validation théorique et empirique : L'article fournit un modèle théorique montrant que la CPL augmente la probabilité de générer des théorèmes difficiles à prouver par rapport aux cadres de génération simultanée. Expérimentalement, il vérifie que la CPL a réussi à redécouvrir un théorème spécifique de niveau recherche que le cadre de base n'a pas réussi à trouver.

Résultats expérimentaux
Les auteurs ont évalué la CPL par rapport à une base de référence de boucle simple (SL) en utilisant des notions topologiques (semi-ouverture, $\alpha$-ouverture et préouverture) définies dans Mathlib mais pas encore incluses dans la bibliothèque. La cible était le théorème affirmant que l'intersection de deux ensembles $\alpha$-ouverts est $\alpha$-ouverte.

• Taux de découverte : Sur 20 runs expérimentaux, la CPL a découvert le théorème cible 5 fois. En revanche, le cadre SL, qui a généré significativement plus de théorèmes en moyenne (328 contre 106), n'a pas réussi à générer le théorème cible une seule fois. Le test exact de Fisher a confirmé que cette différence était statistiquement significative ($p = 0,024$).
• Longueur de la preuve : La CPL a généré des théorèmes avec des longueurs de preuve significativement plus grandes (en nombre de caractères) par rapport à la SL, soutenant l'affirmation théorique selon laquelle le cadre déplace l'accent vers des preuves plus difficiles.
• Efficacité du contexte :
  • Re-preuve : Lors de la re-preuve des théorèmes générés, fournir la bibliothèque comme contexte a augmenté le taux de réussite de 91 % à 99 % ($p = 4 \times 10^{-35}$).
  • Théorème cible : Lors de la tentative de re-preuve du théorème cible d'intersection $\alpha$-ouverte, le prouveur a réussi 7 fois sur 80 tentatives lorsque la bibliothèque générée était fournie comme contexte. Sans la bibliothèque, il a échoué 100 % du temps.
  • Base de référence en langage naturel : Lorsqu'on demandait de prouver le théorème en langage naturel, ChatGPT-4o jugeait fréquemment le théorème faux ou fournissait des preuves incorrectes, et ChatGPT-o3 le jugeait systématiquement faux, indiquant que le théorème était en dehors des connaissances pré-entraînées des modèles. Le succès en Lean 4 a été attribué à l'apprentissage en contexte des stratégies de preuve à partir de la bibliothèque générée.

Signification et affirmations
L'article affirme que la CPL adresse efficacement la limitation des LLM dans la découverte de théorèmes non triviaux en exploitant l'apprentissage en contexte à partir de preuves vérifiées auto-générées. Les auteurs soulignent que cette approche permet l'expansion automatique des bibliothèques de mathématiques formelles (comme Mathlib) en générant des propositions sur des notions données qui peuvent ne pas être explicitement connues du LLM. Le travail suggère que la séparation des phases de conjecture et de preuve, combinée à un enrichissement itératif du contexte, est une stratégie viable pour la preuve de théorèmes par réseaux de neurones, en particulier pour les modèles à source fermée où les méthodes d'entraînement traditionnelles ne sont pas applicables. Les auteurs adoptent une position modeste, notant que si le cadre a réussi à redécouvrir un théorème connu de niveau recherche, des travaux futurs sont nécessaires pour affiner le processus de génération afin d'obtenir des affirmations mathématiques plus profondes et plus perspicaces.