Résumé technique : Analyse de la robustesse neuro-symbolique pour les systèmes discrets par rapport aux déviations de transition

Énoncé du problème

Dans le contrôle supervisé des systèmes à événements discrets (SED), des contrôleurs sont synthétisés pour imposer des spécifications sur un modèle de plante. Bien que les méthodes classiques fournissent des garanties de type « correct par construction », ces garanties dépendent strictement de l'exactitude du modèle de la plante. En pratique, les écarts résultant de dynamiques non modélisées, du bruit des capteurs ou d'erreurs d'abstraction font que le système réel dévie de son modèle nominal, ce qui peut compromettre la sécurité.

Des travaux récents ont abordé ce problème en définissant la robustesse discrète comme l'ensemble de toutes les déviations de transition possibles (transitions supplémentaires ajoutées à la plante nominale) contre lesquelles un superviseur maintient la sécurité. Cependant, cette approche basée sur les transitions fait face à deux limitations critiques :

1. Scalabilité : L'espace des déviations possibles croît exponentiellement avec les espaces d'états et d'actions, rendant l'énumération exhaustive impossible pour tous les systèmes sauf les plus petits.
2. Conservatisme : La vaste majorité des déviations mathématiquement possibles sont physiquement infaisables (par exemple, une machine produisant spontanément une pièce sans entrée). L'inclusion de ces déviations infaisables gonfle l'espace de recherche et produit des résultats de robustesse qui ne reflètent pas fidèlement le comportement réel du système.

Les tentatives existantes pour filtrer les déviations infaisables à l'aide de contraintes de système formelles ($P_{sys}$) nécessitent que des experts métier encodent manuellement les lois physiques dans des spécifications formelles, ce qui crée une charge importante et ajoute une surcharge au pipeline d'analyse.

Méthodologie

Le papier propose un cadre de calcul neuro-symbolique pour répondre à ces défis de scalabilité et de faisabilité. L'approche découple le raisonnement sur la faisabilité physique de la computation formelle des garanties de robustesse, en utilisant un processus en deux étapes :

1. Filtrage de faisabilité neurale (Couche LLM)

La première étape exploite les grands modèles de langage (LLM) pour inférer un sous-ensemble de transitions de déviation physiquement faisables ($D$).

• Entrée : Le cadre ingère des modèles LTS formels de la plante et du superviseur, des descriptions en langage naturel des états et événements du système, des spécifications de sécurité et des connaissances du domaine concernant les lois physiques (ex. : « une pièce ne peut pas être à deux endroits à la fois »).
• Processus : Un modèle de prompt structuré guide le LLM pour raisonner sur ces entrées. Le LLM est chargé d'identifier les transitions qui représentent des fautes ou des déviations réalistes cohérentes avec la sémantique du système et les contraintes physiques.
• Sortie : Un ensemble réduit de déviations faisables $D \subseteq (Q_E \times Act_E \times Q_E) \setminus R_E$, significativement plus petit que l'espace de transition complet.

2. Vérification de robustesse symbolique (Couche Symbolique)

La seconde étape effectue une vérification formelle sur l'ensemble réduit $D$.

• Processus : Un algorithme de force brute (Algorithme 1) itère à travers tous les sous-ensembles des déviations faisables $D$. Pour chaque ensemble de déviation candidat $d$, il utilise la model checking standard pour vérifier si le système dévié $E_d$ contrôlé par le superviseur $S$ satisfait la propriété de sécurité $P$ (c'est-à-dire $E_d/S \models P$).
• Raffinement : L'algorithme extrait uniquement les déviations de robustesse maximale (celles qui ne sont pas contenues dans d'autres déviations robustes) pour former l'ensemble de robustesse final $\Delta_f$.
• Garantie : Comme la vérification est effectuée de manière symbolique sur un système de transition formellement défini, les garanties de robustesse résultantes restent mathématiquement correctes par rapport à l'ensemble de déviation $D$ inféré.

