Running Probabilistic Programs Backwards

TL;DR

This paper develops a measure-theoretic semantics for a probabilistic programming language with recursion, enabling advanced inference, rare event simulation, and verification tasks through an abstract, implementable framework.

Contribution

It introduces a measure-theoretic foundation for recursive probabilistic programs and derives an abstract semantics that supports practical inference and verification.

Findings

Successfully implemented the abstract semantics for Bayesian inference.

Enabled stochastic ray tracing for rare event simulation.

Performed probabilistic verification of floating-point error bounds.

Abstract

Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other uses such as rare event simulation and probabilistic verification---except that all such probabilistic languages are necessarily limited because they are defined or implemented in terms of an impoverished theory of probability. Measure-theoretic probability provides a more general foundation, but its generality makes finding computational content difficult. We develop a measure-theoretic semantics for a first-order probabilistic language with recursion, which interprets programs as functions that compute preimages. Preimage functions are generally uncomputable, so we derive an abstract semantics. We implement the abstract semantics and use the implementation to carry out Bayesian inference, stochastic ray tracing (a rare event simulation), and probabilistic verification of floating-point error bounds.