Twitch: Learning Abstractions for Equational Theorem Proving

Ce papier présente Twitch, un outil qui découvre automatiquement des abstractions (modèles de termes récurrents) à partir d'échecs de preuve ou de théorèmes réussis pour guider le prouveur de théorèmes équationnels Twee, permettant ainsi de résoudre de nouveaux problèmes et d'accélérer significativement les preuves.

L'essentiel

🧠 Twitch : L'art d'apprendre à un robot à "voir" les motifs cachés

Imaginez que vous essayez de résoudre un immense labyrinthe de mathématiques. Vous êtes un détective (le logiciel de preuve automatique) qui doit trouver le chemin vers la sortie (la preuve d'un théorème). Le problème ? Le labyrinthe contient des milliards de couloirs. Si vous essayez de tout explorer, vous allez passer des siècles à chercher, et vous n'arriverez jamais à la sortie.

C'est là qu'intervient Twitch, un nouvel outil créé par des chercheurs suédois. Son but est d'apprendre au détective à repérer les indices importants sans avoir besoin d'un humain pour lui dire quoi chercher.

1. Le Problème : Trop d'informations, pas assez de temps

Les logiciels de preuve mathématique (comme celui appelé Twee) fonctionnent en générant des millions de petites étapes logiques. La plupart de ces étapes sont inutiles, comme essayer de toutes les clés d'un trousseau pour ouvrir une porte.
Habituellement, le logiciel choisit les étapes les plus courtes. Mais parfois, les étapes les plus courtes ne mènent nulle part, et la solution se cache dans un motif complexe et répétitif que le logiciel ne remarque pas.

2. La Solution : Apprendre à "résumer" (L'Abstraction)

C'est ici que l'idée de Twitch devient brillante. Imaginez que vous écrivez un roman très long. Si vous voyez le mot "le grand château de pierre" répété 500 fois, vous pourriez décider de l'appeler simplement "le Château" pour alléger votre texte.

Twitch fait la même chose avec les mathématiques :

1. Il regarde des preuves réussies (ou des tentatives échouées) dans un domaine donné.
2. Il repère les formes de phrases mathématiques qui reviennent tout le temps (comme "le Château").
3. Il crée une abstraction : une sorte de raccourci ou de "sticker" qui remplace ces formes complexes par un symbole simple.

L'analogie du Lego :
Imaginez que vous construisez une maison en Lego. Au lieu de dire "prends une brique rouge, puis une bleue, puis une rouge...", vous créez un bloc préfabriqué que vous appelez "Mur".
Twitch apprend à créer ces blocs "Mur" automatiquement en regardant comment d'autres maisons ont été construites.

3. Les Deux Manières d'Apprendre

Twitch a deux méthodes pour trouver ces indices, comme un étudiant qui révise :

• Méthode 1 : L'analyse de l'échec (Preuve partielle)
  Le logiciel essaie de résoudre un problème difficile, échoue, mais laisse derrière lui un tas de notes (des étapes intermédiaires). Twitch analyse ces notes pour trouver des motifs récurrents dans les erreurs. C'est comme si, après avoir raté un examen, vous regardiez vos brouillons pour voir quels types de questions vous avez toujours manqués, et vous apprenez à les reconnaître.

• Méthode 2 : L'apprentissage par l'exemple (Domaine)
  Le logiciel regarde des problèmes plus faciles qu'il a déjà résolus dans le même domaine (par exemple, la théorie des groupes ou les treillis). Il dit : "Tiens, dans tous ces problèmes faciles, on utilise souvent cette forme bizarre. Peut-être que cette forme sera utile pour le problème difficile que je dois résoudre maintenant ?" C'est un peu comme un chef cuisinier qui, après avoir fait 100 sauces tomate simples, crée une "sauce tomate de base" qu'il utilise pour accélérer la préparation de plats complexes.

4. Comment ça marche dans la pratique ?

Les chercheurs ont utilisé un outil appelé Stitch (comme une aiguille à coudre) pour trouver ces motifs. Stitch regarde des tas de termes mathématiques et dit : "Si on remplace cette partie par un nouveau nom, on gagne beaucoup de temps d'écriture."

Une fois que Twitch a trouvé ces raccourcis, il les donne au logiciel de preuve (Twee). Au lieu de dire "cherche tout", le logiciel dit : "Ah, je vois ce motif 'Mur' ! C'est important, je vais le privilégier !"
Résultat :

• Le logiciel trouve des preuves qu'il ne pouvait pas résoudre avant.
• Il est beaucoup plus rapide (parfois 10 fois plus rapide !).

5. Pourquoi c'est génial ?

Avant, il fallait qu'un humain expert dise : "Hé, attention, dans ce type de problème, il faut toujours chercher la forme X". C'était lent et fastidieux.
Avec Twitch, le logiciel devient son propre professeur. Il apprend tout seul à reconnaître les structures importantes, comme un enfant qui apprend à reconnaître les visages de sa famille parmi une foule.

En résumé :
Twitch est un outil qui apprend aux ordinateurs à résumer les mathématiques. En trouvant des motifs récurrents et en les transformant en raccourcis, il aide les robots à traverser le labyrinthe des preuves mathématiques beaucoup plus vite et à résoudre des énigmes qui étaient auparavant trop difficiles. C'est une victoire de l'intelligence artificielle appliquée à la logique pure, rendue possible par une idée simple : parfois, pour avancer vite, il faut savoir ce qu'on peut ignorer et ce qu'il faut garder.

Résumé technique

1. Problématique

Les prouveurs de théorèmes automatisés basés sur la saturation (comme Twee, un prouveur équationnel) doivent naviguer dans un espace de recherche immense. Pour un problème donné, le prouveur peut générer des centaines de millions de paires critiques (inférences potentielles), mais ne peut en sélectionner qu'un petit nombre pour former la preuve finale.

Le défi principal réside dans l'identification rapide des inférences « intéressantes ». Les heuristiques actuelles de Twee reposent principalement sur la taille des termes (poids), ce qui est une métrique simple mais souvent insuffisante pour des problèmes complexes. Bien que des stratégies humaines (comme la stratégie de pondération ou de résonance) puissent guider le prouveur en spécifiant des formes de termes préférées, cela nécessite une intervention manuelle. L'objectif de ce papier est de découvrir automatiquement ces formes de termes intéressantes (appelées abstractions) à partir des preuves existantes ou des tentatives de preuve échouées, afin de guider la recherche sans intervention humaine.

2. Méthodologie

L'approche proposée, nommée Twitch, repose sur l'apprentissage d'abstractions en utilisant un outil existant appelé Stitch (initialement conçu pour l'apprentissage de bibliothèques de fonctions en synthèse de programmes).

A. Le concept d'Abstraction

Une abstraction est définie comme un motif de terme qui apparaît fréquemment dans des preuves pertinentes. L'idée est de compresser les termes en introduisant de nouvelles définitions de fonctions (par exemple, remplacer $f(x, x)$ par $g(x)$).

• Outil Stitch : Il prend un ensemble de termes (issus d'une preuve) et cherche un ensemble de définitions de fonctions qui maximise la compression (réduction de la taille totale des termes).
• Intégration dans Twee : Au lieu d'ajouter ces définitions comme de nouveaux axiomes (ce qui élargirait l'espace de recherche et pourrait ralentir le prouveur), Twitch modifie la fonction heuristique de Twee. Lorsqu'une paire critique correspond à une abstraction apprise, son poids (coût) est réduit, augmentant ainsi sa probabilité d'être sélectionnée pour la preuve.

B. Deux modes de génération d'abstractions

Twitch opère selon deux stratégies distinctes :

1. Abstractions de preuves partielles (Partial Proof Abstractions) :

   • Scénario : Utilisé lorsqu'aucun problème similaire n'est disponible.
   • Processus : Twee tente de prouver un problème difficile ($P_h$) pendant un temps limité. S'il échoue, il a généré un ensemble de règles de réécriture et de lemmes intermédiaires.
   • Sélection : Les lemmes sont classés selon une métrique d'« intérêt » ($s$) basée sur le rapport entre la complexité de la preuve du lemme et la simplicité de l'énoncé du lemme ($s = |T| / |lemme|^2$).
   • Extraction : Les $k$ meilleurs lemmes sont extraits, et Stitch est exécuté sur leurs termes pour trouver des motifs récurrents.

2. Abstractions de domaine (Domain Abstractions) :

   • Scénario : Utilisé lorsqu'un corpus de problèmes d'un même domaine (ex: théorie des groupes, algèbre de Boole) est disponible, dont certains sont déjà résolus (« faciles »).
   • Processus (Apprentissage par curriculum) :
     1. Stitch génère des abstractions locales pour chaque problème facile résolu.
     2. Ces abstractions sont testées pour vérifier si elles accélèrent la résolution du problème d'origine (métrique de vitesse).
     3. Les abstractions « bonnes » sont agrégées et compressées une seconde fois par Stitch pour découvrir des abstractions de domaine communes et de haut niveau.
   • Application : Ces abstractions de domaine sont ensuite appliquées aux problèmes difficiles du même domaine.

3. Contributions Clés

1. Méthode automatique de génération d'abstractions : Une approche novatrice pour extraire des motifs de termes récurrents à partir de preuves échouées ou de corpus de preuves réussies, sans intervention humaine.
2. Intégration native dans Twee : Extension du prouveur Twee pour supporter nativement les abstractions via une modification de l'heuristique de pondération, évitant ainsi l'explosion de l'espace de recherche liée à l'ajout d'axiomes.
3. Validation empirique : Une évaluation rigoureuse sur un ensemble de problèmes d'égalité unitaire (UEQ) du TPTP (Théorèmes de Problèmes de Théorie des Preuves), démontrant des gains de performance significatifs.

4. Résultats Expérimentaux

Les expériences ont été menées sur 1041 problèmes UEQ du TPTP v9.2.1.

• Résolution de problèmes difficiles : Twitch a permis de prouver 18 problèmes « difficiles » (note TPTP $\ge$ 0.9, c'est-à-dire que 90% des prouveurs échouent) qui étaient insolubles pour Twee seul dans la limite de temps.
  • 11 problèmes résolus via des abstractions de preuves partielles.
  • 18 problèmes résolus via des abstractions de domaine (incluant tous ceux résolus par la méthode précédente).
  • Exemple notable : Le problème LAT075-1 (note 1.00) concernant l'axiomatisation de l'opérateur NAND (stroke de Sheffer) a été résolu en 32 secondes grâce à des abstractions comme $f(x, x)$ (négation) et $f(f(x, y), f(x, y))$ (conjonction).
• Amélioration des temps d'exécution :
  • L'utilisation d'abstractions de domaine combinée à la stratégie de « flattening » (aplatissement) des objectifs a permis de résoudre environ 25 problèmes supplémentaires dans la limite de 300 secondes par rapport à la version de base.
  • Pour les problèmes déjà résolus par Twee, l'ajout d'abstractions a réduit le temps d'exécution de moitié en moyenne.
• Comparaison avec les axiomes : L'approche par abstractions (modification de l'heuristique) s'est révélée plus robuste que l'ajout de définitions comme axiomes. L'ajout d'axiomes tend à augmenter l'espace de recherche et provoque plus de dépassements de temps (timeouts) lorsque le nombre d'abstractions augmente, tandis que l'approche par abstractions maintient des performances stables.

5. Signification et Impact

Ce travail démontre que l'apprentissage automatique de structures syntaxiques (abstractions) à partir de preuves existantes est une stratégie prometteuse pour l'inférence automatique.

• Efficacité : Cela permet de transformer des problèmes autrefois insolubles en problèmes résolubles en quelques secondes.
• Interprétabilité : Contrairement aux modèles de boîte noire (comme les réseaux de neurones pour la sélection de clauses), les abstractions sont des motifs de termes explicites et compréhensibles par les humains. Elles peuvent correspondre à des constructions algébriques significatives (comme la négation ou la conjonction dans le cas de l'opérateur NAND).
• Futur : Bien que le système soit encore simple (heuristiques basiques pour le scoring des lemmes, gestion fragile des réécritures qui peuvent détruire les abstractions), il ouvre la voie à une recherche plus poussée sur l'extraction automatique de connaissances structurelles pour guider les prouveurs de théorèmes.

En résumé, Twitch réussit à automatiser le rôle d'un expert humain qui identifierait les motifs clés d'une preuve, permettant ainsi au prouveur de se concentrer sur les inférences les plus pertinentes et de résoudre des problèmes complexes beaucoup plus rapidement.