Moment-based loop analysis

Abstract

In this thesis, we explore automated analysis of loops of probabilistic programs (PPs). We look specifically at finding a quantitative loop invariant: a property of a given loop that describes its behaviour. Loop invariants are key for reasoning about program loops. In the context of probabilistic programs, variables represent distributions, and the invariant needs to capture the statistical properties of these distributions. In our work, we focus on computing so-called moment-based invariants (MBIs), invariant properties that describe the expected value and higher (and mixed) moments of program variables. While it is not feasible to compute all moments, which would fully characterize the underlying distribution, our methods are able to compute moments of arbitrary order, hence allowing us to capture the loop properties relatively precisely. As one of the main results in this thesis, we give a characterization of Prob-solvable loops, a class of PP loops, for which MBIs can be, in principle, always computed. We also describe a fully automated method of computing MBIs of arbitrary order for any program of this class. The method is implemented and evaluated on several challenging benchmarks from the literature. In the second part of the thesis, we study how moment-based analysis of Prob-solvable loops and MBIs can be applied to reasoning about various challenges in Bayesian networks (BNs). We extend the framework introduced earlier to accommodate encoding BNs as PPs and also provide a way to encode several tasks in BN analysis as computing MBIs in a corresponding PP - such as exact inference, expected number of samples, or sensitivity analysis. In the last part of the thesis, we briefly discuss extensions of this work. We fully characterize the class of programs for which MBIs can be computed (moment-computable programs) and investigate how to automatically estimate probability distributions from MBIs. We also consider programs that are not moment-computable, for which we look at combinations of variables and approximations.