I saw this work presented at ESOP 2015 by Neil Toronto, and the talk was excellent (slides).

Running Probabilistic Programs Backwards

Neil Toronto, Jay McCarthy, David Van Horn

2015

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.

(also on SciRate)

The introduction sells the practical side of the work a bit better than the abstract.

Stochastic ray tracing [30] is one such rare-event simulation task. As illus-
trated in Fig. 1, to carry out stochastic ray tracing, a probabilistic program
simulates a light source emitting a single photon in a random direction, which
is reflected or absorbed when it hits a wall. The program outputs the photon’s
path, which is constrained to pass through an aperture. Millions of paths that
meet the constraint are sampled, then projected onto a simulated sensor array.

The program’s main loop is a recursive function with two arguments: `path`

,
the photon’s path so far as a list of points, and `dir`

, the photon’s current direction.

simulate-photon path dir :=
case (find-hit (fst path) dir) of
absorb pt −→ (pt, path)
reflect pt norm −→ simulate-photon (pt, path) (random-half-dir norm)

Running `simulate-photon (pt, ()) dir`

, where `pt`

is the light source’s location and
`dir`

is a random emission direction, generates a photon path. The `fst`

of the path
(the last collision point) is constrained to be in the aperture. The remainder of
the program is simple vector math that computes ray-plane intersections.

In contrast, hand-coded stochastic ray tracers, written in general-purpose
languages, are much more complex and divorced from the physical processes they
simulate, because they must interleave the advanced Monte Carlo algorithms
that ensure the aperture constraint is met.

Unfortunately, while many probabilistic programming languages support random real numbers, none are capable of running a probabilistic program like `simulate-photon`

under constraints to carry out stochastic ray tracing. The reason is not lack of
engineering or weak algorithms, but is theoretical at its core: they are all either
defined or implemented using [density functions]. [...] Programs whose outputs are deterministic
functions of random values and programs with recursion generally cannot denote
density functions. The program `simulate-photon`

exhibits both characteristics.

Measure-theoretic probability is a more powerful alternative to this naive
probability theory based on probability mass and density functions. It not only
subsumes naive probability theory, but is capable of defining any computable
probability distribution, and many uncomputable distributions. But while even
the earliest work [15] on probabilistic languages is measure-theoretic, the theory’s
generality has historically made finding useful computational content difficult.
We show that measure-theoretic probability can be made computational by

- Using measure-theoretic probability to define a compositional, denotational
semantics that gives a valid denotation to every program.
- Deriving an abstract semantics, which allows computing answers to questions
about probabilistic programs to arbitrary accuracy.
- Implementing the abstract semantics and efficiently solving problems.

In fact, our primary implementation, Dr. Bayes, produced Fig. 1b by running a probabilistic program like `simulate-photon`

under an aperture constraint.

## Recent comments

5 hours 24 min ago

6 hours 59 min ago

7 hours 7 min ago

22 hours 51 min ago

23 hours 52 min ago

1 day 7 hours ago

2 days 5 hours ago

2 days 10 hours ago

3 days 4 hours ago

3 days 5 hours ago