Verifying Variances for Probabilistic Programs (Negative Results)

This project concerns Hoare Logics and Weakest Pre-expectation Calculi for probabilistic programs. Verifying upper bounds to central moments has been a very hard problem for probabilistic programs. The naive approach is to decompose the central moment into a polynomial of raw moments, thereby reducing the problem to finding upper bounds and lower bounds of raw moments. However, in general, verifying lower bounds is known to be a difficult problem (e.g. see Hark et al. 2020).

In this project, we focus on the variance. We attempt to give a direct approach to the verification thereof, without using the polynomial expansion. We successfully give a sound weakest ‘pre-variance’ calculus, compositional by leveraging a simple insight. However, unfortunately, we discover that the calculus lacks some really important properties to allow for upper bounding, thus making it unusable.