💻 computer science

noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning

Le papier présente noDice, une extension de l'inférence probabiliste discrète Dice qui intègre le nondéterminisme en modélisant les programmes sans boucle sous forme de processus de décision markoviens optimisés par des diagrammes de décision pour réduire l'espace d'état.

Auteurs originaux : Tobias Gürtler, Benjamin Lucien Kaminski

Publié 2026-02-24

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Tobias Gürtler, Benjamin Lucien Kaminski

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

🎲 noDice : Le Détective des Hasards et des Choix Mystérieux

Imaginez que vous essayez de prédire l'avenir dans un monde où deux forces s'affrontent :

Le Hasard pur (comme lancer une pièce de monnaie ou un dé).
Le Choix mystérieux (comme un joueur d'échecs qui décide de son prochain coup, ou un vent qui souffle dans une direction inconnue).

Jusqu'à présent, les ordinateurs étaient très bons pour gérer le Hasard (les probabilités), mais ils avaient du mal à gérer le Choix mystérieux (ce qu'on appelle la "non-détermination") quand on essaie de filtrer les résultats avec des observations (comme dire : "Je ne veux considérer que les scénarios où il a plu").

noDice est un nouvel outil (un moteur d'inférence) créé par des chercheurs pour résoudre ce casse-tête. Voici comment il fonctionne, expliqué avec des métaphores.

🌟 Le Problème : La Tempête de Possibilités

Imaginons que vous vouliez calculer la probabilité qu'un avion atterrisse en toute sécurité alors qu'une voiture traverse la piste.

La voiture peut rouler vite ou lentement (Hasard).
Mais elle peut aussi décider de changer de vitesse à chaque instant, et nous ne savons pas comment elle va décider (Choix mystérieux).
De plus, nous avons des capteurs qui nous disent où elle est, mais ils sont parfois faux. Nous devons donc ignorer les scénarios où le capteur ment.

Si vous essayez de lister tous les scénarios possibles à la main, vous vous retrouvez avec une montagne de papiers (des milliards de combinaisons). C'est trop gros pour qu'un ordinateur puisse le lire en une vie. C'est là que les anciens outils échouaient : ils devenaient perdus dans cette montagne.

🛠️ La Solution de noDice : Le "Téléphone Arabe" Géant

noDice ne compte pas les scénarios un par un. Au lieu de cela, il utilise une astuce géniale en trois étapes, comme un chef cuisinier qui prépare un plat complexe :

1. La Traduction (Compilation) 📝

D'abord, noDice prend le programme informatique (le scénario de l'avion et de la voiture) et le traduit en une formule mathématique géante, un peu comme un immense puzzle logique fait de "Vrai" et de "Faux".

Analogie : C'est comme si on prenait une recette de cuisine complexe et qu'on la transformait en une liste d'instructions binaires (Allumer le feu / Éteindre le feu).

2. Le Compression (Les Diagrammes de Décision) 🗜️

Ensuite, noDice utilise une structure appelée Diagramme de Décision Algébrique (ADD). Imaginez un immense arbre généalogique où chaque branche représente un choix.

Le problème : Cet arbre est souvent énorme et rempli de branches inutiles (par exemple, deux branches qui mènent exactement au même résultat).
La magie de noDice : Il utilise l'ADD pour coller ensemble les branches identiques et supprimer les doublons. C'est comme si vous preniez un livre de 1000 pages et que vous le résumiez en une seule carte mentale compacte, en gardant toute l'information mais en supprimant le papier perdu.
Résultat : Au lieu de milliards de scénarios, vous avez une petite carte intelligente.

3. Le Voyage (Le Processus de Décision de Markov) 🗺️

Enfin, noDice transforme cette carte compacte en un jeu de société appelé "Processus de Décision de Markov" (MDP).

