Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications

Cet article présente une nouvelle méthode qui étend l'extraction de spécifications à partir de traces d'exécution au-delà des abstractions booléennes en combinant la synthèse guidée par la syntaxe et la logique temporelle TSL$_f$ pour apprendre des transformations de données et des spécifications temporelles, permettant ainsi de générer des programmes réactifs plus robustes et nettement plus efficaces en échantillons que les approches d'apprentissage passif.

L'essentiel

Imaginez que vous essayez d'enseigner à un robot comment jouer à un jeu vidéo, comme FrozenLake (où un personnage doit glisser sur la glace pour atteindre une destination sans tomber dans un trou).

Habituellement, les chercheurs utilisent deux méthodes principales :

1. L'imitation : On montre au robot des milliers d'exemples de parties gagnées, et il essaie de mémoriser les mouvements (comme un perroquet qui répète des phrases sans comprendre le sens).
2. L'analyse logique : On lui donne des règles écrites à la main, mais c'est long et sujet aux erreurs humaines.

Ce papier propose une troisième voie, beaucoup plus intelligente et efficace. Voici comment cela fonctionne, expliqué simplement :

1. Le problème des "Booléens" (Les étiquettes tout-ou-rien)

Les anciennes méthodes regardent le monde comme une série de lumières qui s'allument ou s'éteignent (vrai/faux, 0/1).

• Analogie : C'est comme si vous décriviez une voiture en disant seulement "La roue est là" ou "La roue n'est pas là". Vous ne savez pas si la roue est ronde, carrée, ou si elle tourne vite.
• La limite : Si le robot apprend que "la roue est à la position X", il panique dès qu'on change la taille du jeu ou la position de la roue. Il ne comprend pas la logique derrière le mouvement.

2. La solution : Apprendre les "Recettes" (Transformations de données)

Les auteurs de ce papier disent : "Arrêtons de regarder seulement les positions. Regardons comment les choses changent."

• L'analogie du chef cuisinier : Au lieu de dire "Le plat est prêt", le robot apprend la recette. Il comprend que "Si je prends un œuf et que je le casse, j'obtiens un jaune et un blanc".
• Comment ils font : Ils utilisent une technique magique appelée SynGuS (Synthèse guidée par la syntaxe). Imaginez un détective qui regarde une série de photos d'un jeu et devine les règles mathématiques cachées.
  • Exemple : Le robot voit que le joueur passe de (0,0) à (0,1). Il ne mémorise pas la position, il déduit la règle : "Pour avancer, j'ajoute 1 à la coordonnée Y".

3. Le langage des règles : TSLf (Le livre de règles temporelles)

Une fois que le robot a trouvé les "recettes" (comment les nombres changent), il doit apprendre les règles du jeu (les spécifications).

• Ils utilisent un nouveau langage appelé TSLf. C'est comme un langage de programmation qui permet de dire : "Tant que tu n'as pas touché le trou, continue de glisser" ou "Tu dois finalement atteindre le but".
• Contrairement aux anciennes méthodes qui disent juste "Évite le trou", cette méthode dit : "Évite n'importe quel trou, peu importe où il est placé". C'est une règle universelle, pas une mémorisation de cas précis.

4. Le résultat : Un robot qui comprend, pas qui mémorise

Ils ont testé leur méthode sur plusieurs jeux (FrozenLake, CliffWalking, Taxi, Blackjack).

• L'efficacité : Là où les autres méthodes avaient besoin de 1000 exemples pour apprendre à jouer correctement, leur robot en avait besoin de moins de 20. C'est comme si un humain apprenait à jouer aux échecs en regardant seulement 20 parties, alors que l'ordinateur en avait besoin de milliers.
• La généralisation : Si vous changez la taille du plateau de jeu ou la position des obstacles, le robot ne panique pas. Parce qu'il a appris la logique (les relations entre les objets) et non pas la position exacte, il s'adapte instantanément.
  • Métaphore : Un élève qui a appris à faire des additions (la règle) peut additionner n'importe quels nombres. Un élève qui a mémorisé la réponse "5+5=10" sera perdu si on lui demande "6+6".

