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

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.

Supported by the Vienna Science and Technology Fund (WWTF ICT19-018), the TU Wien Doctoral College (SecInt), the FWF research projects LogiCS W1255-N23 and P 30690-N35, and the ERC Consolidator Grant ARTIST 101002685.

Appendices

Appendix 1. Proof of Theorem 1

Proof

(Theorem 1). Since $f(z) = 0$ $\forall z\notin \left[ a, b\right]$,

$$\begin{aligned} \begin{array}{c} \left\| g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right\| _{f}^{2} = \int \limits _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}f(z)dz \quad \\ =\int \limits _{-\infty }^{\infty }\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}f(z)dz \\ = \int \limits _{-\infty }^{a}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}f(z)dz + \int \limits _{b}^{\infty }\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}f(z)dz \\ + \int \limits _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}f(z)dz \\ \le \int \limits _{-\infty }^{a}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}\phi (z)dz + \int \limits _{b}^{\infty }\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}\phi (z)dz \\ + \int \limits _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}\phi (z)dz + \int _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}(f(z)-\phi (z))dz \\ = A + B + C + D \end{array} \end{aligned}$$

(20)

Since $f(z) -\phi (z) \le \phi (z) + f(z)$, D satisfies

$$\begin{aligned}\begin{gathered} \int \limits _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}(f(z)-\phi (z))dz \\ \le \int \limits _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}dz\int \limits _{a}^{b}(\phi (z) + f(z))dz \\ = (1 + \varPhi (b) - \varPhi (a)) \times \int \limits _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}dz, \end{gathered}\end{aligned}$$

with $(1 + \varPhi (b) - \varPhi (a)) < 2.$ Now,

$$\begin{aligned} 1 \le \frac{\phi (z)}{\min {(\phi (a), \phi (b))}} \quad \forall z \in \left[ a, b\right] , \end{aligned}$$

and hence

$$\begin{aligned} \begin{array}{c} \int \limits _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}dz \\ \le \min {(\phi (a), \phi (b))}^{-1}\int \limits _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}\phi (x)dz \\ \le \min {(\phi (a), \phi (b))}^{-1} C. \end{array} \end{aligned}$$

(21)

By (21) and (15), (20) satisfies

$$\begin{aligned}\begin{gathered} A+B+C+D \le \left( \frac{2}{\min {(\phi (a), \phi (b))}} + 1 \right) \Bigg \{ \int \limits _{-\infty }^{a} \left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}\phi (z)dz \\ + \int \limits _{b}^{\infty }\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}\phi (z)dz + \int \limits _{a}^{b}\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}\phi (z)dz \Bigg \} \\ = \left( \frac{2}{\min {(\phi (a), \phi (b))}} + 1 \right) \int \limits _{-\infty }^{\infty }\left( g(z) - \sum \limits _{i=0}^{T}c_{i}p_{i}(z)\right) ^{2}\phi (z)dz \\ = \left( \frac{2}{\min {(\phi (a), \phi (b))}} + 1 \right) \sum \limits _{i=T+1}^{\infty }c_{i}^{2} \le \left( \frac{2}{\min {(\phi (a), \phi (b))}} + 1 \right) \mathbb {V}\textrm{ar}_{\phi }\left[ g(Z)\right] \end{gathered}\end{aligned}$$

since $\mathbb {V}\textrm{ar}_\phi (g(Z))=\sum _{i=1}^\infty c_i^2$. In consequence, the error (16) can be upper bounded by (18).

Appendix 2. Computation Algorithm in Detail

We let ${\textbf{D}}\in \mathbb {Z}^{L \times k}$ be the matrix with each row $j=1, \ldots , L$ containing the degrees of $Z_i$ (in column i) of the corresponding polynomial in (9). For example, the first row corresponds to the constant polynomial (1), and the last row to $\bar{p}_{1}^{\bar{d}_1}(z_1) \ldots \bar{p}_{k}^{\bar{d}_k}(z_k)$. That is,

The computer implementation of the algorithm computes $c_j$ in (10) for each j combination (row) of degrees of the corresponding polynomials.

