We study provably correct and efficient instantiations of Sequential Monte Carlo (SMC) inference in the context of formal operational semantics of Probabilistic Programs (PPs). We focus on universal PPs featuring sampling from arbitrary measures and conditioning/reweighting in unbounded loops. We first equip Probabilistic Program Graphs (PPGs), an automata-theoretic description format of PPs, with an expectation-based semantics over infinite execution traces, which also incorporates trace weights. We then prove a finite approximation theorem that provides bounds to this semantics based on expectations taken over finite, fixed-length traces. This enables us to frame our semantics within a Feynman-Kac (FK) model, and ensures the consistency of the Particle Filtering (PF) algorithm, an instance of SMC, with respect to our semantics. Building on these results, we introduce VPF, a vectorized version of the PF algorithm tailored to PPGs and our semantics. Experiments conducted with a proof-of-concept implementation of VPF show very promising results compared to state-of-the-art PP inference tools.

翻译：我们在概率程序的形式化操作语义背景下，研究可证明正确且高效的序贯蒙特卡洛推理实例化方法。我们重点关注具有以下特征的通用概率程序：从任意测度中采样，以及在无界循环中进行条件化/重加权。我们首先为概率程序图（一种概率程序的自动机理论描述格式）配备了一种基于期望的、涵盖无限执行轨迹的语义，该语义同时包含了轨迹权重。随后，我们证明了一个有限逼近定理，该定理基于在有限、固定长度轨迹上计算的期望，为此语义提供了界限。这使得我们能够将我们的语义置于Feynman-Kac模型框架内，并确保了粒子滤波算法（序贯蒙特卡洛的一个实例）相对于我们语义的一致性。基于这些结果，我们引入了VPF，这是为概率程序图及我们的语义量身定制的一种向量化粒子滤波算法。通过VPF的概念验证实现进行的实验表明，与最先进的概率程序推理工具相比，其结果非常具有前景。