Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions - LAFI'24

Explore a novel technique for finding guaranteed upper and lower bounds on the posterior distribution of probabilistic programs with loops in this 10-minute conference talk from ACM SIGPLAN's LAFI'24. Learn how probability generating functions are utilized to represent distributions, with lower bounds obtained through Kleene iteration. Discover the innovative approach to finding upper bounds by searching for an inductive invariant, which is reduced to solving a system of polynomial inequalities. Understand how this provably sound method yields bounds on probability masses, moments, and tail behavior of program distributions. Gain insights into the prototype implementation that automatically finds guaranteed bounds for various examples from literature, previously requiring human input to solve.