Design and Implementation of Probabilistic Programming Languages for Sound and Scalable Inference

Abstract

Probabilistic programming languages (PPLs) provide a powerful framework for specifying and solving complex Bayesian inference problems using general-purpose programming constructs. However, the same linguistic expressiveness that makes PPLs appealing also introduces challenges for performing sound and scalable inference.

This thesis explores the design and implementation of PPLs by developing novel compilation strategies targeting different inference methods and compilation artifacts. This thesis centers on four major systems. Fidelio addresses deep amortized inference by generating neural guide programs via a type-preserving and dependence-aware translation, ensuring soundness with respect to absolute continuity; Mappl targets exact inference via variable elimination, compiling probabilistic programs with bounded recursion to factor functions guided by an information-flow type system; Geni enables scalable exact inference for discrete models by compiling to generating functions, offering a mathematically principled and efficient representation; Tessa reframes probabilistic model checking for step-bounded reachability as tensor computations, enabling sound compilation into JAX programs and accelerator-backed execution for substantial speedups. The central thesis is that the compiler perspective leads to sound, scalable ways to automate probabilistic inference for a rich class of probabilistic models.