Probabilistic Inference in Hybrid Domains by Weighted Model Integration

1 Introduction

Weighted model counting (WMC) is a basic reasoning task on propositional knowledge bases. It extends the model counting task, or #SAT, which is to count the number of satisfying assignments (that is, models) to a given logical sentence [Gomes et al., 2009]. InWMC, one accords a weight to every model, and computes the sum of the weights of all models. The weight of a model is often factorized into weights of assignments to individual variables.

The WMC formulation has recently emerged as an assembly language for probabilistic reasoning, o�ering a basic formalism for encoding various inference problems. State-ofthe-art reasoning algorithms for Bayesian networks [Chavira and Darwiche, 2008], their relational extensions [Chavira et al., 2006], factor graphs [Choi et al., 2013], probabilistic programs [Fierens et al., 2013], and probabilistic databases [Suciu et al., 2011] reduce their inference problem to a WMC computation. Exact WMC solvers are based on knowledge compilation [Darwiche, 2004; Muise et al., 2012] or exhaustive DPLL search [Sang et al., 2005]. Approximate WMC algorithms use local search [Wei and Selman, 2005] or sampling [Chakraborty et al., 2014]. More recently, the task has also been generalized to first-order knowledge bases [Van den Broeck et al., 2011; Gogate and Domingos, 2011].

The popularity of WMC can be explained as follows. Its formulation elegantly decouples the logical or symbolic representation from the statistical or numeric representation, which is encapsulated in the weight function. When building

Guy Van den Broeck

Dept. of Computer Science KU Leuven, Belgium

guy.vandenbroeck@cs.kuleuven.be

solvers, this allows us to reason about logical equivalence and reuse SAT solving technology (such as constraint propagation and clause learning). WMC also makes it more natural to reason about deterministic, hard constraints in a probabilistic context. Nevertheless, WMC has a fundamental limitation: it is purely Boolean. This means that the advantages mentioned above only apply to discrete probability distributions.

A similar observation can be made for the classical satisfiability (SAT) problem and related tasks, which for the longest time could only be applied in discrete domains. This changed with the increasing popularity of satisfiability modulo theories (SMT), which enable us to, for example, reason about the satisfiability of linear constraints over the rationals.

This paper generalizes the weighted model counting task to hybrid domains. The resulting weighted model integration task (WMI) is defined on the models of an SMT theory �, containing mixtures of Boolean and continuous variables. For every assignment to the Boolean and continuous variables, the WMI problem defines a density. The WMI for � is computed by integrating these densities over the domain of solutions to �, which is a mixed discretecontinuous space. Consider, for example, the special case when � has no Boolean variables, and the weight of every model is 1. Then, WMI simplifies to computing the volume of the polytope encoded in � [Ma et al., 2009]. When we additionally allow for Boolean variables in �, this special case becomes a hybrid version of #SAT [Luu et al., 2014; Chistikov et al., 2015]. 1

To illustrate WMI, we explore its application to inference and learning in hybrid Markov networks. Existing inference algorithms for hybrid graphical models are either approximate (e.g., Murphy [1999] or Lunn et al. [2000]), or they make strong assumptions on the form of the potentials, such as Gaussian distributions [Lauritzen and Jensen, 2001]. The need for novel approaches to hybrid graphical models is also noted by two approaches that use piecewise-polynomial potentials: Shenoy and West [2011] generalize the join-tree algorithm and Sanner and Abbasnejad [2012] generalize symbolic variable elimination. We also consider the piecewisepolynomial setting in this paper, but in a very general framework where constraints can be defined over arbitrary Boolean connectives. This setting is expressive enough to e�ectively approximate any continuous distribution, while still permitting exact and e�cient computations [De Loera et al., 2012]. In sum, the WMI formulation admits a general and powerful methodology for exact inference in hybrid domains, and is e�cient for piecewise-polynomial specifications.

