Parallelizable Feynman-Kac Models for Universal Probabilistic Programming

TL;DR

This paper develops a formal semantics for universal probabilistic programs, ensuring correct SMC inference, and introduces a vectorized particle filtering algorithm that outperforms existing tools in experiments.

Contribution

It provides a formal, expectation-based semantics for PPs with unbounded loops and arbitrary measures, and introduces a novel, efficient vectorized particle filtering method.

Findings

VPF outperforms state-of-the-art PP inference tools in experiments.

Semantics ensures the correctness and consistency of SMC inference for universal PPs.

Finite approximation bounds enable practical implementation of the semantics.

Abstract

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.