Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bayesian Networks and Proof-Nets: a proof-theoretical account of Bayesian Inference

Thomas Ehrhard, Claudia Faggian, Michele Pagani

TL;DR

The paper builds a formal bridge between Bayesian Networks and Multiplicative Linear Logic Proof-Nets by introducing Bayesian proof-nets (bpn) and a Probabilistic Coherence Space (PCoh) semantics. It shows that a bpn with valuation $\iota$ denotes the same joint distribution as the corresponding Bayesian Network via $\llbracket \mathcal{R} \rrbracket^{\iota}$, and that this denotation is invariant under normalization and other transformations. By factorizing bpns into cut-nets and wiring components, the authors align the proof-theoretic decomposition with BN clique-tree decompositions, enabling efficient inference that mirrors message passing on clique trees. They also provide methods to compute individual marginals efficiently, and establish a tight correspondence between factorized interpretation and standard probabilistic inference, yielding a proof-theoretical perspective on Bayesian reasoning and practical implications for inference costs.

Abstract

We uncover a strong correspondence between Bayesian Networks and (Multiplicative) Linear Logic Proof-Nets, relating the two as a representation of a joint probability distribution and at the level of computation, so yielding a proof-theoretical account of Bayesian Inference.

Bayesian Networks and Proof-Nets: a proof-theoretical account of Bayesian Inference

TL;DR

The paper builds a formal bridge between Bayesian Networks and Multiplicative Linear Logic Proof-Nets by introducing Bayesian proof-nets (bpn) and a Probabilistic Coherence Space (PCoh) semantics. It shows that a bpn with valuation denotes the same joint distribution as the corresponding Bayesian Network via , and that this denotation is invariant under normalization and other transformations. By factorizing bpns into cut-nets and wiring components, the authors align the proof-theoretic decomposition with BN clique-tree decompositions, enabling efficient inference that mirrors message passing on clique trees. They also provide methods to compute individual marginals efficiently, and establish a tight correspondence between factorized interpretation and standard probabilistic inference, yielding a proof-theoretical perspective on Bayesian reasoning and practical implications for inference costs.

Abstract

We uncover a strong correspondence between Bayesian Networks and (Multiplicative) Linear Logic Proof-Nets, relating the two as a representation of a joint probability distribution and at the level of computation, so yielding a proof-theoretical account of Bayesian Inference.
Paper Structure (61 sections, 41 theorems, 4 equations, 11 figures, 2 algorithms)

This paper contains 61 sections, 41 theorems, 4 equations, 11 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Factorized representation and factorized computation.
  3. Contents.
  4. Related work
  5. Motivating Examples
  6. An example of Bayesian Inference
  7. An example of Proof-Net
  8. Preliminaries
  9. Bayesian modeling
  10. Joint and Conditional Distributions
  11. Factorized, representation and computation.
  12. Bayesian Networks
  13. Factorized computation
  14. $\mathsf{MLL^{\mathtt B}}$: Multiplicative Linear Logic (with Boxes)
  15. Normalization and normal forms
  16. ...and 46 more sections

Key Result

Theorem 12

Let $\mathcal{M}$ be a pre-module without premises. $\mathcal{M}$ is a proof-net if, and only if, $\mathcal{M}$ is the image of a sequent calculus derivation.

Figures (11)

  • Figure 1:
  • Figure 2: Proof-net $\mathcal{R}_D$
  • Figure 3: A sequentialization of the proof-net $\mathcal{R}_D$
  • Figure 4: Grammar of nodes
  • Figure 5: Reduction Rules
  • ...and 6 more figures

Theorems & Definitions (109)

  • Example 1: Sampling from a proof-net
  • Definition 3: Joint probability distribution
  • Definition 4: Bayesian Network over variables $\mathbb X$
  • Definition 5: CPT
  • Definition 6: Factors
  • Remark 7: Cost of operations on factors
  • Definition 8: pre-modules
  • Remark 10: Weakening and Contraction
  • Definition 11: Proof-nets
  • Theorem 12: Sequentialization
  • ...and 99 more