1 In an independent e�ort, Chistikov et al. [2015] introduce a related definition for the unweighted model counting of SMT theories, which they refer to as #SMT. Moreover, their focus is on approximate counting and they do not consider parameter learning.

We structure the work as follows. We begin by considering some preliminaries, including the logical language and the standard notion of WMC. We then provide a definition for WMI, consider important classes of specifications and finally turn to parameter learning and empirical evaluations.

2 Preliminaries

We introduce the preliminaries for this work in three steps, beginning with probabilistic models, and then turning to the necessary logical background and WMC.

Probabilistic Models

Let B and X denote sets of Boolean and real-valued random variables, that is, b 2 B is assumed to take values from f0; 1g and x 2 X takes values from R : We let (b; x) = (b1; : : : ; bm; x1; : : : ; xn) be an element of the probability space f0; 1g m �R n , which denotes a particular assignment to the random variables from their respective domains. We let the joint probability density function be denoted by Pr. Then, Pr(b; x) determines the probability of the assignment vector.

When these random variables are defined by a set of dependencies, as can be represented using a graphical model, the density function can be compactly factorized [Koller and Friedman, 2009]. In this work, we are concerned with undirected graphical models (that is, Markov networks), where the joint density function can be expressed in terms of the cliques of the graph:

where bk and xk are those random variables participating in kth clique, and �k(�; �) is non-negative, real-valued potential function. It is not necessary that �k denote probabilities, and so Z is a normalization constant, also referred to as the partition function, defined as:

Logical Background

Propositional satisfiability (SAT) is the problem of deciding whether a logical formula over Boolean variables and logical connectives can be satisfied by some truth value assignment of the Boolean variables. Given a formula � and assignment (or model or world) M, we write M j= � to denote satisfaction. We write l 2 M to denote the literals (that is, propositions or their negations) that are satisfied at M:

A generalization to this decision problem is that of Satisfiability Modulo Theories (SMT). In SMT, we are interested in deciding the satisfiability of a (typically quantifier-free) firstorder formula with respect to some decidable background theory, such as linear arithmetic over the rationals LRA. Standard first-order models can be used to formulate SMT. For example, LRA is the fragment of first-order logic over the signature (0; 1; + ; �) restricting the interpretation of these symbols to standard arithmetic. See Barrett et al. [2009] for a comprehensive treatment.

In this paper, the logical language is assumed to be a combination of LRA and propositional logic, for which satisfaction is defined in an obvious way. We use p; q and r to range over propositional letters, and x; y; z and c to range over constants of the language [Barrett et al., 2009]. So, ground atoms are of the form q; :p and x + 1 � y. For convenience, we also use a ternary version of � written y � x � z to capture intervals. (This is easily seen to not a�ect the expressive power.)

For our purposes, we also need the notion of formula abstraction and refinement [Barrett et al., 2009]. Here, a bijection is established between ground atoms and a propositional vocabulary in that propositions are mapped to themselves and ground LRA atoms are mapped to fresh propositional symbols. Abstraction proceeds by replacing the atoms by propositions, and refinement replaces the propositions with the atoms. We refer to the abstraction of a SMT formula � as � � and the refinement of a propositional formula � as � + : Abstraction and refinement are extended to complex formulas in a manner that is homomorphic with respect to the logical operators: [�_ ] � = � � _ � ; [:�] � = :[�] � and [true] � = true, and likewise for refinement. For example, [p _ (x � 10)] � is p _ q; and [p _ q] + is p _ (x � 10).

Weighted Model Counting

Weighted model counting (WMC) [Chavira and Darwiche, 2008] is a generalization of model counting [Gomes et al., 2009]. In model counting, also known as #SAT, one counts the number of satisfying assignments of a propositional sentence. In WMC, each assignment has an associated weight and the task is to compute the sum of the weights of all satisfying assignments. WMC has applications in probabilistic inference in discrete graphical models.

Definition 1: Given a formula � in propositional logic over literals L, and a weight function w : L ! R �0 , the weighted model count (WMC) is defined as:

