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.

翻译：概率推理的高效精确与近似算法开发是人工智能研究的长期目标。尽管在处理纯离散或纯连续域方面已取得显著进展，但将现有解决方案适配至包含离散与连续变量及其关系的混合域仍极具挑战。加权模型集成（WMI）近期成为混合域概率推理的统一形式化框架。尽管近期研究众多，但提升WMI算法应对混合问题复杂性的可扩展性仍是难题。本文揭示了现有最优方法存在的若干根本性局限，并提出了一种融合SMT枚举技术与问题结构有效编码的算法。该算法通过避免生成冗余模型，实现了计算效率的显著提升。此外，我们展示了基于SMT的方法如何无缝适配精确与近似等不同积分技术，极大地拓展了WMI技术可处理的问题范畴。在合成数据集与真实数据集上的大量实验验证了本方案相较现有替代方案的显著优势。该技术在验证概率程序公平性的原型任务中的应用潜力，进一步彰显了其实用价值。