Résumé Technique : Découverte Auto-Supervisée de Théorèmes dans un Système Axiomatique Formel

Énoncé du Problème

Bien que les systèmes d'IA récents, en particulier les grands modèles de langage (LLM), aient démontré des progrès significatifs dans le raisonnement mathématique, ils reposent largement sur des connaissances préalables fournies par l'humain, telles que des textes mathématiques, du code et des bibliothèques de théorèmes existantes. Une question cruciale demeure : un agent peut-il découvrir de manière autonome des théorèmes utiles en partant uniquement des règles primitives d'un système axiomatique formel, sans accès à la connaissance préalable humaine, aux bibliothèques de théorèmes existantes ou à des ensembles de problèmes d'entraînement ?

Les méthodes actuelles dépendent souvent de la connaissance construite par l'humain pour amorcer le raisonnement. Même les agents auto-améliorables dans les domaines axiomatiques dépendent souvent de juges externes pour évaluer l'utilité des théorèmes découverts. Ce document étudie si un agent peut non seulement découvrir des théorèmes, mais aussi identifier et utiliser ceux qui sont « utiles » pour améliorer sa propre recherche de preuves et la performance de systèmes de raisonnement externes, en s'appuyant exclusivement sur les axiomes et les règles d'inférence.

Méthodologie

1. Cadre Formel : Système de Hilbert comme Machine à Pile

Les auteurs instancient le problème au sein d'un système axiomatique de Hilbert pour la logique propositionnelle. Le système est délibérément minimal, composé de :

• Trois Axiomes :
  • $Ax1: A \to (B \to A)$ (Affaiblissement)
  • $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ (Distribution)
  • $Ax3: (\neg A \to \neg B) \to (B \to A)$ (Contraposition)
• Une Règle d'Inférence : Modus Ponens (MP), dérivant $Y$ de $X$ et $X \to Y$.

Pour faciliter l'apprentissage, les auteurs formulent la démonstration de théorèmes comme un processus de décision déterministe, conditionné par l'objectif, de type machine à pile $(S, A, s_0, P)$ :

• État ($S$) : Une pile finie de formules.
• Actions ($A$) : Pousser des instances de $Ax1, Ax2, Ax3$ sur la pile, ou appliquer le Modus Ponens (MP).
• Mécanisme : L'action MP utilise l'unification de Hindley–Milner. Si l'élément supérieur de la pile s'unifie avec $X \to Y$ et que l'élément en dessous s'unifie avec $X$, les deux sont retirés (pop) et $Y$ est poussé (push) sur la pile.
• Succès : Une démonstration est réussie si la pile contient une seule formule correspondant à l'objectif visé.

2. Algorithme de Découverte de Théorèmes Auto-Supervisé

La contribution centrale est un algorithme qui alterne entre recherche de preuves et extraction de théorèmes utiles, construisant une bibliothèque de théorèmes qui servent de lemmes pour la recherche future.

A. Apprentissage de Politique Conditionné par l'Objectif

L'agent apprend une politique $\pi_\theta(A|S, g)$ pour prédire l'action suivante étant donné la pile actuelle $S$ et un objectif $g$.

• Apprentissage par Regard Rétrospectif (Hindsight Learning) : Durant un épisode de recherche, tout état où la pile contient une seule formule $f_t$ est traité comme un « théorème atteint », qu'il s'agisse ou non de l'objectif original.
• Signal d'Entraînement : Le préfixe d'actions menant à $f_t$ est traité comme une preuve de $f_t$. Ces préfixes sont ajoutés à un ensemble d'entraînement $D_{train}$ pour mettre à jour la politique via une perte d'entropie croisée.
• Tampon d'Objectifs ($G$) : Un tampon maintient les théorèmes découverts. L'agent échantillonne les objectifs uniformément à partir de $G$ pour les épisodes de recherche ultérieurs, amorçant ainsi son propre curriculum.

B. Extraction de Théorèmes Utiles

Pour éviter que la bibliothèque ne soit encombrée de théorèmes triviaux ou redondants, l'algorithme filtre les théorèmes découverts selon deux critères :

1. Généralité : Les théorèmes sont filtrés pour éliminer ceux qui ne sont que des spécialisations d'autres candidats. Le système ne conserve que les éléments « minimaux » sous un ordre partiel défini par la substitution de formules (c'est-à-dire en gardant les formes les plus générales).
2. Reprouvabilité : Le système estime la probabilité que la politique actuelle puisse reprover un théorème. En utilisant une moyenne de l'a posteriori bayésien (prior Beta(1,1)), il donne la priorité aux théorèmes qui ont été découverts mais qui sont difficiles à reprover de manière fiable. Ces théorèmes « difficiles à reprover » sont précieux car l'ajout de ces lemmes compresse les chemins de preuve complexes.

