We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly unbounded loops. Our method is built on a 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 exhibits comparable performance to state-of-the-art exact inference tools over loop-free benchmarks.

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