💻 computer science

Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning

L'article présente RNN-ProVe, un cadre probabiliste qui estime la probabilité de comportements indésirables dans des politiques basées sur des réseaux de neurones récurrents pour l'apprentissage par renforcement à agent unique et multi-agents, en utilisant un échantillonnage piloté par la politique pour surmonter les limites des outils de vérification existants dans des environnements partiellement observables.

Auteurs originaux : Luca Marzari, Enrico Marchesini

Publié 2026-05-15

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Luca Marzari, Enrico Marchesini

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 entraînez un robot à naviguer dans un labyrinthe. Ce robot possède une « mémoire » spéciale (un réseau de neurones récurrent, ou RNN) qui l'aide à se souvenir de son parcours, afin qu'il ne réagisse pas uniquement à ce qu'il voit à l'instant présent, mais qu'il prenne des décisions basées sur l'ensemble de son trajet jusqu'ici.

Le problème est le suivant : Comment savoir si ce robot ne va pas accidentellement percuter un mur ?

L'ancienne méthode : La supposition du « pire cas »

Les vérificateurs de sécurité traditionnels tentent de prouver que le robot est sûr en examinant toutes les choses possibles qui pourraient jamais se produire. Ils imaginent chaque mémoire possible que le robot pourrait avoir, même celles qui sont impossibles dans la vie réelle (comme un robot se souvenant d'un mur qui n'existe pas).

Parce qu'ils doivent vérifier chaque possibilité unique, y compris les impossibles, ils sont souvent bloqués. C'est comme essayer de trouver une aiguille spécifique dans une botte de foin en examinant chaque brin de paille, même ceux qui n'ont jamais été dans la grange dès le départ. Cela rend le processus incroyablement lent, et souvent, ils abandonnent en disant : « Nous ne pouvons pas être sûrs », ou ils supposent que le robot est dangereux simplement pour être prudents, ce qui n'est pas très utile.

La nouvelle méthode : RNN-ProVe (Le détective de la « vie réelle »)

Les auteurs de cet article, Luca Marzari et Enrico Marchesini, ont créé un nouvel outil appelé RNN-ProVe. Au lieu de vérifier chaque fantasme impossible, ils posent une question plus intelligente : « Quelles sont les réelles mémoires que ce robot a accumulées pendant son apprentissage ? »

Voici comment cela fonctionne, en utilisant une analogie simple :

1. L'« Oracle de faisabilité » (Le filtre de mémoire)

Imaginez que le robot ait effectué des milliers de sessions d'entraînement. Pendant ce temps, il a constitué un ensemble spécifique de mémoires « réelles ».

Les anciens outils examinent toute la bibliothèque de toutes les mémoires possibles (y compris les fausses).
RNN-ProVe entraîne un « Filtre de mémoire » spécial (un classifieur). Ce filtre apprend à distinguer une mémoire réelle (celle que le robot a réellement vécue) d'une mémoire fausse (celle qui ne pourrait jamais se produire).

Pensez-y comme à un videur dans une boîte de nuit. Le videur (le filtre) vérifie votre pièce d'identité. Si votre pièce d'identité indique que vous étiez réellement à la fête (un historique faisable), vous entrez. Si votre pièce d'identité est fausse (un historique impossible), vous êtes refoulé. RNN-ProVe ne vérifie la sécurité que des personnes qui ont réellement réussi à passer le videur.

2. La vérification de « Probabilité » (Le compteur de risque)

Une fois que le filtre a séparé les mémoires réelles des fausses, RNN-ProVe ne tente pas de vérifier chaque mémoire réelle (ce qui est encore trop difficile). Au lieu de cela, il prend un échantillon aléatoire des mémoires réelles.

Il se demande : « Sur 1 000 mémoires réelles que nous avons sélectionnées, combien ont conduit à un crash ? »

Si 10 sur 1 000 ont conduit à un crash, il ne dit pas « Le robot est dangereux ».
Il dit : « Il y a 1 % de chances que le robot percute dans cette situation spécifique, et nous sommes 99 % sûrs que ce chiffre est exact. »

C'est comme un prévisionniste météorologique. Au lieu de dire « Il va pleuvoir à coup sûr » ou « Il ne pleuvra pas à coup sûr », il dit : « Il y a 30 % de chances de pluie, basé sur les données que nous avons ». Cela donne une réponse beaucoup plus utile et quantitative.

Pourquoi cela compte

L'article a testé cela sur deux types de jeux :

Agent unique : Un robot naviguant dans une grille.
Multi-agents : Deux robots travaillant ensemble pour pousser une boîte.

Les résultats :

