带循环的离散概率程序后验分布的保证界限

我们研究具有无界支持、循环和条件化的离散概率程序后验分布的界限问题。循环是该设定下的主要难点：即使精确贝叶斯推断可行，现有技术也需要用户提供循环不变量模板。相比之下，我们旨在寻找保证界限，即能夹住真实分布的上下界。它们完全自动化，适用于更多程序，并比近似采样推断提供更多可证明的保证。由于下界可通过循环展开获得，主要挑战在于上界，我们从两方面着手解决。第一种称为残余质量语义，它是基于循环残余概率质量的平坦界限。该方法简单、高效，且具有可证明的保证。本工作的主要创新是第二种方法，称为几何界限语义。它作用于一类新的分布族——最终几何分布（EGDs），并能利用一种新型循环不变量——收缩不变量，来界定循环的分布。不变量综合问题归结为一个多项式不等式约束系统，这是一个可判定问题，存在自动求解器。若存在解，则能得到整个分布上指数衰减的界限，从而不仅能界定概率（如第一种方法），还能界定矩和尾部渐近行为。两种语义都具有良好的理论性质。特别是，我们证明了可靠性和收敛性，即随着循环进一步展开，界限收敛到精确后验。在实践方面，我们描述了Diabolo——一种两种语义的全自动实现，并在文献中的多种基准上进行评估，展示了它们的普遍适用性和所得界限的实用性。