En résumé

Ce papier présente un système qui apprend à comprendre la structure du monde (les transformations de données) et les règles du temps (ce qui doit arriver maintenant ou plus tard) directement à partir de l'observation, sans avoir besoin de milliers d'exemples ni d'intervention humaine pour définir les règles.

C'est un pas géant vers une Intelligence Artificielle symbolique : une IA qui ne se contente pas de deviner des probabilités, mais qui construit un modèle logique du monde, capable de s'adapter à des situations qu'elle n'a jamais vues auparavant.

Résumé technique

Voici un résumé technique détaillé de l'article "Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications" (Au-delà des booléens : Apprentissage des transformations de données et des spécifications temporelles).

1. Problématique

L'extraction de spécifications (specification mining) à partir de traces d'exécution vise à automatiser la découverte de propriétés logiques régissant le comportement d'un système. Cependant, les approches existantes reposent majoritairement sur des logiques temporelles propositionnelles comme LTL (Linear Temporal Logic) ou LTLf (version à préfixe fini).

• Limitation principale : Ces logiques traitent tous les événements comme des atomes booléens. Pour exprimer des propriétés dépendant de l'évolution de variables (ex: "déplacer x vers la case au-dessus de l'obstacle le plus proche"), il faut soit créer manuellement des prédicats (intervention humaine), soit "éclater" les données en bits (bit-blasting), ce qui augmente la taille des formules et introduit des relations sémantiques spuriées.
• Objectif : Développer une méthode capable d'extraire des spécifications temporelles riches qui intègrent nativement les transformations de données et les relations entre variables de types arbitraires (entiers, etc.), sans connaissance préalable du domaine.

2. Méthodologie

L'approche proposée combine la synthèse guidée par la syntaxe (SyGuS) et une nouvelle logique temporelle pour apprendre à la fois les fonctions de transformation et les règles temporelles.

A. Formalisme : TSLf (Temporal Stream Logic finite)

Les auteurs introduisent TSLf, une interprétation à préfixe fini de la Temporal Stream Logic (TSL).

• Séparation Contrôle/Data : Contrairement à LTLf, TSLf permet d'exprimer des propriétés sur des fonctions et des prédicats appliqués à des variables.
• Syntaxe : Les formules utilisent des termes de mise à jour (ex: [x ← f(y)] signifiant que x est mis à jour par la fonction f appliquée à y au prochain pas de temps) et des prédicats.
• Sémantique : Les formules sont interprétées sur des traces finies. Une contrainte de "bien-forme" (well-formedness) impose qu'à chaque pas de temps, une variable ne soit mise à jour qu'une seule fois.

B. Pipeline d'Extraction (Mining Procedure)

L'algorithme fonctionne en trois étapes principales :

1. Découverte de Fonctions (Function Discovery) :

   • À partir de traces brutes, le système doit identifier quelles fonctions expliquent l'évolution des variables.
   • Utilisation de SyGuS (Syntax-Guided Synthesis) via le solveur CVC5.
   • Stratégie "Bottom-Up" : L'algorithme commence par traiter chaque transition de variable comme une contrainte isolée. Il tente ensuite de fusionner (merge) des groupes de contraintes en une seule fonction si une fonction unique peut expliquer les deux ensembles d'exemples entrée-sortie. Une stratégie de "swapping" d'entrées permet d'explorer des hypothèses alternatives si la fusion échoue.
   • Le résultat est un ensemble minimal de fonctions couvrant toutes les transformations observées.

2. Construction de Traces Bien-Formées (Lifting) :

   • Une fois les fonctions découvertes, les traces brutes sont converties en traces TSLf.
   • Pour chaque variable et chaque pas de temps, le système sélectionne l'application de fonction la plus fréquente (ranking) pour déterminer la mise à jour unique, garantissant ainsi la bien-forme de la trace.
   • Les prédicats (ex: égalité, ordre) sont appliqués entre variables de même type à chaque instant.

