Probabilistic Inference in Hybrid Domains

1 Introduction

Hybrid Domains are characterized by a mixture of continuous and discrete variables, as well as logical and algebraic constraints involving them. Reasoning in these domains is a daunting task and currently few approaches have been proposed. Developing methods that can efficiently handle Hybrid Domains is of primary importance, as they would allow to model a wide range of problems in a more expressive way, as well as performing learning and inference tasks more efficiently by leveraging the knowledge encoded in the constraints.

Currently, my research focuses on performing exact probabilistic inference in Hybrid Domains by leveraging Weighted Model Integration, a generalization of Weighted Model Counting to continuous distributions.

2 Background

Weighted Model Counting (WMC) [Chavira and Darwiche, 2008] is the problem of computing the weighted sum of the models of a propositional formula.

where typically the weight of each model µ is computed as the product of the weights associated to its literals ℓ:

Recently, it was shown that probabilistic inference in the case of discrete distributions can be posed as a WMC problem [Chavira and Darwiche, 2008; Choi et al., 2013; Suciu et al., 2011; Fierens et al., 2013].

Satisfiability Modulo Theories (SMT) [Barrett et al., 2009] generalizes propositional satisfiability to theories such as Linear Arithmetic over Real or Integers. A SMT formula is a

(typically quantifier-free) formula in which the atoms can either be Boolean or theory atoms. Encoding a problem in SMT allows to represent logical and algebraic constraints involving the variables, like:

Weighted Model Integration [Belle et al., 2015a] (WMI) is a recent generalization of WMC to the case of continuous variables, in which the problem is encoded as a SMT formula and the weighted sum of models is replaced with the sum of the definite integrals of the weight functions of each model, which act as unnormalized density functions.

The integral is computed over the subspace defined by the truth assignments on the numerical constraints, which in the case of Linear Arithmetic over Reals (LRA) is a convex polytope.

3 WeightedModel Integration, Revisited

We present a reformulation of WMI which fixes some theoretical limitations of the original formulation and we provide a novel algorithm which drastically improves the performance. A drawback of the original formulation is that the WMI of the same weight function may give different results on two different LRA-equivalent formulas. For instance, consider:

Then WMI(ϕ1,w) = 3 ̸= WMI(ϕ2,w) = 32 . A major source of inefficiency in the original method is that it requires to find (and integrate over) total truth assignments, although in many cases this is not necessary. As an intuitive example, consider two models having the same associated weight and differing only on the truth assignment of a single theory atom (e.g. such atom has constant weight 1 regardless of its truth value). In the original method, this would require to compute two integrals with the same integrand and sum up the results.

Instead of formulating the weight of a model as the product of the weights associated with its literals, we define the notion of conditional weight function. In this formulation, the weight function is described by:

• a support formula χ, which defines the subspace of the assignments in which the function is defined (strictly positive),
• a set Ψ of formulas called conditions

such that each (partial) assignment to the atoms of χ and Ψ intuitively represents a branch of a weight function defined by means of nested if-then-elses.

Our algorithm exploits state-of-the-art SMT-based Predicate Abstraction techniques [Graf and Sa¨ıdi, 1997] together with this refined formulation of weight function to find and integrate over the partial truth assignments which are relevant in the query computation. The advantage is twofold: first, finding the truth assignments is significantly faster compared to the original method. Second, the number of integrals to be computed is minimal wrt the query.

This approach was applied to the Strategic Road Network dataset 1 , which contains traffic data on the motorways managed by the English Highways Agency. From this dataset we extrapolated polynomial distributions of journey times between all junctions, with a 15 minutes granularity. In this setting, the task is to perform queries of the form:

To the best of our knowledge, the only other system that can perform exact probabilistic inference in this hybrid setting is PRAISE, which implements a method called Probabilistic Inference Modulo Theories [de Salvo Braz et al., 2016]. We compared the execution times of our implementation (WMIPA) with PRAISE for increasingly longer paths. In this setting, our method is significantly more efficient, as shown in Figure 1.

4 Future work

Future plans include exploiting decomposition and caching techniques to further improve scalability by partitioning the problem in independently-integrable components, as it was done for WMC [Sang et al., 2004; Bacchus et al., 2009]. This could be implemented by building the dependency graph of variables, in which two variables are connected by an edge if they appear in the same atom. Finding a partitioning would require to find the connected components on such graph. One of the main issues here is that in many scenarios, unlike in the purely propositional case, numerical variables tend to be coupled together by appearing in the same theory atoms. Nevertheless, implementing such techniques would allow to effectively broaden the set of problems that can be solved by our method. Another direction is to leverage the exact approach as a basis to perform approximate inference in Hybrid Domains, as it was done for the original WMI formulation [Belle et al., 2015b].

1 https://data.gov.uk/dataset/dft-eng-srn-routes-journey-times