Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating ...
summary
Technique finds guaranteed upper and lower bounds on the posterior of discrete probabilistic programs with unbounded loops by representing distributions as probability generating functions. Lower bounds come from Kleene iteration (finite unrolling); upper bounds come from searching for a shaped inductive invariant, reduced to solving polynomial-inequality constraints in the theory of the reals. Prototype extends GenFun, uses Z3 SMT solver, and automatically produces sound bounds on probability masses, moments and tails for 6 of 11 examples within seconds.
AI-written summary · about