C. Expansion de la Bibliothèque Multi-Générationnelle

Le processus opère par générations :

1. Apprentissage de la Politique : Entraîner la politique sur l'espace d'actions actuel (initialement uniquement les axiomes et MP).
2. Extraction : Identifier les théorèmes utiles à partir du tampon d'objectifs $G$ basés sur la généralité et la reprovabilité.
3. Expansion de l'Espace d'Actions : Ajouter les théorèmes extraits comme de nouveaux actions de bibliothèque (ex: $Thm_1, Thm_2$). Lorsqu'ils sont sélectionnés, ces actions poussent le théorème correspondant sur la pile, agissant comme un lemme pré-vérifié.
4. Itération : Répéter le processus, permettant à l'agent d'utiliser les théorèmes précédemment découverts pour trouver de nouveaux théorèmes plus complexes.

Contributions Clés

1. Formulation : La démonstration de propositions est formulée comme un processus de machine à pile basé directement sur les axiomes de Hilbert et les règles d'inférence, évitant ainsi le recours à des corpus de preuves externes.
2. Algorithme : Un algorithme de découverte de théorèmes auto-supervisé est proposé, qui développe une bibliothèque de théorèmes à partir des règles primitives seules. Il réutilise les théorèmes extraits comme lemmes pour la recherche de preuves ultérieure.
3. Découverte Autonome : L'agent découvre des dizaines de milliers de théorèmes et trouve des preuves pour des problèmes de référence écrits par des humains sans utiliser de priors humains pour l'entraînement.
4. Transférabilité : Les théorèmes extraits servent de connaissances externes efficaces, améliorant les performances de raisonnement de LLM externes lorsqu'ils sont fournis comme lemmes dans un prompt.

Résultats Expérimentaux

1. Découverte de Théorèmes et Couverture

• Croissance : Le nombre de théorèmes découverts augmente sur six générations, démontrant la capacité de l'agent à étendre sa base de connaissances de manière autonome.
• Performance sur les Benchmarks : L'agent trouve avec succès des preuves dans le système de Hilbert pour 30 % d'un ensemble de référence écrit par des humains (dérivé du manuel de Kleene).
• Comparaison : Alors que GPT-5-high (le baseline le plus fort) n'atteint qu'environ 23 % de précision sur ces benchmarks sans assistance, la capacité de l'agent à trouver des preuves pour 30 % suggère qu'il découvre des preuves non triviales qui sont significatives d'un point de vue mathématique pour l'humain.

2. Impact sur le Raisonnement des LLM

• Lemmes de Prompt : Lorsque les théorèmes extraits sont fournis comme lemmes de prompt aux variantes de GPT-4o et GPT-5, leurs taux de succès de preuve sur les problèmes de référence s'améliorent considérablement.
• Analyse Qualitative :
  • Certains théorèmes découverts correspondent à des principes bien connus (ex: le principe d'explosion, $\neg A \to (A \to B)$), qui sont facilement interprétables.
  • D'autres (ex: élévation d'implication complexe) ne sont pas immédiatement évidents pour l'humain mais fonctionnent efficacement comme connaissances de support dans les preuves des LLM.
  • Cela indique que l'agent peut faire émerger des lemmes utiles que les humains n'ont pas explicitement fournis, et que ces lemmes sont transférables entre différentes architectures de raisonnement (de l'agent vers les LLM).

Signification et Revendications

Le papier affirme fournir la preuve que des théorèmes utiles peuvent émerger de la recherche de preuves sans dépendre de bibliothèques de théorèmes fournies par l'humain.

• IA Auto-Évolutive : Ce travail suggère une voie vers des systèmes d'IA auto-évolutifs pour les mathématiques, capables d'étendre de manière autonome leur connaissance formelle par la recherche de preuves, tout en garantissant que chaque découverte reste formellement vérifiable.
• Vérifiabilité Formelle : Contrairement aux LLM qui peuvent halluciner des énoncés plausibles mais incorrects, les découvertes de l'agent sont strictement ancrées dans les axiomes et les règles d'inférence du système de Hilbert.
• Modestie : Les auteurs ne prétendent pas avoir surpassé les LLM de pointe dans le raisonnement général. Au lieu de cela, ils démontrent que dans un cadre contraint et formel, un agent peut apprendre à découvrir et à utiliser sa propre connaissance pour résoudre des problèmes difficiles même pour les LLM avancés, et que cette connaissance auto-découverte peut augmenter des systèmes externes.

L'étude est limitée à un seul système axiomatique (logique propositionnelle de Hilbert), mais les auteurs postulent que le cadre est généralisable à des systèmes plus riches comme la logique du premier ordre ou la théorie des ensembles, ce qui constitue une direction pour des travaux futurs.