noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning

1. Il Problema

I linguaggi di programmazione probabilistica (PPL) sono strumenti espressivi per modellare distribuzioni di probabilità complesse. Tuttavia, la maggior parte dei moderni motori di inferenza per PPL presenta due limitazioni critiche:

1. Mancanza di supporto per il nondeterminismo: I PPL esistenti gestiscono bene la casualità probabilistica (es. lanci di monete), ma non supportano scelte nondeterministiche (come quelle presenti nei Processi Decisionali di Markov - MDP), fondamentali per l'apprendimento per rinforzo e la verifica di modelli.
2. Difficoltà nella combinazione con il condizionamento: Combinare il nondeterminismo con il condizionamento (osservazioni Bayesiane) è un problema aperto. Quando si introduce il nondeterminismo, un programma non modella più una singola distribuzione, ma un insieme di distribuzioni. Questo rende l'inferenza non composizionale: la probabilità massima condizionata di un programma non può essere dedotta semplicemente dalle probabilità massime dei suoi sottoprogrammi.

L'approccio attuale consiste nell'usare direttamente i model checker probabilistici sulla semantica operativa dei programmi, ma questo porta spesso a spazi degli stati esplosivi e ingestibili.

2. Metodologia: Il Framework noDice

Gli autori introducono noDice, un motore di inferenza che estende il linguaggio e il motore Dice (specializzato in programmi discreti senza cicli) per gestire il nondeterminismo e il condizionamento.

La metodologia si basa su tre fasi principali:

A. Compilazione Booleana e Tracciatura

NoDice compila il programma probabilistico in una coppia di formule booleane:

• Una formula che modella il comportamento del programma (ignorando le osservazioni).
• Una formula che modella esclusivamente le osservazioni (condizioni di successo).
  A differenza di Dice, noDice genera anche una traccia annotata delle operazioni di "flip" (lanci di moneta). Questa traccia distingue tra flip probabilistici (con una probabilità $\theta$) e flip nondeterministici (etichettati come $n$), mantenendo l'ordine di esecuzione per preservare la semantica corretta.

B. Costruzione di Diagrammi Decisionali (ADD)

Le formule booleane vengono rappresentate internamente come Binary Decision Diagrams (BDD). Successivamente, noDice combina queste due BDD in un singolo Algebraic Decision Diagram (ADD).

• Gli ADD sono una generalizzazione delle BDD che permettono valori di uscita diversi da booleani (in questo caso, valori di output del programma o uno stato di "Rifiuto").
• Gli ADD sfruttano la struttura del programma (come l'indipendenza condizionale) per comprimere drasticamente la rappresentazione, eliminando stati ridondanti.

C. Sollevamento a Processi Decisionali di Markov (MDP)

L'ADD viene "sollevato" (lifted) per costruire un MDP:

• Ogni nodo dell'ADD diventa uno stato dell'MDP.
• Gli archi dell'ADD diventano transizioni.
• I nodi che rappresentano flip probabilistici diventano stati con transizioni probabilistiche.
• I nodi che rappresentano flip nondeterministici diventano stati con transizioni nondeterministiche (scelta di azioni).
• Gli stati terminali che corrispondono a osservazioni fallite sono etichettati come "Rifiuto" ($R$) e vengono gestiti tramite un meccanismo di riciclo (simile al rejection sampling) per calcolare le probabilità condizionate.

L'inferenza finale si riduce al calcolo della probabilità di raggiungimento condizionata (conditional reachability probability) nell'MDP costruito: si cerca la massima probabilità di raggiungere uno stato di output desiderato, condizionata al fatto che non si sia raggiunto lo stato di "Rifiuto". Per questo calcolo, noDice utilizza un algoritmo di bisezione implementato nel model checker Storm, ottimizzato per MDP aciclici.

3. Contributi Chiave

1. Linguaggio noDice: Un linguaggio funzionale di primo ordine, non ricorsivo, che supporta scelte probabilistiche, scelte nondeterministiche e osservazioni di prima classe.
2. Algoritmo di Inferenza Teorico: Una fondazione teorica che collega la semantica dei programmi probabilistici con nondeterminismo (insiemi convessi di distribuzioni) alle probabilità di raggiungimento massimali negli MDP.
3. Uso degli ADD per la Compressione: L'uso innovativo degli ADD come passo intermedio per costruire MDP compatti, sfruttando la struttura del codice per evitare l'esplosione combinatoria dello spazio degli stati.
4. Implementazione e Valutazione: Un prototipo in OCaml che dimostra la fattibilità dell'approccio su una vasta gamma di benchmark.

4. Risultati Sperimentali

Gli autori hanno valutato noDice confrontandolo con il motore Dice (per programmi puramente probabilistici) e con il model checker Storm (che risolve il problema direttamente come MDP). I benchmark includono problemi di tracciamento veicoli, raccolta coupon, raggiungibilità di rete, scambio equo e reti Bayesiane.

• Riduzione dello Spazio degli Stati: NoDice costruisce MDP significativamente più piccoli rispetto alla codifica diretta utilizzata da Storm. In molti casi, la dimensione dell'MDP compresso da noDice è ordini di grandezza inferiore a quella di Storm.
• Efficienza di Inferenza:
  • Su programmi con molte variabili e alta dimensionalità (es. problemi di raccolta coupon, tracciamento veicoli), noDice supera Storm in termini di tempo di esecuzione totale, grazie alla rapida costruzione di MDP compatti.
  • Su problemi con spazi degli stati semplici o bassa dimensionalità (es. alcune reti di comunicazione), Storm può essere più veloce perché il costo di compilazione in ADD di noDice non è compensato da una riduzione significativa dello stato.
• Impatto del Nondeterminismo: La quantità di nondeterminismo nel programma non influisce significativamente sul tempo di compilazione (costruzione dell'ADD), ma aumenta leggermente il tempo di model checking. Tuttavia, il tempo totale rimane dominato dalla fase di compilazione.
• Compressione degli Stati: L'ottimizzazione di "state compression" riduce ulteriormente la dimensione dell'MDP, ma non ha sempre un impatto diretto sul tempo di esecuzione del model checker, poiché il collo di bottiglia è spesso la compilazione.

5. Significato e Impatto

Il lavoro di noDice è significativo perché:

• Colma un divario fondamentale: Fornisce il primo motore di inferenza pratico che gestisce simultaneamente nondeterminismo, condizionamento e distribuzioni discrete in un linguaggio di programmazione.
• Supera le limitazioni dei metodi esistenti: Dimostra che l'approccio "naive" di unrollare la semantica operativa in un MDP (usato dai model checker tradizionali) è inefficiente per programmi complessi, e che l'uso di strutture dati simboliche (ADD) è cruciale per scalare.
• Nuova direzione per i PPL: Apre la strada all'uso di PPL in contesti dove l'incertezza non è solo probabilistica ma anche strutturale o strategica (es. sicurezza, pianificazione robusta, sistemi multi-agente), permettendo di calcolare il "caso peggiore" (massima probabilità) in presenza di osservazioni parziali.

In sintesi, noDice dimostra che è possibile eseguire inferenza esatta su programmi probabilistici complessi con nondeterminismo, trasformando il problema in una ricerca di percorsi ottimali su MDP compatti generati simbolicamente.