🤖 machine learning

SMT-Based Active Learning of Weighted Automata

Cet article présente un algorithme d'apprentissage actif paramétré et basé sur SMT pour les automates pondérés non déterministes, qui garantit des résultats minimaux, assure la terminaison pour les semi-anneaux finis et démontre une efficacité et une compacité supérieures aux méthodes existantes dans le cadre d'expériences extensives.

Auteurs originaux : Tiago Ferreira, Kevin Batz, Alexandra Silva

Publié 2026-05-11

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Tiago Ferreira, Kevin Batz, Alexandra Silva

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 essayez d'enseigner à un robot comment naviguer dans un labyrinthe, mais que vous ne connaissez pas sa disposition. Vous pouvez poser au robot deux types de questions :

"Que se passe-t-il si je prends ce chemin ?" (Le robot vous indique le résultat, par exemple : "Je reste coincé" ou "Je trouve un trésor valant 5 pièces d'or.")
"La carte que vous avez dessinée est-elle correcte ?" (Le robot compare votre carte au vrai labyrinthe et répond "Oui" ou "Non, vous avez manqué un tournant ici.")

C'est l'idée centrale de l'Apprentissage Actif : un algorithme qui apprend un modèle en posant des questions intelligentes à un "Enseignant" (le système réel).

Pendant longtemps, ces algorithmes d'apprentissage ont très bien fonctionné pour des labyrinthes simples de type "Oui/Non" (comme : cette porte est-elle ouverte ou fermée ?). Mais les systèmes du monde réel sont souvent plus complexes. Ils impliquent des poids : des coûts, des probabilités ou du temps. Par exemple : "Quel est le chemin le moins cher pour atteindre la sortie ?" ou "Quelle est la probabilité de se crasher ?"

Cet article présente une nouvelle méthode puissante pour enseigner aux ordinateurs à apprendre ces Automates Pondérés (des labyrinthes avec des nombres attachés aux chemins).

L'Ancienne Méthode : La Méthode du "Tableau"

Auparavant, les chercheurs utilisaient une méthode basée sur d'énormes tableaux (appelés matrices de Hankel). Imaginez essayer de résoudre un puzzle en remplissant une immense feuille de calcul où chaque cellule dépend de règles algébriques complexes.

Le Problème : Cette méthode de feuille de calcul devient très désordonnée et difficile à résoudre lorsque les nombres ne sont pas de simples entiers. Elle échoue souvent à trouver la carte la plus simple possible, ou elle reste bloquée en essayant de prouver qu'elle peut terminer le travail. C'est comme essayer de résoudre un cube Rubik en notant chaque mouvement possible sur un papier ; cela fonctionne pour les petits cubes, mais devient impossible pour les grands.

La Nouvelle Méthode : La Méthode "SMT"

Les auteurs proposent une approche différente : la Résolution de Contraintes. Au lieu de remplir une feuille de calcul, ils transforment le problème d'apprentissage en un immense puzzle logique.

