Inference and Verification for Statistical Probabilistic Programming

This project falls within the EPSRC Information and communication technologies (ICT) research area.

Statistical probabilistic programming is a framework for constructing probabilistic models by writing programs that can sample from prior distributions and condition on observations, and then automatically performing Bayesian inference to extract the posterior distribution over parameters using general-purpose inference algorithms.
The dream is to allow users to declare complex stochastic generative models that incorporate domain-specific knowledge, with model specification being decoupled from the inference method.
This project aims to develop tools for verifying the correctness of widely-used inference algorithms, as well as extending them to work on wider classes of probabilistic programs.

One aim is to establish properties that are necessary for correctness of inference algorithms in an automated manner by developing static analyses.
For gradient-based inference algorithms (such as Hamiltonian Monte-Carlo), almost-everywhere differentiability of the program's weight function is important for correctness, and can be established by proving that the program almost-surely terminates.
We hope to create better algorithmic methods for proving almost-sure termination, based on martingale theory.
Similar challenges arise in variational inference methods, where the "guide" program that is used as a variational approximation must be compatible with the respect to the true posterior to guarantee properties such as convergence.
Such compatibility properties can be established statically using tools from programming language theory, such as abstract interpretation, and we hope to extend this to new inference algorithms and program properties.

A second aim is to increase the generality of existing inference algorithms such that they can be applied to wider classes of programs. This is a necessary aim if we are to fully decouple model specification from inference.
A probabilistic program with dynamic control-flow can represent a model with an unbounded number of parameters (non-parametric).
It remains challenging to perform efficient inference for models that are non-parametric and which combine continuous and discrete latent variables (mixed support).
Although recent work has made progress towards adapting variational inference and Monte-Carlo methods to programs with mixed support, handling non-parametric models remains an open area of research that we hope to address.

Within the ICT theme, this project is part of the Programming languages and compilers area, since it aims to inform new designs for probabilistic programming languages, and develop new tools such as static analyses that could be integrated in practical languages.
It is also part of the Artificial Intelligence technologies area, since it aims to extend existing inference algorithms to wider classes of models, as well building tools for establishing the correctness of existing inference frameworks.