💻 computer science

Leveraging System-Level Observations to Inform Bayesian Learning of Model Parameters for Quantitative Verification

L'article introduit EPIK, une nouvelle approche qui améliore l'apprentissage bayésien pour la vérification quantitative en exploitant des propriétés systémiques directement observables pour susciter et intégrer des connaissances a priori, surmontant ainsi les limites liées à la dépendance envers des hypothèses inexactes ou peu informatives concernant les paramètres du modèle formel.

Auteurs originaux : Simos Gerasimou, Xingyu Zhao

Publié 2026-08-05

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Simos Gerasimou, Xingyu Zhao

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 essayiez de prédire l'avenir d'une machine complexe, comme une voiture autonome ou un robot qui cueille des fruits. Pour ce faire, les ingénieurs utilisent une « carte » de probabilités appelée modèle de Markov. Considérez cette carte comme un immense jeu de société où chaque case est un état dans lequel la machine peut se trouver, et les lancers de dés déterminent comment elle passe d'une case à l'autre. Le problème, c'est que pour jouer correctement au jeu, vous devez savoir exactement quelles sont les chances que le dé retombe sur chaque chiffre. Dans le monde réel, ces « dés » sont les probabilités de transition — comme la probabilité qu'un bras de robot glisse ou qu'un serveur plante.

Traditionnellement, pour remplir ces chiffres, les experts doivent deviner les probabilités exactes de chaque minuscule mouvement que la machine pourrait effectuer. C'est comme demander à un chef de deviner la température exacte de chaque grain de riz dans une casserole juste pour savoir quand le dîner sera prêt. C'est incroyablement difficile, et si la supposition est même légèrement erronée, toute la prédiction sur la fiabilité ou la vitesse de la machine peut être fausse. C'est là qu'intervient l'apprentissage bayésien. C'est une méthode mathématique pour mettre à jour vos suppositions à mesure que vous obtenez de nouvelles informations, mais cela nécessite toujours un point de départ, ou un « a priori ». Si cette supposition initiale est mauvaise, la réponse finale le sera aussi.

Entrez en scène EPIK, une nouvelle approche introduite par Simos Gerasimou et Xingyu Zhao. Au lieu de forcer les experts à deviner les minuscules et invisibles lancers de dés à l'intérieur de la machine, EPIK leur demande de décrire les grands résultats observables qu'ils peuvent réellement voir. C'est comme demander au chef : « Combien de temps le riz met-il habituellement à cuire ? » ou « À quelle fréquence la casserole déborde-t-elle ? » plutôt que de demander la température de chaque grain de riz. Les chercheurs ont découvert qu'en utilisant ces observations de haut niveau, ancrées dans le monde réel, ils pouvaient remonter en arrière pour déterminer les lancers de dés cachés avec une précision bien plus grande. Ils ont testé cela sur un robot cueilleur de fruits et sur un système de trading de devises étrangères, démontrant que cette méthode non seulement fonctionne, mais aide aussi à prédire des choses complexes et difficiles à mesurer, comme la consommation d'énergie ou des défaillances rares pour lesquelles on n'a pas encore de données.

L'idée maîtresse : Deviner les dés en regardant le jeu

L'article traite d'un problème délicat en génie logiciel : comment s'assurer que nos modèles informatiques de systèmes complexes sont précis ? Lorsque nous construisons un modèle de robot ou de service cloud, nous utilisons les mathématiques pour prédire des choses comme : « Va-t-il planter ? » ou « À quelle vitesse aura-t-il terminé ? ». Mais ces prédictions ne sont aussi bonnes que les chiffres que nous injectons dedans. Généralement, ces chiffres sont les probabilités que le système passe d'un état à un autre.

Les auteurs soutiennent que demander à des experts de deviner ces probabilités spécifiques de bas niveau revient à demander à une personne de deviner la vitesse exacte du vent sur chaque feuille d'un arbre juste pour prédire si un cerf-volant va voler. C'est trop détaillé, et les experts se trompent souvent ou n'ont pas les données. Si les chiffres de départ sont faux, tout le processus de vérification échoue, menant à de mauvaises décisions d'ingénierie.

EPIK : Le « Détective à l'envers »

