Enhancing SMT-based Weighted Model Integration by Structure Awareness

TL;DR

An algorithm is developed that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure, resulting in drastic computational savings and significantly expanding the set of problems that can be tackled by WMI technology.

Abstract

The development of efficient exact and approximate algorithms for probabilistic inference is a long-standing goal of artificial intelligence research. Whereas substantial progress has been made in dealing with purely discrete or purely continuous domains, adapting the developed solutions to tackle hybrid domains, characterised by discrete and continuous variables and their relationships, is highly non-trivial. Weighted Model Integration (WMI) recently emerged as a unifying formalism for probabilistic inference in hybrid domains. Despite a considerable amount of recent work, allowing WMI algorithms to scale with the complexity of the hybrid problem is still a challenge. In this paper we highlight some substantial limitations of existing state-of-the-art solutions, and develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure. This allows our algorithm to avoid generating redundant models, resulting in drastic computational savings. Additionally, we show how SMT-based approaches can seamlessly deal with different integration techniques, both exact and approximate, significantly expanding the set of problems that can be tackled by WMI technology. An extensive experimental evaluation on both synthetic and real-world datasets confirms the substantial advantage of the proposed solution over existing alternatives. The application potential of this technology is further showcased on a prototypical task aimed at verifying the fairness of probabilistic programs.

Figures (10)

• Figure 1: Example highlighting the efficiency issues of the knowledge compilation algorithms for WMI. ( a) definition of a weight function consisting of a product of conditional statements. ( b) decision diagram generated by knowledge compilation approaches over the weight function. Round nodes indicate if-then-else conditions, with true and false cases on the right and left outgoing edges respectively. Squared nodes indicate ${\sf FI}^{\mathcal{LRA}\xspace}$ weight functions. Note how the diagram has a number of branches which is exponential in the number of conditions, and no compression is achieved. ( c) definition of the weight functions at the leaves of the diagram. In naming weight functions, we use $\bar{A}$ for $\lnot A$ for the sake of compactness.
• Figure 3: Example highlighting the efficiency issues of the WMI-PA algorithm. ( a) definition of formula $\varphi$ (trivially true) and support $\chi\xspace$. ( b) definition of the weight function $w(\mathbf{x}\xspace,\mathbf{A}\xspace)\xspace$. Round nodes indicate if-then-else conditions, with true and false cases on the right and left outgoing edges respectively. Squared nodes indicate ${\sf FI}^{\mathcal{LRA}\xspace}$ weight functions. ( c) novel version of the formula $\varphi^{*}(\mathbf{x}\xspace,\mathbf{A}\xspace\cup\mathbf{B}\xspace)\xspace$ after the application of the ${\sf LabelConditions(\ldots)}$ step of WMI-PA. ( d) novel version of the weight function $w^{*}(\mathbf{x}\xspace,\mathbf{A}\xspace\cup\mathbf{B}\xspace)\xspace$, where all $\mathcal{LRA}$ conditions have been replaced with the fresh Boolean atoms introduced in $\varphi^{*}(\mathbf{x}\xspace,\mathbf{A}\xspace\cup\mathbf{B}\xspace)\xspace$. ( e) List of assignments obtained by WMI-PA on $\mathbf{A}\xspace\cup\mathbf{B}\xspace$ (split on two columns for the sake of compactness). Notice the amount of assignments sharing the same ${\sf FI}^{\mathcal{LRA}\xspace}$ weight function.
• Figure 4: Graphical representation of the effectiveness of SAE4WMI as compared to the alternatives: (a) WMI problem from Example \ref{['exmp:example_skv2_cnf']}, with 4 non-convex areas of ${\sf FI}^{\mathcal{LRA}\xspace}$ weights. Notice that the weight function includes non-literal conditions; (b) WMI-PA computes 20 distinct integrals; (c) SA-WMI-PA, using both the implicit and explicit non-CNF skeleton versions, computes 11 distinct integrals; (d) SAE4WMI, that uses the "local" CNF explicit skeleton, computes 8 distinct integrals, the minimum number of integrals that is needed to retain convexity of their areas (i.e., ${\sf FI}^{\mathcal{LRA}\xspace}$ weights).
• Figure 5: Cactus plots of the synthetic experiments reporting execution time (left) for all the methods; number of integrals (right) for WMI-PA, SA-WMI-PA and SAE4WMI.
• Figure 6: Cactus plots representing average query execution times in seconds on a set of DET problems with $H \in \{0.25, 0.5, 0.75, 1\}$.

Theorems & Definitions (17)

• Example 1
• Example 2
• Example 3
• Example 4
• Remark 1
• Example 5
• Definition 1: Conditional skeleton of $w$, ${\sf sk}(w\xspace)$
• Example 6
• Example 7
• Example 8