⚡ electrical engineering

Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers

Ce papier présente un cadre de faisabilité différentiable et parallélisable en JAX qui combine des flowpipes de modèles de Taylor avec une propagation de bornes de type CROWN pour permettre un entraînement certifié et une planification basée sur le gradient pour les dynamiques et contrôleurs de réseaux de neurones sous incertitude.

Auteurs originaux : Keyi Shen, Glen Chou

Publié 2026-05-26

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Keyi Shen, Glen Chou

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 enseigniez à un robot à accomplir une tâche délicate, comme pousser un objet en forme de T sur une table ou faire voler un drone à travers un espace étroit. Vous utilisez un « cerveau » (un réseau de neurones) pour aider le robot à déterminer comment se déplacer. Ce cerveau est incroyablement efficace pour prédire ce qui va se produire ensuite, en se basant sur l'expérience passée.

Cependant, il y a un gros problème : Et si le robot se trompait légèrement ? Peut-être que le sol est glissant, ou qu'un capteur a mal mesuré la distance d'un tout petit peu. Dans le monde réel, ces petites erreurs peuvent s'accumuler. Une minuscule erreur à l'étape un peut mener à une collision à l'étape dix.

Traditionnellement, les ingénieurs ont deux choix :

Faire entièrement confiance au robot : C'est rapide et cela fonctionne bien la plupart du temps, mais si quelque chose tourne mal, le robot peut entrer en collision car il n'a pas pris en compte les « et si ».
Vérifier les mathématiques formellement : Cela garantit la sécurité en calculant chaque issue possible, mais c'est si lent et compliqué que cela ne peut pas être utilisé pendant que le robot se déplace ou apprend réellement.

Cet article présente un nouvel outil appelé DiffReach qui agit comme un « calculateur de sécurité ultra-rapide » capable de fonctionner en temps réel. Voici comment il fonctionne, en utilisant quelques analogies du quotidien :

1. L'analogie de l'« Ombre » (Faisabilité)

Imaginez que le robot est une personne marchant dans une forêt brumeuse. Vous ne savez pas exactement où elle se trouve, seulement qu'elle est quelque part à l'intérieur d'un petit cercle autour d'un point connu.

L'ancienne méthode : Pour être en sécurité, vous pourriez dessiner un nuage géant et flou autour de la personne, qui grossit à chaque pas, finissant par couvrir toute la forêt. C'est sûr, mais c'est trop effrayant à utiliser car cela indique « ils pourraient heurter un arbre » même s'ils sont loin.
La méthode de l'article : DiffReach dessine une ombre étroite et flexible autour du robot. Au fur et à mesure que le robot se déplace, cette ombre s'étire et se tord pour suivre exactement le chemin du robot, mais elle ne grossit jamais plus que nécessaire. Elle vous dit : « Si le robot commence ici, il pourrait finir n'importe où à l'intérieur de cette forme spécifique, mais nulle part ailleurs. »

2. L'analogie de la « Chaîne de montage » (Parallèle et Différentiable)

Habituellement, calculer ces ombres revient à une seule personne résolvant un problème mathématique sur un papier. Cela prend une éternité.

L'innovation : Les auteurs ont construit cet outil en utilisant JAX (un moteur de calcul puissant). Imaginez qu'au lieu d'une seule personne, vous ayez une usine avec des milliers d'ouvriers (GPU) effectuant les calculs simultanément.
Différentiable : C'est la partie magique. Habituellement, les vérifications de sécurité sont comme un « panneau stop » — vous vérifiez, et si ce n'est pas sûr, vous vous arrêtez. Vous ne pouvez pas utiliser le panneau stop pour enseigner au robot à mieux conduire. DiffReach est comme une rampe lisse et glissante. Parce que les mathématiques sont « différentiables », le robot peut regarder l'ombre, voir où elle devient trop large, et ajuster immédiatement son cerveau (réseau de neurones) pour rendre l'ombre plus étroite. Cela transforme la sécurité d'un « panneau stop » en un « volant ».

