Verification of Unknown Dynamical Systems via Autoencoder Latent Space

Résumé Technique : Vérification de Systèmes Dynamiques Inconnus via l'Espace Latent d'un Autoencodeur

Formulation du Problème
La vérification formelle des systèmes dynamiques à espace continu est essentielle pour garantir que les systèmes autonomes satisfont des spécifications de sûreté et de vivacité, souvent exprimées en Logique Temporelle Linéaire (LTL). Les approches standards consistent à construire des abstractions à états finis pour permettre la vérification de modèles. Cependant, ces techniques font face à des défis de scalabilité sévères dans les contextes de haute dimension, car la taille de l'abstraction croît de manière exponentielle avec la dimension de l'espace d'états. Ce problème est exacerbé dans les systèmes intégrant l'intelligence artificielle (par exemple, ceux contrôlés par des réseaux de neurones traitant des données LiDAR ou de caméras) où les dynamiques sont complexes, partiellement inconnues ou de type boîte noire. Bien que des techniques de réduction de dimensionnalité basées sur les données, telles que les autoencodeurs, offrent une solution potentielle pour la scalabilité, elles manquent généralement de garanties formelles de correction. Plus précisément, mapper des spécifications de haute dimension vers un espace latent appris et s'assurer que les dynamiques latentes apprises représentent fidèlement le comportement du système original (y compris le non-déterminisme) reste un défi ouvert. Les méthodes existantes sacrifient souvent la correction pour la flexibilité ou reposent sur des hypothèses fortes concernant les dynamiques du système qui ne tiennent pas pour les représentations apprises.

Méthodologie
Le cadre proposé répond à ces défis en combinant la réduction de dimensionnalité avec la vérification basée sur l'abstraction pour fournir des garanties formelles pour les systèmes de haute dimension à dynamiques inconnues. L'approche se compose de quatre étapes principales :

1. Architecture d'Autoencodeur Convexe : Pour garantir que l'espace latent soit interprétable et supporte un raisonnement sain, les auteurs emploient un Autoencodeur Convexe. L'encodeur est restreint à être un Réseau de Neurones Convexe d'Entrée (ICNN) avec des contraintes structurelles spécifiques : fonctions d'activation strictement monotones (pour agir comme des homéomorphismes), premières couches et couches de saut injectives, et matrices de poids de rang complet. Cette architecture, qualifiée de réseau « Entrée Connectée - Sortie Connectée » (CICO), garantit que l'image réciproque de n'importe quel ensemble connexe dans l'espace latent est un ensemble connexe dans l'espace d'états original. Cette propriété est cruciale pour gérer la non-injectivité de l'application lorsque la dimension latente est inférieure à la réalisation minimale du système.

2. Apprentissage de Dynamiques d'Inclusion Latentes : Parce que la réduction de dimensionnalité peut entraîner une perte d'information, l'évolution dans l'espace latent est modélisée comme des dynamiques d'inclusion (à valeurs d'ensembles) plutôt que comme des équations aux différences déterministes. Les auteurs introduisent les « Processus Gaussiens d'Inclusion » (Inclusion GPs), une formulation novatrice de la Régression par Processus Gaussiens (GPR) pour des dynamiques à valeurs d'ensembles. Cette méthode relève les dynamiques vers un espace de dimension supérieure où elles suivent des équations aux différences impliquant un paramètre non observé $c$. En apprenant un noyau profond qui incorpore cette coordonnée non observée, la méthode prédit l'évolution du système comme un ensemble (spécifiquement, une boule dans l'espace latent) et fournit des bornes d'erreur rigoureuses basées sur l'analyse des Espaces de Hilbert à Noyau Reproduisant (RKHS).

3. Construction d'une Abstraction Finie Saine : En utilisant le Processus Gaussien d'Inclusion appris, les auteurs construisent un Système de Transition Non-Déterministe (NTS) dans l'espace latent.

   • Cartographie des Régions : Les régions d'intérêt de haute dimension (ensembles sûrs, dangereux et objectifs) sont mappées vers l'espace latent. La convexité de l'encodeur permet une sous-approximation efficace basée sur l'échantillonnage et une sur-approximation probabiliste (utilisant $\epsilon$-RandUp) de ces ensembles.
   • Relation de Transition : Les transitions entre états abstraits sont calculées en propageant les régions à travers le modèle de Processus Gaussien d'Inclusion, en tenant compte des erreurs de régression et du paramètre non observé $c$. Cela garantit que l'abstraction capture de manière conservatrice tous les comportements possibles du système original.
   • Garanties de Correction : Le cadre démontre que si un état dans le NTS latent satisfait une spécification de type « atteindre-éviter », alors toutes les trajectoires correspondantes dans le système original de haute dimension satisfont la spécification avec un niveau de confiance élevé ($1-\delta$).

