Training with Hard Constraints: Learning Neural Certificates and Controllers for SDEs

1. Problématique et Contexte

Le papier aborde le problème de la synthèse de contrôleurs et de certificats de sécurité pour des systèmes dynamiques continus régis par des Équations Différentielles Stochastiques (EDS). L'objectif spécifique est de garantir des propriétés de type « atteindre-éviter » (reach-avoid) : assurer qu'un système, partant d'un ensemble initial $X_0$, atteint un ensemble objectif $X_g$ sans jamais entrer dans un ensemble dangereux $X_u$.

Défis principaux :

• Garanties formelles : Les performances empiriques des réseaux de neurones (RN) sont insuffisantes pour les applications critiques. Il faut des garanties mathématiques que les contraintes sont satisfaites sur tout le domaine continu.
• Contraintes dures (Hard Constraints) : La théorie des surmartingales exige que certaines inégalités (liées à la fonction de certificat $V$ et son générateur infinitésimal $\mathcal{G}[V]$) soient satisfaites strictement partout dans le domaine.
• Limites des méthodes existantes :
  • Les méthodes « soft » (pénalités dans la fonction de perte) ne garantissent pas la satisfaction des contraintes en dehors de l'ensemble d'entraînement.
  • Les méthodes « vérificateur-apprenant » (Learner-Verifier) utilisant des solveurs SMT ou des partitions d'espace souffrent d'une mauvaise évolutivité (curse of dimensionality) et de contraintes restrictives (dynamiques linéaires/polynomiales).

2. Méthodologie

Les auteurs proposent deux cadres d'entraînement complémentaires pour encoder directement les contraintes dures dans l'apprentissage des réseaux de neurones.

A. Approche par Bornes (Bound-Training / Hard-SAT)

Cette méthode vise à garantir la satisfaction des contraintes sur l'ensemble du domaine via une discrétisation adaptative.

