一句话：提出用多项式求解静态推断贝叶斯概率程序的归一化后验分布边界，并支持 score 递归程序。
在贝叶斯概率编程中，核心问题是在带 score/observe 条件语句的程序中估计归一化后验分布（NPD）。现有 MCMC 与变分推断无法在有限时间内给出保证结果，而精确推断方法又常受语法限制或不能保证成功。本文提出一种自动静态方法，通过多项式求解为 NPD 推导可保证的上下界。作者首先针对几乎必然终止且仅在程序终止处含单个有界 score 的 score-at-end 程序建立不动点定理；随后提出 Optional Stopping Theorem 的乘法变体，以处理循环内可能含权重大于 1 的 score 语句的 score-recursive 程序，并可表示存在可积性困难的贝叶斯非参数模型。实现上使用多项式求解，并引入截断操作及跨多个程序输入的界综合以提高精度。实验表明，该方法可处理无界 while 循环和无限支撑连续分布；与 Beutner 等（PLDI 2022）基于递归展开的方法相比更省时，得到的 NPD 边界相当甚至更紧，且能处理此前方法无法处理的 score-recursive 程序。
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. Bayesian nonparametric models, enjoying a renaissance in statistics and machine learning, can be represented by score-recursive Bayesian programs and are difficult to handle due to an integrability issue. 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{WangYFLO24,
title = {Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving},
author = {Peixin Wang and Tengshun Yang and Hongfei Fu and Guanyan Li and C.-H. Luke Ong},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656432}
}