Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming
| Autor: | Beutner, Raven, Ong, Luke, Zaiser, Fabian |
|---|---|
| Rok vydání: | 2022 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: Extended version of the PLDI 2022 article, including proofs and other supplementary material |
| Databáze: | arXiv |
| Externí odkaz: |
|