Piecewise Analysis of Probabilistic Programs via k-Induction
summary
Proposes a method that extracts region splits from k-induction operators and combines them with the Optional Stopping Theorem to synthesize piecewise polynomial bounds on loop-exit expectations. Algorithms reduce the linear case to bilinear programming and relax the polynomial case to semidefinite programming; numerical repair checks ensure soundness. Evaluation over POPL benchmarks yields exact results on several examples, solves about 80% of polynomial cases within seconds, and beats or succeeds where other tools fail on roughly 40% of cases.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:51Monolithic bound synthesis challenges
- 3:14K-induction for piecewise bounds
- 6:47Theoretical foundations of k-induction
- 9:22Algorithm design with random walk
- 13:45Loop unrolling and case analysis
- 16:17Constraint solving for linear/polynomial cases
- 18:24Experimental results and benchmarks
- 21:14Summary and future work
- 22:21Q&A: Numerical solver limits
- 23:28Q&A: Tool failure analysis
- 24:13Q&A: State space partitioning
- 24:55Q&A: Context sensitivity
related talks
20mStatic Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
24mExact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions
14mMulti-Language Probabilistic Programming
14mExact Probabilistic Inference Using Generating Functions
22mStochastic Lazy Knowledge Compilation for Inference in Discrete Probabilistic Programs
17mProgrammatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Progr...
21mGuaranteed inference for probabilistic programs: a parallelisable, small-step o...
15mScaling Optimization Over Uncertainty via Compilation