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

TL;DR

This work couples Bayesian reasoning with resource-aware proof theory by encoding Bayesian Networks as Bayesian proof-nets in a linear-logic setting. It develops a factor-based semantics where CPTs become probabilistic boxes and the joint distribution is computed via factor products and sums, enabling compositional and graph-centric inference. The authors prove that semantics are invariant under graph reductions and demonstrate graphical d-separation reasoning directly on proof-nets, while addressing computational costs through cut-net decompositions and width-based cost bounds. The approach provides a unified, cost-aware framework for exact Bayesian inference that leverages the strengths of both probabilistic reasoning and proof-theoretic graphical representations, with potential implications for scalable, compositional probabilistic reasoning in complex systems.

Abstract

We study the correspondence between Bayesian Networks and graphical representation of proofs in linear logic. The goal of this paper is threefold: to develop a proof-theoretical account of Bayesian inference (in the spirit of the Curry-Howard correspondence between proofs and programs), to provide compositional graphical methods, and to take into account computational efficiency. We exploit the fact that the decomposition of a graph is more flexible than that of a proof-tree, or of a type-derivation, even if compositionality becomes more challenging.

Figures (2)

• Figure 1: Example of Bayesian Network
• Figure 2: Proof-net $\mathcal{R}_D$