In Bayesian probabilistic programming, a central problem is to estimate the normalised posterior distribution (NPD) of a probabilistic program with conditioning via score (a.k.a. observe) statements. Most previous approaches address this problem by Markov Chain Monte Carlo and variational inference, and therefore could not generate guaranteed outcomes within a finite time limit. Moreover, existing methods for exact inference either impose syntactic restrictions or cannot guarantee successful inference in general. In this work, we propose a novel automated approach to derive guaranteed bounds for NPD via polynomial solving. We first establish a fixed-point theorem for the wide class of score-at-end Bayesian probabilistic programs that terminate almost-surely and have a single bounded score statement at program termination. Then, we propose a multiplicative variant of Optional Stopping Theorem (OST) to address score-recursive Bayesian programs where score statements with weights greater than one could appear inside a loop. Finally, we use polynomial solving to implement our fixed-point theorem and OST variant. To improve the accuracy of the polynomial solving, we further propose a truncation operation and the synthesis of multiple bounds over various program inputs. Our approach can handle Bayesian probabilistic programs with unbounded while loops and continuous distributions with infinite supports. Experiments over a wide range of benchmarks show that compared with the most relevant approach (Beutner et al., PLDI 2022) for guaranteed NPD analysis via recursion unrolling, our approach is more time efficient and derives comparable or even tighter NPD bounds. Furthermore, our approach can handle score-recursive programs which previous approaches could not.

翻译：在贝叶斯概率编程中，一个核心问题是通过评分（即observe）语句估计带条件概率程序的归一化后验分布（NPD）。以往大多数方法通过马尔可夫链蒙特卡洛和变分推断解决该问题，因此无法在有限时间内生成保证性结果。此外，现有精确推断方法要么施加语法限制，要么无法保证通用情况下的成功推断。本文提出一种新颖的自动化方法，通过多项式求解推导NPD的保证性边界。首先，针对一类在程序末尾具有单个有界评分语句且几乎必然终止的宽类"末尾评分"贝叶斯概率程序，我们建立了不动点定理。然后，我们提出可选停止定理（OST）的乘法变体，以处理权重大于1的评分语句可能出现在循环内部的递归评分贝叶斯程序。最后，我们利用多项式求解实现所提出的不动点定理和OST变体。为提高多项式求解精度，我们进一步提出截断操作以及在多个程序输入上合成多重边界的方法。该方法可处理包含无界while循环和连续分布（具有无限支撑）的贝叶斯概率程序。在广泛基准上的实验表明，与最相关的通过递归展开进行保证性NPD分析的方法（Beutner等人，PLDI 2022）相比，我们的方法在时间效率上更优，并能推导出相当甚至更紧致的NPD边界。此外，我们的方法可处理以往方法无法处理的递归评分程序。