一句话：提出经 Coq 形式验证的 Zar 编译器，将带循环与条件化的离散概率程序编译为正确采样器。
论文解决如何从含无界循环与条件化的离散概率程序生成分布正确的可执行采样器的问题。作者提出 Zar：一条在 Coq 中完整形式验证的编译流水线。其核心思想是将离散概率分布归约为无偏抛硬币方案。流水线先把条件概率守卫命令语言 cpGCL 程序翻译为 choice-fix 树，以便归约有偏概率选择；再翻译为共归纳交互树，在随机位模型下执行。组合翻译的正确性给出采样等分布定理：编译出的采样器相对于 cpGCL 源程序的条件最弱前置期望语义是正确的。Zar 已实现并验证，可提取为 OCaml 与 Python 采样器，并在若干示例上做了经验验证。
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 cpGCL programs 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.
@article{paperbot1954,
title = {Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning},
author = {Alexander Bagnall and Gordon Stewart and Anindya Banerjee},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591220}
}