一句话：提出基于生成函数的精确贝叶斯推断，可处理带无界循环的概率程序。
本文研究带无界循环的概率程序的精确贝叶斯推断问题，目标是从条件观测中推断后验分布。此类程序中离散概率循环与条件化交织，会带来复杂的语义与计算挑战。作者提出以概率生成函数为核心的指称语义，用以刻画并消解这些语义纠缠，从而支持精确推断。该方法在工具 Prodigy 中实现，通过扩展现有计算机代数系统，为条件概率程序提供（半）自动推断与定量验证。实验表明，Prodigy 能处理多种无限状态循环程序，并且在无循环基准上与最先进的精确推断工具性能相当。
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.
@article{paperbot2548,
title = {Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions},
author = {Lutz Klinkenberg and Christian Blumenthal and Mingshuai Chen and Darion Haase and Joost-Pieter Katoen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649844}
}