Résumé technique : Apprentissage par renforcement contraint par la sécurité avec vérification de la faisabilité post-entraînement pour la navigation robotique

1. Formulation du problème

L'article aborde le défi critique du déploiement de robots mobiles autonomes dans des environnements encombrés où l'incertitude de la perception (par exemple, le bruit des capteurs) peut entraîner des défaillances catastrophiques. Les auteurs soutiennent que les métriques de sécurité standard de l'apprentissage par renforcement (RL), qui reposent sur le coût cumulatif moyen, sont insuffisantes car elles masquent les comportements à « risque de queue » — des événements rares mais aux conséquences élevées où une politique pourrait entrer en collision malgré un coût moyen faible.

Le problème est formalisé comme un Processus de Décision Markovien Contraint (CMDP). Contrairement aux CMDP traditionnels qui contraignent le coût cumulatif attendu $E[C_\pi] \leq b$, ce travail cherche une politique $\pi$ qui maximise la récompense attendue tout en satisfaisant une contrainte de Valeur à Risque Conditionnelle (CVaR) :
$$\max_{\pi} J_R(\pi) \quad \text{s.t.} \quad \text{CVaR}_\alpha(C_\pi) \leq b$$
Ici, $\text{CVaR}_\alpha$ représente le coût attendu dans la pire fraction $(1-\alpha)$ des épisodes, ciblant explicitement la queue de la distribution des coûts plutôt que la moyenne.

De plus, l'article identifie un écart entre les garanties statistiques d'entraînement et la vérification formelle de la sécurité. Une politique avec des statistiques CVaR favorables peut encore produire des actions non sécurisées sous une incertitude d'observation bornée. Par conséquent, l'objectif est d'unifier l'entraînement sensible au risque avec la vérification de la faisabilité des réseaux de neurones post-entraînement pour garantir que les sorties d'action de la politique restent dans les marges de sécurité même lorsque les entrées sont perturbées.

2. Méthodologie : Le cadre VIA

Le cadre proposé, VIA (Vérification-Informed safe reinforcement learning for Autonomous navigation), fonctionne en deux phases distinctes :

Phase I : Entraînement hors politique contraint par CVaR

Les auteurs adaptent l'algorithme hors politique TD3 (Twin Delayed DDPG) pour optimiser les contraintes CVaR. Les composants techniques clés incluent :

• Augmentation de l'état : Pour estimer le CVaR dans un contexte hors politique, l'espace d'état est augmenté d'une variable dynamique de budget de coût $e_t$. L'état augmenté est $\bar{s}_t = (s_t, e_t)$, où $e_t$ suit l'historique des coûts accumulés, permettant au critique de distinguer les états atteints sous différents historiques de coûts.
• Critic de coût distributionnel : Au lieu d'estimer une seule valeur de coût attendue, le critic de coût $Q^C_\phi$ sort $M$ quantiles de la distribution du coût cumulatif. Pour prévenir le « problème de croisement » (où les quantiles prédits violent la monotonie), un réseau de logits de quantiles non croissants est employé en utilisant une paramétrisation spécifique impliquant une sommation softmax cumulative.
• Mise à jour adaptative de la VaR : Un défi critique dans l'optimisation CVaR hors politique est de suivre le seuil de quantile de la Valeur à Risque (VaR) sans évaluations en politique. Les auteurs introduisent une règle de mise à jour sans gradient pour le paramètre VaR $u$ basée sur la probabilité d'excès empirique des coûts dans le tampon de rejeu, assurant une convergence stable vers le quantile cible.
• Optimisation Lagrangienne : La politique est optimisée en utilisant une relaxation Lagrangienne de l'objectif contraint par CVaR. La perte de l'acteur combine le critic de récompense de la tâche et le coût CVaR estimé, pondérés par un multiplicateur de Lagrange $\lambda$ qui est mis à jour en fonction de la marge de contrainte empirique.

Phase II : Vérification de la faisabilité post-entraînement

Après l'entraînement, le cadre effectue une évaluation formelle de la sécurité en utilisant POLAR (Polynomial Arithmetic for Reachability), un outil qui combine l'arithmétique des modèles de Taylor (TM) avec l'interpolation par polynômes de Bernstein.

