Bayesian Separation Logic

TL;DR

Bayesian separation logic (BaSL) introduces a formal framework for reasoning about Bayesian updating and probabilistic properties in probabilistic programming languages, enabling modular analysis of complex statistical models.

Contribution

BaSL is the first separation logic that models Bayesian updating, providing semantics for BPPLs and supporting properties like conjugate priors and conditional distributions.

Findings

Proves an internal version of Bayes' theorem using measure theory.

Models Bayesian models such as Gaussian mixtures and Bayesian networks.

Demonstrates properties like expected values and correlations in statistical models.

Abstract

Bayesian probabilistic programming languages (BPPLs) let users denote statistical models as code while the interpreter infers the posterior distribution. The semantics of BPPLs are usually mathematically complex and unable to reason about desirable properties such as expected values and independence of random variables. To reason about these properties in a non-Bayesian setting, probabilistic separation logics such as PSL and Lilac interpret separating conjunction as probabilistic independence of random variables. However, no existing separation logic can handle Bayesian updating, which is the key distinguishing feature of BPPLs. To close this gap, we introduce Bayesian separation logic (BaSL), a probabilistic separation logic that gives semantics to BPPL. We prove an internal version of Bayes' theorem using a result in measure theory known as the Rokhlin-Simmons disintegration theorem. Consequently, BaSL can model probabilistic programming concepts such as Bayesian updating, unnormalised distribution, conditional distribution, soft constraint, conjugate prior and improper prior while maintaining modularity via the frame rule. The model of BaSL is based on a novel instantiation of Kripke resource monoid via $\sigma$-finite measure spaces over the Hilbert cube, and the semantics of Hoare triple is compatible with an existing denotational semantics of BPPL based on the category of $s$-finite kernels. Using BaSL, we then prove properties of statistical models such as the expected value of Bayesian coin flip, correlation of random variables in the collider Bayesian network, the posterior distributions of the burglar alarm model, a parameter estimation algorithm, and the Gaussian mixture model.