Vitesse : Les anciens outils prenaient des minutes ou des heures pour vérifier de petites grilles et abandonnaient pour les plus grandes. RNN-ProVe a effectué les mêmes vérifications en millisecondes.
Précision : Les anciens outils trouvaient souvent de « faux » problèmes (fausses alertes) parce qu'ils vérifiaient des mémoires impossibles. RNN-ProVe a ignoré les impossibles et a trouvé les vrais risques.
Travail d'équipe : Les anciens outils ne pouvaient pas gérer des équipes de robots travaillant ensemble. RNN-ProVe a géré l'équipe multi-agents parfaitement, vérifiant si n'importe quel membre de l'équipe pourrait faire une erreur.

La conclusion

RNN-ProVe est une nouvelle façon de vérifier la sécurité de l'IA qui cesse d'essayer de vérifier chaque scénario impossible. Au lieu de cela, il se concentre sur ce qui se produit réellement pendant l'entraînement. En filtrant l'impossible et en échantillonnant le réel, il nous offre un « pourcentage de risque » mathématique, rapide et fiable, indiquant à quelle fréquence un robot intelligent pourrait faire une erreur.

Il transforme un problème mathématique effrayant et insoluble en une estimation statistique gérable qui nous dit exactement à quel point notre IA dépendante de l'historique est réellement sûre.

Résumé technique : Vérification probabiliste des RNN (RNN-ProVe)

Énoncé du problème

Les réseaux de neurones récurrents (RNN) sont largement utilisés en apprentissage par renforcement (RL) pour gérer l'observabilité partielle et la coordination multi-agents en maintenant des états cachés latents qui encodent l'historique des interactions. La vérification de ces politiques est fondamentalement difficile car le processus de prise de décision dépend de l'ensemble de l'historique des observations et des actions, et non uniquement de l'entrée actuelle.

Les outils de vérification existants pour les RNN se concentrent principalement sur l'analyse de robustesse face à des perturbations d'entrée bornées sur un horizon fixe. Ces méthodes reposent généralement sur des sur-approximations géométriques grossières (par exemple, des intervalles ou des hyperrectangles) de l'espace des états cachés. Dans le contexte du RL, cette approche admet des états cachés spuriaires — des combinaisons de valeurs de neurones mathématiquement possibles dans les limites du réseau mais non réalisables compte tenu de la politique spécifique et de la dynamique de l'environnement. Par conséquent, ces outils produisent souvent des résultats excessivement conservateurs ou de faux positifs.

De plus, la vérification exacte des politiques basées sur les RNN nécessite d'énumérer toutes les configurations d'états cachés accessibles pour vérifier l'existence de comportements indésirables. Ce problème équivaut au calcul des mesures d'antécédents des réseaux de neurones, ce qui est #P-difficile en raison de la non-linéarité et de la non-convexité des réseaux de neurones. La caractérisation exacte est computationnellement irréalisable pour des politiques non triviales, et les méthodes existantes ne parviennent pas à s'adapter aux paramètres multi-agents ou aux espaces de haute dimension.

Méthodologie : RNN-ProVe

Les auteurs proposent la Vérification Probabiliste des RNN (RNN-ProVe), un cadre qui passe de la vérification exacte du pire cas à une vérification probabiliste sur les historiques réalisables. Au lieu de tenter d'énumérer tous les états cachés possibles, RNN-ProVe estime la probabilité de comportements indésirables en quantifiant le volume de l'espace des états cachés réalisables menant à des violations.

Le cadre fonctionne en trois phases principales :

Apprentissage d'un oracle de faisabilité :
- Pendant la phase d'entraînement du RL, l'agent explore l'environnement, générant un ensemble de données de paires état-état caché $(s, h)$ .
- RNN-ProVe entraîne un classificateur de faisabilité $C: S \times H \to \{0, 1\}$ sur cet ensemble de données. Ce classificateur apprend à distinguer les états cachés réellement accessibles sous la politique entraînée (réalisables) de ceux qui ne le sont pas (non réalisables).
- Cette étape exploite le théorème d'approximation universelle pour approximer la variété complexe et de dimension inférieure des historiques réalisables au sein de l'espace des états cachés de haute dimension.
Échantillonnage et vérification pilotés par la politique :
- Pour un état spécifique d'intérêt, la méthode échantillonne des vecteurs d'historique candidats depuis le domaine des états cachés.
- Le classificateur entraîné $C$ agit comme un oracle, filtrant les échantillons non réalisables et ne conservant que les états cachés $h^*$ correspondant à des historiques d'interaction valides menant à l'état actuel.
- La politique est ensuite évaluée sur ces historiques validés pour déterminer s'ils entraînent une violation (par exemple, la sélection d'une action non sûre).
Estimation statistique avec bornes d'erreur :
- Le cadre calcule le rapport entre les historiques validés violants et le nombre total d'historiques validés pour estimer le volume de violation.
- Crucialement, RNN-ProVe dérive des bornes de confiance statistiques en utilisant l'inégalité de Hoeffding. Il décompose la tolérance d'erreur totale $\epsilon$ $ϵ$ et le paramètre de confiance $\delta$ $δ$ en deux composantes :
  - Erreur du classificateur : La précision de l'oracle de faisabilité.
  - Variance d'échantillonnage : L'erreur statistique provenant de l'estimation par Monte Carlo.