Dans ce jeu, il y a des cases (états) et des dés.
Les cases "Hasard" sont des cases où vous lancez un dé (50% chance d'aller à gauche, 50% à droite).
Les cases "Choix mystérieux" sont des cases où un joueur malin (ou un adversaire) choisit le chemin le plus dangereux pour nous.
L'objectif : noDice demande au jeu : "Quelle est la pire situation possible (la probabilité maximale) où l'avion s'écrase, en supposant que le joueur malin fasse tout pour nous piéger, mais que nos capteurs aient raison ?"

🚀 Pourquoi c'est génial ?

Il trouve le pire des cas : Contrairement aux autres outils qui disent "en moyenne, ça va", noDice vous dit : "Même si le destin et le hasard s'acharnent contre vous, voici la probabilité maximale de catastrophe." C'est crucial pour la sécurité.
Il est rapide grâce à la compression : Grâce à l'étape des "Diagrammes", noDice ne regarde pas chaque grain de sable de la plage, mais il regarde la forme de la plage. Cela réduit la taille du problème de manière spectaculaire.
Il gère les observations : Il sait ignorer les scénarios où les capteurs mentent, ce qui rend le calcul beaucoup plus précis.

🏁 En Résumé

Imaginez que vous devez traverser une forêt remplie de pièges (Hasard) et de gardes qui peuvent changer de position (Choix mystérieux), tout en regardant une carte un peu floue (Observations).

Les anciens outils essayaient de marcher dans chaque sentier possible un par un. Ils s'épuisaient et s'arrêtaient avant d'arriver.
noDice prend une vue aérienne, identifie les sentiers qui mènent au même endroit, les fusionne, et calcule instantanément le chemin le plus dangereux possible.

C'est un outil puissant pour les ingénieurs qui veulent s'assurer que leurs systèmes (avions, réseaux, intelligence artificielle) restent sûrs, même dans les pires scénarios imaginables.

1. Problématique

Les langages de programmation probabiliste (PPL) sont des outils puissants pour modéliser des distributions de probabilité complexes. Cependant, la plupart des moteurs d'inférence modernes se concentrent sur les distributions discrètes ou continues mais manquent de support pour le nondéterminisme (choix non probabilistes, comme dans les Processus de Décision de Markov - MDP).

La combinaison du nondéterminisme et de la conditionnalité (observations) pose des défis majeurs :

Non-compositionnalité : Contrairement aux programmes purement probabilistes, l'inférence avec nondéterminisme ne peut pas être résolue de manière compositionnelle. Le choix optimal local ne garantit pas un choix optimal global.
Complexité de l'espace d'états : Les approches existantes qui tentent de combiner ces deux features (souvent via la sémantique opérationnelle directe) génèrent des espaces d'états exponentiellement grands, rendant l'inférence impraticable pour des programmes de taille moyenne.
Limites des outils actuels : Les vérificateurs de modèles probabilistes (comme Storm) peuvent gérer les MDPs, mais ils souffrent de l'explosion combinatoire de l'espace d'états lorsqu'ils sont appliqués directement à la sémantique des programmes.

L'objectif de ce travail est de combler ce vide en proposant un moteur d'inférence capable de traiter des programmes discrets contenant à la fois des choix probabilistes, des choix nondéterministes et des observations (conditionnement).

2. Méthodologie : Le Framework noDice

Les auteurs introduisent noDice, un moteur d'inférence qui étend le langage et le compilateur Dice (spécialisé dans l'inférence exacte pour les programmes discrets sans boucles). L'approche repose sur une transformation en trois étapes clés :

A. Compilation en Formules Booléennes Annotées

Le programme noDice est compilé en une paire de formules booléennes et une trace annotée :

Formule de modèle ( $\phi$ ) : Représente le comportement du programme (les sorties).
Formule d'acceptation ( $\gamma$ ) : Représente la réussite de toutes les observations (les contraintes observe).
Trace annotée ( $t$ ) : Une liste ordonnée des opérations de "flip" (probabilistes ou nondéterministes). Contrairement à Dice qui utilise un ensemble de poids, noDice utilise une liste pour préserver l'ordre d'évaluation, crucial pour la sémantique du nondéterminisme.

B. Construction de Diagrammes de Décision Algébriques (ADD)

Les formules booléennes sont représentées sous forme de Diagrammes de Décision Binaire (BDD). Pour gérer les sorties non binaires et les probabilités, noDice combine ces BDDs en un seul Diagramme de Décision Algébrique (ADD).

L'ADD encode la fonction qui mappe les résultats des flips (entrées) aux sorties du programme.
Si une observation échoue, la sortie est marquée par un état spécial "Rejet" ( $R$ ).
L'utilisation des ADDs permet d'exploiter la structure du programme (indépendance conditionnelle, déterminisme local) pour réduire drastiquement la taille de la représentation par rapport à une énumération brute.

C. Lifting vers un Processus de Décision de Markov (MDP)

