Learning Robust Control Lyapunov Functions through Lipschitz Neural Networks

Résumé Technique : Apprentissage de Fonctions de Lyapunov de Contrôle Robustes via des Réseaux de Neurones Lipschitziens

Énoncé du Problème
L'article traite du défi de la conception de contrôleurs stabilisants pour des systèmes dynamiques non linéaires soumis à des perturbations additives. Bien que les fonctions de Lyapunov soient un outil fondamental pour l'analyse de la stabilité, leur construction automatique pour des systèmes non linéaires généraux reste un problème ouvert. Les méthodes de calcul existantes, telles que les sommes de carrés (SOS) ou les inégalités matricielles linéaires (LMI), peinent souvent en termes de scalabilité ou de généralité. De plus, les approches récentes d'apprentissage profond qui apprennent des Fonctions de Lyapunov de Contrôle (CLF) à l'aide de réseaux de neurones se concentrent généralement sur des dynamiques exactes sans perturbations ou reposent sur des méthodes de vérification qui sont coûteuses en termes de calcul ou conservatrices (par exemple, en utilisant uniquement des informations d'ordre zéro). Le défi spécifique abordé ici est l'apprentissage d'une Fonction de Lyapunov de Contrôle Robuste (RCLF) et d'un contrôleur de rétroaction d'état correspondant qui garantit la Borne Ultime Uniformément Bornée (UUB) en présence de perturbations additives dépendant de l'état, tout en assurant que la vérification de ces conditions soit calculablement traitable.

Méthodologie
Le cadre proposé intègre des Réseaux de Neurones Lipschitziens (LNN) avec un algorithme de vérification de type Branch-and-Bound (BnB) d'ordre élevé.

1. Réseaux de Neurones Lipschitziens (LNN) :
   Les auteurs utilisent des LNN pour apprendre conjointement la RCLF ($V_{\theta_1}$) et le contrôleur stabilisant ($\pi_{\theta_2}$). Contrairement aux réseaux standards, les LNN imposent une constante de Lipschitz prédéfinie via des paramétrages de couches spécifiques (par exemple, Normalisation Spectrale, Couches Orthogonales ou Couches Sandwich). Cette contrainte est critique car elle permet de dériver des bornes explicites et serrées sur les dérivées d'ordre supérieur (Hessienne et dérivées de troisième ordre) de la sortie du réseau par rapport à son entrée. La RCLF est définie comme la sortie décalée d'un réseau pour garantir la condition d'équilibre $V(0)=0$.

2. Algorithme d'Apprentissage :
   Le processus d'apprentissage minimise une fonction de perte composite sur un espace d'états et une frontière échantillonnés. Les termes de perte imposent :

   • La Définition Positive : Garantir que $V(x) > 0$ pour $x \neq 0$.
   • La Condition de Décroissance : Garantir que la dérivée temporelle $\dot{V}$ est négative en dehors d'une petite boule autour de l'origine, en tenant compte de la pire perturbation possible. Cela implique de borner par le haut le terme de perturbation en utilisant la fonction de borne de la perturbation $\epsilon(x)$ connue et les constantes de Lipschitz de la dynamique du réseau et du système.
   • La Frontière et la Couverture : Encourager l'ensemble de sous-niveau de $V$ à couvrir une portion maximale de l'espace d'états et à maintenir une valeur cohérente sur la frontière.
     L'algorithme initialise les paramètres à l'aide de solutions de Régulateur Linéaire Quadratique (LQR) et les affine de manière itérative, en stockant les paramètres qui produisent la plus grande région de l'ensemble invariant vers l'avant vérifiée empiriquement.

3. Vérification d'Ordre Supérieur (Branch-and-Bound) :
   Un nouvel algorithme de BnB compatible avec les GPU est introduit pour vérifier formellement la RCLF apprise. Contrairement aux solveurs traditionnels (par exemple, dReal) qui reposent sur des bornes d'ordre zéro ou les solveurs SMT qui font face à des limites de scalabilité, cette méthode exploite la lissité des LNN.

   • Bornes d'Ordre Supérieur : Les auteurs dérivent des bornes explicites de norme spectrale pour la Hessienne et les dérivées de troisième ordre des LNN. Ces bornes sont utilisées pour construire des enveloppes inférieures et supérieures serrées sur la valeur du réseau via des développements de Taylor (jusqu'au second ordre).
   • Efficacité de l'Algorithme : En incorporant des informations de premier et second ordre, l'algorithme crée des enveloppes nettement plus serrées des valeurs de la fonction dans les rectangles de recherche. Cela permet un élagage beaucoup plus agressif de l'espace de recherche par rapport aux méthodes d'ordre zéro.
   • Complexité : L'article établit des bornes de complexité temporelle dans le pire des cas, montrant que le nombre de rectangles évalués croît de manière polynomiale avec la dimension du système et inversement avec la tolérance, mais est considérablement réduit en pratique par les bornes plus serrées.

