# Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming

arXiv: https://arxiv.org/abs/2204.02948 · HTML: https://mlsanity.com/paper/2204.02948/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 68 references that are in the map.
- First posted on arXiv 6 Apr 2022.

## Builds on (most cited first, 16 of 16)

- [Pyro: Deep Universal Probabilistic Programming](https://mlsanity.com/paper/1810.09538/) (2018)
- [Advances in Variational Inference](https://mlsanity.com/paper/1711.05597/) (2017)
- [Validating Bayesian Inference Algorithms with Simulation-Based Calibration](https://mlsanity.com/paper/1804.06788/) (2018)
- [An Introduction to Probabilistic Programming](https://mlsanity.com/paper/1809.10756/) (2018)
- [Sandwiching the marginal likelihood using bidirectional Monte Carlo](https://mlsanity.com/paper/1511.02543/) (2015)
- [Automatic Reparameterisation of Probabilistic Programs](https://mlsanity.com/paper/1906.03028/) (2019)
- [Etalumis: Bringing Probabilistic Programming to Scientific Simulators at Scale](https://mlsanity.com/paper/1907.03382/) (2019)
- [SPPL: Probabilistic Programming with Fast Exact Symbolic Inference](https://mlsanity.com/paper/2010.03485/) (2020)
- [A Lambda-Calculus Foundation for Universal Probabilistic Programming](https://mlsanity.com/paper/1512.08990/) (2015)
- [Measuring the reliability of MCMC inference with bidirectional Monte Carlo](https://mlsanity.com/paper/1606.02275/) (2016)
- [Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere](https://mlsanity.com/paper/2004.03924/) (2020)
- [AIDE: An algorithm for measuring the accuracy of probabilistic inference algorithms](https://mlsanity.com/paper/1705.07224/) (2017)
- [Nonparametric Hamiltonian Monte Carlo](https://mlsanity.com/paper/2106.10238/) (2021)
- [LF-PPL: A Low-Level First Order Probabilistic Programming Language for Non-Differentiable Models](https://mlsanity.com/paper/1903.02482/) (2019)
- [Supermartingales, Ranking Functions and Probabilistic Lambda Calculus](https://mlsanity.com/paper/2102.11164/) (2021)
- [On Probabilistic Termination of Functional Programs with Continuous Distributions](https://mlsanity.com/paper/2104.04990/) (2021)

## Built on by (most cited first, 1 of 1)

- [Rethinking Variational Inference for Probabilistic Programs with Stochastic Support](https://mlsanity.com/paper/2311.00594/) (2023)

## Abstract (arXiv)

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.