Inferring Covariances for Probabilistic Programs

TL;DR

This paper investigates the complexity of inferring covariances in probabilistic programs, showing that approximating (co)variances is highly computationally difficult and proposing invariant-based techniques to approximate bounds.

Contribution

It establishes the computational hardness of (co)variance approximation and introduces invariant-based methods for bounding (co)variances and run-time variances in probabilistic programs.

Findings

Computing (co)variance bounds is $\, ext{Sigma}_2^0$-complete.

Invariant-based techniques enable enumeration of bounds.

The approach extends to run-time variance reasoning.

Abstract

We study weakest precondition reasoning about the (co)variance of outcomes and the variance of run-times of probabilistic programs with conditioning. For outcomes, we show that approximating (co)variances is computationally more difficult than approximating expected values. In particular, we prove that computing both lower and upper bounds for (co)variances is $\Sigma^{0}_{2}$-complete. As a consequence, neither lower nor upper bounds are computably enumerable. We therefore present invariant-based techniques that do enable enumeration of both upper and lower bounds, once appropriate invariants are found. Finally, we extend this approach to reasoning about run-time variances.