Résumé Technique : Les Fonctions de Valeur comme Certificats de Supermartingales

Énoncé du Problème

La vérification de systèmes stochastiques par rapport à des propriétés $\omega$-régulières (incluant la logique temporelle linéaire, LTL) sur des espaces d'états généraux (finis, dénombrablement infinis et continus) repose typiquement sur des certificats de supermartingales. Ce sont des fonctions à valeurs réelles qui satisfont des règles de preuve spécifiques, servant de garanties mathématiques pour la satisfaction presque sûre d'une spécification. Cependant, la synthèse de ces certificats est difficile ; les méthodes existantes reposent souvent sur l'optimisation sous contraintes, ce qui ne passe pas bien à l'échelle pour les espaces d'états larges ou continus.

Inversement, l'Apprentissage par Renforcement (RL) est largement appliqué pour synthétiser des politiques pour des tâches $\omega$-régulières. Bien que les méthodes de RL puissent maximiser la probabilité de satisfaction, elles manquent généralement de garanties formelles qu'une politique entraînée (non optimale) satisfait la spécification avec une probabilité donnée, particulièrement en dehors des espaces d'états et d'actions finis. Il existe un décalage entre la machinerie théorique de la vérification par supermartingales et la machinerie pratique de l'évaluation de politique par RL.

Méthodologie

Cet article établit un nouveau lien théorique entre la fonction de valeur d'une politique dans un cadre de RL avec escompte (discounted) et les certificats de supermartingales de Streett. L'hypothèse centrale est que, sous des conceptions de récompenses spécifiques, la fonction de valeur $V^\pi$ d'une politique $\pi$ qui satisfait presque sûrement une spécification LTL encode une supermartingale de Streett valide.

Les auteurs proposent deux conceptions de récompenses distinctes pour y parvenir :

1. Conception de Récompense 1 (Connaissance de l'Ensemble Absorbant) :

   • Exigence : Connaissance des ensembles absorbants induits par la politique (spécifiquement, le plus grand sous-ensemble absorbant du complément de l'union des ensembles de la paire de Streett).
   • Mécanisme : La récompense est fixée à 1 lorsque le processus entre dans l'ensemble cible $B$ ou dans un ensemble absorbant à partir duquel ni $A$ ni $B$ ne peuvent être visités à nouveau.
   • Base Théorique : La fonction de valeur $V^\pi$ représente la somme escomptée de ces récompenses. En définissant le certificat $W(s) = C - V^\pi(s)$ (où $C$ est une constante liée au facteur d'escompte), les auteurs prouvent que $W$ satisfait les conditions de la supermartingale de Streett : elle diminue strictement en espérance lorsqu'on est dans $A \setminus B$ (en raison de bornes uniformes sur les temps de premier passage) et reste non croissante ailleurs.

2. Conception de Récompense 2 (Connaissance de la Spécification Uniquement) :

   • Exigence : Uniquement la connaissance de la spécification (la paire de Streett $(A, B)$), sans nécessiter la connaissance des ensembles absorbants spécifiques de la politique.
   • Mécanisme : Cette conception utilise un facteur d'escompte dépendant de l'état $\Gamma(s)$ et une fonction de récompense qui attribue des récompenses positives pour la visite de $B$ et des récompenses négatives pour la visite de $A \setminus B$.
   • Base Théorique : Le facteur d'escompte est fixé à $\gamma < 1$ lorsque les récompenses sont non nulles et à $1$ sinon. Sous une hypothèse de « borne de récurrence positive » (limitant le nombre d'étapes attendues dans $A$ avant d'atteindre $B$), la fonction de valeur encode à nouveau une supermartingale. Le ratio des récompenses positives sur les négatives est ajusté pour garantir que le certificat reste non négatif et strictement décroissant là où cela est requis.

Les deux approches sont prouvées valables pour des espaces d'états finis, dénombrablement infinis et continus. Les preuves s'appuient sur des lemmes reliant les fonctions de valeur aux temps de premier passage et aux changements attendus d'une étape de la valeur.

Contributions Clés

• Pont Théorique : L'article prouve que la fonction de valeur d'une politique satisfaisant une spécification LTL est un certificat de supermartingale de Streett valide sous des conceptions de récompenses appropriées (Théorèmes 1 et 2).
• Deux Schémas de Récompense : Les auteurs fournissent deux méthodes distinctes pour construire ces récompenses : l'une exploitant les ensembles absorbants spécifiques à la politique (Théorème 1) et l'autre reposant uniquement sur la structure de la spécification avec un escompte dépendant de l'état (Théorème 2).
• Généralité : Les résultats ne sont pas limités aux MDP finis ; ils s'appliquent à des espaces d'états généraux, comblant un fossé dans la vérification basée sur le RL qui manque souvent de garanties formelles pour les espaces infinis ou continus.
• Validation Expérimentale : Les auteurs valident la théorie sur des processus de décision markoviens (MDP) finis en utilisant un environnement de type "grid-world". Ils synthétisent des certificats pour diverses spécifications LTL couvrant la hiérarchie de Manna-Pnueli, vérifient les règles de preuve de la supermartingale et effectuent une vérification croisée avec les probabilités de satisfaction via le vérificateur de modèles PRISM.

Résultats

• Vérification Expérimentale : Dans les expériences de grid-world, les conceptions de récompense proposées ont synthétisé avec succès des certificats valides pour des politiques qui satisfaisaient les spécifications (probabilité de satisfaction = 1.0). Pour les politiques qui ne satisfaisaient pas les spécifications, les règles de preuve ont échoué (certificats invalides), et PRISM a confirmé des probabilités de satisfaction strictement inférieures à 1.
• Cohérence : Les résultats expérimentaux s'alignent parfaitement avec les garanties théoriques, démontrant que l'approche par fonction de valeur identifie correctement les politiques satisfaisantes et non satisfaisantes.
• Limitations Expérimentales : Les expériences actuelles sont restreintes aux MDP finis où les fonctions de valeur sont calculées exactement via des systèmes linéaires. L'article note que l'extension de cela aux espaces infinis/continus utilisant des approximations paramétriques (par exemple, des réseaux de neurones) est laissée pour des travaux futurs.

Signification et Revendications

L'article affirme ouvrir une « voie fondée sur des principes pour la synthèse de certificats via le RL ». En recadrant le problème de la recherche de certificats de supermartingales (traditionnellement un problème d'optimisation sous contraintes) comme un problème d'évaluation de politique suivie d'un contrôle de certificat, les auteurs suggèrent une voie pour porter la vérification à l'échelle des espaces d'états larges et continus en utilisant des méthodes de RL basées sur les données.

Les auteurs soulignent que, bien que les théorèmes fournissent des conditions suffisantes pour que la fonction de valeur soit un certificat, le certificat lui-même est valide si les règles de preuve sont respectées, indépendamment du fait que les hypothèses du théorème (comme les bornes de temps de premier passage uniformes) soient vérifiées de manière indépendante. Cela permet un flux de travail pratique : entraîner une politique, estimer sa fonction de valeur, puis vérifier directement les conditions de la supermartingale.

L'article positionne ce travail comme une étape fondamentale vers l'apprentissage par renforcement certifié, où les politiques entraînées peuvent être formellement vérifiées pour des propriétés $\omega$-régulières au-delà des espaces d'états finis, comblant ainsi le fossé entre la scalabilité du RL et la rigueur de la vérification formelle.