The probabilistic termination tool amber

Probabilistic programming obviates the need to manually provide inference methods for different stochastic models and enables rapid prototyping [1, 2]. Automated formal verification of probabilistic programs, however, is still in its infancy. With our current work, we provide a step towards closing this gap when it comes to automating the termination analysis of probabilistic programs, which is an active research topic [3‐12]. Probabilistic programs are almost-surely terminating (AST) if they terminate with probability 1 on all inputs. They are positively AST (PAST) if their expected runtime is finite [13].

Addressing the challenge of (P)AST analysis, in this paper we describe Amber, a fully automated software artifact to prove/disprove (P)AST. Amber supports the analysis of a class of polynomial probabilistic programs. Probabilistic programs supported in our programming model consist of single loops whose body is a sequence of random assignments with acyclic variable dependencies. Moreover, Amber’s programming model supports programs parametrized by symbolic constants and drawing from common probability distributions, such as Uniform or Normal (Sect. 3). To automate termination analysis, Amber automates relaxations of various existing martingale-based proof rules ensuring (non-)(P)AST [14] and combines symbolic computation with asymptotic bounding functions (Sects. 4–5). Amber certifies (non-)(P)AST without relying on user-provided templates/bounds over termination conditions. Our experiments demonstrate Amber outperforming the state-of-the-art in automated termination analysis of probabilistic programs (Sect. 7). Our tool Amber is available at https://​github.​com/​probing-lab/​amber.

Related work. While probabilistic termination is an actively studied research challenge, tool support for probabilistic termination is limited. We compare Amber with computer-aided verification approaches proving probabilistic termination. The tools MGen [4] and LexRSM [7] use linear programming techniques to certify PAST and AST, respectively. A modular approach verifying AST was recently proposed in [11]. Automated techniques for refuting (P)AST were proposed in [8] and techniques for synthesizing polynomial ranking supermartingales using semi-definite programming in [6]. The work [12] introduced a sound and relatively complete algorithm to prove lower bounds on termination probabilities. However, the works of [6, 8, 11, 12] lack full tool support. The recent tools Absynth [15], KoAT2 [16] and ecoimp [17] can establish upper bounds on expected costs, therefore also on expected runtimes, and thus certify PAST. While powerful on respective AST/PAST domains, we note that none of the aforementioned tools support both proving and disproving AST or PAST. Our tool Amber is the first to prove and/or disprove (P)AST in a unifying manner. Our recent work [18] introduced relaxations of existing proof rules for probabilistic (non-)termination together with automation techniques based on asymptotic bounding functions. We utilize these proof rule relaxations in Amber and extend the technique of asymptotic bounds to programs drawing from various probability distributions and including symbolic constants.

Contributions. This paper describes the tool Amber, a fully automatic open-source software artifact for certifying probabilistic (non-)termination.Extensions to [19]. This paper is an extended version of the Amber tool demonstration paper [19]. Extending [19], we provide the theoretical prerequisites in Sect. 2. Sections 4‐5 complement [19] with new material introducing the supported termination proof rules and illustrating Amber’s algorithmic approach towards termination analysis. Moreover, Sect. 5 describes extensions of the asymptotic bound algorithm [18] to programs drawing from common probability distributions and containing symbolic constants. Section 6 goes beyond the details of [19] in describing the different components of Amber and their interplay.

By \(\mathbb {N}\), \(\mathbb {Q}\) and \(\mathbb {R}\) we denote the set of natural, rational, and real numbers, respectively. We write \(\overline{\mathbb {Q}}\), the real algebraic closure of \(\mathbb {Q}\), to denote the field of real algebraic numbers. We write \(\overline{\mathbb {Q}}[x_1,\ldots ,x_k]\) for the polynomial ring of all polynomials \(P(x_1, \ldots , x_k)\) in k variables \(x_1,\ldots ,x_k\) with coefficients in \(\overline{\mathbb {Q}}\) (with \(k\in \mathbb {N}\) and \(k\ne 0\)). We assume the reader to be familiar with Markov chains and probability theory in general. For more details we refer to [20, 21].