4. Vérification et Décodage : Des outils standards de vérification de modèles sont appliqués au NTS latent pour identifier les états garantis satisfaire la spécification ($Q_{yes}$), les états qui ne peuvent pas la satisfaire ($Q_{no}$), et les états incertains ($Q_?$). Parce que l'encodeur est convexe, les états latents satisfaisants peuvent être décodés efficacement vers l'espace original de haute dimension en utilisant l'optimisation convexe pour identifier l'ensemble des états initiaux dans le système original qui sont garantis sûrs.

Contributions Clés
L'article apporte quatre contributions principales :

1. Cartographie Prouvée Correcte : Une méthode pour mapper des spécifications de haut niveau vers un espace latent en utilisant un encodeur CICO, permettant un raisonnement efficace sur des représentations compressées tout en préservant les garanties formelles.
2. Processus Gaussiens d'Inclusion : Une formulation novatrice de la régression par Processus Gaussiens pour des dynamiques à valeurs d'inclusion (à valeurs d'ensembles), permettant l'apprentissage de dynamiques latentes gouvernées par des inclusions aux différences sans nécessiter de connaissance explicite des paramètres non observés sous-jacents.
3. Cadre d'Abstraction Sain : Un cadre complet pour générer des abstractions finies saines dans l'espace latent basé sur les Processus Gaussiens d'Inclusion, incluant des procédures pour mapper les garanties de satisfaction vers le système original avec des preuves de correction.
4. Validation Empirique : Démonstration de l'approche sur plusieurs systèmes, y compris un système de 26 dimensions contrôlé par un réseau de neurones (utilisant des entrées LiDAR), montrant des améliorations significatives de scalabilité par rapport aux méthodes d'abstraction traditionnelles.

Résultats
L'approche a été évaluée sur trois études de cas :

• 3D vers 2D : Un système de réalisation minimale où la méthode a vérifié avec succès l'ensemble de l'espace latent, tandis que l'abstraction basée sur les données traditionnelle dans l'espace 3D original a échoué à vérifier la reachabilité en raison de l'incertitude dans les dimensions à mouvement lent.
• 6D vers 2D : Un système sur-paramétré avec des observations non linéaires. La méthode a vérifié 100 % de l'espace latent pour le cas sans obstacle et 59,78 % pour le cas avec un obstacle. En revanche, tenter une abstraction dans l'espace 6D original a entraîné une explosion d'états, échouant à vérifier toute région au-delà de l'objectif lui-même dans la limite de temps.
• 26D vers 2D : Une tâche de navigation robotique avec des entrées LiDAR et un contrôleur par réseau de neurones. La méthode a appris avec succès un espace latent 2D qui a capturé les dynamiques du système avec un non-déterminisme minimal, vérifiant 50,0001 % de l'espace latent. Cela a démontré la capacité à gérer des espaces d'observation de haute dimension où les méthodes traditionnelles sont irréalisables.

Signification
L'article prétend combler un fossé critique entre la réduction de dimensionnalité et la vérification formelle. En fournissant des garanties de validité à la fois pour le mappage des spécifications et pour les dynamiques latentes apprises, le travail élimine les faux positifs dans les résultats de vérification, un problème courant dans le contrôle basé sur l'apprentissage. Les auteurs soulignent que leur approche permet une vérification évolutive pour les systèmes de haute dimension à dynamiques inconnues, une capacité auparavant inaccessible avec les méthodes formelles existantes. Bien que le cadre soit sain, les auteurs notent modestement des limitations, notamment la restriction aux encodeurs convexes (ce qui limite l'expressivité) et des questions ouvertes concernant l'incorporation du bruit et la synthèse de contrôle, qui sont identifiées comme des pistes pour un travail futur.