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.
翻译:我们提出了 Zar:从条件概率受保护命令语言(cpGCL)中带有无限循环的离散随机程序到随机比特模型中经过证明的执行取样器的形式验证编译器管道。我们利用的关键思想是所有离散概率分布都可以简化为无偏的抛硬币方案。编译器管道首先将 cpGCL 程序转换成选择固定树,这是一种适用于减小偏向性概率选择的中间表示。选择固定树然后被翻译成交互式合作树,在随机比特模型中执行。所作翻译的正确性证明了采样等分布定理:编译的取样器在 cpGCL 源程序的条件最弱预期语义上是正确的。Zar 在 Coq 证明助手中实现和完全验证。我们提取了验证过的取样器并在一些说明性例子中对它们进行了实验证明。