3. Le moteur en deux parties

L'article combine deux techniques mathématiques différentes en une seule machine fluide :

Modèles de Taylor (La partie analytique) : Pour les parties du robot que nous comprenons avec la physique (comme l'aérodynamique d'un drone), ils utilisent une méthode qui prédit le chemin comme une courbe lisse.
CROWN (La partie neuronale) : Pour les parties « cerveau » (les réseaux de neurones), ils utilisent une technique qui vérifie les limites des hypothèses de l'IA.
L'unification : Ils ont créé un langage universel (une « Interface TM-CROWN unifiée ») afin que ces deux méthodes différentes puissent communiquer entre elles sans perdre de précision. C'est comme traduire une conversation entre un physicien et un expert en IA sans perdre aucun détail dans la traduction.

4. Ce qu'ils ont réellement fait (Les résultats)

Les auteurs n'ont pas seulement construit l'outil ; ils l'ont utilisé pour faire deux choses spécifiques :

Entraînement certifié : Ils ont enseigné au cerveau du robot à être « conscient de la sécurité ». Au lieu d'apprendre simplement à atteindre une cible, le cerveau a appris à garder son « ombre » petite. Si l'ombre devient trop grande (ce qui signifie que le robot est incertain), l'entraînement le pénalise. Le résultat ? Des robots tout aussi performants dans leurs tâches, mais beaucoup plus sûrs lorsque les choses tournent mal.
Planification sûre (MPC) : Ils ont utilisé l'outil pour planifier des trajectoires en temps réel.
- En simulation : Ils l'ont testé sur un bras robotique et un essaim de drones (jusqu'à 72 dimensions de mouvement !). L'outil était 100 fois plus rapide que les méthodes précédentes tout en maintenant des bornes de sécurité étroites.
- Dans le monde réel : Ils l'ont testé sur un vrai bras robotique poussant un objet en forme de T. Le robot a planifié ses mouvements avec succès tout en évitant les obstacles, même lorsque l'environnement était légèrement imprévisible.

La conclusion

Cet article présente un moyen de rendre les robots à la fois intelligents et sûrs en même temps. En rendant la vérification de sécurité assez rapide pour fonctionner sur une carte graphique de jeu vidéo (GPU) et assez flexible pour faire partie du processus d'apprentissage, ils permettent aux robots d'apprendre de l'expérience sans oublier de surveiller les « et si ».

Ce qu'ils n'ont PAS affirmé :

Ils n'ont pas affirmé que cela fonctionne pour la chirurgie médicale ou la conduite autonome sur les routes publiques pour l'instant.
Ils n'ont pas affirmé que cela résout tous les problèmes de sécurité (ils admettent qu'il a encore du mal avec des horizons temporels très longs ou des contacts physiques complexes comme des balles qui rebondissent).
Ils se sont concentrés strictement sur des tâches robotiques comme pousser des objets et faire voler des drones.

Résumé technique : Atteignabilité différentiable parallèle pour l'apprentissage et la planification avec des dynamiques et contrôleurs neuronaux certifiés

Énoncé du problème

Les modèles de dynamiques basés sur des réseaux de neurones (RN) et les politiques de contrôle ont démontré de solides performances empiriques en robotique, en particulier dans des environnements complexes où la modélisation analytique est irréalisable. Cependant, fournir des garanties de sécurité robustes pour les systèmes en boucle fermée avec RN sous incertitude reste un défi majeur. L'analyse d'atteignabilité classique offre des garanties formelles via des sur-approximations d'ensembles atteignables, mais elle s'avère souvent peu évolutive, peine à intégrer les composants neuronaux et produit des bornes excessivement conservatrices. À l'inverse, les méthodes modernes de vérification de réseaux de neurones (NNV) comme CROWN s'adaptent bien aux grands réseaux mais sont principalement conçues pour une vérification statique, manquent de prise en charge des dynamiques en temps continu et sont généralement non différentiables.