L'article présente EPIK (Eliciting Prior Knowledge - Élicitation de connaissances a priori), un outil ingénieux qui inverse la donne. Au lieu de demander à l'expert : « Quelle est la probabilité que le robot échoue à cueillir un fruit ? », EPIK demande : « D'après votre expérience, à quelle fréquence le robot termine-t-il une mission avec succès, et combien de temps cela prend-il en moyenne ? ».

Ce sont des propriétés de niveau système. Ce sont les résultats globaux que les experts comprennent réellement et pour lesquels ils possèdent des données. EPIK traite ces résultats connus comme des indices. Il utilise un processus mathématique appelé apprentissage bayésien pour remonter à partir de ces grands indices afin de découvrir les petits lancers de dés cachés qui les ont causés.

Voici comment le processus fonctionne, étape par étape :

La configuration : Imaginez un robot qui cueille des fruits. Il possède un « état » où il se positionne, un état où il cueille, et un état où il décide de réessayer ou d'abandonner. La probabilité exacte qu'il échoue à cueillir un fruit est inconnue (appelons cela les « dés cachés »).
Les indices : Les experts disent à EPIK : « Nous savons, d'après 200 missions passées, que le robot réussit 80 % du temps et prend environ 4,75 secondes en moyenne ». Ce sont les propriétés informées par la connaissance a priori (PK-informed).
L'ingénierie inverse : EPIK lance une recherche complexe (utilisant des algorithmes évolutionnaires, qui sont comme des versions numériques de la sélection naturelle) pour trouver l'ensemble des lancers de dés cachés qui produiraient le mieux ces résultats de 80 % de réussite et de 4,75 secondes. Il ne trouve pas seulement une réponse ; il trouve toute une famille de réponses possibles qui correspondent aux indices.
Le bénéfice : Une fois qu'EPIK a déterminé les lancers de dés cachés grâce aux indices connus, il peut les utiliser pour prédire des choses que nous ne connaissons pas encore. Ce sont les propriétés insaisissables (elusive properties). Par exemple, personne n'a jamais mesuré la consommation de batterie du robot pour cette tâche spécifique. Mais maintenant qu'EPIK sait comment le robot se déplace, il peut calculer la consommation d'énergie probable, même si personne ne l'a jamais enregistrée auparavant.

Ce que les expériences ont montré

Les chercheurs ont testé EPIK sur deux scénarios réels : le robot cueilleur de fruits et un système de trading de devises étrangères. Ils ont créé différentes versions de ces systèmes avec des niveaux de complexité et des variables inconnues variés.

Précision : Lorsqu'ils ont comparé les prédictions d'EPIK à la « vérité terrain » (les valeurs mathématiquement correctes), les résultats étaient incroyablement proches. La différence entre la supposition d'EPIK et la vraie réponse était infime (moins de 0,00389 dans les cas de test). Cela suggère qu'EPIK peut de manière fiable rétro-concevoir la mécanique cachée d'un système simplement en observant le panorama global.
Le test de « conflit » : L'équipe a également testé ce qui se passe si les experts donnent des conseils contradictoires (par exemple, un expert dit que le robot est très fiable, un autre dit qu'il est lent). Ils ont constaté que lorsque les indices étaient contradictoires, EPIK peinait à trouver une correspondance parfaite, et l'« erreur » dans ses suppositions augmentait. C'est une bonne chose, car cela agit comme un voyant d'alerte : si les indices ne concordent pas, le modèle sait que quelque chose ne va pas avec les données d'entrée.
La victoire de l'« insaisissable » : La partie la plus excitante était la vérification des propriétés « insaisissables ». Dans le test du robot cueilleur de fruits, ils avaient des données sur les taux de réussite et le temps, mais aucune donnée sur la consommation d'énergie. EPIK a utilisé les données connues pour estimer la consommation d'énergie. La distribution de la consommation d'énergie qui en résulte était une supposition raisonnable et bien documentée que les décideurs pouvaient réellement utiliser, alors que sans EPIK, ils auraient dû faire une supposition aveugle ou ignorer totalement le problème.

Pourquoi cela importe

L'article ne prétend pas avoir résolu tous les problèmes de la vérification logicielle, mais il propose une nouvelle façon puissante d'entamer la discussion. Il suggère que nous n'avons pas besoin d'être des experts des détails microscopiques d'un système pour construire un bon modèle ; nous avons seulement besoin d'être des experts des résultats du système.

