GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

Ce papier présente GAR, un cadre d'apprentissage par renforcement adversarial qui entraîne conjointement un générateur de problèmes et un prouveur dans une boucle itérative, permettant d'améliorer significativement l'efficacité de l'entraînement et la performance des modèles sur la preuve de théorèmes formels complexes.

L'essentiel

Imagine que vous essayez d'enseigner à un élève très brillant, mais un peu têtu, comment résoudre des énigmes mathématiques complexes. C'est un peu ce que fait cette recherche, mais au lieu d'un élève humain, il s'agit d'une intelligence artificielle (IA) apprenant à prouver des théorèmes mathématiques dans un langage informatique très strict appelé Lean.

Voici l'explication de la méthode GAR (Generative Adversarial Reinforcement Learning) racontée comme une histoire, avec des analogies simples.

1. Le Problème : L'Élève qui s'ennuie ou qui est perdu

Jusqu'à présent, pour entraîner ces IA, les chercheurs leur donnaient un gros manuel de problèmes fixes (comme un livre d'exercices de 1000 pages).

• Le problème : Si l'IA est débutante, les problèmes du milieu du livre sont trop durs et elle abandonne. Si elle devient experte, les problèmes du début sont trop faciles et elle s'ennuie.
• Le résultat : L'entraînement est inefficace. L'IA perd du temps sur des choses trop simples ou trop difficiles, et n'arrive pas à progresser vraiment sur les défis complexes.

2. La Solution : Le Duo "Professeur vs Élève" (GAR)

Les auteurs de ce papier ont eu une idée géniale : au lieu d'avoir un livre d'exercices fixe, ils créent un système à deux joueurs qui s'entraînent ensemble en permanence.

Imaginez un jeu vidéo où deux IA s'affrontent :

• Joueur A : Le "Compositeur de Problèmes" (Le Fuser)

  • Son rôle est de créer de nouveaux problèmes mathématiques.
  • Sa mission ? Créer des énigmes qui sont juste un peu plus difficiles que ce que l'autre IA sait faire actuellement. Ni trop faciles, ni impossibles.
  • L'analogie : C'est comme un entraîneur de sport qui ajuste la charge de poids. Si vous soulevez 10 kg facilement, il vous donne 12 kg. Si vous échouez, il vous redonne 11 kg. Il cherche toujours le "juste milieu" pour vous faire progresser.

• Joueur B : Le "Résolveur" (Le Prover)

  • Son rôle est de résoudre les problèmes que le Compositeur lui donne.
  • Sa mission ? Trouver la preuve mathématique parfaite.
  • L'analogie : C'est l'athlète qui s'entraîne. Plus l'entraîneur lui donne de défis adaptés, plus il devient fort.

