🤖 AI

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization

L'article présente ImProver 2, un cadre neurosymbolique qui combine une itération d'experts économe en données avec un système d'échafaudage structurel pour permettre aux petits modèles de langage d'optimiser efficacement des preuves formelles complexes en Lean 4, surpassant des modèles nettement plus grands tout en établissant l'optimisation de preuves comme une tâche évolutive et apprenable.

Auteurs originaux : Riyaz Ahuja, Tate Rowney, Jeremy Avigad, Sean Welleck

Publié 2026-05-25

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Riyaz Ahuja, Tate Rowney, Jeremy Avigad, Sean Welleck

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous possédiez une bibliothèque massive et grandissante de preuves mathématiques. Ce ne sont pas de simples histoires ; ce sont des plans rigides, vérifiés par ordinateur, qui prouvent que certaines choses sont vraies. Récemment, les ordinateurs (spécifiquement l'IA) ont commencé à aider les humains à rédiger ces preuves, provoquant une explosion de la taille de la bibliothèque.

Mais il y a un problème : la bibliothèque devient désordonnée. Certaines preuves sont correctes mais rédigées dans un style confus, d'autres sont trop longues, et certaines reposent sur une immense liste d'autres règles qui les rendent difficiles à maintenir. C'est comme avoir une maison où la plomberie fonctionne, mais où les tuyaux sont emmêlés, les murs peints dans des couleurs qui s'entrechoquent, et où vous devez transporter un sac à dos rempli d'outils supplémentaires juste pour allumer une lumière.

Voici ImProver 2.

Pensez à ImProver 2 comme à un bibliothécaire super organisé et auto-améliorant qui ne se contente pas de ranger les livres, mais les réécrit pour les rendre meilleurs. Sa tâche consiste à prendre une preuve correcte et à la réécrire pour la rendre plus courte, plus propre ou plus modulaire, sans briser les mathématiques.

Voici comment cela fonctionne, en utilisant quelques analogies simples :

1. La boucle « La pratique rend parfait » (Auto-amélioration itérative)

Habituellement, pour enseigner à un ordinateur comment accomplir une tâche, vous lui montrez des milliers d'exemples rédigés par des humains. Mais pour l'optimisation des preuves, les bons exemples sont rares.

ImProver 2 résout ce problème en s'enseignant lui-même.

Le Brouillon : Il prend une preuve et tente de la réécrire de nombreuses façons différentes (comme un écrivain imaginant 10 fins différentes pour une histoire).
La Notation : Il vérifie quelles réécritures restent mathématiquement correctes. Ensuite, il les note en fonction de ce que nous souhaitons : Est-elle plus courte ? Utilise-t-elle moins de références externes ? Est-elle découpée en étapes plus claires ?
La Leçon : Il compare ses réécritures « gagnantes » à ses réécritures « perdantes ». Il apprend : « Oh, quand j'ai fait cela, la preuve est devenue plus courte et est restée correcte. Quand j'ai fait ça, elle s'est brisée. »
Le Tampon de Replay : Pour empêcher l'IA d'oublier ce qu'elle a appris ou de rester coincée dans une boucle d'idées mauvaises, elle conserve une « banque de mémoire » d'anciens bons exemples mélangés à de nouveaux. Cela garantit qu'elle continue de s'améliorer avec le temps, plutôt que de simplement répéter les mêmes erreurs.

2. L'« Échafaudage Neurosymbolique » (Les Roues d'Entraînement)

Imaginez essayer de réparer un moteur complexe sans manuel ni schéma. C'est difficile. Maintenant, imaginez avoir un schéma qui met en évidence exactement la partie sur laquelle vous travaillez, explique ce que fait cette partie en anglais simple, et liste les outils nécessaires à proximité.

ImProver 2 fournit à l'IA ce « schéma » pour chaque preuve. Cela s'appelle l'Augmentation Neurosymbolique. Elle fournit :

La Carte : Elle montre l'état actuel de la preuve (ce qui est prouvé jusqu'ici, ce qui reste à faire).
Le Contexte : Elle récupère les définitions et règles spécifiques pertinentes pour cette preuve précise, afin que l'IA n'ait pas à deviner.
La Traduction : Elle donne un résumé en « anglais simple » de ce que la preuve tente de faire, aidant l'IA à comprendre l'objectif avant de commencer à écrire le code.

Cet « échafaudage » aide même les petits ordinateurs, moins puissants, à performer comme des machines beaucoup plus grandes et intelligentes.

3. Les Trois Objectifs (Métriques)

Le bibliothécaire ne veut pas seulement que la preuve soit « correcte ». Il souhaite optimiser des qualités spécifiques, comme un chef ajustant une recette :

