Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming
This work addresses the challenge of ensuring correctness in posterior inference for probabilistic programming, which is crucial for reliable applications in fields like machine learning and statistics, though it is incremental in providing bounds rather than exact solutions.
The authors tackled the problem of approximating posterior distributions in probabilistic programming by developing a method to compute guaranteed bounds, proving that the actual posterior is sandwiched between these bounds and that they converge to it. Their tool, GuBPI, demonstrated utility in evaluations, including detecting errors in stochastic inference outputs.
We propose a new method to approximate the posterior distribution of probabilistic programs by means of computing guaranteed bounds. The starting point of our work is an interval-based trace semantics for a recursive, higher-order probabilistic programming language with continuous distributions. Taking the form of (super-/subadditive) measures, these lower/upper bounds are non-stochastic and provably correct: using the semantics, we prove that the actual posterior of a given program is sandwiched between the lower and upper bounds (soundness); moreover the bounds converge to the posterior (completeness). As a practical and sound approximation, we introduce a weight-aware interval type system, which automatically infers interval bounds on not just the return value but also weight of program executions, simultaneously. We have built a tool implementation, called GuBPI, which automatically computes these posterior lower/upper bounds. Our evaluation on examples from the literature shows that the bounds are useful, and can even be used to recognise wrong outputs from stochastic posterior inference procedures.