Central Moment Analysis for Cost Accumulators in Probabilistic Programs

TL;DR

This paper introduces a novel analysis method for probabilistic programs that automatically derives bounds on central moments, including variance, leading to tighter tail probability bounds than traditional raw moment-based methods.

Contribution

It presents a new algebraic analysis framework for central moments in probabilistic programs, including moment-polymorphic recursion and a practical LP-based implementation.

Findings

The analyzer provides tighter tail bounds than raw moment-based systems.

It successfully derives bounds on variances and higher moments.

Experimental results demonstrate improved accuracy in probabilistic property estimation.

Abstract

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 tail probabilities. Such bounds can be obtained via concentration inequalities, which rely on the moments of a distribution, such as the expectation (the first raw moment) or the variance (the second 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 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 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.