Weighted model integration (WMI) is a very appealing framework for probabilistic inference: it allows to express the complex dependencies of real-world problems where variables are both continuous and discrete, via the language of Satisfiability Modulo Theories (SMT), as well as to compute probabilistic queries with complex logical and arithmetic constraints. Yet, existing WMI solvers are not ready to scale to these problems. They either ignore the intrinsic dependency structure of the problem at all, or they are limited to too restrictive structures. To narrow this gap, we derive a factorized formalism of WMI enabling us to devise a scalable WMI solver based on message passing, MP-WMI. Namely, MP-WMI is the first WMI solver which allows to: 1) perform exact inference on the full class of tree-structured WMI problems; 2) compute all marginal densities in linear time; 3) amortize inference inter query. Experimental results show that our solver dramatically outperforms the existing WMI solvers on a large set of benchmarks.

Probabilistic inference in the hybrid domain, i.e. inference over discrete-continuous domains, requires tackling two well known #P-hard problems 1)~weighted model counting (WMC) over discrete variables and 2)~integration over continuous variables. For both of these problems inference techniques have been developed separately in order to manage their #P-hardness, such as knowledge compilation for WMC and Monte Carlo (MC) methods for (approximate) integration in the continuous domain. Weighted model integration (WMI), the extension of WMC to the hybrid domain, has been proposed as a formalism to study probabilistic inference over discrete and continuous variables alike. Recently developed WMI solvers have focused on exploiting structure in WMI problems, for which they rely on symbolic integration to find the primitive of an integrand, i.e. to perform anti-differentiation. To combine these advances with state-of-the-art Monte Carlo integration techniques, we introduce \textit{Monte Carlo anti-differentiation} (MCAD), which computes MC approximations of anti-derivatives. In our empirical evaluation we substitute the exact symbolic integration backend in an existing WMI solver with an MCAD backend. Our experiments show that that equipping existing WMI solvers with MCAD yields a fast yet reliable approximate inference scheme.

Weighted model integration (WMI) extends Weighted model counting (WMC) to the integration of functions over mixed discrete-continuous domains. It has shown tremendous promise for solving inference problems in graphical models and probabilistic programming. Yet, state-of-the-art tools for WMI are limited in terms of performance and ignore the independence structure that is crucial to improving efficiency. To address this limitation, we propose an efficient model integration algorithm for theories with tree primal graphs. We exploit the sparse graph structure by using search to performing integration. Our algorithm greatly improves the computational efficiency on such problems and exploits context-specific independence between variables. Experimental results show dramatic speedups compared to existing WMI solvers on problems with tree-shaped dependencies.