- Cela permet au cadre de produire des certificats à erreur bornée et à haute confiance concernant la probabilité de violations comportementales.

Contributions clés

L'article fait les contributions spécifiques suivantes :

Formulation du problème : Il définit formellement le problème de la vérification probabiliste pour les politiques RL récurrentes sous observabilité partielle, en tenant explicitement compte de l'ensemble des états cachés réalisables induits par une politique entraînée.
Cadre RNN-ProVe : Il introduit un cadre novateur combinant l'apprentissage de faisabilité et l'estimation par Monte Carlo pour évaluer quantitativement les violations comportementales dans les politiques basées sur les RNN.
Extension multi-agents : Il étend le problème de vérification au RL multi-agents (MARL) entièrement coopératif. Il dérive des garanties à erreur bornée et à haute confiance pour l'identification d'historiques réalisables et l'estimation de violations dans des contextes décentralisés, offrant une approximation traitable d'un problème autrement #P-difficile.
Garanties théoriques : Il fournit une preuve théorique (Théorème 2) que le volume de violation estimé satisfait des bornes d'erreur et de confiance spécifiques, sous réserve des tailles d'échantillons de la validation du classificateur et de l'échantillonnage de vérification.

Résultats expérimentaux

Les auteurs ont évalué RNN-ProVe sur des tâches de navigation en agent unique et des tâches coopératives multi-agents "BoxPushing" (BP) utilisant des politiques DRQN.

Évolutivité : RNN-ProVe a démontré des avantages significatifs en matière d'évolutivité. Dans les tâches de navigation, les méthodes de base basées sur la linéarisation nécessitaient de minutes à des heures pour de petits environnements (4x4, 8x8) et ont expiré sur des environnements plus grands (16x16). En revanche, RNN-ProVe a produit des résultats quantitatifs en millisecondes pour toutes les tailles de grille testées.
Précision par rapport aux bases de référence :
- Comparé au Monte Carlo naïf (échantillonnage uniforme sans filtrage de faisabilité), RNN-ProVe a fourni des estimations précises. L'échantillonnage naïf a produit des taux de violation considérablement gonflés (par exemple, ~23 % contre ~1,6 % en 4x4) car il testait des états cachés non réalisables qui ne se produisent pas en pratique.
- Comparé aux bases de référence de linéarisation exacte (lorsque possible), RNN-ProVe a produit des estimations de violation comparables (par exemple, ~1,42 % contre ~1,44 % en 4x4) mais avec des garanties probabilistes et un temps de calcul inférieur de plusieurs ordres de grandeur.
Performance multi-agents : Le cadre a vérifié avec succès des politiques coopératives dans le domaine BP (grilles 10x10 et 20x20), identifiant des taux de violation moyens d'environ 1,18 % et 1,7 %, respectivement. Les outils existants ne pouvaient pas être appliqués directement à ces contextes coopératifs.
Insight : Les expériences ont révélé que même les politiques avec des retours moyens élevés présentent une généralisation non uniforme à travers les états cachés réalisables, avec des sensibilités spécifiques près des obstacles que les évaluations empiriques standard ne détectent pas.

Importance et affirmations

L'article soutient que la vérification exacte du pire cas pour les politiques RL récurrentes est non seulement computationnellement prohibitive, mais aussi inadaptée à la structure de la prise de décision dépendante de l'historique. Les auteurs affirment que la vérification probabiliste sur les historiques réalisables n'est pas simplement un relâchement heuristique, mais une réponse fondée sur des principes aux barrières computationnelles fondamentales.

En se concentrant sur l'ensemble des états cachés réellement accessibles sous une politique, RNN-ProVe fournit des garanties probabilistes quantitatives et conscientes de la faisabilité. Cette approche produit des certificats plus informatifs que les résultats binaires "sûr/insûr" ou les vérifications de robustesse excessivement conservatrices, permettant une meilleure compréhension de la fiabilité et de la généralisation des politiques dans des environnements complexes, partiellement observables et multi-agents. L'ouvrage plaide en faveur de cette perspective probabiliste comme approche fondamentale pour raisonner sur la sécurité dans les systèmes dépendants de l'historique.