• Principe : L'espace d'état est partitionné en cellules. Pour chaque cellule, on calcule des bornes analytiques (via l'arithmétique des intervalles) sur la valeur du réseau de neurones $V_\theta$ et sur son générateur infinitésimal $\mathcal{G}[V_\theta]$.
• Fonction de perte : Une perte basée sur les bornes ($L_{bound}$) est définie. Elle somme les violations potentielles (via des fonctions ReLU) sur toutes les cellules.
  • Si $L_{bound} = 0$, alors les contraintes sont garanties pour tout $x$ dans le domaine (théorème de validité).
• Optimisation conjointe : Cette approche permet d'entraîner simultanément le certificat $V_\theta$ et le contrôleur $\pi_{\theta_\pi}$ en rétropropageant à travers un graphe de calcul différentiable dérivé de la dynamique de l'EDS fermée.
• Stratégies d'efficacité : Pour gérer l'explosion combinatoire des cellules en haute dimension, l'algorithme utilise :
  • Un raffinement adaptatif (split) des cellules où les contraintes sont violées.
  • Un mécanisme de fusion (merging) des cellules adjacentes qui satisfont déjà les contraintes avec une marge.
• Limites : Méthode exacte (garantie absolue), mais limitée en pratique aux systèmes jusqu'à 5 dimensions (5D) en raison de la complexité de la partition.

B. Approche par Scénarios (Scenario-based Training / PAC)

Pour les systèmes de haute dimension (au-delà de 5D), où la partition est impossible, les auteurs proposent une méthode statistique basée sur l'optimisation de scénarios.

• Principe : Au lieu de partitionner l'espace, on échantillonne un ensemble fini d'états $\hat{X}$.
• Formulation : On optimise uniquement les paramètres de la dernière couche du réseau de certificat (les poids et biais linéaires), en supposant que les couches précédentes sont figées (après un pré-entraînement).
• Garanties PAC : En utilisant la théorie de l'approche convexe par scénarios (Campi et al.), on obtient des garanties Probablement Approximativement Correctes (PAC).
  • Avec une confiance $1-\delta$, les contraintes sont satisfaites partout sauf sur un ensemble de mesure $\le \epsilon$.
  • La complexité en échantillons est indépendante de la dimension de l'espace d'état.
• Avantage : Évolutivité jusqu'à 10 dimensions et au-delà, avec des garanties arbitrairement serrées en augmentant le nombre d'échantillons.

3. Contributions Clés

1. Framework Hard-SAT : Un cadre d'entraînement par bornes qui garantit la validité d'un certificat de surmartingale pour les EDS dès que la fonction de perte atteint zéro. C'est la première méthode à fournir des garanties globales pour des réseaux de neurones sur des EDS continues.
2. Synthèse Conjointe : Extension du cadre pour l'entraînement simultané du contrôleur et du certificat, guidant l'apprentissage du contrôleur vers des politiques non seulement performantes mais aussi vérifiables.
3. Méthode PAC Évolutif : Une approche sans partition, basée sur l'optimisation de scénarios linéaires (sur la dernière couche), permettant de traiter des systèmes de haute dimension (10D+) avec des garanties de confiance élevées.
4. Évaluation Empirique : Démonstration de la supériorité de la méthode par rapport à l'état de l'art (notamment Neustroev et al., 2025) en termes de temps de calcul et de capacité à traiter des dimensions plus élevées.

4. Résultats Expérimentaux

Les auteurs ont évalué leurs méthodes sur plusieurs benchmarks, incluant un pendule inversé stochastique, des mouvements browniens géométriques (GBM) de dimensions 2 à 10, un système de Lorenz stochastique et un avion tilt-rotor (XV-15).

• Vérification (Certificat seul) :
  • La méthode Hard-SAT a réussi à certifier des systèmes jusqu'à 5D, surpassant la méthode de l'état de l'art qui échouait souvent ou nécessitait des temps de calcul prohibitifs.
  • La méthode PAC a réussi à certifier des systèmes jusqu'à 10D avec une probabilité de réussite de 99,99% et une erreur de mesure négligeable ($\epsilon \approx 10^{-4}$).
• Synthèse de Contrôle (Contrôleur + Certificat) :
  • L'algorithme Hard-SAT a réussi à synthétiser des contrôleurs neuronaux pour 4 systèmes complexes (y compris le Lorenz 3D et le XV-15 3D).
  • Les simulations de Monte Carlo ont confirmé une probabilité d'atteinte-évitement empirique de 1,0 pour tous les systèmes bouclés.
  • Les visualisations montrent que les trajectoires contrôlées évitent efficacement les zones dangereuses et atteignent l'objectif, contrairement aux trajectoires non contrôlées ou pré-entraînées sans garantie.

5. Signification et Impact

Ce travail représente une avancée significative dans le domaine du contrôle formel des systèmes stochastiques basés sur l'apprentissage automatique :

• Transition du "Soft" au "Hard" : Il démontre qu'il est possible d'intégrer des contraintes mathématiques strictes directement dans le processus d'entraînement des réseaux de neurones, éliminant le besoin de vérification post-hoc incertaine.
• Évolutivité : En combinant une approche exacte (pour les dimensions moyennes) et une approche statistique (pour les hautes dimensions), le papier offre une solution pratique pour des problèmes réels complexes (comme le contrôle d'aéronefs ou de systèmes biologiques) qui étaient auparavant hors de portée des méthodes formelles.
• Robustesse : La capacité à garantir la sécurité sous incertitude stochastique est cruciale pour le déploiement de l'IA dans des applications critiques (robotique, aviation, systèmes autonomes).

En résumé, le papier propose une boîte à outils complète pour apprendre des politiques de contrôle et des certificats de sécurité pour des systèmes stochastiques, en offrant un compromis contrôlé entre la rigueur des garanties (Hard-SAT) et l'évolutivité computationnelle (PAC).