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

TL;DR

This paper introduces a method to automatically approximate moment-based invariants in probabilistic programs with complex non-polynomial updates, using polynomial chaos expansion to handle non-linear dynamics.

Contribution

It presents a novel approach leveraging polynomial chaos expansion to estimate moments in probabilistic loops with non-polynomial updates, enhancing analysis of complex systems.

Findings

Accurately estimates moments in probabilistic loops with non-polynomial updates.

Demonstrates effectiveness on models like turning vehicle and monetary policy.

Provides a new tool for analyzing complex 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.