Résumé technique : Surveillance de propriétés temporelles conscientes des données

Définition du problème

L'article aborde le défi de la vérification d'exécution anticipative pour des systèmes d'IA complexes et dynamiques dont les spécifications internes sont inaccessibles (systèmes boîte noire). Les méthodes traditionnelles de vérification au moment de la conception, telles que la vérification de modèles, sont souvent inapplicables dans ces scénarios. Bien que la vérification d'exécution (RV) offre une solution en surveillant les traces d'exécution, les approches existantes rencontrent deux limitations principales :

1. Nature propositionnelle : La logique temporelle linéaire standard sur les traces finies ($LTL_f$) ne peut pas exprimer des propriétés impliquant des données structurées (par exemple, l'arithmétique, les ensembles, les fonctions non interprétées), qui sont omniprésentes dans les agents d'IA modernes et les processus métier.
2. Absence d'anticipation : La plupart des moniteurs n'évaluent que le préfixe de la trace vu jusqu'à présent. Ils échouent à détecter les violations qui sont inévitables, quelle que soit la manière dont la trace se poursuit (par exemple, si un système s'est déjà engagé dans un état rendant un objectif futur impossible).

Les auteurs se concentrent sur $LTLMT_f$ (Logique temporelle linéaire sur les traces finies modulo théories), qui enrichit $LTL_f$ avec des théories SMT arbitraires. Le problème spécifique est la surveillance anticipative : déterminer l'état de surveillance d'une propriété $\psi$ après une trace $\tau$ en considérant $\tau$ et toutes ses continuations finies possibles. Les états de surveillance sont définis comme suit :

• Satisfaction actuelle (CS) : $\tau$ satisfait $\psi$, mais une violation est possible dans une certaine extension.
• Satisfaction permanente (PS) : $\tau$ satisfait $\psi$, et aucune extension ne peut la violer.
• Violation actuelle (CV) : $\tau$ viole $\psi$, mais une satisfaction est possible dans une certaine extension.
• Violation permanente (PV) : $\tau$ viole $\psi$, et aucune extension ne peut la satisfaire.

Le problème général de surveillance pour $LTLMT_f$ est indécidable, en particulier lorsqu'il implique l'arithmétique linéaire sur les réels. L'article vise à identifier des fragments décidables et pratiquement pertinents de cette logique.

Méthodologie

Le cadre proposé combine des méthodes automates pour le raisonnement temporel avec des techniques de raisonnement automatisé (SMT) pour la dimension des données.

1. Logique et sémantique

Les auteurs définissent $LTLMT_f$ sur une signature multisortie $\Sigma$ contenant des variables de données, des fonctions et des prédicats. Un choix sémantique clé est le traitement du modèle sous-jacent $M$ :

• Extension conservatrice : Le modèle sous-jacent à une trace n'est pas fixe ; plutôt, une continuation de la trace fournit une extension du modèle (via des plongements). Les faits concernant les éléments déjà vus restent fixes, mais de nouveaux éléments et faits peuvent être introduits. Cela correspond à des scénarios comme les systèmes de billetterie où les prix passés sont fixes, mais de nouveaux billets apparaissent.
• Opérateur de retour en arrière : La logique utilise un opérateur de « retour en arrière » ($\triangleleft$) pour faire référence à la valeur précédente d'une variable, plutôt qu'un opérateur de prévision.

2. Construction d'automates

Pour une propriété $LTLMT_f$ sans quantificateurs donnée (désignée comme dataLTLf), les auteurs construisent un Automate Fini Non Déterministe (AFND), $N_\psi$.

• L'alphabet $\Theta$ consiste en des ensembles de formules du premier ordre (FO) (et de leurs négations) trouvés dans la propriété.
• L'AFND suit l'évolution temporelle de la propriété, acceptant les mots correspondant aux traces satisfaisant la propriété.
• Une restriction de « retour en arrière sûr » est imposée pour garantir que les variables de retour en arrière ne contraignent pas l'état initial de la trace.

3. Graphes de co-accessibilité et régression

Pour gérer la dimension des données et déterminer les états anticipatifs, les auteurs introduisent un graphe de co-accessibilité ($CG^+$) et un graphe dual de non-co-accessibilité ($CG^-$).

• Régression : Le mécanisme central est l'opération regress, qui propage les obligations de vérification en arrière à travers les transitions de l'AFND. Étant donné une formule d'état $\phi$ et une contrainte de transition $C$, regress($\phi$, $C$) calcule la condition sur l'état précédent requise pour satisfaire $\phi$ après application de $C$.
• Complétion de modèle : Pour garantir que la régression aboutit à des formules sans quantificateurs (essentiel pour la décidabilité), le cadre repose sur le fait que la théorie $T$ possède une complétion de modèle $T^*$. Cela permet d'éliminer les quantificateurs existentiels introduits lors de la régression, en les convertissant en formules équivalentes sans quantificateurs dans $T^*$.
• Construction du graphe : Les nœuds du graphe sont des paires $(q, \phi)$, où $q$ est un état de l'AFND et $\phi$ est une formule sans quantificateurs représentant la condition requise pour atteindre un état final (ou non final) depuis $q$.

