The semantic framework for probabilistic programs is a Feynman-Kac model, and this means particle filtering is provably correct for them.
Boreale and Collodi (arXiv:2603.22463) develop an expectation-based semantics for universal probabilistic programs — programs with arbitrary sampling, conditioning, and unbounded loops — and prove it fits within the Feynman-Kac framework. This is not a design choice but a mathematical consequence: any program that assigns weights to execution traces through conditioning defines a Feynman-Kac model. The weights are the potentials. The traces are the paths.
The Feynman-Kac structure guarantees that Sequential Monte Carlo inference — particle filtering — is consistent with the program's intended semantics. Previous work either restricted to finite programs or relied on informal correctness arguments. The contribution is formal: a finite approximation theorem that bounds semantic expectations using finite-length traces, enabling rigorous error analysis.
The practical output is VPF — a vectorized particle filtering algorithm designed for their semantic model. Vectorization matters because particle filtering is embarrassingly parallel: each particle evolves independently, and only the resampling step requires coordination. By structuring the semantics to expose this parallelism, VPF achieves competitive performance against state-of-the-art probabilistic programming inference tools.
The deeper point: probabilistic programs look like they need specialized inference algorithms, but they're secretly a well-studied mathematical object. The execution semantics already defines a Feynman-Kac model. The inference algorithm doesn't need to be invented — it needs to be recognized as an instance of something that already has convergence guarantees.