We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly unbounded looping behaviors. Our method is built on an extended denotational semantics represented by probability generating functions, which resolves semantic intricacies induced by intertwining discrete probabilistic loops with conditioning (for encoding posterior observations). We implement our method in a tool called Prodigy; it augments existing computer algebra systems with the theory of generating functions for the (semi-)automatic inference and quantitative verification of conditioned probabilistic programs. Experimental results show that Prodigy can handle various infinite-state loopy programs and outperforms state-of-the-art exact inference tools over benchmarks of loop-free programs.

翻译：我们提出了一种针对由可能包含无界循环行为的概率程序所编码的后验分布的精确贝叶斯推断方法。该方法建立在由概率生成函数扩展的指称语义之上，该语义解决了离散概率循环与条件化（用于编码后验观测）相互交织所引发的语义复杂性。我们将该方法实现于名为Prodigy的工具中，它利用生成函数理论对现有计算机代数系统进行增强，以支持条件化概率程序的（半）自动推断与定量验证。实验结果表明，Prodigy能够处理各类无限状态循环程序，并在针对无环程序基准测试中优于当前最先进的精确推断工具。