Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops

This video presents a research talk from POPL 2025 that explores novel approaches for bounding posterior distributions in discrete probabilistic programs containing loops and conditioning. Discover two groundbreaking methods for addressing the challenges of Bayesian inference in programs with unbounded support: the residual mass semantics approach, which provides flat bounds based on residual probability mass, and the geometric bound semantics approach, which works with eventually geometric distributions using contraction invariants. Learn how these fully automated techniques provide guaranteed bounds that sandwich true distributions, offering more provable guarantees than sampling-based inference methods. The presentation covers theoretical properties including soundness and convergence, as well as Diabolo, a practical implementation evaluated on various benchmarks. The research demonstrates how to bound not just probabilities but also moments and tail asymptotics, particularly valuable for programs where exact Bayesian inference is challenging. Presented by researchers from the University of Oxford and Nanyang Technological University, this 20-minute talk includes access to the published article and supplementary materials with reusable artifacts.