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技术可以处理的一系列问题。对合成和真实的解决方案进行广泛的实验性评估,将基于SMT的公平性技术的高效技术纳入正式核查,从而进一步验证现有技术的正确性方案。