In Bayesian probabilistic programming, a central problem is to estimate the normalised posterior distribution (NPD) of a probabilistic program with conditioning. Prominent approximate approaches to address this problem include Markov chain Monte Carlo and variational inference, but neither can generate guaranteed outcomes within limited time. Moreover, most existing formal approaches that perform exact inference for NPD are restricted to programs with closed-form solutions or bounded loops/recursion. A recent work (Beutner et al., PLDI 2022) derived guaranteed bounds for NPD over programs with unbounded recursion. However, as this approach requires recursion unrolling, it suffers from the path explosion problem. Furthermore, previous approaches do not consider score-recursive probabilistic programs that allow score statements inside loops, which is non-trivial and requires careful treatment to ensure the integrability of the normalising constant in NPD. In this work, we propose a novel automated approach to derive bounds for NPD via polynomial templates. Our approach can handle probabilistic programs with unbounded while loops and continuous distributions with infinite supports. The novelties in our approach are three-fold: First, we use polynomial templates to circumvent the path explosion problem from recursion unrolling; Second, we derive a novel multiplicative variant of Optional Stopping Theorem that addresses the integrability issue in score-recursive programs; Third, to increase the accuracy of the derived bounds via polynomial templates, we propose a novel technique of truncation that truncates a program into a bounded range of program values. Experiments over a wide range of benchmarks demonstrate that our approach is time-efficient and can derive bounds for NPD that are comparable with (or tighter than) the recursion-unrolling approach (Beutner et al., PLDI 2022).

翻译：在贝叶斯概率编程中，核心问题之一是估计带条件概率程序的正则化后验分布（NPD）。解决该问题的典型近似方法包括马尔可夫链蒙特卡洛和变分推断，但两者均无法在有限时间内生成有保证的结果。此外，现有大多数对NPD进行精确推断的形式化方法受限于具有闭式解或有界循环/递归的程序。近期工作（Beutner等，PLDI 2022）为包含无界递归的程序推导了NPD的保证界。然而，该方法因需要递归展开而面临路径爆炸问题。更关键的是，现有方法未考虑允许循环内包含评分语句的评分递归概率程序——这类程序需要谨慎处理以确保NPD中归一化常数的可积性。本文提出一种基于多项式模板的自动化方法，可推导NPD的界。该方法能处理包含无界while循环及连续分布（支持域无限）的概率程序。创新点有三：第一，利用多项式模板规避递归展开导致的路径爆炸问题；第二，提出可选停止定理的新型乘法变体，解决评分递归程序中的可积性问题；第三，针对多项式模板推导精度的提升，提出截断技术，将程序截断至有界程序值范围。在广泛基准测试上的实验表明，该方法具有时间效率优势，且推导的NPD界可与递归展开方法（Beutner等，PLDI 2022）媲美（或更紧致）。