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技术可解决的问题范围。在合成数据集与真实世界数据集上的大量实验评估证实，所提方法相较于现有替代方案具有显著优势。通过一项验证概率程序公平性的原型任务，进一步展示了该技术的应用潜力。