Deterministic World Models for Verification of Closed-loop Vision-based Systems

1. Problématique et Contexte

Les contrôleurs visuels de bout en bout (end-to-end), qui mappent directement des images brutes de caméras vers des actions de contrôle, sont de plus en plus déployés dans des systèmes critiques (véhicules autonomes, robots). Cependant, leur vérification formelle en boucle fermée reste un défi majeur pour deux raisons fondamentales :

1. Absence de modèle analytique État-Image : Contrairement aux dynamiques physiques qui sont souvent décrites par des équations, il n'existe pas de fonction mathématique fermée reliant l'état physique du système (position, vitesse) à l'image générée par la caméra. Sans cette relation, la boucle de vérification ne peut pas être fermée.
2. Croissance explosive de la sur-approximation : Les méthodes existantes utilisant des modèles génératifs (comme les GAN conditionnels ou cGAN) introduisent des variables latentes stochastiques (bruit aléatoire) pour améliorer la diversité des images. En vérification formelle, ces variables sans signification physique doivent être bornées de manière très large, ce qui entraîne une sur-approximation massive des ensembles d'images. Cette erreur s'accumule à chaque pas de temps, rendant les ensembles de reachabilité (reachable sets) trop grands pour être utiles (faux positifs massifs).

2. Méthodologie Proposée

Les auteurs proposent un cadre de vérification basé sur trois piliers principaux :

A. Modèle de Monde Déterministe (DWM)

Au lieu d'utiliser des variables latentes stochastiques, les auteurs introduisent un Modèle de Monde Déterministe (DWM).

• Fonctionnement : C'est un décodeur neuronal sans espace latent qui mappe directement un état physique $s$ vers une image synthétique $\hat{I}$.
• Avantage : Chaque image dans un ensemble considéré correspond à un état physique réalisable. La variabilité des images provient uniquement de l'incertitude des états physiques, éliminant ainsi le bruit artificiel qui gonfle les ensembles de vérification.
• Architecture : Un réseau de décodeur convolutif (couche fully-connected suivie de couches de convolution transposée).

B. Stratégie d'Entraînement à Double Perte (Dual Loss)

Pour garantir que l'image synthétique soit non seulement visuellement fidèle mais aussi fonctionnelle pour le contrôleur, le DWM est entraîné avec une fonction de perte combinée :

1. Perte de reconstruction pixel (Pixel-level reconstruction) : Une erreur quadratique moyenne (MSE) pondérée, accordant plus d'importance aux régions critiques pour le contrôle (ex: le pôle, la voiture) qu'au fond.
2. Perte de cohérence de contrôle (Control-consistent loss) : Une pénalité sur la différence entre l'action de contrôle générée par l'image réelle et celle générée par l'image synthétique ($||C(\hat{I}) - C(I)||^2$). Cela force le modèle à préserver les caractéristiques visuelles qui influencent la décision du contrôleur, même si l'image n'est pas parfaite visuellement.

C. Pipeline de Vérification et Conformal Prediction

• Vérification en boucle fermée : Le DWM est intégré dans un pipeline de vérification basé sur les Star sets (représentation d'ensembles d'états). Le flux est : Ensemble d'états initiaux $\to$ DWM (génération d'images) $\to$ Contrôleur CNN (génération d'actions) $\to$ Dynamiques du système (mise à jour des états).
• Garantie Statistique (Conformal Prediction) : Reconnaissant que le DWM est un modèle approximatif, les auteurs utilisent la Prédiction Conformale (CP) pour transférer les garanties du modèle vers le système réel.
  • Ils calculent une borne statistique $\Delta_{1-\alpha}$ sur l'écart maximal de trajectoire entre le système réel et le modèle DWM.
  • Les ensembles de reachabilité du modèle sont ensuite « gonflés » (inflated) par cette borne pour garantir que, avec une probabilité de $1-\alpha$, la trajectoire réelle reste à l'intérieur de l'ensemble vérifié.

3. Contributions Clés

1. Modélisation de monde déterministe : Une approche pour créer des substituts génératifs vérifiables de capteurs caméra en éliminant les variables latentes stochastiques.
2. Extension des analyses de reachabilité : La première extension de l'analyse de reachabilité basée sur les Star sets pour la vérification en boucle fermée de systèmes basés sur la vision.
3. Garanties réalistes : L'utilisation de la prédiction conformale pour fournir des garanties de sécurité probabilistes pour le système réel, en comblant l'écart entre le modèle substitut et la réalité.
4. Performance supérieure : Une validation expérimentale montrant une précision de vérification nettement supérieure aux méthodes de base (cGAN).

4. Résultats Expérimentaux

L'approche a été évaluée sur quatre environnements : CartPole, MountainCar, Pendulum et un système de freinage.

• Comparaison avec les cGAN :
  • Les modèles cGAN (baseline) produisent des ensembles d'images avec une incertitude spatiale excessive et du bruit de fond, entraînant une sur-approximation qui rend la vérification conservatrice (taux de vrais négatifs de 0% sur MountainCar et Freinage, c'est-à-dire que tout est marqué comme dangereux).
  • Le DWM produit des ensembles d'images beaucoup plus serrés.
• Métriques de Performance (F1-Score) :
  • Le DWM atteint des scores F1 très élevés (ex: 0.9817 pour MountainCar, 0.9842 pour le système de freinage) contre des scores bien inférieurs pour les cGAN (ex: 0.7990 et 0.6639 respectivement).
  • Le DWM maintient une précision de 1.0 sur tous les benchmarks (aucun faux positif), prouvant la soundness (sûreté) de la méthode.
• Impact de la Perte de Cohérence de Contrôle :
  • L'ablation montre que l'ajout de la perte $L_{ctrl}$ réduit encore davantage la borne de prédiction conformale ($\Delta_{0.95}$), améliorant la fidélité de la trajectoire par rapport à la simple reconstruction visuelle.
• Impact de la Prédiction Conformale :
  • L'inflation des ensembles par la borne CP réduit légèrement le rappel (recall) dans les systèmes très sensibles aux erreurs (comme CartPole), mais c'est le prix à payer pour une garantie mathématique rigoureuse sur le système réel.

5. Signification et Conclusion

Ce travail résout un problème fondamental en vérification formelle des systèmes autonomes visuels : l'incompatibilité entre la diversité générative (nécessaire pour l'apprentissage) et la précision déterministe (nécessaire pour la vérification).

En éliminant les variables latentes et en introduisant une contrainte de comportement de contrôle, les auteurs démontrent qu'il est possible de fermer la boucle de vérification pour des contrôleurs basés sur des images sans sacrifier la précision. L'ajout de la prédiction conformale permet de transformer une garantie sur un modèle approximatif en une garantie probabiliste robuste pour le système physique réel.

Limitations et perspectives : Le modèle actuel peine avec des scènes très complexes (arrière-plans encombrés, variations lumineuses). Les auteurs suggèrent des architectures à « mélange d'experts » et une extension vers une surveillance en temps réel (runtime monitoring) pour des applications de sécurité critiques déployées.