Probabilistic programming meets automata theory: Exact inference using weighted automata

Theoretical Computer Science, vol. 1087, pp. 116224

Abstract

In probabilistic programming, inference means characterizing a program’s posterior distribution conditioned on data incorporated via observe instructions. Problems from a wide range of application areas can be phrased as inference tasks in probabilistic programming languages, often in an intuitive, programmer-friendly manner. This has sparked the development of many inference algorithms, which typically rely on statistical approximation to achieve scalability. When exact inference results are required, however, algorithmic inference remains challenging, and the boundaries of decidability are still not well-understood. This is especially true for programs operating over infinite state spaces, induced, e.g., via samples from infinite-support distributions. To address this challenge, we propose encoding distributions on N k as weighted automata over a commutative alphabet with k symbols. In analogy to probability generating functions , we call our automaton model probability generating automata (PGA). We map the semantics of selected imperative programming statements to automata-theoretic standard constructions, such as products and concatenations. For a rich class of programs, this yields an algorithmic translation from the prior to the posterior distribution, both encoded as PGAs, which we prove sound relative to an established operational Markov chain semantics. Finally, we show how to query PGAs to characterize posterior probabilities, expected values, and higher as well as mixed moments, thereby enabling exact inference on a non-trivial class of programs featuring infinite-support distributions.

Authors 1

1. Dominik Geißler corresponding

   Technische Universität Berlin

   Affiliation as printed

   Technische Universität Berlin, Berlin, Germany