Central Moment Analysis for Cost Accumulators in Probabilistic Programs
Thu 24 Jun 2021 21:35 - 21:40 at PLDI-A - Talks 3A: Analysis and Synthesis
For probabilistic programs, it is usually not possible to automatically derive exact information about their properties, such as the distribution of states at a given program point.
Instead, one can attempt to derive approximations, such as upper bounds on \emph{tail probabilities}.
Such bounds can be obtained via concentration inequalities, which rely on the \emph{moments} of a distribution, such as the expectation (the first \emph{raw} moment) or the variance (the second \emph{central} moment).
Tail bounds obtained using central moments are often tighter than the ones obtained using raw moments, but automatically analyzing central moments is more challenging.
This paper presents an analysis for probabilistic programs that automatically derives symbolic upper and lower bounds on variances, as well as higher central moments, of \emph{cost accumulators}.
To overcome the challenges of higher-moment analysis, it generalizes analyses for expectations with an algebraic abstraction that simultaneously analyzes different moments, utilizing relations between them.
A key innovation is the notion of \emph{moment-polymorphic recursion}, and a practical derivation system that handles recursive functions.
The analysis has been implemented using a template-based technique that reduces the inference of polynomial bounds to linear programming.
Experiments with our prototype central-moment analyzer show that, despite the analyzer's upper/lower bounds on various quantities, it obtains tighter tail bounds than an existing system that uses only raw moments, such as expectations.