Amber analyzes the probabilistic termination behavior of a class of probabilistic programs involving polynomial arithmetic and random drawings from common probability distributions, parameterized by symbolic constants. The grammar in Fig. 1 defines the input programs to Amber. Inputs to Amber consist of an initialization part and a while-loop, whose guard is a polynomial inequality over program variables. The initialization part is a sequence of assignments either assigning (symbolic) constants or values drawn from probability distributions. Within the loop body, program variables are updated with either (i) a value drawn from a distribution or (ii) one of multiple polynomials over program variables with some probability. Additional to the structure imposed by the grammar in Fig. 1, input programs are required to satisfy the following structural constraint: Each variable updated in the loop body only depends linearly and non-negatively on itself and in a polynomial way on variables preceding it in the loop body. On a high level, this structural constraint is what enables the use of algebraic recurrence relations in probabilistic termination analysis. More concretely, the restriction to linear self-dependencies is necessary to ensure that the resulting recurrence relations (cf. Sect. 5) are C-finite and guaranteed to have computable closed-forms. Even seemingly simple first-order quadratic recurrences are problematic: the recurrence \(f(n{+}1) = r \cdot f(n)^2 - r \cdot f(n)\) does not have known analytical closed-form solutions for most values of \(r \in \mathbb {R}\) [25]. Furthermore, coefficients in linear self-dependencies are required to be non-negative to prevent oscillating dynamics. For instance, the sequence defined by the recurrence \(f(n{+}1) = {-}1 \cdot f(n)\) oscillates between 1 and \({-}1\) for \(f(0)=1\). Amber computes asymptotic bounds for monomials in program variables using recurrences. A central requirement of the termination analysis technique implemented in Amber (cf. Sect. 5) is that the asymptotic bounds are eventually monotone and non-negative or non-positive. Restricting coefficients in linear self-dependencies to be non-negative ensures this necessary property. Moreover, the algorithm computing asymptotic bounds for a program variable x first recursively computes the asymptotic bounds for all (monomials in) program variables on which x depends. Hence, to ensure termination, the dependencies among variables must be acyclic. This is guaranteed by restricting variable dependencies to preceding variables.

Despite the syntactical restrictions, most existing benchmarks on automated probabilistic termination analysis [18] and dynamic Bayesian networks [26] can be encoded in our programming language. Figure 2 shows three example input programs to Amber. For each of these examples, Amber automatically infers the respective termination behavior, by relying on its workflow described in Sect. 6. Our programming model extends Prob-solvable loops [27] with polynomial inequalities as loop guards. For a loop with loop guard \(\mathcal {G}\) of the form \(P > Q\) we write G for the expression \(P{-}Q\). In the sequel, we refer to programs of our programming model simply by loops or programs.

We now describe the theoretical foundations of existing proof rules for establishing probabilistic (non-)termination, which are used and further refined in Amber (Sect. 5).

Loop space. Operationally, every program loop represents a Markov chain (MC) with state space \(\mathbb {R}^m\) if the loop has m program variables. This MC in turn induces a canonical probability space. In this way, every loop \(\mathcal {L}\) is associated with a (filtered) probability space \((\Omega ^\mathcal {L}, \Sigma ^\mathcal {L}, (Run_i^\mathcal {L}), \mathbb {P}^\mathcal {L})\). We omit the superscripts if \(\mathcal {L}\) is clear from context. The sample space \(\Omega \) is the set of all infinite program runs. More precisely, if \(\mathcal {L}\) has m program variables, then \(\Omega = (\mathbb {R}^m)^\omega \). \(\Sigma \) is the \(\sigma \)-algebra constructed from all finite program run prefixes. The purpose of the loop filtration \((Run_i)\) is to capture the information gain as the loop is executed. Every \(\sigma \)-algebra \(Run_i\) of the filtration is constructed from all finite program run prefixes of length \(i{+}1\). In this way, \(Run_i\) allows measuring events concerned with the first i loop iterations. Finally, \(\mathbb {P}\) is the probability measure defined according to the intended semantics of the program statements. For a formal definition of \(\mathbb {P}\) and more details regarding the semantics of probabilistic loops we refer to [18]. For an expression E over the program variables, \(E_i\) denotes the random variable mapping a program run to the value of E after the i-th iteration. With the loop space at hand, the notions of AST and PAST (originally considered in [28]) can be defined in terms of a random variable capturing the termination time.

The conditions in the proof rules from Sect. 4.1 contain three types of inequalities:In the sequel we detail how these three type of inequalities are handled in Amber for proving/disproving (P)AST.