Par conséquent, l'analyse d'atteignabilité est généralement limitée à une certification a posteriori, créant des cycles coûteux d'apprentissage non certifié, d'échec de vérification et de réentraînement. Il existe un besoin critique d'un cadre intégrant directement l'atteignabilité certifiée dans les pipelines d'apprentissage robotique et de planification en ligne, supportant à la fois les systèmes en temps continu et discret avec des composants analytiques et basés sur des RN, tout en restant différentiable et efficace.

Méthodologie

Les auteurs proposent DiffReach, un cadre d'atteignabilité parallélisable et différentiable implémenté dans JAX. L'innovation centrale est une représentation unifiée combinant la construction de tubes d'écoulement par modèles de Taylor (TM) pour les dynamiques analytiques et la propagation de bornes linéaires de style CROWN pour les composants neuronaux.

1. Représentation unifiée (Interface Taylor-CROWN)

Pour permettre le calcul par lots sur GPU et la différenciation automatique, le cadre adopte une représentation de modèle de Taylor à forme fixe. Au lieu de polynômes de taille variable, les ensembles atteignables sont représentés comme suit :
$F(z) = c + Az \oplus I \quad \text{ou} \quad F(z) = c + Az + B \tau z \oplus I$
où $z$ augmente l'état avec le temps, $c$ est une constante, $A$ et $B$ sont des matrices capturant les dépendances affines et quasi-quadratiques, et $I$ est un reste d'intervalle. Cette représentation préserve les dépendances affines sans relâchement d'intervalle intermédiaire.

Composants neuronaux : Le cadre exploite CROWN (via jax_verify) pour calculer des bornes affines pour les réseaux de neurones. Une contribution clé est l'imposition d'une contrainte de pente partagée dans CROWN, garantissant que les bornes inférieure et supérieure partagent le même terme linéaire. Cela permet de représenter les sorties des réseaux de neurones comme des modèles de Taylor linéaires, maintenant la compatibilité avec le pipeline de dynamiques analytiques.
Systèmes en temps continu (CT) : Pour les systèmes CT avec contrôle de rétroaction neuronal, le cadre alterne entre :
1. Certification du contrôleur : Utilisation de l'interface TM-CROWN pour certifier la sortie du contrôleur neuronal étant donné l'enveloppe TM de l'état actuel.
2. Propagation des dynamiques : Propagation des dynamiques du système (équations différentielles ordinaires analytiques ou neuronales) en utilisant des tubes d'écoulement TM sous une politique de maintien d'ordre zéro pour l'entrée de contrôle.
Systèmes en temps discret (DT) : L'atteignabilité se réduit à une propagation étape par étape où l'interface TM-CROWN certifie la carte d'un pas à chaque instant.

2. Applications DiffReach-Robotique

En s'appuyant sur le moteur DiffReach, les auteurs développent deux méthodes axées sur la robotique :

Apprentissage certifié : Une méthode d'apprentissage pour les dynamiques et contrôleurs neuronaux qui enrichit les pertes standard de prédiction ou de suivi d'un terme de régularisation conscient de l'atteignabilité. Ce terme pénalise la croissance du volume des ensembles atteignables certifiés sous incertitude bornée. Pour stabiliser l'apprentissage, une stratégie d'apprentissage par curriculum est employée, augmentant progressivement l'horizon de déploiement et réduisant le rayon de perturbation.
MPC conscient de l'atteignabilité : Un schéma de commande prédictive modèle (MPC) basé sur l'échantillonnage qui intègre les ensembles atteignables certifiés dans la planification en ligne. Le planificateur optimise une fonction de coût comprenant l'objectif de la tâche et une pénalité pour les trajectoires dangereuses ou les grands ensembles atteignables. La parallélisation permet une évaluation efficace de nombreuses trajectoires candidates, avec un raffinement basé sur le gradient appliqué aux meilleures candidates pour réduire davantage le conservatisme.

Contributions clés

