概率编程语言中序贯蒙特卡罗推断的正确性
Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages
AI总结：
该研究针对概率编程语言中序贯蒙特卡罗（SMC）推断缺乏操作语义下正确性证明的问题，扩展PPL lambda演算加入显式重采样项，证明重采样位置不影响通用SMC推断的正确性，并形式化自举粒子滤波器，为SMC算法在PPL中的应用提供理论支撑。
摘要：
概率编程是一种通过将推断问题编码为程序来进行不确定性推理的方法。为了解决这些推断问题，概率编程语言（PPLs）采用了不同的推断算法，例如序贯蒙特卡罗（SMC）、马尔可夫链蒙特卡罗（MCMC）或变分方法。现有关于这类算法的研究主要关注其实现与效率，而非算法本身应用于表达能力强的PPL时的正确性。为弥补这一不足，我们在一种具有强表达能力的PPL演算（可代表WebPPL、Anglican和Birch等主流PPL）的框架下，给出了SMC方法的正确性证明。此前的研究已利用操作语义研究了MCMC的正确性，也在无项递归的指称设定下研究了SMC和MCMC的正确性，但对于SMC推断——这是目前PPL中最常用的算法之一——尚未有操作语义框架下的形式化正确性证明。尤其一个悬而未决的问题是：概率程序中的重采样位置是否会影响SMC的正确性。我们解决了这一根本问题，并做出四项新贡献：（i）我们扩展了一种无类型PPL lambda演算及其操作语义，加入显式重采样项，用于表示SMC推断中的同步点；（ii）我们首次证明，在温和的限制条件下，对于通用形式的SMC推断，显式重采样项的任意放置都是有效的；（iii）作为（ii）的结果，我们的演算可受益于SMC领域的经典结论：大数定律以及模型证据的无偏估计；（iv）我们为该演算形式化了自举粒子滤波器，并讨论了如何将我们的结果进一步扩展到其他SMC算法。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