L'étape finale consiste à "relever" (lift) l'ADD vers un MDP :

Chaque nœud de l'ADD devient un état du MDP.
Les arêtes de l'ADD deviennent des transitions.
Nature des transitions :
- Si le nœud correspond à un flip probabiliste, la transition est probabiliste (avec les probabilités données).
- Si le nœud correspond à un flip nondéterministe (nflip), la transition est non-déterministe (l'agent choisit l'action).
Inférence par Reachabilité Conditionnelle : La question d'inférence (probabilité maximale de retourner une valeur $v$ étant donné que toutes les observations ont réussi) est transformée en un problème de probabilité de reachabilité conditionnelle dans le MDP : $P(\diamond v \mid \diamond A)$ , où $A$ est l'ensemble des états acceptés.
L'algorithme utilise une méthode de bissection (implémentée dans le vérificateur Storm) pour calculer cette probabilité maximale sur les MDPs acycliques.

3. Contributions Clés

Langage noDice : Définition d'un langage fonctionnel non récursif, premier ordre, supportant les choix probabilistes (flip), les choix nondéterministes (nflip) et les observations (observe).
Algorithme d'Inférence Novel : Une méthode qui réduit l'inférence de programmes probabilistes avec nondéterminisme à la recherche de reachabilité conditionnelle sur un MDP compact, construit via des ADDs.
Preuve de Correction (Soundness) : Démonstration formelle que la probabilité maximale de reachabilité dans le MDP construit correspond exactement à la probabilité maximale de sortie du programme original sur l'ensemble des résolutions du nondéterminisme.
Implémentation et Évaluation : Une implémentation prototype en OCaml et une évaluation comparative contre des solveurs d'état de l'art (Dice pour le cas probabiliste pur, Storm pour les MDPs directs).

4. Résultats Expérimentaux

Les auteurs ont évalué noDice sur une série de benchmarks incluant des problèmes de suivi de véhicules, de collecte de coupons, de réseaux, et de réseaux bayésiens, avec des degrés variables de nondéterminisme.

Réduction de l'espace d'états : noDice construit systématiquement des MDPs beaucoup plus petits que l'encodage direct utilisé par Storm. Dans certains cas (ex: benchmarks "Coupon"), la réduction est exponentielle grâce à l'exploitation de la structure via les ADDs.
Performance :
- noDice surpasse Storm sur des problèmes à haute dimensionnalité (beaucoup de variables), là où Storm souffre de l'explosion de l'espace d'états.
- Sur des benchmarks avec peu de variables mais beaucoup de structure (ex: réseaux simples), Storm peut être plus rapide car le coût de compilation de noDice (construction de l'ADD) n'est pas amorti.
- Le temps d'inférence (model checking) dans noDice est négligeable par rapport au temps de compilation, grâce à la compacité des MDPs générés.
Impact du nondéterminisme : La présence de nondéterminisme n'augmente pas significativement le temps de compilation (car la construction de l'ADD est agnostique à la nature des flips), mais augmente légèrement le temps de vérification sur le MDP.
Optimisations : L'utilisation de la "compression d'états probabilistes" réduit encore la taille du MDP, bien que cela n'ait pas toujours entraîné une accélération significative du temps total d'exécution dans les tests.

5. Signification et Impact

Ce travail est une avancée significative dans le domaine de la programmation probabiliste :

Combinaison de concepts : Il résout le problème ouvert de la combinaison du nondéterminisme et du conditionnement dans les PPLs discrets, un domaine où les solutions existantes étaient soit inexistantes, soit non scalables.
Efficacité Scalable : En démontrant que l'on peut utiliser des structures de données compactes (ADDs) pour réduire l'espace d'états des MDPs avant l'inférence, noDice ouvre la voie à l'analyse de systèmes complexes (sécurité, réseaux, IA) qui nécessitent à la fois de l'incertitude probabiliste et de l'abstraction nondéterministe.
Fondation Théorique : L'approche fournit une sémantique formelle et des preuves de correction pour ce type de programmes, établissant un cadre rigoureux pour les travaux futurs.

En résumé, noDice démontre qu'il est possible d'effectuer une inférence exacte et efficace sur des programmes probabilistes complexes avec nondéterminisme, en évitant l'explosion combinatoire grâce à une compilation intelligente vers des diagrammes de décision et des MDPs réduits.