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）无界while循环和/或递归，（2）具有无限支撑的分布，以及（3）条件化（通过后验观测）。我们展示了当前利用生成函数应对这些挑战（重点关注条件化）的研究进展，并阐明了它们在促进离散概率程序精确概率推断中的潜力。