论文标题
概率计划中成本累积因子的中央时刻分析
Central Moment Analysis for Cost Accumulators in Probabilistic Programs
论文作者
论文摘要
对于概率程序,通常不可能自动获取有关其属性的精确信息,例如在给定程序点处的状态分布。取而代之的是,可以尝试得出近似值,例如尾部概率上的上限。可以通过浓度不平等获得这种界限,这些不平等取决于分布的力矩,例如期望(第一个原始力矩)或方差(第二个中央力矩)。使用中央力矩获得的尾界通常比使用原始力矩获得的尾部范围更紧密,但是自动分析中央矩的范围更具挑战性。 本文介绍了对概率程序的分析,该程序会自动在成本蓄能器的方差以及较高的中央力矩上自动得出符号上限和下限。为了克服高音阶分析的挑战,它以代数抽象的方式概括了对期望的分析,同时利用它们之间的关系,同时分析了不同的时刻。一个关键的创新是力矩 - 晶状体递归的概念,也是处理递归功能的实用推导系统。 该分析是使用基于模板的技术来实施的,该技术将多项式界限的推理对线性编程进行了推理。使用我们的原型中央音量分析仪的实验表明,尽管分析仪的上/下限在各种数量上,但比仅使用原始矩(例如期望)的现有系统获得了更紧密的尾巴界限。
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.