Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
summary
Derives guaranteed upper and lower bounds for normalized posteriors by reducing inference to polynomial solving over templates guided by a new fixed‑point theorem; introduces a multiplicative Optional Stopping Theorem to handle score weights >1 and score‑recursive Bayesian programs; adds a truncation operation plus synthesized multi‑input bounds to make polynomials effective on unbounded loops and continuous supports; evaluation across benchmarks shows faster analysis and comparable or tighter NPD bounds than Beutner et al. (PLDI 2022) and supports programs previous methods cannot solve; artifacts available.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:06Bayesian probabilistic programming
- 3:39Unbounded loops and continuous distributions
- 8:24Pedestrian random walk example
- 12:29Posterior distribution analysis
- 17:09Truncation operation
- 18:39Experimental results
- 19:21Q&A
related talks
24mExact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions
06mPitfalls of Full Bayesian Inference in Universal Probabilistic Programming
31mProbabilistic Programming: The What, Why and How
26mPiecewise Analysis of Probabilistic Programs via k-Induction
01h 03mA Personal Viewpoint on Probabilistic Programming
01h 03mAn Overview of Probabilistic Programming
14mMulti-Language Probabilistic Programming
14mExact Probabilistic Inference Using Generating Functions