• Analyse de faisabilité : Étant donné une incertitude d'observation bornée $\epsilon$, la méthode propage les TM à travers le réseau de neurones entraîné pour calculer un ensemble d'actions atteignables garanti $A(s, \epsilon)$. Cet ensemble représente toutes les actions possibles que la politique pourrait produire étant donnée l'incertitude d'entrée.
• Métrique de taux de sécurité : Les auteurs définissent une métrique de Taux de Sécurité. Pour un état donné, ils échantillonnent des actions à partir des bornes de l'ensemble atteignable (incluant les extrémités et les milieux) et simulent le mouvement du robot. Un état est « vérifié sûr » si toutes les actions échantillonnées résultent en des trajectoires sans collision. Le Taux de Sécurité est la proportion d'états évalués qui satisfont ce critère.
• Intégration : L'article postule que l'entraînement contraint par CVaR façonne naturellement la politique vers des distributions d'action conservatrices et étroitement bornées, rendant les ensembles atteignables résultants plus petits et plus propices à la vérification formelle par rapport aux bases de référence fondées sur l'espérance.

3. Contributions clés

1. Cadre TD3 contraint par CVaR : La conception d'un cadre d'optimisation CVaR hors politique comprenant un critic de coût distributionnel avec régression de quantiles non croissants et un mécanisme de mise à jour adaptative de la VaR pour stabiliser la convergence des quantiles.
2. Métrique de sécurité informée par la vérification : Le développement d'un cadre de vérification de sécurité combinant l'analyse de faisabilité POLAR avec des limites de sécurité en couches, introduisant la métrique de Taux de Sécurité pour quantifier la robustesse de la politique sous une incertitude d'observation bornée.
3. Validation empirique : Validation complète en simulation à travers dix scénarios de navigation et six bases de référence, ainsi qu'un transfert réussi sim-to-real sur un robot physique Clearpath Jackal.

4. Résultats expérimentaux

Les expériences ont été menées dans une simulation Gazebo (arène de 10m $\times$ 10m avec obstacles) et sur un robot physique.

• Performance vs. Bases de référence : VIA a atteint le Taux de Succès le plus élevé (98,3 %) et le Taux de Collision le plus faible (1,7 %) parmi toutes les méthodes comparées (incluant TD3, SAC-Lagrangien, RCPO, WCSAC et CVaR-CPO).
• Divergence des métriques : Une découverte clé est la divergence entre les classements de coûts moyens et les classements de sécurité basés sur la faisabilité. Par exemple, RCPO a atteint le coût moyen le plus faible (1,17) mais un Taux de Sécurité inférieur (98,5 % pour les épisodes réussis) par rapport à VIA (99,6 %). Cela démontre que les métriques de coût moyen peuvent manquer des risques latents que la vérification formelle capture.
• Impact de $\alpha$ : Des études d'ablation ont montré que l'augmentation du niveau de confiance CVaR $\alpha$ (se concentrant sur des queues plus extrêmes) a amélioré à la fois les taux de succès et les métriques de sécurité, avec $\alpha=0,9$ produisant les performances les plus conservatrices et robustes.
• Transfert sim-to-real : Lorsqu'il a été déployé sur un robot Clearpath Jackal, le taux de succès a chuté à 90,0 % en raison du bruit physique et des délais, mais le Taux de Sécurité Global est resté presque identique à celui de la simulation (99,2 % contre 99,1 %), confirmant que la politique maintient des marges de sécurité vérifiées dans le monde réel.

5. Signification et affirmations

L'article affirme que la vérification de la faisabilité capture les risques manqués par les métriques de coût empiriques seules. En combinant un entraînement sensible au risque (CVaR) avec une vérification formelle post-entraînement, les auteurs démontrent que des politiques peuvent être entraînées non seulement pour être sûres en moyenne, mais pour maintenir des marges de sécurité sous incertitude.

Les auteurs déclarent que ce travail est le premier à intégrer l'optimisation de politique contrainte par CVaR avec la vérification de la faisabilité des réseaux de neurones spécifiquement pour la navigation robotique. Ils soulignent que, bien que la vérification formelle soit coûteuse en calcul et généralement limitée aux réseaux de faible dimension ou de petite taille, leur approche utilise des architectures légères pour permettre cette intégration.

L'article conclut modestement, reconnaissant que la dépendance à l'arithmétique des modèles de Taylor restreint la complexité des réseaux de politiques vérifiables. Un travail futur est identifié comme l'exploration de méthodes de faisabilité accélérées par GPU et l'intégration de signaux de vérification directement dans la boucle d'entraînement pour une optimisation de sécurité en boucle fermée.