4. Algorithme de surveillance

La procédure MONITOR fonctionne comme suit :

1. Calculer l'AFND $N_\psi$ et les graphes de co-accessibilité $CG^+$ et $CG^-$.
2. Simuler la trace $\tau$ sur $N_\psi$ pour identifier l'état courant $q$.
3. Évaluer la dernière affectation $\alpha_n$ par rapport aux formules associées à l'état $q$ :
   • Si $q$ est acceptant : Vérifier si $EXTVIOL(q)$ (la condition pour une violation future) est satisfaite. Si oui $\to$ CS ; sinon $\to$ PS.
   • Si $q$ est non acceptant : Vérifier si $EXTSAT(q)$ (la condition pour une satisfaction future) est satisfaite. Si oui $\to$ CV ; sinon $\to$ PV.

Contributions clés

1. Formalisation de la surveillance anticipative pour $LTLMT_f$ : Il s'agit du premier travail à définir formellement et à aborder le problème de la surveillance anticipative pour des propriétés linéaires enrichies de théories SMT sur les traces finies.
2. Cadre novateur : Les auteurs présentent un cadre fondamental combinant le raisonnement temporel basé sur les AFND avec le raisonnement sur les données basé sur SMT. Une nouveauté technique clé est l'utilisation de la complétion de modèle pour gérer l'élimination des quantificateurs lors de la régression en arrière des obligations de vérification, permettant la construction de graphes de co-accessibilité finis.
3. Identification de fragments décidables : L'article identifie des fragments spécifiques et pratiquement pertinents de $LTLMT_f$ où le problème de surveillance est soluble (terminaison garantie) :
   • DB-LTLf : Propriétés combinant des références de base de données (modélisées via l'égalité et les fonctions non interprétées - EUF) avec l'arithmétique, sous des contraintes structurelles spécifiques.
   • Signatures acycliques : Garantit un nombre fini de termes.
   • Contraintes de monotonie (MC) : Restreint l'arithmétique à des comparaisons simples ($=, \neq, \leq, <$) entre termes, courantes dans la surveillance des processus métier.
   • Finitude locale : Une condition plus large garantissant un nombre fini de formules non équivalentes.
   • Retour en arrière borné : Une restriction syntaxique sur l'interaction des contraintes dans la propriété, généralisant la « liberté de rétroaction ».
4. Implémentation prototype : La faisabilité de l'approche est démontrée par MONTHE, un outil prototype implémenté en Python qui utilise le solveur SMT CVC5 pour le raisonnement sur les données et l'élimination des quantificateurs.

Résultats et évaluation

• Résultats théoriques : L'article fournit des preuves formelles de la correction de l'algorithme de surveillance (Théorème 18) et établit la décidabilité pour les fragments identifiés (Théorèmes 19–24).
• Application pratique : Le cadre est montré comme couvrant les processus métier conscients des données et les systèmes dynamiques opérant sur des bases de données en lecture seule (par exemple, l'exemple de billetterie où un agent sélectionne le billet le moins cher).
• Évaluation préliminaire : Les auteurs rapportent des expériences préliminaires utilisant l'outil MONTHE. L'outil traite avec succès les propriétés et les traces, en sortant l'état de surveillance correct. L'évaluation est décrite comme préliminaire, une évaluation empirique extensive étant laissée pour un travail futur.

Importance et affirmations

L'article affirme être le premier à aborder la surveillance anticipative pour des propriétés temporelles conscientes des données. Son importance réside dans le pont qu'il établit entre le pouvoir expressif requis pour les systèmes d'IA modernes (données structurées, arithmétique) et le besoin de garanties de sécurité rigoureuses et en temps réel.

Les auteurs soulignent que si la surveillance anticipative générale est indécidable, leur identification de DB-LTLf (combinant l'arithmétique avec des références de base de données) fournit un « point idéal » d'expressivité et de décidabilité. Cela est particulièrement pertinent pour :

• Processus métier conscients des données : Où les transitions dépendent des valeurs de la base de données et des contraintes arithmétiques.
• Systèmes dynamiques : Où les agents interagissent avec des bases de données en lecture seule (par exemple, marchés de billets, systèmes d'inventaire).

Le travail est modeste dans ses affirmations concernant un déploiement industriel immédiat, notant que l'implémentation actuelle est un prototype et que les travaux futurs exploreront les systèmes dynamiques où la composante de données change au fil du temps (par exemple, la mise à jour des prix des billets), ce qui nécessite de gérer des mises à jour contrôlées de la base de données.