Longueur (La Métrique « Golf ») : Tout comme au golf, l'objectif est de mettre la balle dans le trou avec le moins de coups possible. ImProver 2 tente de raccourcir les preuves en supprimant les étapes inutiles.
Dépendances (La Métrique « Autonome ») : Imaginez une recette qui dit « ajoutez la sauce secrète de la maison du voisin ». C'est une dépendance. ImProver 2 tente de réécrire les preuves afin qu'elles ne reposent pas sur autant de « sauces du voisin » externes, les rendant plus faciles à comprendre et à utiliser de manière autonome.
Modularité (La Métrique « Lego ») : Une preuve désordonnée est comme un gros bloc d'argile. Une preuve modulaire est comme un ensemble de Legos : de petites pièces distinctes et réutilisables. ImProver 2 tente de décomposer les grandes preuves en sous-preuves plus petites et indépendantes (comme « avoir h1 », « avoir h2 ») afin que la logique soit plus claire.

Les Résultats : Le Petit est Puissant

La découverte la plus surprenante est qu'ImProver 2 a pris un modèle d'IA petit (7 milliards de paramètres) et l'a entraîné à être meilleur dans ces tâches que des modèles d'IA massifs (certains avec des centaines de milliards de paramètres) qui n'ont pas reçu cette formation spéciale.

C'est comme prendre une voiture de sport compacte et efficace, régler son moteur avec une telle perfection qu'elle bat un camion massif et lourd dans une course spécifique, même si le camion a un moteur plus gros. Le petit modèle, lorsqu'il reçoit le bon « échafaudage » et la bonne « boucle de pratique », a appris à restructurer des arguments mathématiques complexes mieux que les géants.

En résumé : ImProver 2 est un système qui enseigne aux petits modèles d'IA à devenir des éditeurs experts de preuves. En leur donnant une carte claire du problème et en les laissant apprendre de leurs propres meilleures tentatives, il peut nettoyer des bibliothèques mathématiques désordonnées, les rendant plus courtes, plus propres et plus faciles à maintenir, le tout sans avoir besoin des superordinateurs les plus coûteux et les plus massifs.

Résumé Technique : ImProver 2

Énoncé du Problème

L'expansion rapide des bibliothèques de mathématiques formelles (par exemple, Mathlib de Lean) a créé un double défi : la maintenabilité de ces bibliothèques est menacée par des styles de preuve hétérogènes et une faible modularité, tandis que la qualité des données d'entraînement pour les prouveurs de théorèmes neuronaux est dégradée par des preuves correctes mais structurellement sous-optimales. Les méthodes existantes d'optimisation automatique des preuves font face à des obstacles significatifs, notamment des objectifs hétérogènes et définis de manière heuristique, une pénurie de données d'optimisation de haute qualité, et des coûts prohibitifs d'entraînement et d'inférence pour les modèles à grande échelle. De plus, les travaux antérieurs s'appuyaient souvent sur des modèles propriétaires à usage général ou se concentraient étroitement sur le nombre de jetons, échouant à traiter des métriques structurelles plus larges comme la modularité et la gestion des dépendances.

Méthodologie

Les auteurs présentent ImProver 2, un cadre neurosymbolique conçu pour améliorer itérativement de manière autonome les petits modèles de langage (SLM) pour l'optimisation de preuves dans Lean 4. Le système fonctionne via un pipeline multi-composants :

1. Augmentation Neurosymbolique (Échafaudage)

Pour combler le fossé entre le raisonnement informel et la vérification formelle, le cadre expose le modèle à un contexte riche provenant de l'environnement Lean. Cet « échafaudage » ( $\Psi$ ) comprend :

Tranches de Contexte : Définitions, théorèmes et lemmes pertinents directement référencés par la preuve cible, sérialisés avec des métadonnées.
Chaîne d'États (CoS) : Traces explicites des états d'objectif avant et après chaque étape de tactique, entrelacées sous forme de commentaires pour révéler le flux logique de la preuve.
Auto-informalisation : Résumés en langage naturel des étapes de preuve, générés en traduisant la preuve formelle en une séquence de descriptions de haut niveau.

2. Métriques d'Optimisation

Le système vise trois objectifs structurels distincts, définis comme des fonctions calculables $\mu$ :

Longueur : Minimiser le nombre de tactiques utilisées (« golfing » de preuve).
Dépendances : Minimiser le nombre de lemmes externes uniques explicitement nommés dans la preuve, encourageant des preuves autonomes.
Modularité : Maximiser le nombre de « objectifs générés effectifs » (sous-preuves indépendantes introduites via have, calc, etc.), ce qui sert de proxy pour la décomposition de la preuve et sa maintenabilité.

3. Pipeline d'Optimisation Préférentielle Itérative (IRPO)

ImProver 2 emploie une boucle d'entraînement itérative pour amorcer les SLM :

