# Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops

## TL;DR

This paper introduces a static analysis method for probabilistic programs with user-labelled sample statements and loops, enabling graphical representation and optimizations for inference algorithms.

## Contribution

It extends operational semantics and control-flow graph translation to represent unbounded variable dependencies in probabilistic programs with loops and labels.

## Key findings

- Provides a sound static factorisation for programs with loops and labels.
- Enables optimizations that reduce variance and improve inference speed.
- Empirically outperforms existing inference techniques.

## Abstract

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.