概率编程语言中的顺序蒙特卡洛推断的正确性
摘要：概率编程是一种将推理问题编码为程序的方法，用于在不确定性下进行推理。为了解决这些推理问题，概率编程语言（PPLs）采用不同的推理算法，例如串行蒙特卡洛（SMC）、马尔可夫链蒙特卡洛（MCMC）或变分方法。现有的关于这些算法的研究主要关注它们的实现和效率，而不是在表达性强的PPLs上应用时算法本身的正确性。为了解决这个问题，我们给出了一个在表达性强的PPL演算中SMC方法的正确性证明，该演算代表了诸如WebPPL、Anglican和Birch等流行的PPLs。之前的工作通过操作语义研究了MCMC的正确性，并通过含义设置而不涉及术语递归的情况下研究了SMC和MCMC的正确性。然而，对于目前最常用的 PPLs算法之一，即SMC推理，尚无操作性环境下的形式正确性证明。特别是，一个悬而未决的问题是，概率性程序中的重采样位置是否会影响SMC的正确性。我们解决了这个基本问题，并提出了四个新的贡献：（i）我们扩展了一个无类型的PPL lambda演算和操作语义，以包括显式的重采样术语，从而表达SMC推理中的同步点；（ii）我们首次证明，在适当的限制条件下，任何显式重采样术语的放置都对于通用形式的SMC推理是有效的；（iii）由于（ii）的结果，我们的演算可以从SMC文献中受益：大数定律和模型证据的无偏估计；以及（iv）我们对演算进行了自助粒子滤波器的形式化，并讨论了如何进一步将我们的结果推广到其他SMC算法。
作者：Daniel Lund''en, Johannes Borgstr"om, David Broman
论文ID：2003.05191
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-05-04