Génération : Le modèle actuel $G_t$ génère $n$ réécritures candidates pour chaque théorème de l'ensemble d'entraînement, en utilisant l'échafaudage neurosymbolique.
Filtrage et Rejeu : Les candidats sont notés en fonction de leur correction (vérification par le noyau Lean) et de l'amélioration des métriques. Un tampon de rejeu est utilisé pour équilibrer les données nouvellement générées avec les données historiques, empêchant l'effondrement du modèle et assurant une amélioration monotone. Les problèmes triviaux ou de faible qualité sont filtrés.
Construction de Paires Préférentielles : L'ensemble de données est partitionné en « gagnants » (preuves compilantes à forte amélioration) et « perdants » (échecs ou preuves à faible amélioration). Deux types de paires préférentielles sont formés : gagnant–gagnant (ordonnées par l'ampleur de l'amélioration) et gagnant–perdant.
Entraînement : Le modèle est mis à jour en utilisant l'Optimisation Préférentielle de Raisonnement Itératif (IRPO), qui combine une perte d'Optimisation Préférentielle Directe (DPO) avec une perte de vraisemblance négative (NLL) sur les preuves gagnantes. Ce processus se répète jusqu'à convergence ou épuisement du budget.

Contributions Clés

SLM Auto-améliorants pour le Refactoring : L'article démontre que l'optimisation préférentielle itérative peut efficacement amorcer de petits modèles de langage (spécifiquement un modèle de 7 milliards de paramètres) pour optimiser des preuves dans des bibliothèques de recherche spécialisées, les rendant compétitifs face à des modèles nettement plus grands.
Métriques d'Optimisation Structurelle : Au-delà de la simple réduction de longueur, les auteurs introduisent et évaluent les métriques de modularité et de dépendance. Ces métriques exploitent la structure de la preuve et le contexte de la bibliothèque pour cibler des objectifs de refactoring distincts pertinents pour la maintenabilité de la bibliothèque.
Augmentation Neurosymbolique : Le cadre extrait et intègre les traces d'états d'objectif, le contexte pertinent et les auto-informalisations. Les auteurs montrent que cette augmentation améliore considérablement les performances des petits modèles et des modèles de pointe, facilitant la découverte de réécritures valides et à haute valeur.

Résultats Expérimentaux

Le système a été évalué sur miniCTX-v2, un benchmark de mathématiques de niveau recherche écrites par des humains, en utilisant un modèle de base de 7 milliards de paramètres (DeepSeek-R1-Distill-Qwen-7B).

Performance vs Échelle : ImProver 2 surpasse le modèle DeepSeek-R1 671B, beaucoup plus grand, sur les trois métriques (Longueur, Modularité, Dépendance) lorsqu'il n'est pas échafaudé. Par exemple, pour la modularité, ImProver 2 a atteint une amélioration moyenne de 0,143 contre 0,055 pour le modèle 671B.
Comparaison avec les Modèles de Pointe : Le modèle ImProver 2 de 7B est compétitif avec des modèles de pointe de milieu de gamme (par exemple, GPT-5-mini) sur les métriques de longueur et de dépendance. Il devance tous les systèmes non échafaudés évalués sur la modularité.
Impact de l'Échafaudage : L'ajout de l'échafaudage neurosymbolique améliore considérablement les performances dans toutes les familles de modèles. Par exemple, le score d'amélioration de la longueur du modèle 7B est passé de 0,118 (base) à 0,236 (échafaudé). Même de grands modèles comme GPT-5-high ont enregistré des gains substantiels (de 0,660 à 0,875) avec l'échafaudage.
Dynamique d'Itération : La plupart des gains de performance se produisent au cours des 2 à 3 premières itérations IRPO. Le système montre que les petits modèles peuvent apprendre à restructurer efficacement des preuves de niveau recherche, bien que les performances finissent par stagner à mesure que le modèle absorbe les motifs de refactoring courants.
Compromis de Précision : L'article note un compromis entre l'optimisation et la précision de compilation. Bien que les preuves optimisées offrent souvent des améliorations de métriques plus élevées, elles peuvent avoir des taux de compilation légèrement inférieurs à ceux des réécritures conservatrices, reflétant la nature plus risquée des transformations structurelles.

Importance et Revendications

L'article postule que l'optimisation des preuves n'est pas uniquement une fonction de l'échelle du modèle, mais est significativement pilotée par la spécialisation spécifique à la tâche et l'auto-amélioration itérative. En combinant un pipeline d'optimisation préférentielle avec tampon de rejeu et un échafaudage neurosymbolique, ImProver 2 établit que de petits modèles accessibles peuvent efficacement restructurer des preuves complexes de niveau recherche.

Les auteurs affirment que leur travail établit l'optimisation des preuves comme une tâche évolutive et apprenable. Ils soutiennent que leur approche répond au besoin critique de maintenir les bibliothèques formelles et d'améliorer la qualité des données d'entraînement pour les prouveurs futurs, offrant une voie pour automatiser le refactoring des preuves pour la maintenabilité sans dépendre exclusivement de modèles de pointe massifs et coûteux. Le travail met en évidence que, avec un échafaudage et un entraînement appropriés, les petits modèles peuvent égaler ou dépasser les performances de systèmes nettement plus grands sur des objectifs structurels spécifiques.