Guaranteed Bounds for Normalised Posterior Distribution in Bayesian Probabilistic Programming via Polynomial Solving

This work proposes a novel automated approach to derive guaranteed bounds for the normalised posterior distribution (NPD) of Bayesian probabilistic programs via polynomial solving. The approach handles a wide class of programs, including those with unbounded while loops and continuous distributions with infinite supports, and can address the integrability issue in score-recursive programs.