Enhancing SMT-based Weighted Model Integration by Structure Awareness

要約

確率的推論のための効率的な正確アルゴリズムと近似アルゴリズムの開発は、人工知能研究の長年の目標です。
純粋な離散または純粋な連続ドメインの処理では大幅な進歩が見られましたが、離散変数と連続変数およびそれらの関係を特徴とするハイブリッド ドメインに取り組むために開発されたソリューションを適応させることは、非常に簡単ではありません。
加重モデル統合 (WMI) は、ハイブリッド ドメインにおける確率的推論のための統一形式主義として最近登場しました。
最近かなりの量の研究が行われているにもかかわらず、WMI アルゴリズムをハイブリッド問題の複雑さに合わせて拡張できるようにすることは依然として課題です。
この論文では、既存の最先端ソリューションのいくつかの重大な制限を強調し、形式検証における効率的な手法である SMT ベースの列挙と、問題構造の効果的なエンコードを組み合わせたアルゴリズムを開発します。
これにより、アルゴリズムが冗長なモデルの生成を回避できるようになり、計算量が大幅に節約されます。
さらに、SMT ベースのアプローチが、正確および近似の両方のさまざまな統合手法にどのようにシームレスに対処できるかを示し、WMI テクノロジによって対処できる一連の問題を大幅に拡大します。
合成データセットと現実世界のデータセットの両方に対する広範な実験評価により、提案されたソリューションが既存の代替案よりも大きな利点があることが確認されています。
このテクノロジーの応用可能性は、確率的プログラムの公平性を検証することを目的としたプロトタイプ タスクでさらに実証されます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google