where

Intuitively, the weight of a formula is given in terms of the total weight of its models; the weight of a model is defined in terms of the literals that are true in that model.

Example 2: Consider the following Markov network in feature representation [Della Pietra et al., 1997; Richardson and Domingos, 2006] over Boolean variables fp; q; rg:

0:1 p

1:2 p _ r

2:5 q ) r

In English: the first feature is a hard constraint that p and q are mutually exclusive, whereas the third feature increases the weight of a world by a factor 1:2 if p or r is true. The weight of a world is 0 if it does not satisfy the hard constraints, and is otherwise equal to the product of the weights of the satisfied features. The sum of the weights of all worlds is the partition function Z. Note that Z equals the WMC of �:

with weights: w(p) = 0:1, w(f1) = 1:2, w(f2) = 2:5 and for all other symbols, the weight is 1. �

We are often interested in computing the probability of a query q given evidence e in a Boolean Markov network N, for which we use:

where � encodes N and w encodes the potential. The following correctness result is straightforward to establish:

Theorem 3: Let N be a Markov network over Boolean random variables B and potentials f�1; : : : ; �kg : Let � and w be the corresponding encodings over Boolean variables B: Then for any q; e 2 B, the probability PrN(q j e) is given by (1).

Proof (Sketch): An assignment to the random variables in N can be exactly mapped to a corresponding model of � : In that regard, the probability of the assignment equals the weight of the model, and so the partition function equals the sum of weights of all models of � ; and the case of the conditional probability is a simple corollary.

Finally, we remark that generalizing Boolean random variables to arbitrary discrete ones, that is, where these variables take values from finite sets is also easily achieved [Sang et al., 2005; Chavira and Darwiche, 2008], and so we restrict all discussions to the Boolean setting without loss of generality.

3 WeightedModel Integration

We are interested in exact inference with a mix of discrete and continuous random variables (under certain limitations). However, an inherent limitation of WMC is that it only admits the inference of discrete probability distributions. That is, because it is based on annotating a propositional theory, it encodes a finite sample space, as appropriate for Boolean or discrete Markov networks.

A Definition

In this section, we introduce weighted model integration that is a strict generalization of WMC. The main idea here is to annotate a logical theory with rational and Boolean variables, that is, from a combination of LRA and propositional logic. Nonetheless, a simple semantic formulation is given based on propositional logic, where, as before, propositional assignments are denoted using M:

Definition 4: Suppose � is a SMT theory over Boolean and rational variables B and X, and literals L: Suppose w : L ! EXPR(X), where EXPR(X) are expressions over X. Then the weighted model integral (WMI) is defined as:

where

The intuition is this. The WMI of a SMT theory � is defined in terms of the models of its propositional abstraction � � : For each such model, we compute its volume, that is, we integrate the w-values of the literals that are true at the model. The interval of the integral is defined in terms of the refinement of the literal. The w-function is to be seen as mapping an expression e to its density function, which is usually another expression mentioning the variables in e:

Let us remark that while the interval is defined in terms of SMT literals, this is meant to denote standard integrals in an obvious fashion; for example:

If the subscript is a propositional literal, then it is simply ignored. In general, the standard integral for a LRA-formula � over variables x1; : : : ; xn can be obtained by:

where Ie is the indicator function for the event e: So, for example, we obtain the following equivalence:

Conditional Probabilities

As usual, given a Markov network N over Boolean and realvalued random variables, conditional probabilities are obtained using:

where � and w denote the network and potential encodings.

To see WMI in action, consider a simple example:

Example 5: Suppose � is the following formula:

For weights, let w(p) = :1, w(:p) = 2x, w(q) = 1 and w(:q) = 0, where q is the propositional abstraction of (0 � x � 10): Roughly, this can be seen to say that x is uniformly distributed when p holds and otherwise it is characterized by a triangular distribution in the interval [0, 10]. There are 3 models of � � :