3. Comment ça marche ? (Le Cycle de l'Entraînement)

Le système fonctionne comme une boucle infinie, un peu comme un tournoi d'échecs où les deux joueurs s'améliorent à chaque partie :

1. La Fusion (Création du problème) : Le Compositeur prend deux petits problèmes existants et les "fusionne" (comme mélanger deux ingrédients pour créer une nouvelle recette) pour en faire un problème plus complexe.
2. La Tentative (Résolution) : Le Résolveur essaie de prouver ce nouveau problème.
3. Le Feedback (La Récompense) :
   • Si le Résolveur réussit, le Compositeur reçoit un "mauvais point" (car il n'a pas été assez difficile) et doit créer un problème encore plus dur la prochaine fois.
   • Si le Résolveur échoue parce que c'est trop dur, le Compositeur reçoit un "mauvais point" (car c'était impossible) et doit simplifier un peu.
   • Si le Résolveur réussit sur un problème difficile, il reçoit un "bon point".
4. L'Évolution : Grâce à ce jeu de chat et de souris, le Compositeur apprend à créer des problèmes parfaitement calibrés, et le Résolveur apprend à résoudre des choses de plus en plus complexes. C'est ce qu'on appelle un curriculum implicite : le programme d'études s'écrit tout seul en fonction de la progression de l'élève.

4. Pourquoi c'est révolutionnaire ?

Avant, les chercheurs devaient annoter des milliers de problèmes manuellement ou utiliser des ensembles de données fixes. C'était lent et rigide.

Avec GAR :

• L'IA s'auto-entraîne : Elle crée ses propres défis adaptés à son niveau.
• Pas de gaspillage : L'IA ne perd pas de temps sur des problèmes trop faciles.
• Résultats impressionnants : Les tests montrent que les IA entraînées avec cette méthode (comme DeepSeek-Prover ou Goedel-Prover) réussissent beaucoup mieux à résoudre des problèmes de mathématiques avancées (comme ceux des olympiades ou des manuels universitaires) que les anciennes méthodes.

En résumé

Imaginez un coach de gymnastique (le Compositeur) et un gymnaste (le Résolveur).

• Le coach ne donne pas toujours le même exercice. Il regarde le gymnaste : "Tu as réussi l'équilibre ? Super, maintenant fais-le sur une poutre plus fine." "Tu as tombé ? Ok, on remet une poutre un peu plus large."
• Grâce à cette adaptation constante, le gymnaste atteint un niveau d'expert beaucoup plus vite que s'il s'entraînait sur un parcours fixe.

C'est exactement ce que fait GAR : il permet aux intelligences artificielles de devenir de véritables maîtres en mathématiques en leur donnant des défis qui grandissent avec elles.

Résumé technique

1. Problème et Contexte

La résolution de problèmes mathématiques via des langages vérifiables comme Lean a transformé les communautés de mathématiques et d'informatique. Cependant, les modèles de pointe actuels souffrent de limitations majeures :

• Ensembles de données fixes : Les approches d'apprentissage par renforcement (RL) ou d'itération d'experts reposent sur des ensembles de théorèmes statiques. Cela entraîne un gaspillage de ressources computationnelles sur des tâches triviales ou insolubles et limite la capacité du modèle à progresser vers des problèmes complexes.
• Absence de curriculum adaptatif : Les méthodes RL existantes ne disposent pas d'un mécanisme pour ajuster dynamiquement la difficulté des énoncés en fonction des capacités évolutives du prouveur.
• Complexité de la vérification : L'ambiguïté du langage naturel (NL) rend difficile la vérification des étapes intermédiaires, d'où la nécessité d'utiliser des langages formels (FL) comme Lean, qui sont difficiles à maîtriser pour les LLMs standards.

2. Méthodologie : Le Framework GAR

Les auteurs proposent GAR (Generative Adversarial Reinforcement Learning), un cadre d'entraînement RL qui optimise conjointement deux agents dans une boucle adversaire :

1. Le Prouveur (Solver) : Génère des preuves formelles en Lean4.
2. Le Fuseur d'Énoncés (Statement Fuser) : Génère des énoncés de problèmes plus difficiles à partir de problèmes existants.

Le processus s'articule autour de deux étapes itératives :

A. Phase de Génération (Statement Fusion)

• Fusion d'énoncés : Le Fuser (basé sur un modèle de type "thinking" comme Qwen3 ou DeepSeek-R1) prend deux énoncés naturels (NL) issus d'un référentiel de base et les combine pour créer un nouvel énoncé plus complexe.
• Stratégie de fusion : Contrairement aux méthodes précédentes qui fusionnent des énoncés formels, GAR fusionne d'abord les énoncés en langage naturel, puis les formalise en Lean via un autoformalisateur. Cela évite les erreurs de compilation fréquentes lors de la fusion directe de code formel.
• Génération de preuves : Le Prouveur tente de résoudre ces nouveaux énoncés en générant plusieurs candidats de preuves (ex: 16 par énoncé).

B. Phase d'Apprentissage par Renforcement Adversaire

Les deux modèles sont mis à jour via une variante de l'algorithme GRPO (Group Relative Policy Optimization) :

• Récompense du Fuser : Il est récompensé pour générer des problèmes difficiles mais solubles. La récompense est conçue pour minimiser le taux de réussite du prouveur (en augmentant la difficulté) tout en évitant de créer des problèmes impossibles (taux de réussite = 0).
  • Mécanisme clé : Une pénalité douce est appliquée si le prouveur modifie l'énoncé original pour le simplifier (phénomène de "reward hacking"), garantissant que la difficulté est réelle.
• Récompense du Prouveur : Il est récompensé pour produire des preuves correctes sur des problèmes de difficulté moyenne à élevée. Les problèmes trop faciles (taux de réussite > 0.5) ou trop difficiles (taux = 0) sont filtrés pour concentrer l'apprentissage sur la zone de défi optimal.

Ce mécanisme crée un curriculum implicite : la difficulté des problèmes évolue naturellement au rythme des améliorations du prouveur.

3. Contributions Clés

1. Framework GAR : Un système RL complet qui établit un curriculum implicite, améliorant l'efficacité de l'entraînement et évitant le gaspillage sur des tâches hors de portée du modèle.
2. Technique de Fusion d'Énoncés : Une méthode innovante qui combine des énoncés en langage naturel avant la formalisation, permettant de créer de nouveaux théorèmes mieux alignés avec les capacités du modèle que la simple formalisation de problèmes NL existants.
3. Paradigme de Co-évolution : Une approche générale pour l'évolution conjointe de la génération et de la résolution de problèmes dans des environnements vérifiables, applicable au-delà des preuves de théorèmes.

4. Résultats Expérimentaux

Les expériences ont été menées sur les benchmarks MiniF2F-Test et ProofNet-Test en utilisant deux modèles de base : Goedel-Prover-V2-8B et DeepSeek-Prover-V2-7B.

• Améliorations sur MiniF2F-Test :
  • Goedel-Prover-V2-8B : Le taux de réussite (pass@32) passe de 77.87% à 80.33% (+3.16% relatif).
  • DeepSeek-Prover-V2-7B : Le taux de réussite passe de 70.49% à 74.18% (+5.23% relatif).
• Améliorations sur ProofNet-Test (Mathématiques avancées) :
  • Pour DeepSeek-Prover-V2, le pass@32 augmente de 22.58% à 25.81%, démontrant la capacité du modèle à résoudre des théorèmes universitaires complexes.
• Efficacité et Robustesse :
  • L'analyse montre que le modèle de base voit son taux de réussite chuter drastiquement sur les énoncés générés par GAR (confirmant l'augmentation de la difficulté), tandis que le modèle entraîné par GAR maintient une performance stable (~21%).
  • Des études d'ablation confirment que sans la pénalité de modification d'énoncé, le modèle exploite des failles (simplification abusive des problèmes), et que sans le fuseur entraîné (fuser gelé), aucune amélioration n'est obtenue.

5. Signification et Impact

L'article GAR représente une avancée significative dans l'apprentissage automatique pour les mathématiques formelles :

• Surmonter la stagnation du RL : Il démontre que même pour des modèles déjà fortement entraînés par RL, une approche adversaire dynamique permet de continuer à progresser, là où l'entraînement RL statique échoue.
• Efficacité computationnelle : En générant des données "à la demande" adaptées au niveau actuel du modèle, GAR réduit le besoin d'annotation massive et de données fixes, rendant l'entraînement plus efficace.
• Généralité : Le paradigme de co-évolution adversaire proposé offre une nouvelle voie pour les domaines intensifs en raisonnement, suggérant que l'alignement dynamique entre la difficulté de la tâche et la capacité de l'agent est crucial pour atteindre des niveaux d'expertise supérieurs.

Le code d'entraînement et d'inférence de GAR sera open-sourcé, facilitant la reproduction et l'extension de ces travaux par la communauté.