Bayesian Networks and Proof-Nets: the proof-theory of Bayesian Inference

Sintesi Tecnica: Reti Bayesiane e Proof-Net: la teoria della prova dell'inferenza Bayesiana

Definizione del Problema
Le Reti Bayesiane (BN) sono uno strumento standard per il ragionamento probabilistico, offrendo rappresentazioni compatte e fattorizzate di distribuzioni di probabilità congiunte e consentendo algoritmi di inferenza efficienti. Tuttavia, gli approcci categoriali esistenti al ragionamento probabilistico, pur fornendo un linguaggio composizionale e grafico ricco (ad esempio, i diagrammi a stringa), spesso non tengono conto del costo computazionale (tempo e spazio) dell'inferenza. Al contrario, gli algoritmi standard delle BN sono efficienti ma mancano di un fondamento teorico della prova profondo che unifichi il ragionamento grafico con le proprietà strutturali della logica. Gli autori identificano una lacuna nel fornire un framework che accolga simultaneamente il ragionamento grafico e composizionale e l'efficienza computazionale, affrontando specificamente la prospettiva "consapevole del costo" (cost-aware) che spesso manca nella probabilità categoriale.

Metodologia
Il saggio propone un account teorico della prova dell'inferenza bayesiana utilizzando la Logica Lineare (LL), specificamente la sua sintassi di grafi nota come proof-nets. La metodologia prevede:

1. Estensione del Formalismo: Gli autori estendono la Logica Lineare Moltiplicativa (MLL) con scatole probabilistiche (probabilistic boxes). Queste scatole codificano le Tabelle di Probabilità Condizionata (CPT) associate ai nodi di una Rete Bayesiana. La sintassi include i nodi standard della MLL (tensor, par, cut, axiom) più le regole strutturali (weakening, contraction) e queste nuove scatole probabilistiche.
2. Corrispondenza: Gli autori stabiliscono una corrispondenza sonora e completa tra Reti Bayesiane e Bayesian Proof-Nets (bpn). Un bpn è definito come un proof-net in cui le scatole memorizzano CPT, le conclusioni positive sono distinte e tutte le conclusioni sono positive.
3. Semantica tramite Fattori: Adottando la semantica basata sui fattori del lavoro precedente (ad es. [8]), la semantica di un bpn è definita come il prodotto dei fattori (CPT) associati alle sue scatole, seguito dalla marginalizzazione (somma delle variabili) delle variabili non presenti nelle conclusioni. Ciò allinea la semantica direttamente con la definizione standard delle BN.
4. Decomposizione del Grafo: A differenza dei proof-trees, che si decompongono strettamente secondo la sintassi induttiva, i proof-nets permettono una decomposizione grafica flessibile. Gli autori utilizzano lo splitting (tramite ax-expansion) per decomporre un bpn in sub-net connesse da nodi di cut, formando una struttura chiamata cut-net.
5. Graph Rewriting: Il saggio impiega l'eliminazione del cut (cut-elimination) e il suo duale (cut-expansion) come processo di graph-rewriting. Questo include regole di riduzione standard e una specifica riduzione box/weakening utilizzata per "potare" il grafo, eseguendo efficacementmente la marginalizzazione rimuovendo le variabili irrilevanti.

Contributi Chiave

• Account Teorico della Prova dell'Inferenza: Il saggio fornisce una comprensione fondamentale in cui l'eliminazione del cut e l'espansione del cut giocano un ruolo centrale nell'inferenza bayesiana. Inquadra l'inferenza non solo come un calcolo, ma come una trasformazione strutturale delle prove.
• Componibilità più Forte: Gli autori introducono una nozione di "componente" specifica per i grafi, che è più forte delle precedenti definizioni basate su alberi. Dimostrano il Teorema 5.2 (Graphs Compositionality), dimostrando che la semantica di un proof-net può essere computata in modo composizionale indipendentemente da come il grafo viene decomposto in sub-net connesse da cut.
  $$\llbracket Cut(R_1, R_2) \rrbracket = \sum_Z (\llbracket R_1 \rrbracket \odot \llbracket R_2 \rrbracket)$$
  dove $Z$ rappresenta i nomi da marginalizzare.
• Dimostrazione Grafica della d-Separazione: Nella Sezione 7, gli autori forniscono una dimostrazione diagrammatica diretta della correttezza della d-separazione (un criterio di indipendenza condizionata). Utilizzando la decomposizione del grafo e la componibilità della semantica, mostrano che se due insiemi di variabili sono disconnessi nel grafo (dopo la rimozione degli archi etichettati da un insieme di condizionamento), essi sono condizionatamente indipendenti.
• Inferenza Efficiente tramite Cut-Nets: Il saggio dimostra come mimare gli algoritmi efficienti di inferenza delle BN (come l'eliminazione delle variabili) utilizzando i proof-net. Trasformando un bpn in una rooted cut-net (una struttura a albero di sub-net), gli autori mostrano che il costo computazionale può essere significato ridotto. Il costo è determinato dalla larghezza (width) della cut-net (il numero massimo di variabili in una qualsiasi sub-net), piuttosto che dal numero totale di variabili.
• Tipizzazione e Sequenzializzazione: Gli autori affrontano la sfida per cui le decomposizioni di grafi (cut-nets) non sempre corrispondono direttamente a proof-trees del calcolo dei sequenti. Dimostrano (Teorema 8.3) che qualsiasi cut-net può essere trasformata tramite $\otimes/\parr$-espansioni in una forma equivalente in cui le sub-net sono connesse da al massimo un cut, consentendo così alla decomposizione di essere tradotta nuovamente in un valido proof-tree del calcolo dei sequenti.

Risultati

• Soundness e Completezza: La corrispondenza tra BN e bpn è provata come sonora e completa. Ogni BN mappa a un bpn positivo, e la forma normale di qualsiasi bpn positivo mappa nuovamente a una BN.
• Terminazione e Confluenza: I sistemi di riduzione (inclusi il cut-elimination standard e la nuova riduzione box/weakening) sono provati come terminanti e confluenti.
• Efficienza dei Costi: Il saggio mostra che fattorizzando un proof-net in una cut-net, la complessità di spazio e tempo per calcolare la semantica scende da $O(m \cdot 2^n)$ (dove $n$ è il numero totale di variabili) a $O(n \cdot 2^w)$, dove $w$ è la larghezza della cut-net. Questo rispecchia i guadagni di efficienza dell'eliminazione delle variabili nelle BN.
• Invarianza: La semantica di un bpn è invariante rispetto alla riduzione e all'espansione, garantendo che il significato probabilistico sia preservato durante il processo di rewriting.

Significato
Il saggio sostiene di "sbloccare il meglio di entrambi gli approcci": l'efficienza del calcolo fattorizzato tipico delle Reti Bayesiane e il ragionamento grafico e composizionale della teoria della prova. Fondando l'inferenza bayesiana nel ricco arsenale della Logica Lineare, gli autori forniscono un framework che è intrinsecamente "consapevole delle risorse". Ciò consente un trattamento unificato in cui la manipolazione strutturale delle prove (graph rewriting) corrisponde direttamente ai passi di inferenza probabilistica (marginalizzazione e condizionamento). Il lavoro colma il divario tra l'elegante astrazione strutturale della probabilità categoriale e i requisiti pratici e orientati al costo del ragionamento probabilistico, offrendo una nuova prospettiva in cui la "pietra angolare della teoria della prova" (cut-elimination) funge da meccanismo per l'inferenza efficiente.