论文标题
程序会产生正确的分配吗？通过生成功能验证概率程序
Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
论文作者
论文摘要
我们研究具有无限状态空间上潜在无限循环行为的离散概率程序。据我们所知，我们介绍了确定该程序是否在其输出上精确生成指定分布的问题的第一个可决定性结果（前提是该程序几乎可以肯定终止）。可以在我们的形式主义中指定的分布类别包括标准分布（几何，统一等）及其有限的卷积。我们的方法依赖于将这些（可能是无限支持）分布表示为概率生成的函数，这些函数吸收了有效的算术操作。我们已经在一种称为Prodigy的工具中自动化了我们的技术，该工具支持自动不变性检查，嵌套环的组成推理以及在各种数量到输出分布的有效查询，如实验所示。
We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the best of our knowledge, the first decidability result for the problem of determining whether such a program generates exactly a specified distribution over its outputs (provided the program terminates almost surely). The class of distributions that can be specified in our formalism consists of standard distributions (geometric, uniform, etc.) and finite convolutions thereof. Our method relies on representing these (possibly infinite-support) distributions as probability generating functions which admit effective arithmetic operations. We have automated our techniques in a tool called prodigy, which supports automatic invariance checking, compositional reasoning of nested loops, and efficient queries on various quantities of to the output distribution, as demonstrated by experiments.