1. M = fp; :qg: since w(:q) = 0, by definition we have weight(M; w) = 0 and so vol(M; w) = 0;
2. M = f:p; qg: vol(M; w) = R 0�x�10 2x dx = h x 2 i10 0 = 100:
3. M = fp; qg: vol(M; w) = R 0�x�10 :1 dx = [:1 � x] 10 0 = 1:

Thus, WMI(� ; w) = 100 + 1 = 101:

Suppose that we are interested in the probability of the query x � 3 given that :p is observed. Suppose r is the abstraction of x � 3: First, WMI(� ^ :p; w) corresponds to the weight of a single interpretation, that of item 2, yielding a value of 100: Next, WMI(� ^ :p ^ x � 3; w) also corresponds to the weight of a single interpretation M = f:p; q; rg, an extension to that in item 2. In this case:

Therefore, the conditional probability is 9=100 = :09: �

Generality

Recall that propositions as intervals to integrals are simply ignored, and propositional logic is a fragment of the logical language considered here. So, we get:

Proposition 6: Suppose � is a formula in propositional logic over literals L and w : L ! R �0 : Then WMI(� ; w) = WMC(� ; w):

Classes of Weight Functions

The weight function in the WMI formulation does not commit to any restrictions on EXPR(X), in which case arbitrary continuous functions (including exponential families) can be encoded. In practice, it will be useful to identify two special cases. We are motivated by inference for two classes of representations: piecewise-constant hybrid Markov networks (CHMN) and piecewise-polynomial hybrid Markov networks (PHMN). These are Markov networks in feature representation, as shown before, where now the features are SMT sentences, and the weights are constants and polynomials respectively. That is, inference for CHMNs can be reduced to WMI where w : L ! R �0 , and for PHMNs, w maps L to polynomials over X:

Although CHMN subsume discrete Markov networks, they are still very limited in the continuous distributions they can represent. In Example 5, a uniform distribution was represented, but consider the case of a Gaussian:

Example 7: Suppose u is normally distributed with mean 0 and variance 1, conditioned to be in the three-deviation interval [�3; 3]. We can approximate 2 this distribution with the following CHMN:

2 The weights were computed using the software Matlab (www.mathworks.com) to be the least-squares approximation.

whose density is depicted in Figure 1a. The unweighted formula is a hard constraint. �

PHMNs, of course, give us considerably more expressive power in the weight function:

Example 8: Suppose u is as before, but approximated using the following PHMN:

which appeals to polynomials of degree 3, and is plotted in Figure 1c. We might compare it to Figure 1b that shows a coarser approximation than this one using polynomial weights of degree 1. �

Correctness

Finally, we provide an appropriate companion to Theorem 3:

Theorem 9 : Let N be a Markov network over Boolean and real-valued random variables B and X and potentials f�1; : : : ; �kg : Let � and w be the corresponding encodings. Then for any q; e 2 B[X, PrN(q j e) is given by (2).

Proof (Sketch): The argument is similar in spirit to the one provided for Theorem 3. For any N; suppose � is the density accorded to all assignments (b; x) of the random variables in B[X, where c1 � x1 � d1; : : : ; cn � xn � dn: Then the subset of the probability space obtained from b1 �� � ��bn �[c1; d1]� � � � � [cn; dn] can be exactly mapped to a model of � � , in the sense of being accorded the same density. (The assumption here, of course, is that � would encode these intervals as SMT literals of the form ci � xi � di with an appropriate w-value.) The partition function Z is calculated by integrating over R n for all such subsets. Using the definition:

together with the observation:

we find that WMI(� ; w) is also obtained by integrating over R n for all corresponding models of � � . Thus, WMI(� ; w) = Z, and the case of the conditional probability is a simple corollary.

Inference Complexity

To conclude the section, let us discuss the complexity of the volume computations that need to be performed for WMI. One may be concerned about the degree of the polynomials being integrated. Indeed, these degrees can become large.

Proposition 10: Suppose �, B, X, L and w is as before, where w encodes a PHMN. Let k be the maximum degree of the polynomials in fw(l) j l 2 Lg : Let n be the number of propositions in � � : Then WMI(� ; w) computes volumes of polynomials of degree k � n:

Proof: Suppose M is a model of � � : By assumption size(fl + j l 2 Mg) = n: Then weight(M; w) would be a product of n polynomials each of degree k, giving us (k � n):

However, Baldoni et al. [2011] show that for a fixed number of variables, the integration is e�cient, even for polynomials of high degree. 3 Smoother function approximations therefore come at a reasonable cost.

4 Parameter Learning for CHMN

This section focuses on the weight learning task for CHMNs. Weight learning uses data D to automatically learn the density associated with each feature (that is, an SMT formula) by optimizing a given objective function. This section explores how the standard practice of parameter learning [Koller and Friedman, 2009] can be understood for our framework. 4

Let us recall some preliminaries. We appeal to the notion of maximum likelihood estimation where given a set of parameters w1; : : : ; wk, and D, we seek to maximize the likelihood (MLE) of these parameters given the data:

For technical reasons, given a Markov network N, a loglinear model for the joint density function is often considered, as follows:

where clique potentials are replaced by an exponentiated weighted sum of features. Then, the likelihood can be shown to be maximum precisely when:

which says the empirical expectation of fi in D (for example, the count) equals its expectation according to the current parameterization.

In our setting, we first observe that for PHMNs, taking a logistic model would mean that the density function is the Euler number e raised to a complex high degree polynomial, 5

3 See Baldoni et al. [2011] also for discussions on how this relates to the more general problem of computing volumes of arbitrary polytopes [Dyer and Frieze, 1988].

4 While we consider maximum likelihood estimation here, maxmargin learning of weighted SMT theories has also been recently proposed [Teso et al., 2015].

5 No approximations for Gaussians would then be needed.

which would be prohibitive in practice. 6 We focus instead on CHMNs, which can be given a fully logistic formulation.

Given D and a SMT theory � ; the empirical expectation of a formula � 2 � can be obtained by calculating:

That is, we simply count the items in Dwhich are true for �: For example, if (x = 3:5) 2 D and (p _ x � 7) 2 � ; then the count of the feature (p _ x � 7) increases.

Given a SMT theory � and a weight function w, the expectation of � 2 � wrt w is given by

With this formulation, standard iterative methods from convex optimization can be used [Koller and Friedman, 2009]. Building on Theorem 9, we prove:

Theorem 11: Suppose N is a Markov network provided as a log-linear model (with numeric weights). Given its encoding as an SMT theory �, the parameter estimates for � 2 � maximizing the likelihood given D are those minimizing the di�erence between ED[�] and Ew[�].

5 Experimental Evaluations

In this section, we discuss results on an implementation of WMI inference and CHMN parameter learning. The WMI implementation scheme is an exhaustive DPLL search modulo an SMT oracle. 7

Our system is implemented using the Z3 SMT solver v4.3.2, 8 and the LattE software v1.6 for computing integrals. 9 All experiments were run using a system with 1.7 GHz Intel Core i7 and 8GB RAM.

Scaling Behavior

To test the scaling behavior, we are mainly concerned with the volume computation aspect of the WMI task. Observe that WMI for � can be seen to implicitly compute #SAT on � � . Therefore, to evaluate our implementation, the system is also made to compute #SAT(� � ), which can be enabled by simply letting vol(M; w) = 1 for any M and w:

For our tests, we randomly generated SMT theories and weight functions, involving intricate dependencies and hard constraints. These included weighted sentences of the form:

with additional hard constraints of the sort:

6 The MLE formulation can be given for non-logistic models under certain reasonable assumptions, which can be applied to PHMNs. We leave this to an extended version of the paper.

7 We remark that our implementation does not yet consider the full range of e�ective WMC techniques [Sang et al., 2005], such as component caching [Bacchus et al., 2009]. This is an interesting avenue for the future.

8 http://z3.codeplex.com

9 https://www.math.ucdavis.edu/�latte

While iteratively increasing the number of variables and constraints in the SMT theories, we plot the WMI behavior and use #SAT(� � ) as the baseline against all instances of a certain model count in Figure 2a. (The plots are smoothed for readability.) This compares, for example, the e�ort for weight and volume computations as the number of models of the input theory increases. We see that the implementation scales well relative to #SAT(� � ). While our theories sparingly mention high-degree polynomials, integration is still necessary for almost all real-valued variables and so this demonstrates that WMI and its volume computation approach is both feasible and can be made e�ective.

Real-World Dataset

Next, we demonstrate parameter learning, and the diversity of applications that WMI can characterize, well beyond the standard hybrid examples. We consider the following novel application involving conditional queries over arithmetic constraints. It uses a data series released by the UK government that provides average journey time, speed and tra�c flow information on all motorways, known as the Strategic Road Network, in England. 10 Motorways are split into junctions, and each information record refers to a specific junction, day and time period. In the following we consider the 2012 dataset, with over 7 million entries, and focus on a set of junctions surrounding Heathrow airport (J12-J16).

The task is as follows. Think of a commuter going to work. She expresses assumptions about her journey in terms of the time period of the journey, its duration, the average speed that she can drive at through a junction using soft constraints:

which can be read as if her travel is during the morning, the total journey time is (hopefully) less than 800 seconds, that the average speed exceeds 80 kmh in the afternoon, and so on. Together with hard constraints, such as:

10 http://data.gov.uk/dataset/dft-eng-srn-routes-journey-times

she is interested in complex conditional queries about the journey time given certain conditions such as the day of week and the time of travel.

In our experiments, we applied the parameter learning formulation to learn the weights of such assumptions against the 2012 dataset, mapping terms in the theory to actual data points as appropriate. The weights are initialized to 1, and Figure 2b plots how the weights diverge for the formulas f1 and f2 when likelihood estimation terminates. In essence, mornings being peak tra�c hours, it is unlikely that a morning journey lasts less than 800 seconds, and so f1 is accorded a low probability. In contrast, the commuter's afternoon assumptions are reasonable relative to the data, leading to f2 have a high(er) probability.

Finally, Figure 2c shows how the conditional probability of getting to work on time changes according to the increasing amount of evidence. We observe that the query can be conditioned wrt arbitrary Boolean combinations of arithmetic and propositional constraints. Consider, for example, the second query. After taking into account that at least 320 seconds has been currently spent in the first junction on a Friday morning (i.e., evidence M^F), the driver concludes that the probability of getting to work on time (J < 1000) is now fairly low. She then refers to a colleague who has passed through the last junction to report that the current average speed in the junction j3 is over 95 kmh. With this evidence, the probability of getting to work on time increases.

6 Conclusions

WMC is a prominent and general approach to probabilistic inference in Boolean (and discrete) graphical models. In the recent years, the performance of SAT solvers has greatly improved, not only due to massive engineering e�orts, but also because of theoretical insights on SAT algorithms themselves. While WMC benefits from these developments, it remains restricted to discrete probability distributions. In this work, we proposed the generalization WMI, proved its correctness, expressiveness as well as its downward compatibility with WMC. It is based on SMT technology that has also enjoyed tremendous progress together with SAT. The notion allows us to address exact inference in mixtures of discrete and continuous probability distributions. We then demonstrated parameter learning on a real-world dataset. The results are promising and the formulation is general. For the future, we would like to generalize algorithmic insights from WMC, such as component caching [Bacchus et al., 2009], for the WMI task.

Acknowledgements

Vaishak Belle is partially funded by the Research FoundationFlanders (FWO-Vlaanderen) project on Data Cleaning and the KU Leuven's GOA on Declarative Modeling for Mining and Learning. Guy Van den Broeck is supported by the Research Foundation-Flanders (FWO-Vlaanderen).