Type 1. For Amber’s programming model, the expression \(\mathbb {E}(G_{i+1}{-}G_i \mid Run_i)\) is a polynomial in the program variables. For the program in Fig. 2a we have \(G = c {-} x^2 {-} y^2\). The expression \(\mathbb {E}(G_{i+1}{-}G_i \mid Run_i) = \mathbb {E}(G_{i+1} \mid Run_i){-}G_i\) can be computed by starting with G, substituting left-hand sides of assignments by right-hand sides in a bottom-up fashion, averaging over probabilistic statements and finally subtracting G. For Fig. 2a, this leads to the polynomial \(\mathbb {E}(G_{i+1}{-}G_i \mid Run_i) = {-}x_i^2 {-} 11x_i {-} \nicefrac {115}{6}\). Thus, the expected change of the loop guard from an arbitrary iteration i to iteration \(i{+}1\) is \({-}x_i^2 {-} 11x_i {-} \nicefrac {115}{6}\), where \(x_i\) is the value of program variable x after iteration i. For an input program and a polynomial poly, \(\mathbb {E}(poly_{i+1} \mid Run_i)\) itself is always a polynomial. That is because all expressions in probabilistic branching statements are polynomials, all branching probabilities are constants and all distributions input programs can draw from have constant parameters and thus also constant moments. Crucially, all inequalities in the termination proof rules only need to hold eventually. Therefore, knowing the asymptotic behavior of the polynomial \(\mathbb {E}(G_{i+1}{-}G_i \mid Run_i)\) can be helpful in answering the respective inequalities: for instance, an asymptotic upper bound to \(\mathbb {E}(G_{i+1}{-} G_i \mid Run_i)\) that tends to a negative number witnesses that eventually \(\mathbb {E}(G_{i+1}{-}G_i \mid Run_i) \le - \epsilon \) for some \(\epsilon > 0\).

Type 2. After fixing the values drawn from distributions in the loop body at iteration i, every expression, and in particular G, can only progress to finitely many expressions in iteration \(i{+}1\). We refer to these possible follow-up expressions, as branches. For the program in Fig. 2b, the expression G (\(=x\)) is either \(x{+}c\) or \(x{-}c\) after one iteration. If for at least one of these branches B of G, we have that eventually \(B_i{-}G_i \le -d\) for some \(d > 0\) for any choice of values drawn from distributions, then it holds that \(\mathbb {P}(G_{i + 1}{-}G_i \le -d \mid Run_i) \ge p\) for some \(p > 0\). This holds, due to the fact that all probabilities in probabilistic branching statements are constant and non-zero. Similar to the inequalities of type 1, asymptotic bounds provide a method to answer inequalities of type 2: if for some branch B of G and any choice of values drawn from probability distributions, the polynomial \(B_i {-}G_i\) obeys an asymptotic upper bound tending to a negative number, then it holds that eventually \(\mathbb {P}(G_{i + 1}{-}G_i \le -d \mid Run_i) \ge p\) for some \(d > 0\) and \(p \in (0,1]\).

Type 3. In contrast to the inequalities of type 2 that have to hold with at least some non-zero probability, inequalities of type 3 have to hold almost-surely, that means with probability one. Nevertheless, type 3 inequalities can be approached similarly as type 2 inequalities: if for every (in contrast to some as for type 2 inequalities) branch B of G and any choice of values drawn from probability distributions, eventually \(|G_i {-} B_i |< c\) for some \(c > 0\), then eventually and almost-surely \(|G_{i} {-} G_{i+1} |< c\). In contrast to type 1 and 2 inequalities, tackling type 3 inequalities with asymptotic bounds requires one extra step. Due to the presence of the absolute value function, asymptotic upper bounds for the polynomials \(G_i {-} B_i\) do not suffice. Additional to upper bounds, asymptotic lower bounds are needed. Given an asymptotic upper bound u(i) and an asymptotic lower bound l(i) for the polynomial \(G_i {-} B_i\), \(\max (-l(i), u(i))\) is an asymptotic upper bound for \(|G_i {-} B_i |\).