L'Analogie : Le Détective et le Résolveur SMT
Imaginez que vous êtes un détective essayant de reconstituer une scène de crime (le labyrinthe) à partir des déclarations de témoins (les réponses de l'Enseignant).

L'Hypothèse : Vous devinez un suspect et une chronologie (une petite carte avec quelques états).
Les Contraintes : Vous rédigez une liste de règles : "Si le suspect était à la banque, il a dû partir avant 17 h", ou "L'argent total volé doit être égal à 100 $".
Le Résolveur SMT : C'est un programme informatique ultra-intelligent (comme un moteur logique) qui vérifie si vos règles ont du sens. Il demande : "Existe-t-il une façon d'organiser les mouvements du suspect pour que toutes ces règles soient vraies ?"
- Si Oui : Le résolveur vous fournit une carte valide.
- Si Non : Il vous indique que votre carte est impossible.

L'algorithme de l'article fonctionne ainsi :

Il commence avec une carte minuscule et simple.
Il demande à l'Enseignant des réponses pour des chemins spécifiques.
Il alimente ces réponses dans le Résolveur SMT sous forme d'un ensemble de règles mathématiques.
Le Résolveur tente de trouver une carte qui respecte toutes les règles.
Si l'Enseignant dit : "Non, cette carte est fausse car elle échoue sur ce chemin spécifique", l'algorithme ajoute ce chemin aux règles et demande au Résolveur de réessayer.

Pourquoi est-ce mieux ?

L'article revendique trois avantages principaux, expliqués simplement :

1. Il trouve toujours la carte la plus petite (Minimalité)
Les anciennes méthodes vous donnaient parfois une carte avec 10 pièces alors qu'une carte de 3 pièces aurait suffi. La nouvelle méthode SMT est conçue pour trouver la plus petite carte possible qui respecte les règles. C'est comme trouver l'itinéraire le plus efficace plutôt que simplement un itinéraire.

2. Il fonctionne avec des mathématiques "bizarres"
Les anciennes méthodes peinaient avec des systèmes numériques complexes (comme les mathématiques "Tropicales", où l'on additionne des nombres mais on prend le minimum, ou les mathématiques "Goulot d'étranglement"). La nouvelle méthode peut gérer ces systèmes mathématiques "bizarres" en les traduisant en puzzles logiques que le résolveur informatique comprend. C'est comme avoir un traducteur universel capable de transformer des mathématiques complexes en simples questions "Vrai/Faux".

3. Il est plus rapide et nécessite moins de questions
Dans leurs expériences, la nouvelle méthode a appris des cartes complexes beaucoup plus rapidement que l'ancienne méthode de "tableau". Elle a également eu besoin de poser moins de questions à l'Enseignant pour obtenir la bonne réponse.

La Référence "Naïve" : Ils ont comparé leur méthode à une version "bête" qui devine simplement au hasard. La nouvelle méthode était largement supérieure.
Le Concurrent "État de l'Art" : Ils l'ont comparée à la meilleure méthode existante. La nouvelle méthode a produit des cartes significativement plus petites (parfois 10 fois plus petites !) et a tout de même terminé dans un délai raisonnable.

L'Ingrédient "Magique" : Les Résolveurs SMT

Le secret réside dans la Résolution SMT (Satisfiability Modulo Theories). Imaginez un résolveur SMT comme un vérificateur logique surpuissant. Il ne vérifie pas seulement si une phrase est vraie ; il vérifie si un ensemble complexe de règles mathématiques peut être vrai simultanément.

Les auteurs ont prouvé que pour de nombreux types de systèmes mathématiques (y compris les systèmes finis et certains infinis), ce puzzle logique est résoluble.
Ils ont montré que si le système mathématique est fini (comme un ensemble limité de nombres), l'algorithme est garanti de se terminer.

Résumé

L'article présente une nouvelle façon d'enseigner aux ordinateurs de comprendre des systèmes complexes et pondérés. Au lieu d'utiliser d'anciennes et lourdes méthodes de feuilles de calcul, ils ont transformé le problème en un puzzle logique qu'un résolveur informatique moderne peut résoudre.

Résultat : Il trouve le modèle le plus simple possible.
Résultat : Il fonctionne sur une plus grande variété de systèmes mathématiques qu'auparavant.
Résultat : Il est plus rapide et pose moins de questions que les méthodes précédentes.

Les auteurs ont testé cela sur des milliers d'exemples et l'ont trouvé robuste et pratique pour l'apprentissage de ces systèmes complexes, offrant une alternative solide aux méthodes utilisées au cours de la dernière décennie.

Résumé Technique : Apprentissage Actif d'Automates Pondérés Basé sur la Satisfiabilité Modulo Théories (SMT)

Énoncé du Problème

L'apprentissage actif d'automates, initié par l'algorithme $L^\star$ d'Angluin, est devenu une technique standard pour inférer des modèles de composants inconnus dans la vérification formelle. Bien que les méthodes de type $L^\star$ soient bien établies pour les automates booléens (déterministes et non déterministes), leur extension aux Automates Finis Pondérés (AFP) s'est révélée nettement plus difficile. Les AFP généralisent les automates booléens en attribuant des poids issus d'un semi-anneau aux transitions, permettant ainsi de modéliser des propriétés quantitatives telles que le coût, la probabilité et la consommation de ressources.

Les approches existantes pour l'apprentissage d'AFP reposent sur des généralisations de la matrice de Hankel ou de la table d'observation (par exemple, $WL^\star$ ). Ces méthodes nécessitent de raisonner sur la structure algébrique du semi-anneau sous-jacent. Par conséquent, prouver la terminaison et la minimalité est subtil et souvent restreint à des classes algébriques spécifiques (par exemple, les corps, les domaines à idéaux principaux). Pour de nombreux semi-anneaux pertinents en pratique, tels que le semi-anneau Tropical ou le semi-anneau du Goulot d'Étranglement, les garanties de terminaison sont soit inconnues, soit ne garantissent pas des automates minimaux. De plus, les algorithmes existants produisent souvent des modèles non minimaux ou échouent à évoluer efficacement sur des semi-anneaux infinis.

Méthodologie

Les auteurs proposent un nouvel algorithme d'apprentissage actif basé sur les contraintes qui reformule le problème d'apprentissage directement comme un problème de satisfiabilité résoluble par des solveurs SMT (Satisfiability Modulo Theories).

Approche Principale

Au lieu d'affiner une table d'observation, l'algorithme construit incrémentalement un système d'équations sur le semi-anneau donné $S$ . Les solutions de ce système correspondent exactement aux AFP non déterministes qui sont en accord avec le « professeur » (le langage cible) sur toutes les requêtes observées.

Le processus d'apprentissage suit une boucle d'apprentissage actif standard (Algorithme 1) :

Génération d'Hypothèse : L'algorithme tente de trouver un AFP à $n$ états qui est cohérent avec l'ensemble d'observation actuel $O$ . Cela est délégué à une sous-routine getAutomaton.
Requête d'Équivalence : Si une hypothèse cohérente $H$ est trouvée, le professeur est interrogé pour vérifier si $H$ reconnaît le langage cible $L$ .
Traitement des Contre-exemples : Si le professeur fournit un contre-exemple $w$ (où $H(w) \neq L(w)$ ), $w$ est ajouté à $O$ , et la boucle se répète avec des contraintes renforcées.

La Sous-routine `getAutomaton`

L'article présente deux implémentations pour getAutomaton :

Base Naïve : Encode directement la sémantique de l'AFP. Elle traite les poids initiaux, les matrices de transition et les poids finaux comme des variables inconnues et résout l'équation $sortie(w) = \text{sémantique}(w)$ pour tout $w \in O$ .
Optimisée (SWAL) : Utilise une perspective coalgébrique et le concept de langages d'état. Au lieu de résoudre directement pour le langage global, elle introduit des variables intermédiaires représentant le langage accepté depuis chaque état. Cela aboutit à un système d'équations où :
- Les contraintes de stabilisation assurent que les langages d'état sont cohérents avec les poids de transition.
- Les contraintes d'extension assurent que les poids initiaux combinent correctement les langages d'état pour correspondre à la sortie cible.
- Idée Clé : Bien que ce codage introduise plus de variables et d'équations, il expose les sous-structures partagées (suffixes) entre les observations. Cela permet aux solveurs SMT de réutiliser les résultats intermédiaires, améliorant considérablement l'évolutivité par rapport à l'approche naïve.

Décidabilité et Semi-anneaux

L'algorithme est paramétré par le semi-anneau. Les auteurs identifient que pour les semi-anneaux décidables (où la satisfiabilité des systèmes d'équations finis est décidable), la sous-routine getAutomaton peut être implémentée de manière sûre et complète.

Semi-anneaux Finis : Décidables trivialement par force brute ou SMT.
Semi-anneaux Infinis : L'article fournit des codages pour le semi-anneau Tropical ( $\min, +$ ), les semi-anneaux Tropical Bornés, et le semi-anneau du Goulot d'Étranglement ( $\max, \min$ ) vers des théories décidables telles que l'Arithmétique Linéaire Entière Sans Quantificateurs (QF-LIA) et les Vecteurs de Bits Sans Quantificateurs (QF-BV).

Contributions Clés

Nouvel Algorithme : Un nouvel algorithme d'apprentissage actif basé sur SMT pour les AFP non déterministes, paramétré par le semi-anneau.
Garantie de Minimalité : Contrairement aux méthodes de type $L^\star$ qui manquent souvent de garanties de minimalité en dehors de structures algébriques spécifiques, cet algorithme est garanti pour produire des AFP minimaux à la terminaison, quel que soit le semi-anneau.
Conditions de Terminaison : Les auteurs prouvent la correction partielle et fournissent des conditions suffisantes pour la terminaison. Plus précisément, ils prouvent que l'algorithme termine pour tous les semi-anneaux finis. Pour les semi-anneaux infinis, bien que la terminaison ne soit pas théoriquement garantie par les mêmes arguments de cardinalité, l'implémentation démontre un succès pratique.
Synthèse Basée sur les Contraintes : L'article introduit le premier algorithme de génération basé sur les contraintes pour les AFP, permettant une synthèse basée sur SMT. Il identifie des semi-anneaux spécifiques où les systèmes de contraintes résultants sont décidables.
Évaluation Expérimentale : Une évaluation complète comparant la méthode proposée (SWAL) à une base naïve et à l'algorithme $WL^\star$ de l'état de l'art.

Résultats Expérimentaux

Les auteurs ont implémenté l'algorithme (SWAL) en OCaml en utilisant le solveur Z3 et l'ont évalué sur plus de 5 000 benchmarks générés aléatoirement couvrant les semi-anneaux booléens, Tropical, Tropical Borné et du Goulot d'Étranglement.

vs. Base Naïve : SWAL surpasse nettement le codage naïf tant en temps d'exécution qu'en évolutivité. Alors que l'approche naïve peine à apprendre des automates de plus de 2 à 6 états (selon le semi-anneau), SWAL apprend avec succès des automates minimaux jusqu'à 8 états. Le codage optimisé (langages d'état) réduit le nombre de dépassements de temps/out-of-memory de plusieurs ordres de grandeur.
vs. $WL^\star$ : Comparé à $WL^\star$ $W L^{⋆}$ (un algorithme de l'état de l'art pour les domaines à idéaux principaux) :
- Minimalité : SWAL produit systématiquement des automates minimaux, tandis que $WL^\star$ produit souvent des automates jusqu'à 10 fois plus grands.
- Efficacité : SWAL nécessite moins de requêtes de sortie (interactions avec le professeur) que $WL^\star$ .
- Temps d'Exécution : SWAL est compétitif en termes de temps d'exécution, terminant souvent plus rapidement et avec moins d'échecs de ressources (dépassement de temps/out-of-memory) que $WL^\star$ .
Incrémentalité : L'activation de la résolution incrémentale SMT réduit drastiquement le temps d'apprentissage et l'utilisation des ressources, confirmant la pertinence de l'approche basée sur les contraintes pour l'apprentissage incrémental.

Importance et Revendications

L'article positionne l'apprentissage basé sur les contraintes comme une alternative pratique et robuste aux méthodes traditionnelles de type Hankel/ $L^\star$ pour les automates pondérés, en particulier dans des contextes orientés vérification.

Robustesse : L'approche gère une gamme plus large de semi-anneaux (y compris des infinis comme le Tropical) où les preuves de terminaison algébrique pour les méthodes de type $L^\star$ sont difficiles ou inexistantes.
Minimalité : La garantie de minimalité est un avantage crucial, car les modèles minimaux sont essentiels pour une vérification et une abstraction efficaces.
Évolutivité : Les résultats expérimentaux démontrent que la synthèse basée sur SMT peut évoluer pour apprendre des automates pondérés complexes et minimaux qui sont actuellement hors de portée des algorithmes existants.

Les auteurs concluent que, bien qu'ils ne fournissent pas de preuve de terminaison générale pour tous les semi-anneaux infinis (un problème ouvert connu), leur méthode offre une solution pratique qui apprend avec succès des AFP minimaux dans des scénarios où les méthodes précédentes échouent ou produisent des modèles sous-optimaux. Les travaux futurs incluent l'exploration de mises à jour d'hypothèses plus incrémentales et l'extension de l'approche aux automates probabilistes.