3. Apprentissage des Spécifications Temporelles :

   • Les traces TSLf (maintenant "booléanisées" via les termes de mise à jour et les prédicats) sont soumises à un mineur de spécifications (extension de l'outil Bolt).
   • Le problème est décomposé en deux parties pour garantir la synthèse de contrôleurs réactifs :
     • Condition de Vivacité (Liveness) : Ce qui doit finalement se produire (ex: atteindre l'objectif).
     • Condition de Sécurité (Safety) : Ce qui doit toujours être vrai (ex: éviter les trous).
   • L'objectif est de trouver la formule la plus petite discriminant les traces positives des négatives.

C. Synthèse de Contrôleurs

Une fois la spécification TSLf extraite (sous la forme $G\phi \land F\psi$), un synthétiseur (Issy) génère un automate fini (transducteur) qui mappe les observations de l'environnement aux actions, créant ainsi un agent réactif.

3. Contributions Clés

1. Algorithme de Synthèse Ascendante : Un algorithme glouton pour découvrir des ensembles de fonctions couvrant des traces complètes, utilisant une stratégie d'échange d'entrées pour éviter les relations spuriées.
2. Framework TSLf : Introduction de TSLf comme sémantique pour l'extraction de spécifications sur des traces finies, permettant de capturer nativement les mises à jour fonctionnelles.
3. Apprentissage Symbolique Réactif : Démonstration que l'on peut synthétiser des contrôleurs réactifs généralisables à partir de spécifications minées, sans apprentissage par gradient (RL classique) ni étiquettes d'actions explicites.

4. Résultats Expérimentaux

L'évaluation a été menée sur la suite d'environnements OpenAI-Gym ToyText (FrozenLake, CliffWalking, Taxi, Blackjack) avec des configurations généralisées (positions d'obstacles, tailles de grilles, etc.).

• Efficacité Échantillonnaire (Sample Efficiency) : La méthode TSLf nécessite un ordre de grandeur de moins d'exemples (souvent $\le 20$ traces) que les méthodes d'apprentissage passif (Imitation Learning, Behavioral Cloning, Arbres de décision) pour atteindre une performance parfaite.
• Généralisation :
  • Sur FrozenLake et CliffWalking, TSLf atteint 100% de réussite sur des configurations jamais vues (changement de taille de grille, positions d'obstacles), là où les baselines (Alergia, Réseaux de Neurones) plafonnent entre 30% et 50%.
  • Les baselines apprennent des mappings état-action locaux (mémorisation), tandis que TSLf apprend des invariants relationnels (ex: "le joueur ne doit jamais être sur une case de trou").
• Robustesse aux Dynamiques Modifiées : Dans un environnement où les règles de mouvement sont modifiées (ex: $x \to 2x+1$), TSLf redécouvre automatiquement les fonctions de transformation et adapte le contrôleur, alors que les baselines échouent.
• Cas du Blackjack : Bien que ce jeu soit stochastique et sans structure temporelle forte, TSLf parvient à extraire des stratégies de sécurité (quand s'arrêter) basées sur des seuils relationnels, surpassant ou égalant les méthodes stochastiques classiques avec très peu de données.
• Comparaison avec Bit-Blasting : La méthode "Bit-Blasting" (LTLf standard) produit des formules syntaxiquement valides mais sémantiquement inutiles (ex: "le bit 1 de x est vrai"), incapables de généraliser.

5. Signification et Impact

Ce travail représente une avancée vers un paradigme d'apprentissage par renforcement purement symbolique.

• Il démontre que l'on peut apprendre des modèles de monde formels (modèles de données + règles temporelles) directement à partir de traces d'exécution, sans supervision forte.
• La capacité à généraliser à des situations hors distribution (OOD) grâce à la découverte de règles relationnelles abstraites plutôt que de politiques locales est cruciale pour le déploiement de systèmes IA robustes.
• L'approche ouvre la voie à des agents qui interagissent avec un environnement, extraient des spécifications formelles de leurs expériences, et s'améliorent itérativement par synthèse formelle, réduisant ainsi la dépendance aux données massives et aux ajustements manuels.