En déplaçant l'attention de « deviner les dés » vers « observer le jeu », EPIK facilite la construction de modèles fiables pour des systèmes complexes tels que les voitures autonomes, les dispositifs médicaux et les services cloud. Cela transforme la tâche difficile de définir chaque probabilité en une tâche plus gérable consistant à décrire ce que nous savons déjà sur le comportement du système dans le monde réel. Et pour les choses que nous ne connaissons pas encore, cela nous donne un moyen mathématiquement fondé de faire une supposition éclairée, plutôt qu'une supposition aveugle.

Résumé technique : Exploiter les observations au niveau du système pour éclairer l'apprentissage bayésien des paramètres de modèle pour la vérification quantitative

1. Énoncé du problème

La vérification quantitative, en particulier le contrôle de modèles probabilistes (Probabilistic Model Checking - PMC), est un outil critique pour analyser les systèmes logiciels dans des environaux incertains (ex. : robotique, services cloud). Cependant, l'exactitude des résultats de la PMC dépend fortement de la véracité des paramètres du modèle de Markov (probabilités ou taux de transition). Un goulot d'étranglement important existe dans les approches d'apprentissage bayésien utilisées pour affiner ces paramètres : elles nécessitent une Connaissance Préalable (CP) concernant des paramètres de transition spécifiques du modèle (ex. : la probabilité exacte qu'un robot échoue à cueillir un fruit).