Contributions Clés

1. Cadre Novateur : Une approche unifiée pour l'apprentissage de CLF robustes et de contrôleurs stabilisants pour des systèmes non linéaires avec des perturbations additives dépendant de l'état en utilisant des LNN.
2. Bornes de Dérivées : L'établissement de bornes explicites de norme spectrale pour la Hessienne et les dérivées de troisième ordre des LNN. Ces bornes sont plus serrées que celles dérivées des informations d'ordre zéro ou premier degré, répondant ainsi à la non-convexité de la vérification de Lyapunov.
3. Vérification Compatible GPU : Le développement d'un algorithme de BnB qui utilise ces bornes d'ordre supérieur et supporte l'évaluation par lots sur GPU. Cela accélère considérablement le processus de vérification par rapport aux solveurs SMT basés sur CPU.
4. Validation Empirique : Des simulations étendues sur six systèmes dynamiques (pendule inversé, unicycle, système de troisième ordre, cartpole, quadrotor 2D et bras SCARA) démontrant la capacité de la méthode à vérifier la stabilité et à surpasser les outils existants (dReal, $\alpha,\beta$-CROWN) en termes de vitesse et de scalabilité.

Résultats
L'article présente des résultats de simulation comparant la méthode proposée à dReal (SMT basé sur CPU) et $\alpha,\beta$-CROWN (propagation de bornes basée sur GPU).

• Vitesse de Vérification : L'algorithme de BnB proposé, compatible GPU, surpasse systématiquement dReal, réduisant souvent le temps de vérification de plusieurs heures (ou de timeouts) à quelques secondes, même pour des systèmes avec des dimensions d'état plus élevées (par exemple, le bras SCARA avec $n_x=8$).
• Scalabilité : Alors que dReal échoue à vérifier des systèmes avec plus de 2 à 3 couches dans un délai raisonnable, la méthode proposée vérifie avec succès des réseaux allant jusqu'à 4 couches.
• Régions Invariantes vers l'Avant : Les contrôleurs appris atteignent des régions invariantes vers l'avant nettement plus grandes que les approches LQR standard et les approches NLC (Neural CLF) non robustes. Pour le pendule inversé, la méthode proposée a atteint un ratio de région invariante vers l'avant d'environ 75 %, contre environ 23 % pour le LQR.
• Robustesse : La vérification confirme que les contrôleurs appris satisfont la condition UUB, maintenant les trajectoires à l'intérieur d'une région bornée malgré la présence de perturbations.

Signification et Revendications
L'article affirme que sa principale signification réside dans le pont jeté entre l'expressivité de l'apprentissage profond et les exigences rigoureuses de la vérification de contrôle robuste. En exploitant la structure spécifique des réseaux de Lipschitz pour dériver des bornes de dérivées d'ordre supérieur, les auteurs permettent un processus de vérification qui est à la fois mathématiquement rigoureux et calculablement efficace.

Les auteurs précisent explicitement que leur cadre ne certifie pas la stabilité pour un modèle inconnu sans une borne d'erreur connue ; il fournit plutôt une garantie déterministe de robustesse contre un écart de modèle ou une perturbation certifiée. Le travail souligne que, bien que les LNN puissent avoir une expressivité réduite par rapport aux réseaux non contraints, ce compromis est justifié par la capacité de réaliser une vérification d'ordre supérieur efficace, ce qui est essentiel pour les applications de contrôle critiques pour la sécurité. L'article conclut que cette approche rend la vérification formelle de contrôleurs appris et robustes pour des systèmes non linéaires complexes pratiquement réalisable.