🤖 AI

dtControl2+ $\varepsilon$ : Trading Optimality for Explainability in MDPs via Decision Trees

Cet article introduit dtControl2+ $\varepsilon$ , une extension de l'outil de pointe dtControl2 qui génère des contrôleurs d'arbres de décision nettement plus petits et plus compréhensibles pour l'humain pour les processus de décision markoviens en échangeant une quantité contrôlable d'optimalité ( $\varepsilon$ ) contre une explicabilité accrue.

Auteurs originaux : Tereza Kinská, Jan Křetínský, Tobias Meggendorfer, Sabine Rieder, Maximilian Weininger

Publié 2026-07-29

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Tereza Kinská, Jan Křetínský, Tobias Meggendorfer, Sabine Rieder, Maximilian Weininger

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'apprendre à un robot comment naviguer dans un labyrinthe. Dans le monde de l'informatique, cela s'appelle la « synthèse de contrôleur ». Vous donnez au robot un ensemble de règles et un objectif, et un programme informatique détermine les mouvements parfaits pour y parvenir. Mais voici le hic : pour des labyrinthes complexes, l'ordinateur recrache souvent une liste massive et désordonnée d'instructions — une pour chaque case où le robot pourrait atterrir. C'est comme avoir un livre de cuisine de un million de pages où chaque page dit simplement « tourne à gauche » ou « tourne à droite » pour un instant minuscule et spécifique. Bien que cette liste soit mathématiquement parfaite, elle est impossible à lire pour un humain, et encore moins à comprendre. Si le robot s'écrase, personne ne peut regarder cette liste géante et dire : « Ah, je vois, il a tourné à gauche parce qu'il était confus par le mur rouge. » Nous avons besoin que ces instructions soient courtes, simples et explicables, comme une carte claire plutôt qu'un immense tableur.

C'est là qu'interviennent les « arbres de décision ». Voyez l'arbre de décision comme un organigramme ou une partie de « 20 questions ». Au lieu d'une liste géante, vous avez une structure simple : « Si le mur est à gauche, va à droite ; sinon, va tout droit. » Ces structures sont beaucoup plus faciles à comprendre pour les humains. Cependant, même ces arbres peuvent devenir trop grands et compliqués si le robot fait face à des situations délicates ou à des « cas limites » (corner cases). La grande question que se posent les chercheurs est la suivante : pouvons-nous rendre ces arbres encore plus petits et plus simples sans que le robot ne s'écrase ? La réponse réside dans un concept appelé « l'optimalité epsilon ». Imaginez que vous disiez au robot : « Tu n'as pas besoin d'être 100 % parfait ; tu peux être 99,9 % parfait. » Cette infime part d'imperfection autorisée donne au robot (et à l'ordinateur) la liberté d'ignorer les détails minuscules et improbables, ce qui produit un ensemble d'instructions beaucoup plus court et plus propre, tout en accomplissant la tâche en toute sécurité.

C'est ici que l'outil dtControl 2+ε entre en scène. Les chercheurs, travaillant avec des processus de décision markoviens (une façon mathématique sophistiquée de décrire des systèmes avec du caractère aléatoire, comme un robot qui pourrait glisser sur un sol mouillé), ont conçu un système qui prend un contrôleur complexe et parfait et le réduit en un arbre de décision minuscule et lisible par l'homme. Ils y parviennent en autorisant une petite quantité d'erreur contrôlée (appelée $\epsilon$ ).