L'obtention d'une CP aussi fine et au niveau des paramètres auprès des experts du domaine est souvent peu pratique, non triviale et sujette aux biais. Les experts possèdent généralement des connaissances sur des propriétés de haut niveau du système (ex. : taux de succès de la mission, temps d'exécution attendu) plutôt que sur des probabilités de transition abstraites. L'utilisation de priors inexacts ou non informatifs pour les paramètres de transition peut conduire à des résultats de vérification trompeurs et à de mauvaises décisions d'ingénierie.

2. Méthodologie : L'approche EPIK

Les auteurs proposent EPIK, une approche de PMC basée sur le bayésien qui comble le fossé entre la connaissance d'expert de haut niveau et les paramètres de modèle de bas niveau. Au lieu de demander aux experts de définir des probabilités de transition, EPIK extrait la connaissance sur des propriétés systémiques observables et dérive mathématiquement les distributions pour les paramètres de modèle inconnus.

Le flux de travail d'EPIK se compose de trois étapes principales :

A. Extraction de formules algébriques

En utilisant le contrôle de modèles paramétriques (Parametric Model Checking - ParaMC), EPIK dérive des fonctions rationnelles sous forme fermée qui lient les paramètres de transition inconnus du modèle ( $X$ ) à la fois :

Propriétés informées par la CP ( $Y$ ) : Propriétés du système pour lesquelles les experts ont une connaissance préalable (ex. : fiabilité, temps de réponse).
Propriétés évasives ( $Z$ ) : Propriétés du système qui sont nouvelles, rares ou coûteuses à observer (ex. : consommation d'énergie dans un nouveau scénario).

Cette étape transforme le problème de vérification en un problème algébrique, évitant ainsi d'invoquer de manière répétée le contrôleur de modèle probabiliste pendant l'optimisation.

B. Élicitation de connaissances (Optimisation multi-objectif)

EPIK formule un problème d'optimisation multi-objectif pour trouver les paramètres de distribution ( $\theta$ ) des transitions inconnues ( $X$ ) qui approchent le mieux les distributions fournies par l'expert pour les propriétés informées par la CP ( $Y$ ).

Objectif : Minimiser la divergence de Kullback-Leibler (KL) entre la distribution a priori de l'expert pour une propriété et la distribution générée par l'échantillonnage des paramètres de transition dérivés via les formules algébriques.
Algorithme : Le problème est résolu à l'aide d'algorithmes évolutionnaires (ex. : NSGA-II, SPEA2, CMA-ES) pour synthétiser un ensemble de solutions Pareto-optimales ( $PS_{s1}$ ). Cet ensemble représente les compromis entre la satisfaction de connaissances préalables conflictuelles concernant différentes propriétés du système.

C. Intégration de la connaissance

Une fois l'ensemble de distributions des paramètres de transition Pareto-optimal établi, EPIK l'utilise pour vérifier les propriétés évasives ( $Z$ ).

Il résout un second problème d'optimisation (simple ou multi-objectif) pour sélectionner la solution la plus appropriée de l'ensemble de Pareto en fonction des préférences du décideur (ex. : position conservatrice vs optimiste).
Cela permet de quantifier les propriétés évasives (ex. : consommation d'énergie attendue) sans nécessiter de données préalables directes pour celles-ci, en tirant parti de la cohérence établie avec les propriétés informées par la CP.

3. Contributions clés

Cadre EPIK : Une nouvelle approche pour éliciter et intégrer la connaissance préalable pour la PMC basée sur le bayésien en exploitant les propriétés globales du système plutôt qu'en exigeant la spécification directe des paramètres de transition du modèle.
Optimisation en deux étapes : Une formulation qui synthétise d'abord un ensemble de Pareto des distributions de paramètres de transition pour correspondre à la connaissance de l'expert, puis utilise cet ensemble pour vérifier les propriétés évasives.
Outil et évaluation : La publication d'un prototype d'outil open-source et d'une évaluation étendue utilisant des études de cas réels :
- Robot cueilleur de fruits (FPR) : Une tâche de robot autonome.
- Système de trading de change (FX) : Un système basé sur les services.
  L'évaluation couvre diverses variantes avec différents nombres de paramètres inconnus et différents niveaux de conflit de connaissances préalables.

4. Résultats expérimentaux

L'évaluation a traité quatre questions de recherche (RQ) :

RQ1 (Précision) : EPIK a réussi à dériver des distributions pour les paramètres de transition inconnus qui approchaient étroitement la vérité terrain des propriétés informées par la CP. L'écart entre la moyenne dérivée et la vérité terrain était négligeable (< 0,00389).
RQ2 (Efficacité) : L'approche est non triviale et nécessite une optimisation sophistiquée. EPIK, instancié avec NSGA-II et SPEA2, a nettement surpassé tant la recherche aléatoire que l'algorithme CMA-ES en termes d'indicateurs de qualité du front de Pareto (Hypervolume, Epsilon, Distance de génération inversée).
RQ3 (Conformité) : La capacité du système à synthétiser des distributions efficaces dépend de la conformité de la connaissance préalable. Lorsque les experts fournissaient des connaissances conflictuelles (scénarios de haut conflit), la divergence KL augmentait et le front de Pareto devenait moins stable, indiquant qu'EPIK peut détecter et refléter la difficulté de concilier des entrées d'experts contradictoires.
RQ4 (Intégration de la connaissance) : EPIK a permis avec succès la vérification de propriétés évasives (ex. : consommation d'énergie) en exploitant les solutions Pareto-optimales dérivées des propriétés informées par la CP. Cela permet aux décideurs de sélectionner des instanciations de paramètres spécifiques (ex. : maximiser la médiane de la consommation d'énergie pour une estimation conservatrice) qui étaient auparavant invérifiables en raison de l'absence de données directes.

5. Signification et affirmations

L'article affirme qu'EPIK est la première solution supportée par un outil pour extraire la connaissance des paramètres de transition inconnus d'un modèle probabiliste directement à partir de propriétés systémiques globales.

Praticité : Elle s'aligne plus naturellement sur l'expertise du domaine, car les experts sont plus à l'aise pour estimer des comportements de système de haut niveau (ex. : "taux de succès de la mission") que des probabilités de transition abstraites.
Robustesse : En synthétisant un ensemble de Pareto plutôt qu'une estimation ponctuelle unique, EPIK fournit une famille de priors admissibles, gérant explicitement la non-identifiabilité inhérente aux problèmes inverses.
Utilité en aval : EPIK opère entièrement au temps de conception pour générer les priors initiaux ($PK$). Ces priors servent de fondation aux estimateurs bayésiens en aval (ex. : KAMI) qui effectuent des mises à jour au moment de l'exécution, évitant ainsi le biais et l'échec souvent causés par de mauvaises initialisations.
Limites : Les auteurs notent modestement que la validité de la vérification des propriétés évasives est conditionnée par l'exactitude des propriétés informées par la CP et la correction de la structure du modèle sous-jacent. Si les priors des experts sont biaisés, l'évaluation des propriétés évasives qui en résulte sera également biaisée.

En résumé, EPIK offre un pipeline flexible et généralisable pour rendre la vérification quantitative bayésienne plus accessible et robuste en déplaçant la charge de l'élicitation de la connaissance des paramètres de modèle abstraits vers les sémantiques observables du système.