Sound Probabilistic Inference via Guide Types

TL;DR

This paper introduces a new probabilistic programming language that guarantees model-guide compatibility through type-enforced communication protocols, supporting complex control flow and recursion without significant performance loss.

Contribution

It presents a language with coroutine-based model and guide programs, ensuring absolute continuity via guide types and an automatic type inference algorithm.

Findings

Language supports complex models with control flow and recursion.

Type inference algorithm effectively deduces guide types.

Implementation integrates with Pyro with minimal overhead.

Abstract

Probabilistic programming languages aim to describe and automate Bayesian modeling and inference. Modern languages support programmable inference, which allows users to customize inference algorithms by incorporating guide programs to improve inference performance. For Bayesian inference to be sound, guide programs must be compatible with model programs. One pervasive but challenging condition for model-guide compatibility is absolute continuity, which requires that the model and guide programs define probability distributions with the same support. This paper presents a new probabilistic programming language that guarantees absolute continuity, and features general programming constructs, such as branching and recursion. Model and guide programs are implemented as coroutines that communicate with each other to synchronize the set of random variables they sample during their execution. Novel guide types describe and enforce communication protocols between coroutines. If the model and guide are well-typed using the same protocol, then they are guaranteed to enjoy absolute continuity. An efficient algorithm infers guide types from code so that users do not have to specify the types. The new programming language is evaluated with an implementation that includes the type-inference algorithm and a prototype compiler that targets Pyro. Experiments show that our language is capable of expressing a variety of probabilistic models with nontrivial control flow and recursion, and that the coroutine-based computation does not introduce significant overhead in actual Bayesian inference.