Formally Verified Samplers From Probabilistic Programs With Loops and Conditioning

TL;DR

This paper introduces Zar, a fully verified compiler pipeline that translates probabilistic programs with loops into correct executable samplers, ensuring correctness through formal proofs in Coq and empirical validation.

Contribution

The paper presents Zar, a novel verified compiler pipeline for probabilistic programs with loops, reducing distributions to coin-flips and ensuring correctness via formal proofs.

Findings

Verified samplers are correct with respect to source semantics.

The pipeline successfully translates complex probabilistic programs into executable code.

Empirical validation confirms the practical effectiveness of the approach.

Abstract

We present Zar: a formally verified compiler pipeline from discrete probabilistic programs with unbounded loops in the conditional probabilistic guarded command language (cpGCL) to proved-correct executable samplers in the random bit model. We exploit the key idea that all discrete probability distributions can be reduced to unbiased coin-flipping schemes. The compiler pipeline first translates a cpGCL program into choice-fix trees, an intermediate representation suitable for reduction of biased probabilistic choices. Choice-fix trees are then translated to coinductive interaction trees for execution within the random bit model. The correctness of the composed translations establishes the sampling equidistribution theorem: compiled samplers are correct wrt. the conditional weakest pre-expectation semantics of cpGCL source programs. Zar is implemented and fully verified in the Coq proof assistant. We extract verified samplers to OCaml and Python and empirically validate them on a number of illustrative examples.