⚡ electrical engineering

Certified Neural Approximations of Nonlinear Dynamics

Cet article introduit une méthode de vérification nouvelle, adaptative et parallélisable qui fournit des bornes d'erreur formelles pour les approximations par réseaux de neurones de systèmes dynamiques non linéaires, permettant leur déploiement sûr dans des contextes critiques pour la sécurité et surpassant les approches de pointe sur divers benchmarks, incluant la compression de réseaux de neurones et la prédiction de trajectoire basée sur l'opérateur de Koopman.

Auteurs originaux : Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano, Luca Laurenti, Alessandro Abate

Publié 2026-06-04

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano, Luca Laurenti, Alessandro Abate

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 possédez une machine très complexe et imprévisible — comme un moteur de jet ou un système météorologique. Pour comprendre cette machine, prédire son avenir ou la maintenir en sécurité, les ingénieurs ont généralement besoin d'un modèle mathématique. Mais ces modèles du monde réel sont souvent si désordonnés et non linéaires (ondulés, tortueux, difficiles à calculer) que les ordinateurs peinent à vérifier s'ils sont sûrs.

Pour résoudre ce problème, les scientifiques utilisent souvent un « modèle simplifié », comme un réseau de neurones (un type d'IA), pour imiter la véritable machine. Considérez le réseau de neurones comme une version dessin animé du véritable moteur de jet. Il est beaucoup plus facile pour un ordinateur de lire le dessin animé que le plan complexe.

Le Problème :
Le danger est que le dessin animé puisse paraître correct la plupart du temps, mais échouer dans un minuscule point critique. Si vous utilisez le dessin animé pour contrôler le véritable moteur de jet, ce minuscule échec pourrait provoquer un crash. Par le passé, vérifier si le dessin animé est « assez proche » de la réalité nécessitait un ordinateur surpuissant et lent (appelé solveur SMT) qui tentait de vérifier chaque possibilité. C'était comme essayer de compter chaque grain de sable sur une plage un par un pour voir si la plage est sûre. Cela prenait trop de temps et ne pouvait pas gérer des systèmes aussi vastes et complexes.

La Solution : « Approximations Neuronales Certifiées »
Ce document présente une nouvelle façon plus rapide de vérifier si le dessin animé par l'IA est sûr à utiliser. Voici comment ils ont procédé, en utilisant des analogies simples :

1. La stratégie de la « Carte Locale » (Modèles de premier ordre)

Au lieu d'essayer de comprendre toute la machine ondulée et complexe d'un seul coup, les auteurs décomposent le comportement de la machine en morceaux minuscules et gérables.

L'analogie : Imaginez que vous faites une randonnée en montant une montagne très escarpée et sinueuse. Il est difficile de prédire tout le chemin d'un coup. Mais si vous zoomez juste sur vos pieds immédiats, le sol semble plat.
La méthode : Ils divisent tout le « comportement de la montagne » (les états possibles du système) en minuscules boîtes rectangulaires. À l'intérieur de chaque petite boîte, ils prétendent que la courbe complexe est en fait une ligne droite (un « modèle de premier ordre »). C'est beaucoup plus facile à calculer. Ils ajoutent ensuite une « zone de sécurité » (une limite d'erreur) autour de cette ligne droite pour tenir compte du fait que le vrai sol est en fait courbe.

2. Le « Raffinement Intelligent » (Partitionnement adaptatif)

Parfois, une ligne droite n'est pas une supposition suffisante pour une partie très courbe de la montagne.

L'analogie : Si vous marchez sur un chemin plat, une grande carte convient parfaitement. Mais si vous atteignez une falaise abrupte ou un virage sinueux, vous devez zoomer et dessiner une carte beaucoup plus détaillée de cet endroit spécifique.
La méthode : Si leur ordinateur trouve un endroit où la supposition de la « ligne droite » est trop éloignée de la machine réelle, il divise automatiquement cette boîte en deux et réessaie avec des boîtes plus petites et plus détaillées. Il ne zoome que là où c'est réellement nécessaire, ce qui permet d'économiser un temps massif.

3. L'« Équipe Parallèle » (Parallélisation)

L'analogie : Au lieu d'une seule personne vérifiant toute la montagne seule, imaginez une équipe de 8 randonneurs. Chaque randonneur prend une section différente de la montagne pour la vérifier en même temps.
La méthode : Les auteurs ont rendu leur méthode « parallélisable », ce qui signifie qu'elle peut utiliser plusieurs processeurs informatiques à la fois pour vérifier différentes parties du système simultanément. Cela rend le processus de vérification incroyablement rapide.

Ce qu'ils ont accompli

En utilisant cette approche de « zoom, ligne droite et vérification en équipe », ils ont pu :

Aller plus vite : Ils ont vérifié des systèmes jusqu'à 820 fois plus vite que les meilleures méthodes précédentes.
Aller plus loin : Ils ont pu gérer des systèmes beaucoup plus grands et complexes (jusqu'à 7 dimensions) auxquels les méthodes précédentes renonçaient.
Être plus précis : Ils ne se sont pas contentés de dire « c'est sûr » ou « c'est dangereux ». Ils ont pu identifier précisément où c'était sûr et où cela pourrait échouer, même si l'ensemble du système n'était pas parfait.

Deux Nouvelles Aventures

Les auteurs ont également montré que cette méthode fonctionne pour deux tâches délicates nouvelles :

Compression d'IA : Ils ont pris un modèle d'IA énorme et hypertrophié (comme une encyclopédie géante) et l'ont réduit en une version minuscule (comme un guide de poche) tout en prouvant que la version minuscule agit presque exactement comme la géante.
Prédiction de trajectoires avec les opérateurs de Koopman : Ils ont utilisé leur méthode pour vérifier une IA qui prédit toute la trajectoire future d'un système (comme une balle roulant le long d'une colline) d'un seul coup, plutôt que de prédire seulement l'étape suivante. Cela est utile pour guider des engins spatiaux ou contrôler des robots.

En résumé :
Ce document propose une nouvelle façon super rapide de prouver qu'un « dessin animé » d'IA d'une machine complexe est assez sûr pour être utilisé. Au lieu de vérifier tout l'ensemble d'un coup avec une méthode lente de force brute, ils le décomposent en petits morceaux, vérifient les morceaux avec des mathématiques simples, et ne zooment que là où c'est nécessaire. Cela nous permet de faire confiance à l'IA dans des situations critiques pour la sécurité où nous ne le pouvions pas auparavant.

Résumé technique : Approximations neuronales certifiées de la dynamique non linéaire

Énoncé du problème

Les systèmes dynamiques non linéaires sont fondamentaux pour les systèmes cyber-physiques, mais ils sont difficiles à vérifier et à contrôler directement. Une stratégie courante consiste à construire une abstraction — un modèle simplifié qui approxime le système d'origine. Les réseaux de neurones sont devenus des outils efficaces à cette fin, capables de partitionner implicitement les espaces d'états et d'apprendre des dynamiques simplifiées.

Cependant, pour que ces abstractions neuronales soient sûres dans des applications critiques, elles doivent s'accompagner de garanties formelles concernant leur proximité avec le système réel. Plus précisément, il faut pouvoir certifier que le réseau de neurones $N(x)$ approxime la dynamique réelle $f(x)$ avec une erreur bornée $\epsilon$ (c'est-à-dire $\|f(x) - N(x)\|_\infty \le \epsilon$ ) sur un domaine donné.

Les méthodes de vérification existantes reposent fortement sur les solveurs SMT (Satisfiabilité Modulo Théories) (par exemple, dReal) pour raisonner sur l'arithmétique réelle non linéaire. Bien que robustes, ces solveurs souffrent de graves limitations de passage à l'échelle, échouant souvent à vérifier des réseaux plus larges ou des systèmes de dimension supérieure dans des délais raisonnables. Ce goulot d'étranglement computationnel restreint l'application pratique des abstractions neuronales à des scénarios complexes et de haute dimension.

Méthodologie

Les auteurs proposent un nouveau cadre de vérification évolutif qui élimine le recours aux coûteux solveurs SMT pour l'arithmétique non linéaire. Au lieu de cela, la méthode exploite des modèles de Taylor de premier ordre certifiés et une stratégie de partitionnement adaptatif parallélisable.

1. Modèles de Taylor de premier ordre certifiés

Plutôt que de vérifier directement le prédicat non linéaire $\exists x : \|f(x) - N(x)\| > \epsilon$ , la méthode approxime la dynamique réelle $f(x)$ localement à l'aide d'expansions de Taylor de premier ordre.

Linéarisation locale : Le domaine d'entrée $X$ est partitionné en hyperrectangles. Dans chaque hyperrectangle $H_\delta(c)$ centré en $c$ , la dynamique est bornée par une fonction linéaire plus un terme de reste :
$f(x) \in (f(c) + J_f(c)(x - c)) \oplus R$
où $J_f(c)$ est la Jacobienne et $R$ est une borne d'erreur certifiée dérivée de la borne d'erreur de Lagrange (pour les fonctions lisses) ou de CROWN (pour les réseaux ReLU).
Vérification via des solveurs linéaires : Cette transformation convertit le problème de vérification en une vérification de la satisfaisabilité d'inégalités linéaires. Les auteurs utilisent Marabou 2.0, un outil de vérification de réseaux de neurones basé sur la propagation de bornes linéaires, pour vérifier ces conditions. Cela évite le coût computationnel du raisonnement arithmétique non linéaire.

2. Raffinement de certificat adaptatif

Pour remédier au conservatisme introduit par les approximations linéaires (où la borne d'erreur $R$ peut être trop lâche), le cadre emploie une stratégie de raffinement adaptatif :

Critères de division : Un hyperrectangle est divisé si :
1. La borne du reste de Taylor est trop conservatrice ( $R_{max} - R_{min} > \epsilon$ ).
2. Un contre-exemple potentiel trouvé par le solveur ne satisfait pas la condition d'erreur réelle (un contre-exemple « spécieux » dû à la linéarisation).
Partitionnement ciblé : L'axe de division est choisi en fonction de la contribution des dimensions d'entrée à l'erreur d'approximation, en privilégiant les dimensions impliquées dans les termes non linéaires. Cela permet un raffinement dépendant de la sortie, où différentes dimensions de sortie peuvent nécessiter des niveaux de partitionnement différents.
Parallélisation : Le processus de vérification est parallélisé à l'aide d'une pile partagée (recherche en profondeur) accessible par un pool de processus de travail. Chaque processus traite un hyperrectangle, le certifie ou le divise et réinjecte les sous-régions dans la pile.

3. Entraînement

Les réseaux de neurones sont entraînés pour minimiser à la fois l'erreur quadratique moyenne et l'erreur $L_\infty$ maximale sur des entrées échantillonnées. La fonction de perte inclut un terme pour l'erreur du pire cas afin d'améliorer l'efficacité de l'échantillonnage pour la vérification.

Contributions clés

Vérification sans SMT : L'introduction d'une méthode basée sur des linéarisations certifiées qui élimine le principal goulot d'étranglement computationnel (le raisonnement sur l'arithmétique réelle non linéaire) des approches précédentes.
Raffinement parallèle adaptatif : Une stratégie évolutive permettant une vérification adaptative avec une précision non uniforme sur le domaine d'entrée, réduisant considérablement le conservatisme sans sacrifier la robustesse.
Évolutivité : La capacité de gérer des systèmes de dimension supérieure (jusqu'à 7D) et des réseaux de neurones nettement plus grands que les méthodes de l'état de l'art.
Nouvelles applications : L'extension des abstractions neuronales à deux scénarios auparavant intraitables :
- Compression de réseaux de neurones : Vérifier qu'un réseau compressé reste $\epsilon$ -proche d'un réseau « enseignant » plus large.
- Découverte d'opérateurs de Koopman : Vérifier les prédictions de trajectoire où la sortie du réseau représente une séquence d'états futurs (plus de 100 états dans la dernière couche).

Résultats expérimentaux

La méthode a été évaluée sur des benchmarks établis de la littérature (ex. WaterTank, JetEngine, Van der Pol Oscillator) et sur de nouvelles tâches exigeantes.

Performance vs État de l'art : Comparée à l'approche basée sur dReal (Abate et al., 2022), la méthode proposée a démontré des accélérations substantielles. Par exemple, sur le benchmark WaterTank, la nouvelle méthode était environ 820 fois plus rapide. Alors que dReal a dépassé le temps imparti (limite d'une heure) sur la plupart des grands modèles (ex. architecture 3x[64] pour JetEngine, SteamGovernor), la méthode proposée a réussi à certifier 100 % du domaine pour tous les modèles testés, y compris les systèmes de haute dimension comme le Low Thrust Spacecraft (7D).
Opérateurs de Koopman : Le cadre a vérifié avec succès un réseau de prédiction de trajectoire basé sur la théorie de Koopman. Malgré un faible taux d'erreur quadratique moyenne sur les données de validation, la vérification a identifié des contre-exemples spécifiques où l'erreur dépassait la tolérance ( $\epsilon=0.1$ ). Crucialement, elle a certifié 99,03 % du domaine d'entrée, fournissant une vision granulaire de là où le modèle est fiable, une capacité absente des méthodes qui ne renvoient qu'un seul contre-exemple.
Compression neuronale : La méthode a vérifié un réseau compressé (réduit de 4,2M à 67k paramètres, soit une réduction de 98,4 %) approximant la dynamique de l'attracteur de Lorenz. Le processus de vérification a contrôlé plus de 3,5 millions d'hyperrectangles, se terminant en environ 89 heures, démontrant la faisabilité pour des dynamiques non analytiques de grande échelle.

Signification et affirmations

L'article affirme que sa principale signification réside dans la résolution du goulot d'étranglement de l'évolutivité de la vérification des abstractions neuronales. En découplant la vérification du réseau de neurones (gérée par des solveurs linéaires) de la vérification de la dynamique non linéaire (gérée via la linéarisation locale et le raffinement), les auteurs permettent la vérification formelle de systèmes complexes et de haute dimension qui étaient auparavant intraitables.

Les auteurs soulignent que leur approche fournit des bornes d'erreur formelles qui permettent d'utiliser les approximations neuronales en toute sécurité comme substituts en interprétant l'erreur comme des perturbations bornées. Cette robustesse permet aux propriétés vérifiées sur l'abstraction (telles que la sûreté ou la réachabilité) d'être rigoureusement transférées au système concret. Le travail met également en évidence la polyvalence du cadre, montrant qu'il peut être appliqué au-delà des systèmes dynamiques standards à des tâches générales d'approximation de fonctions comme la compression de réseaux et les architectures de deep learning pour la théorie des opérateurs.