MORA - Automatic Generation of Moment-Based
Invariants
Ezio Bartocci
1 , Laura Kov´ acs
1,2 , and Miroslav Stankoviˇ c
1
1 TU Wien, Vienna, Austria
2 Chalmers, Gothenburg, Sweden
Abstract. We introduce MORA, an automated tool for generating invariants of
probabilistic programs. Inputs to MORA are so-called Prob-solvable loops, that
is probabilistic programs with polynomial assignments over random variables
and parametrized distributions. Combining methods from symbolic computation
and statistics, MORA computes invariant properties over higher-order moments
of loop variables, expressing, for example, statistical properties, such as expected
values and variances, over the value distribution of loop variables.
1 Introduction
Probabilistic programs (PPs) are becoming more and more commonplace. Originally
employed in randomized algorithms and cryptographic/privacy protocols, now gaining
momentum due to the several emerging applications in the areas of machine learning
and AI [5]. By introducing randomness into the program, program variables can no
longer be treated as having single values; we must think about them as distributions.
Dealing with distributions is much more challenging and some simplifications are required. Existing approaches, see e.g. [1, 3, 7, 9, 10], usually take into consideration only
expected values or upper and lower bounds over program variables, or rely on user
guidance for providing templates and hints.
One of the main challenges in analyzing PPs and computing their higher-order moments comes with the presence of loops and the burden of computing so-called quantitative invariants [7]. Quantitative invariants are properties that are true before and after
each loop iteration and are crucial for analyzing the behavior of PP loops.
In this paper, we introduce the MORA tool for computing quantitative invariants of
a class of PPs, called Prob-solvable loops [2], with random assignments, parametrized
distributions, and polynomial probabilistic updates. Our implementation is available at:
https://github.com/miroslav21/mora,
and successfully evaluated on a number of challenging examples. Unlike other existing approaches, e.g. [1, 3, 7, 9], MORA computes non-linear invariants in a fully automatic way, without relying on user-provided templates/hints. The proposed automatic
approach can handle an arbitrary number of loop iterations and also infinite loops. On
the contrary, tools like PSI [4] support only the automatic analysis of probabilistic programs with a specified number of loop iterations.
This research was supported by the ERC Starting Grant 2014 SYMCAR 639270, the Wallenberg Academy Fellowship 2014 TheProSE, and the Austrian FWF project W1255-N23.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 492–498, 2020.
https://doi.org/10.1007/978-3-030-45190-5 28
TACAS
Evaluation
Artifact
2020
Accepted
Invariants
Ezio Bartocci
1 , Laura Kov´ acs
1,2 , and Miroslav Stankoviˇ c
1
1 TU Wien, Vienna, Austria
2 Chalmers, Gothenburg, Sweden
Abstract. We introduce MORA, an automated tool for generating invariants of
probabilistic programs. Inputs to MORA are so-called Prob-solvable loops, that
is probabilistic programs with polynomial assignments over random variables
and parametrized distributions. Combining methods from symbolic computation
and statistics, MORA computes invariant properties over higher-order moments
of loop variables, expressing, for example, statistical properties, such as expected
values and variances, over the value distribution of loop variables.
1 Introduction
Probabilistic programs (PPs) are becoming more and more commonplace. Originally
employed in randomized algorithms and cryptographic/privacy protocols, now gaining
momentum due to the several emerging applications in the areas of machine learning
and AI [5]. By introducing randomness into the program, program variables can no
longer be treated as having single values; we must think about them as distributions.
Dealing with distributions is much more challenging and some simplifications are required. Existing approaches, see e.g. [1, 3, 7, 9, 10], usually take into consideration only
expected values or upper and lower bounds over program variables, or rely on user
guidance for providing templates and hints.
One of the main challenges in analyzing PPs and computing their higher-order moments comes with the presence of loops and the burden of computing so-called quantitative invariants [7]. Quantitative invariants are properties that are true before and after
each loop iteration and are crucial for analyzing the behavior of PP loops.
In this paper, we introduce the MORA tool for computing quantitative invariants of
a class of PPs, called Prob-solvable loops [2], with random assignments, parametrized
distributions, and polynomial probabilistic updates. Our implementation is available at:
https://github.com/miroslav21/mora,
and successfully evaluated on a number of challenging examples. Unlike other existing approaches, e.g. [1, 3, 7, 9], MORA computes non-linear invariants in a fully automatic way, without relying on user-provided templates/hints. The proposed automatic
approach can handle an arbitrary number of loop iterations and also infinite loops. On
the contrary, tools like PSI [4] support only the automatic analysis of probabilistic programs with a specified number of loop iterations.
This research was supported by the ERC Starting Grant 2014 SYMCAR 639270, the Wallenberg Academy Fellowship 2014 TheProSE, and the Austrian FWF project W1255-N23.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 492–498, 2020.
https://doi.org/10.1007/978-3-030-45190-5 28
TACAS
Evaluation
Artifact
2020
Accepted