Weakest Preexpectation Semantics for Bayesian Inference

TL;DR

This paper introduces a new semantics for a probabilistic programming language with continuous distributions and soft conditioning, capable of handling divergence with positive probability, and proves its consistency with an alternative trace-based semantics.

Contribution

It extends the weakest preexpectation semantics to support continuous distributions and soft conditioning in probabilistic programs, ensuring soundness and consistency.

Findings

Semantics handles divergence with positive probability

Equivalence between weakest preexpectation and trace-based semantics established

Applicability demonstrated through various examples

Abstract

We present a semantics of a probabilistic while-language with soft conditioning and continuous distributions which handles programs diverging with positive probability. To this end, we extend the probabilistic guarded command language (pGCL) with draws from continuous distributions and a score operator. The main contribution is an extension of the standard weakest preexpectation semantics to support these constructs. As a sanity check of our semantics, we define an alternative trace-based semantics of the language, and show that the two semantics are equivalent. Various examples illustrate the applicability of the semantics.