We apply the above described computation to the following example. Suppose that X has a truncated normal distribution with parameters $\mu = 2$, $\sigma = 0.1$, and is supported over $\left[ 1, 3\right]$, and that Y is uniformly distributed over $\left[ 1, 2\right]$. We expand $g(x, y) = \log (x + y)$ along X and Y, as follows. We choose the relevant highest degrees of expansion to be $\bar{d}_{X} = 2$ and $\bar{d}_{Y} = 2$. The pdf of Y is $f_{Y}(y) \equiv 1$, and of X is $f_{X}(x) = e^{-\frac{(x-2)^{2}}{0.02}}/0.1\alpha \sqrt{2\pi }$, where the truncation multiplier $\alpha$ equals $\int \limits _{1}^{3}e^{-\frac{(x-2)^{2}}{0.02}}dx/0.1\sqrt{2\pi }$.

The two sets of polynomials, $\{p_{i}\} = \{1, x, x^{2}\}$ and $\{q_{i}\} = \{1, y, y^{2}\}$, are linearly independent. Applying the Gram-Schmidt procedure to orthogonalize and normalize them, we obtain $\bar{p}_{0}(x) = 1$, $\bar{p}_{1}(x) = 10x - 20$, $\bar{p}_{2}(x) = 70.71067x^{2} -282.84271x + 282.13561$, and $\bar{q}_{0}(y) = 1$, $\bar{q}_{1}(y) = 3.4641y - 5.19615$, $\bar{q}_{2}(y) = 13.41641y^{2} - 40.24922y + 29.06888$. In this case, $L = (1 + \bar{d}_{X}) * (1 + \bar{d}_{Y}) = 9$, and ${\textbf{D}}$ has 9 rows and 2 columns,

Iterating through the rows of matrix ${\textbf{D}}$ and choosing the relevant combination of degrees of polynomials for each variable, we calculate the Fourier coefficients

$$c_{j} = \int _{1}^{3}\int _{1}^{2}log(x + y)\bar{p}_{d_{j1}}(x)\bar{q}_{d_{j2}}(y)f_{X}(x)f_{Y}(y)dydx.$$

The final estimator can be derived by summing up the products of each coefficient and the relevant combination of polynomials:

$$\begin{aligned}\begin{gathered} \log (x + y) \approx \hat{g}(x, y) = \sum _{j=1}^{9}c_{j}\bar{p}_{d_{j1}}(x)\bar{q}_{d_{j2}}(y) \approx \\ -\,0.01038x^{2}y^{2} + 0.05517x^{2}y- 0.10031x^{2} \\ +\, 0.06538xy^{2} - 0.37513xy + 0.86515x \\ -\, 0.13042y^{2} + 0.93998y - 0.59927. \end{gathered}\end{aligned}$$

The estimation error is

$$\begin{aligned} se(\hat{g}) = \sqrt{\int \limits _{1}^{3}\int \limits _{1}^{2}\left( \log (x+y)) - \hat{g}(x, y)\right) ^{2}f_{X}(x)f_{Y}(y)dydx} \approx 0.000151895 \end{aligned}$$

Appendix 3. PCEs of Exponential and Trigonometric Functions

Table 2 lists examples of functions of up to three random arguments approximated by PCE’s of different degrees and, correspondingly, number of coefficients. We use $TruncNormal \left( \mu , \sigma ^{2}, \left[ a, b\right] \right)$ to denote the truncated normal distribution with expectation $\mu$ and standard deviation $\sigma$ on the (finite or infinite) interval $\left[ a, b\right]$, and $TruncGamma\left( \theta , k, \left[ a, b\right] \right)$ for the truncated gamma distribution on the (finite or infinite) interval $\left[ a, b\right]$, $a,b>0$, with shape parameter k and scale parameter $\theta$. The approximation error in (13) is reported in the last column. The results confirm (8) in practice: the error decreases as the degree or, equivalently, the number of components in the approximation of the polynomial increases.

Table 2. Approximations of 5 non-linear functions using PCE.