Probabilistic programs are typically normal-looking programs describing posterior probability distributions. They intrinsically code up randomized algorithms and have long been at the heart of modern machine learning and approximate computing. We explore the theory of generating functions [19] and investigate its usage in the exact quantitative reasoning of probabilistic programs. Important topics include the exact representation of program semantics [13], proving exact program equivalence [5], and -- as our main focus in this extended abstract -- exact probabilistic inference. In probabilistic programming, inference aims to derive a program's posterior distribution. In contrast to approximate inference, inferring exact distributions comes with several benefits [8], e.g., no loss of precision, natural support for symbolic parameters, and efficiency on models with certain structures. Exact probabilistic inference, however, is a notoriously hard task [6,12,17,18]. The challenges mainly arise from three program constructs: (1) unbounded while-loops and/or recursion, (2) infinite-support distributions, and (3) conditioning (via posterior observations). We present our ongoing research in addressing these challenges (with a focus on conditioning) leveraging generating functions and show their potential in facilitating exact probabilistic inference for discrete probabilistic programs.

翻译：概率程序通常是描述后验概率分布的普通程序。它们本质上是随机算法的编码实现，长期处于现代机器学习和近似计算的核心。我们探索生成函数理论[19]，并研究其在概率程序精确定量推理中的应用。重要课题包括程序语义的精确表示[13]、程序精确等价性的证明[5]，以及——作为本扩展摘要的核心重点——精确概率推理。在概率编程中，推理旨在推导程序的后验分布。与近似推理相比，精确分布的推导具有若干优势[8]，例如：无精度损失、自然支持符号化参数、以及特定结构模型上的高效率。然而，精确概率推理是公认的难题[6,12,17,18]。挑战主要来自三种程序结构：(1)无界循环和/或递归；(2)无限支撑分布；(3)条件化（通过后验观测）。我们介绍了当前应对这些挑战（聚焦于条件化问题）的研究进展，该工作利用生成函数展示了其在促进离散概率程序精确概率推理方面的潜力。