Voici comment leur magie opère : au lieu d'essayer d'expliquer chaque mouvement du robot, l'outil examine la carte et demande : « Quels mouvements comptent réellement ? » Si un robot se trouve dans un endroit où il n'ira presque certainement jamais, ou là où n'importe quel mouvement qu'il fera mènera au même résultat, l'outil dit : « Passons cette partie sans l'expliquer. » Il distille le contrôleur pour n'en garder que l'« essence ». Par exemple, dans un test avec un robot sur un versant de colline, le contrôleur parfait comportait des dizaines de règles complexes. Le nouvel outil, en autorisant une erreur infime de seulement 0,001, a réduit les instructions à seulement cinq nœuds (les points de décision dans l'arbre). La règle résultante était magnifiquement simple : « Monte jusqu'au sommet, va à droite jusqu'au bord, puis descends. » Ce n'était pas mathématiquement parfait dans chaque scénario microscopique, mais c'était si proche de la perfection que la différence était négligeable, et c'était quelque chose qu'un humain pouvait comprendre en quelques secondes.

L'équipe a testé son outil par rapport à d'autres méthodes de pointe et a constaté qu'il s'agissait d'une amélioration massive. Dans de nombreux cas, leur outil a produit des arbres de décision plusieurs ordres de grandeur plus petits que la concurrence. En fait, pour près de la moitié des cas de test qu'ils ont exécutés, autoriser une petite erreur de $\epsilon = 10^{-2}$ (0,01) leur a permis de réduire l'intégralité du contrôleur à un seul nœud. Cela signifie que le robot pourrait simplement choisir une action principale et, si cette action n'est pas possible, choisir n'importe quelle autre action disponible au hasard, et il serait toujours presque aussi performant que la stratégie complexe et parfaite. C'est un fait que les outils précédents avaient totalement manqué.

Les chercheurs veillent à préciser qu'ils n'ont pas simplement deviné ; ils ont utilisé un puissant vérificateur de modèles (un outil qui vérifie mathématiquement si un système fonctionne) pour revérifier chaque arbre simplifié. Ils ont prouvé que même avec ces simplifications agressives, la performance du robot ne descend jamais en dessous de la limite de sécurité autorisée. Ils ont également montré que leur outil fonctionne sur divers types d'objectifs, pas seulement pour atteindre une destination, mais aussi pour éviter un danger ou collecter des récompenses.

En résumé, cet article présente une façon d'échanger une infime quantité de perfection mathématique contre un gain énorme de compréhension humaine. En laissant l'ordinateur admettre qu'il n'a pas besoin d'expliquer chaque minuscule détail, les chercheurs ont créé des contrôleurs qui sont non seulement sûrs et efficaces, mais aussi assez petits pour tenir sur une carte postale et assez simples pour qu'un humain puisse les expliquer à un ami. Cela transforme un manuel d'instructions déroutant de un million de pages en un guide clair en trois étapes.

Résumé technique : dtControl2+ε : Optimisation du commerce pour l'explicabilité dans les MDP via les arbres de décision

Énoncé du problème

La synthèse de contrôleurs pour les processus de décision markoviens (MDP) produit souvent des contrôleurs optimaux représentés par de grandes tables état-action non structurées. Bien que ces tables soient mathématiquement précises, elles sont peu pratiques pour une implémentation sur des dispositifs à ressources limitées et manquent d'explicabilité, ce qui entrave la validation et la certification. Des outils existants, tels que dtControl2, tentent de représenter ces contrôleurs sous forme d'arbres de décision (DT) pour améliorer l'interprétabilité. Cependant, pour les systèmes de grande taille ou ceux possédant de nombreux cas limites, même ces DT peuvent devenir trop complexes pour la compréhension humaine.

Une difficulté critique réside dans le fait que la réduction de la taille d'un DT est non triviale ; supprimer une seule décision cruciale peut rendre un contrôleur incorrect. De plus, de nombreuses méthodes de synthèse évolutives ne fournissent que des contrôleurs $\epsilon$ -optimaux (performances à l'intérieur de $\epsilon$ de la valeur optimale), alors que les outils de construction de DT existants visent généralement une représentation exacte ( $\epsilon=0$ ), échouant ainsi à exploiter l'imprécision autorisée pour simplifier l'explication.

Méthodologie

Le présent article présente dtControl2+ε, un outil qui étend l'état de l'art dtControl2 en introduisant une fonctionnalité « $\epsilon$ ». Le flux de travail central s'intègre étroitement avec le vérificateur de modèles probabilistes Storm pour construire des DT plus petits et explicables, tout en garantissant que le contrôleur résultant reste $\epsilon$ -optimal.

La méthodologie se déroule en trois étapes principales :

1. Résolution de modèle et construction de jeu de données

