Exact probabilistic inference using generating functions

使用生成函数进行精确概率推理

https://arxiv.org/abs/2302.00513

摘要

概率程序通常是看起来普通的程序，用于描述后验概率分布。它们本质上编码了随机算法，并且一直是现代机器学习和近似计算的核心。我们探索了生成函数的理论[19]，并研究了其在概率程序的精确定量推理中的应用。重要主题包括程序语义的精确表示[13]、证明程序的精确等价性[5]，以及——作为本文扩展摘要的主要关注点——精确概率推理。

在概率编程中，推理的目标是推导程序的后验分布。与近似推理相比，推导精确分布具有许多好处[8]，例如没有精度损失、对符号参数的自然支持，以及在某些结构的模型上的高效性。然而，精确概率推理是一个臭名昭著的难题[6,12,17,18]。挑战主要来自三个程序构造：（1）无界while循环和/或递归，（2）无限支持分布，以及（3）条件化（通过后验观测）。我们介绍了我们在应对这些挑战（重点关注条件化）方面的正在进行的研究，并展示了生成函数在促进离散概率程序的精确概率推理方面的潜力。

1. 概率程序中的推理

现状：大多数现有的概率编程语言实现了基于蒙特卡洛原理的采样推理算法，从而产生精确结果的数值近似。许多概率系统采用概率密度函数（PDF）表示分布，这些系统专注于编码（联合离散-）连续分布的程序的推理（带条件）。然而，处理底层PDF表示的推理查询需要解决复杂的积分表达式，这限制了这些技术要么使用（半）数值方法，要么使用有限循环行为的精确方法。DICE使用加权模型计数实现离散概率程序的精确推理，但也限于静态有限循环。MORA支持多种贝叶斯网络的精确推理，但依赖于一种称为概率可解循环的受限中间表示形式。

PGF方法：Klinkenberg等人提供了一种允许对概率程序进行精确定量推理的程序语义，且不涉及条件化。他们采用Kozen的表示方法，将概率程序视为分布转换器，即将输入分布（先验）映射到程序执行后的分布（后验）。在中，离散分布的域用概率生成函数（PGFs）表示，这是生成函数的一种特殊形式。这种表示方式具有以下优势：（a）自然地以紧凑的封闭形式表示常见的无限支持分布（及其变体），如几何分布或泊松分布；（b）支持组合推理，尤其是与基于密度或质量函数的表示相比，可有效计算（高阶）矩；（c）可以从PGF相对容易地提取尾部界限、集中界限等感兴趣属性；（d）自然支持包含概率和为程序变量分配新值的参数的表达式。基于PGF的一些成功实现想法，例如用于决定概率等价性和证明非几乎必然终止，已在中提出，这些研究尤其解决了无条件化精确概率推理的上述挑战（1）和（2）。


 2. 利用PGFs驯服条件化

生成生成模型是一项具有挑战性的任务，因为这些模型通常需要专家领域知识。因此，将条件化作为一门语言的首要元素的概念至关重要，因为它允许以自然和直观的方式创建模型。我们当前的研究旨在将PGF方法扩展到具有条件化的概率程序的精确推理，从而解决挑战（1）、（2）和（3），并尽可能推动自动化的极限。为此，我们正在开发一个基于开源的基于PGF的工具PRODIGY的精确符号推理引擎。我们在下面通过两个例子说明其当前支持条件化的能力。

3 未来方向

一个自然的问题是，我们是否可以在循环内部发生条件化时处理精确推理。正如在[17]中所论述的，需要更先进的推理技术来回答这个问题。事实上，据我们所知，目前还没有任何（半）自动化的精确推理技术允许在（可能是无界的）循环内部存在观测语句（一个例外可能是潜在可自动化的条件最弱前置期望演算[17]）。这正是我们当前研究的重点。一个有前景的想法是开发一种对编程语言的非平凡的语法限制，使得更先进的SOP技术[5]可以被推广以解决循环内的条件化问题。

在PGF表示中纳入符号参数的可能性可以使得将那些广为人知的优化方法（例如，最大似然估计和参数拟合）应用于概率程序的推理成为可能。其他有趣的未来研究方向包括：判断带有条件化的概率程序的等价性、通过使用特征函数将我们的方法扩展到连续分布，以及探索PGF在可微编程中的潜力。

原文链接：https://arxiv.org/abs/2302.00513