Static Factorisation of Probabilistic Programs with User-Labelled Sample Statements and While Loops
This program is tentative and subject to change.
It is commonly known that any Bayesian network can be implemented as a probabilistic program, but the reverse direction is not so clear.
In this work, we address the open question to what extent a probabilistic program with user-labelled sample statements and while loops - features found in languages like Gen, Turing, and Pyro - can be represented graphically.
To this end, we extend existing operational semantics to support these language features.
By translating a program to its control-flow graph, we define a sound static analysis that approximates the dependency structure of the random variables in the program.
As a result, we obtain a static factorisation of the implicitly defined program density, which is equivalent to the known Bayesian network factorisation for programs without loops and constant labels, but constitutes a novel graphical representation for programs that define an unbounded number of random variables via loops or dynamic labels.
We further develop a sound program slicing technique to leverage this structure to statically enable three well-known optimisations for the considered program class:
we reduce the variance of gradient estimates in variational inference and we speed up both single-site Metropolis Hastings and sequential Monte Carlo.
These optimisations are proven correct and empirically shown to match or outperform existing techniques.