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.

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