Table of Contents
Fetching ...

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.

Moment-based Invariants for Probabilistic Loops with Non-polynomial Assignments

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 . The approach provides convergence guarantees under suitable conditions and offers an explicit coefficient computation scheme using multivariate integrals, with complexity on the order of . 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.
Paper Structure (9 sections, 1 theorem, 10 equations, 2 figures)

This paper contains 9 sections, 1 theorem, 10 equations, 2 figures.

Key Result

proposition thmcounterproposition

If functions $f$ and $g$ satisfy conditions (B) and (D), and ${\mathbf Z}=(Z_{1},\ldots, Z_{k_1})$, ${\mathbf Y}=(Y_{1},\ldots, Y_{k_2})$ satisfy conditions (A), (C) and (E) and are mutually independent, then their sum, $f({\mathbf Z}) + g({\mathbf Y})$, and product, $f({\mathbf Z}) \cdot g({\mathbf

Figures (2)

  • Figure 1: On the top left a probabilistic loop modeling the behaviour of a turning vehicle Srirametal2020 using non-polynomial (cos, sin) updates in the loop body. On top right a Prob-Solvable loop obtained by approximating the cos, sin functions using polynomial chaos expansion (up to 5th degree). In the middle the expected position $(x,y)$ computed automatically from the Prob-Solvable loop as a closed-form expression in the number of the loop iterations $n$. In the bottom center and right the comparison among the true and the estimated distribution for a fixed iteration (we execute the loop for $n=20$ iterations and $8 \cdot 10^5$ repetitions).
  • Figure 2: Illustration of PCE algorithm

Theorems & Definitions (2)

  • definition thmcounterdefinition: Prob-solvable loops
  • proposition thmcounterproposition