(joint work with Thomas Ehrhard and Michele Pagani )

This talk proposes a proof-theoretical account of Bayesian Inference, by uncovering a close correspondence between two graphical languages, namely Bayesian Networks and Proof Nets. The former is a prominent graphical model for probabilistic reasoning. The latter is a graph formalism for Linear Logic proofs and (via the Curry-Howard correspondence of proofs as programs) a powerful tool to analyze the dynamics of proof/the execution of programs. Their natural interpretation into Probabilistic Coherence Spaces makes Proof Nets into probabilistic models.

The correspondence which we develop involves both the representation and the computation of a probabilistic model. In particular, we relate the most widely used algorithm for exact inference (message passing over clique trees) with the inductive interpretation of a proof, opportunely factorized into a composition of smaller proofs. The correspondence turns out to be so tight, that even the computational cost of inference is similar. We will also discuss some of the perspectives which proof theory could bring, such as compositionality (via types) and structure (hierarchical models).