用正式验证的方法从具有循环和条件的概率程序中采样
摘要：Zar：从条件概率保护的命令语言（cpGCL）中的离散概率程序的带无限循环到以随机位模型为基础的经证明正确的可执行取样器的形式验证的编译器流水线。我们利用的主要思想是所有离散概率分布可以被简化为无偏的抛硬币方案。编译器流水线首先将cpGCL程序转换为选择修正树，这是一种适用于减少有偏概率选择的中间表示。然后将选择修正树转换为在随机位模型内执行的共归约交互树。组合翻译的正确性确立了采样等分布定理：编译后的取样器在cpGCL源程序的条件最弱先验语义下是正确的。Zar在Coq证明助手中实现和完全验证。我们将经验证的取样器提取到OCaml和Python中，并在许多说明性示例上进行了实证验证。
作者：Alexander Bagnall, Gordon Stewart, Anindya Banerjee
论文ID：2211.06747
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-24