Exact Bayesian Inference for Loopy Probabilistic Programs


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.

arXiv, abs/2307.07314
Mingshuai Chen
Mingshuai Chen
ZJU100 Young Professor

My research interests include formal verification, programming theory, and logical aspects of computer science.