Implementation. Amber is implemented in python3 and relies on the lark-parser¹ package to parse its input programs. Further, Amber uses the diofant² package as its computer-algebra system to (i) construct and manipulate mathematical expressions symbolically; (ii) solve algebraic recurrence relations, and (iii) compute function limits. To compute closed-form expressions for statistical moments of monomials over program variables only depending on the loop counter, Amber uses the tool Mora [27]. However, for efficient integration within Amber, we reimplemented and adapted the Mora functionalities exploited by Amber (Mora v2), in particular by deploying dynamic programming to avoid redundant computations. Altogether, Amber consists of \(\sim 2000\) lines of code. In what follows we discuss the main components of Amber, as illustrated in Fig. 3.

Experimental setup. Amber and our benchmarks are publicly available at https://​github.​com/​probing-lab/​amber. The output of Amber includes the martingale expression and an answer (“Yes”, “No” or “Maybe”) to PAST and AST for the input program. If the answer to (P)AST is definite (“Yes” or “No”), the output additionally contains a witness of the answer. We took all 39 benchmarks from [18] and extended them by 11 new programs to test Amber’s capability to handle symbolic constants and drawing from probability distributions. The 11 new benchmarks are constructed from the 39 original programs, by adding noise drawn from common probability distributions and replacing concrete constants with symbolic ones. As such, we conduct experiments using a total of 50 challenging benchmarks. Further, we compare Amber not only against Absynth and MGen, but also evaluate Amber in comparison to the recent tools LexRSM [7], KoAT2 [16] and ecoimp [17]. Note that MGen can only certify PAST and LexRSM only AST. Moreover, the tools Absynth, KoAT2 and ecoimp mainly aim to find upper bounds on expected costs. Tables 1, 2 and 3 summarize our experimental results, with benchmarks separated into PAST (Table 1), AST (Table 2), and not AST (Table 3). Benchmarks marked with * are part of our 11 new examples. In every table, ( ) marks a tool (not) being able to certify the respective termination property. Moreover, symbolizes that a benchmark is out-of-scope for a tool, for instance, due to not supporting some distributions or polynomial arithmetic. All benchmarks have been run on a machine with a 2.6 GHz Intel i7 (Gen 10) processor and 32 GB of RAM and finished within a timeout of 50 s, where most experiments terminated within a few seconds.

Experimental analysis. Amber successfully certifies 23 out of the 27 PAST benchmarks (Table 1). Although Absynth, KoAT2 and ecosimp can find expected cost upper bounds for large programs [15‐17], they struggle on small programs whose termination is not known a priori. For instance, they struggle when a benchmark probabilistically “chooses” between two polynomials working against each other (one moving the program state away from a termination criterion and one towards it). Our experiments show that Amber handles such cases successfully. MGen supports the continuous uniform distribution and KoAT2 the geometric distribution whose support is infinite. With these two exceptions, Amber is the only tool supporting continuous distributions and distributions with infinite support. To the best of our knowledge, Amber is the first tool certifying PAST supporting both discrete and continuous distributions as well as distributions with finite and infinite support. Amber successfully certifies 12 benchmarks to be AST which are potentially not PAST (Table 2). Whereas the LexRSM tool can certify non-PAST programs to be AST, such programs need to contain subprograms that are PAST [7]. The well-known example of symmetric_1D_random_walk, contained in our benchmarks, does not have a PAST subprogram. Therefore, the LexRSM tool cannot establish AST for it. In contrast, Amber using the SM-Rule can handle such programs. To the best of our knowledge, Amber is the first tool capable of certifying non-AST for polynomial probabilistic programs involving drawing from distributions and symbolic constants. Amber is also the first tool automating (non-)AST and (non-)PAST analysis in a unifying manner for such programs.

Experimental summary. Tables 1, 2 and 3 demonstrate that (i) Amber outperforms the state-of-the-art in certifying (P)AST, and (ii) amber determines (non-)(P)AST for programs with various distributions and symbolic constants.

We described Amber, an open-source tool analyzing the termination behavior for polynomial probabilistic programs, in a fully automatic way. Amber computes asymptotic bounding functions and martingale expressions and is the first tool to prove and/or disprove (P)AST in a unifying manner. Amber can analyze continuous, discrete, finitely- and infinitely supported distributions in polynomial probabilistic programs parameterized by symbolic constants. Our experimental comparisons give practical evidence that Amber can (dis)prove (P)AST for a substantially larger class of programs than state-of-the-art tools.