Contributions clés

Le papier présente deux contributions principales :

1. Un cadre neuro-symbolique : Une architecture novatrice qui combine les LLM pour inférer des modèles de déviation physiquement faisables avec des méthodes symboliques pour calculer les garanties de robustesse. Cette approche automatise l'extraction des contraintes physiques à partir du langage naturel et des connaissances du domaine, éliminant le besoin d'un encodage formel manuel de $P_{sys}$.
2. Prototype et Évaluation : L'implémentation d'un outil prototype et son évaluation expérimentale sur trois études de cas distinctes : un système de fabrication, l'interface de thérapie par radiation Therac-25 et le protocole Alternate Bit (ABP).

Résultats expérimentaux

Le cadre a été évalué sur trois études de cas en utilisant des LLM (GPT-5.2 et Claude 3.5 Sonnet) pour le filtrage de faisabilité et un vérificateur symbolique basé sur Python.

• Système de fabrication : Le LLM a identifié 18 déviations faisables (sur un espace théorique de 108). La couche symbolique a trouvé un ensemble de déviation robuste maximal, confirmant que le système est robuste contre 15 transitions spécifiques mais vulnérable à des fautes spécifiques de déchargement de tampon.
• Therac-25 : L'analyse a identifié 9 déviations faisables. Le système s'est avéré robuste contre les pressions répétées sur « enter » par l'opérateur, mais vulnérable à la condition de concurrence spécifique impliquant la sélection de la thérapie électronique, capturant ainsi avec précision le défaut de conception historique.
• Protocole ABP : Le LLM a identifié 16 déviations faisables. L'analyse a confirmé la robustesse contre la perte, la duplication et la corruption de messages, s'alignant sur l'intention de conception du protocole.

Résultats quantitatifs :

• Réduction de la faisabilité : Les LLM ont considérablement réduit l'espace de recherche. La réduction variait de 67 % (Therac-25) à 99 % (ABP) par rapport à l'espace de transition complet.
• Précision de la faisabilité : Pour l'exemple de fabrication, 89 % des transitions générées par GPT étaient physiquement faisables, contre 54 % pour Claude. Sur des systèmes plus complexes comme ABP, les taux de faisabilité ont chuté pour les deux modèles (respectivement 63 % et 36 %), indiquant un besoin d'amélioration du prompt engineering ou des ontologies de domaine.
• Équivalence de robustesse : Malgré l'utilisation d'un ensemble réduit de déviations, le cadre a produit des garanties de robustesse comparables à celles obtenues par l'analyse complète basée sur les transitions dans les cas évalués.

Signification et affirmations

Le papier affirme que cette approche neuro-symbolique répond avec succès au compromis entre scalabilité et inclusion de déviations infaisables dans l'analyse de robustesse discrète. En utilisant les LLM pour filtrer l'espace de solution basé sur la compréhension sémantique et physique, la méthode rend l'analyse de robustesse traitable pour des systèmes où l'énumération exhaustive est impossible.

Les auteurs soulignent que bien que le composant LLM introduise un élément probabiliste dans l'identification des déviations faisables, la vérification symbolique ultérieure garantit que les garanties de robustesse finales sont formellement correctes par rapport à l'ensemble $D$ inféré. Ce travail démontre qu'il est possible de récupérer des analyses de robustesse comparables aux méthodes de l'espace complet tout en opérant sur un sous-ensemble de déviations beaucoup plus petit et physiquement significatif.

Le papier conclut avec modestie, notant que l'implémentation actuelle de l'algorithme de force brute nécessite une optimisation pour les systèmes plus larges et que les travaux futurs se concentreront sur l'amélioration du prompt engineering, l'incorporation d'ontologies de domaine pour améliorer la précision des LLM, et l'étude de boucles de raffinement interactives où les résultats symboliques guident les requêtes LLM.