Central moment analysis for cost accumulators in probabilistic programs
Central moment analysis for cost accumulators in probabilistic programs
复制标题
DOI：
10.1145/3453483.3454062
复制
发表时间：
2021-06
期刊：
影响因子：
--
通讯作者：
Di Wang;Jan Hoffmann;T. Reps
中科院分区：
文献类型：
--
作者：
Di Wang;Jan Hoffmann;T. Reps
对于有问题的程序，通常不可能自动获取有关其属性的精确信息，例如在给定的程序点上的分布，可以尝试得出近似值，例如尾部可能性可以通过浓度不等式获得，这些不平等取决于分布的矩，例如期望（第一个原始力矩）或方差（第二个中央力矩）。中央时刻通常比使用原始矩获得的时刻更紧密，但是本文自动分析中央时刻是对概率计划的分析，该分析会自动得出象征性的上和下界的方差，以及较高的中央时刻，成本的成本累加器。要克服高音阶分析的挑战，它通常以代数抽象的方式进行期望利用它们之间的关系的不同时刻。编程的实验。现有的系统仅使用原始时刻，例如期望。
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.