Probabilistic programming is an approach to reasoning under uncertainty by encoding inference problems as programs. In order to solve these inference problems, probabilistic programming languages (PPLs) employ different inference algorithms, such as sequential Monte Carlo (SMC), Markov chain Monte Carlo (MCMC), or variational methods. Existing research on such algorithms mainly concerns their implementation and efficiency, rather than the correctness of the algorithms themselves when applied in the context of expressive PPLs. To remedy this, we give a correctness proof for SMC methods in the context of an expressive PPL calculus, representative of popular PPLs such as WebPPL, Anglican, and Birch. Previous work have studied correctness of MCMC using an operational semantics, and correctness of SMC and MCMC in a denotational setting without term recursion. However, for SMC inference -- one of the most commonly used algorithms in PPLs as of today -- no formal correctness proof exists in an operational setting. In particular, an open question is if the resample locations in a probabilistic program affects the correctness of SMC. We solve this fundamental problem, and make four novel contributions: (i) we extend an untyped PPL lambda calculus and operational semantics to include explicit resample terms, expressing synchronization points in SMC inference; (ii) we prove, for the first time, that subject to mild restrictions, any placement of the explicit resample terms is valid for a generic form of SMC inference; (iii) as a result of (ii), our calculus benefits from classic results from the SMC literature: a law of large numbers and an unbiased estimate of the model evidence; and (iv) we formalize the bootstrap particle filter for the calculus and discuss how our results can be further extended to other SMC algorithms.

翻译：概率编程是一种通过对推断问题编码为程序来在不确定性下进行推理的方法。为了解决这些推断问题，概率编程语言（PPLs）采用不同的推断算法，例如序列蒙特卡洛（SMC）、马尔可夫链蒙特卡洛（MCMC）或变分方法。现有关于此类算法的研究主要关注其实现和效率，而非这些算法在应用于表达能力丰富的PPLs时的正确性。为解决这一问题，我们在一个代表性PPL演算（如WebPPL、Anglican及Birch等流行PPLs）的背景下，给出了SMC方法的正确性证明。先前研究已通过操作语义证明了MCMC的正确性，以及在无项递归的指称语义设置中证明了SMC和MCMC的正确性。然而，对于SMC推断——当前PPLs中最常用的算法之一——在操作语义设置中尚无形式化的正确性证明。特别是，概率程序中的重采样位置是否影响SMC的正确性仍是一个悬而未决的问题。我们解决了这一基本问题，并做出了四项创新贡献：（i）扩展了一个无类型的PPL lambda演算及操作语义，纳入显式重采样项，以表达SMC推断中的同步点；（ii）首次证明，在温和限制条件下，显式重采样项的任何放置对于通用形式的SMC推断都是有效的；（iii）作为（ii）的结果，我们的演算受益于SMC文献中的经典结论：大数定律及模型证据的无偏估计；（iv）我们形式化了该演算的自举粒子滤波器，并讨论了如何将我们的结果进一步扩展到其他SMC算法。