Au lieu de partir d'un contrôleur optimal déterministe, l'outil génère un jeu de données initial qui est permissif (mappage des états vers des ensembles d'actions autorisées) ou combiné (restreignant les actions permissives aux états atteignables).

Stratégies permissives : L'outil identifie les actions qui sont optimales ou qui produisent la même valeur, permettant au DT d'« unifier » les états.
Heuristiques de réduction : Avant l'apprentissage du DT, l'outil identifie et supprime les états où le choix spécifique d'une action n'impacte pas le résultat ou bien où l'erreur introduite est bornée par $\epsilon$ $ϵ$ . Les principales techniques de réduction incluent :
- AllOpt : Suppression des états où toutes les actions disponibles sont optimales.
- Agency : Suppression des états où la différence entre le meilleur et le pire résultat possible est inférieure à $\epsilon$ .
- Dominance : Suppression des états qui sont presque sûrement atteints à partir d'autres états, quel que soit le choix effectué.
- Unreach : Suppression des états inaccessibles depuis l'état initial sous n'importe quel contrôleur cohérent.

2. Apprentissage d'arbre de décision

L'outil emploie une version modifiée de l'algorithme standard de construction de DT basé sur des heuristiques (Algorithme 1) avec plusieurs améliorations :

Extraction de prédicats : Extrait automatiquement les prédicats pertinents de la description de haut niveau du modèle (ex: gardes de transition du langage PRISM), améliorant ainsi l'approche semi-automatique par modèles utilisée par les outils précédents.
Mesures d'impureté : Introduit des pondérations spécifiques au modèle pour les calculs d'impureté. Au lieu d'une pondération uniforme, il utilise :
- Imp_Simulation : Pondère les états par fréquence de visite (avec un seuil de sécurité pour garantir l' $\epsilon$ -optimalité).
- Imp_Agency : Pondère les états par leur agence (potentiel d'erreur).
- Imp_CoE (Coût de l'Erreur) : Pondère les états par l'impact du choix de la pire action dans cet état spécifique.
Heuristiques agressives avec vérification : L'outil utilise l'Arrêt précoce (arrêt des divisions lorsque l'impureté est inférieure à un seuil) et l'Élagage gourmand (effondrement des sous-arbres). Contrairement aux approches « agressives » précédentes qui risquaient la validité, dtControl2+ε utilise Storm pour vérifier l' $\epsilon$ -optimalité de l'arbre résultant après ces étapes. Si la contrainte de précision est violée, l'outil relâche les heuristiques et réessaie.

3. Boucle de vérification

Une caractéristique unique est le couplage étroit avec Storm pour la vérification post-construction. L'outil vérifie la précision du DT généré. Si l'écart par rapport à la valeur optimale dépasse $\epsilon$ , il revient en arrière et réduit l'agressivité des heuristiques (par exemple, en augmentant le seuil d'arrêt ou en désactivant l'élagage), garantissant que l'output final est garanti $\epsilon$ -optimal.

Contributions clés

L'outil dtControl2+ε : Un outil autonome qui étend dtControl2 pour construire des DT plus petits en exploitant l'imprécision autorisée $\epsilon$ .
Heuristiques sûres vs agressives : Un cadre qui sépare clairement les réductions « sûres » (qui préservent l' $\epsilon$ -optimalité par définition) des heuristiques « agressives » (qui sont validées via la vérification de modèles).
Extraction automatique de prédicats : Une méthode pour dériver des prédicats de décision directement des gardes de transition du modèle, éliminant le besoin d'expertise manuelle dans la sélection des prédicats.
Support pour divers objectifs : L'approche couvre les objectifs standards (accessibilité, sûreté, atteindre-éviter, basé sur les récompenses) et, de manière unique, supporte les propriétés de la Logique Temporelle Linéaire (LTL) en gérant des contrôleurs à mémoire.

Résultats

Les auteurs ont évalué dtControl2+ε contre dtControl2, dtPaynt, dtNESt et une réimplémentation de l'approche CAV15 sur 38 benchmarks (incluant des modèles PRISM avec jusqu'à 500 000 états).

Réduction de taille : Même pour une représentation exacte ( $\epsilon=0$ ), dtControl2+ε produit des DT ordres de grandeur plus petits que dtControl2 grâce à de meilleurs jeux de données initiaux et des heuristiques sûres.
Impact de $\epsilon$ : En autorisant $\epsilon = 10^{-2}$ , l'outil a produit des DT à un seul nœud pour près de la moitié des benchmarks, révélant qu'une action unique (avec un repli aléatoire uniforme) est souvent suffisante pour l' $\epsilon$ -optimalité.
Comparaison :
- vs. dtControl2 : dtControl2+ε produit systématiquement des arbres plus petits.
- vs. dtPaynt : dtPaynt a expiré sur la plupart des benchmarks et a produit des arbres plus grands là où il a réussi.
- vs. dtNESt : dtNESt est un concurrent sérieux pour $\epsilon=0$ , mais dtControl2+ε produit des arbres au plus deux fois plus petits que dtNESt dans 23 des 38 benchmarks, et un ordre de grandeur plus petits dans 10 d'entre eux. Notamment, dtNESt échoue souvent ou produit des arbres plus grands lorsque $\epsilon > 0$ , tandis que dtControl2+ε excelle à exploiter l'imprécision.
Scalabilité : L'outil a résolu tous les benchmarks sauf un en moins de 20 minutes, démontrant sa faisabilité sur des modèles larges et complexes.

Signification

L'article affirme que dtControl2+ε représente une avancée significative dans l'état de l'art de la synthèse de contrôleurs explicables. En échangeant une quantité contrôlable d'optimalité contre de la compacité, l'outil permet de générer des contrôleurs compréhensibles par l'humain qui étaient auparavant trop complexes à interpréter. La capacité à dériver automatiquement des informations structurelles (par exemple, identifier qu'une règle unique suffit pour l' $\epsilon$ -optimalité) et à supporter les propriétés LTL distingue cet outil des autres. Les auteurs soulignent que leur approche fournit des garanties d' $\epsilon$ -optimalité, contrairement aux méthodes d'élagage heuristiques précédentes qui pouvaient compromettre la correction.