Moment-based Invariants for Probabilistic Loops with Non-polynomial Assignments
Andrey Kofnov, Marcel Moosbrugger, Miroslav Stankovič, Ezio Bartocci, Efstathia Bura
TL;DR
This work tackles the problem of obtaining moment-based invariants for probabilistic programs whose state updates are non-polynomial. It introduces a general polynomial chaos expansion (gPCE) framework to approximate non-polynomial updates as sums of orthogonal polynomials, enabling closed-form moment computations within Prob-solvable loops via $g(Z) \approx \hat g(Z) = \sum_{i=0}^d c_i \phi_i(Z)$. The approach provides convergence guarantees under suitable conditions and offers an explicit coefficient computation scheme using multivariate integrals, with complexity on the order of $O(s d^{2} k + s^{k} d^{k})$. The method is demonstrated on benchmarks including a turning vehicle model and Taylor-rule dynamics, showing accurate moment estimates and favorable computation times compared with polynomial-form baselines. Overall, the paper extends moment-based invariant computation to a broader class of stochastic dynamics, enhancing uncertainty quantification for probabilistic programs.
Abstract
We present a method to automatically approximate moment-based invariants of probabilistic programs with non-polynomial updates of continuous state variables to accommodate more complex dynamics. Our approach leverages polynomial chaos expansion to approximate non-linear functional updates as sums of orthogonal polynomials. We exploit this result to automatically estimate state-variable moments of all orders in Prob-solvable loops with non-polynomial updates. We showcase the accuracy of our estimation approach in several examples, such as the turning vehicle model and the Taylor rule in monetary policy.
