一句话：提出全自动静态分析，为一大类概率循环精确推导程序变量高阶矩，无需外部不变式或模板。
本文面向具有潜在不可数状态空间的一大类概率循环，提出一种新的静态分析技术，用于自动推导程序变量的高阶矩。该工作不依赖外部提供的不变式或模板，而是采用基于线性递推的代数方法；同时引入程序变换，在保持统计性质的前提下简化概率程序，并发展幂约简技术以简化多项式算术。作者还定义了可精确计算高阶矩的“矩可计算概率循环”理论。该方法可用于恢复随机变量的概率分布并计算尾部概率。实证评估在多个挑战性示例上验证了其适用性。
We present a novel static analysis technique to derive higher moments for program variables for a large class of probabilistic loops with potentially uncountable state spaces. Our approach is fully automatic, meaning it does not rely on externally provided invariants or templates. We employ algebraic techniques based on linear recurrences and introduce program transformations to simplify probabilistic programs while preserving their statistical properties. We develop power reduction techniques to further simplify the polynomial arithmetic of probabilistic programs and define the theory of moment-computable probabilistic loops for which higher moments can precisely be computed. Our work has applications towards recovering probability distributions of random variables and computing tail probabilities. The empirical evaluation of our results demonstrates the applicability of our work on many challenging examples.
@article{paperbot1463,
title = {This is the moment for probabilistic loops},
author = {Marcel Moosbrugger and Miroslav Stankovič and Ezio Bartocci and Laura Kovács},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563341}
}