Cadre d'atteignabilité différentiable parallèle : Une représentation unifiée basée sur JAX combinant les tubes d'écoulement de modèles de Taylor et la propagation de bornes de style CROWN pour les systèmes en temps continu et discret avec des dynamiques/contrôleurs analytiques et basés sur des RN.
Méthode d'apprentissage certifié : Une approche d'apprentissage utilisant des objectifs d'ensembles atteignables différentiables pour améliorer la robustesse des composants neuronaux sous incertitude, encourageant des modèles « favorables à l'atteignabilité ».
MPC conscient de l'atteignabilité : Un schéma de planification en ligne intégrant les ensembles atteignables certifiés dans un MPC basé sur l'échantillonnage avec raffinement basé sur le gradient, permettant une planification vérifiée par construction.
Validation expérimentale : Évaluation complète sur la manipulation non préhensile (poussée en T) et des tâches de quadrotor, incluant des expériences matérielles et des évaluations de haute dimension (jusqu'à 72D), démontrant une planification en ligne pratique avec des garanties certifiées.

Résultats

Le cadre a été évalué sur un GPU RTX 4090 selon plusieurs dimensions :

Efficacité et précision : Par rapport aux bases de référence DT (CROWN) et CT (immrax) de l'état de l'art, DiffReach atteint une précision d'ensemble atteignable comparable tout en étant environ 100 fois plus rapide que CROWN pour les systèmes DT. Pour les systèmes CT, il produit des ensembles atteignables substantiellement plus précis que immrax, qui souffre fréquemment de débordements numériques et de tubes de volume infini.
Évolutivité : Le cadre s'adapte efficacement aux systèmes de plus haute dimension, y compris un essaim de 6 quadrotors (état 72D) et un bras planaire à 10 articulations (état 40D). Bien que la mémoire évolue en $O(n^2)$ , le temps d'exécution évolue favorablement grâce aux opérations matricielles parallèles sur GPU.
Apprentissage certifié : Les modèles entraînés avec régularisation d'atteignabilité ont atteint des performances nominales comparables à l'entraînement standard mais ont produit des ensembles atteignables substantiellement plus précis. Ces ensembles correspondaient étroitement aux volumes de bornes inférieures échantillonnées, tandis que les modèles non certifiés produisaient des prédictions lâches et moins vérifiables.
Planification robuste : Dans les expériences MPC sous perturbations bornées, le planificateur conscient de l'atteignabilité a maintenu des taux de réussite élevés et satisfait les contraintes, tandis que le MPC standard avec des modèles non certifiés a échoué significativement sous de plus grandes perturbations (par exemple, un contact non intentionnel dans les tâches de poussée en T).
Déploiement matériel : Le système a été déployé sur une plateforme Kuka iiwa pour la poussée en T, fonctionnant en ligne à environ 10 Hz (5 Hz avec raffinement), démontrant la faisabilité de l'intégration de l'atteignabilité différentiable dans le contrôle robotique en temps réel.

Importance et revendications

L'article revendique que DiffReach comble le fossé entre la vérification formelle et l'apprentissage robotique en fournissant une primitive d'atteignabilité différentiable et accélérée par GPU. Contrairement aux méthodes précédentes limitées à la vérification hors ligne, ce cadre permet aux objectifs d'ensembles atteignables d'informer directement l'entraînement des dynamiques et contrôleurs neuronaux ainsi que l'exécution de la planification en ligne.

Les auteurs soulignent que leur approche permet un apprentissage et une planification « vérifiés par construction », réduisant la dépendance aux cycles coûteux de certification a posteriori. En unifiant les modèles de Taylor et CROWN au sein d'un seul graphe de calcul, la méthode préserve les dépendances affines et prend en charge à la fois les systèmes en temps continu et discret, répondant à une limitation critique des outils d'analyse actuels intégrant des RN dans la boucle.

L'ouvrage conclut en reconnaissant les limitations actuelles, telles que les défis liés au conservatisme sur les longs horizons et aux dynamiques hybrides ou riches en contacts, mais postule que ce cadre motive la recherche future sur l'atteignabilité différentiable évolutive et une intégration plus étroite entre la vérification formelle, l'apprentissage robotique et le contrôle.