Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees

要約

充足可能性モジュロ計数 (SMC) には、記号的意思決定と統計的推論の両方を必要とする問題が含まれます。
その一般的な定式化は、記号的人工知能と統計的人工知能の交差点における多くの現実世界の問題を捉えています。
SMC は、確率的な結果を制御するための政策介入を模索します。
SMC を解くことは、統計的推論と記号的推論を組み込む非常に難解な性質 ($\text{NP}^{\text{PP}}$-complete) のため、困難です。
SMC の解決に関するこれまでの研究では、証明可能な保証が不足していたり​​、特に組み合わせ制約が存在する場合に最適ではない経験的パフォーマンスに悩まされたりしています。
我々は、NP オラクルにアクセスできる多項式アルゴリズムである XOR-SMC を提案し、一定の近似を保証する非常に難解な SMC 問題を解決します。
XOR-SMC は、SMC のモデルカウントをランダム化された XOR 制約の対象となる SAT 式に置き換えることにより、非常に扱いにくい SMC を充足可能性問題に変換します。
社会的利益のための AI における重要な SMC 問題を解決する実験では、XOR-SMC が真の最適解に近い解を見つけ、SMC での扱いにくいモデル計数の適切な近似値を見つけるのに苦労しているいくつかのベースラインを上回るパフォーマンスを示したことが実証されました。

要約(オリジナル)

Satisfiability Modulo Counting (SMC) encompasses problems that require both symbolic decision-making and statistical reasoning. Its general formulation captures many real-world problems at the intersection of symbolic and statistical Artificial Intelligence. SMC searches for policy interventions to control probabilistic outcomes. Solving SMC is challenging because of its highly intractable nature($\text{NP}^{\text{PP}}$-complete), incorporating statistical inference and symbolic reasoning. Previous research on SMC solving lacks provable guarantees and/or suffers from sub-optimal empirical performance, especially when combinatorial constraints are present. We propose XOR-SMC, a polynomial algorithm with access to NP-oracles, to solve highly intractable SMC problems with constant approximation guarantees. XOR-SMC transforms the highly intractable SMC into satisfiability problems, by replacing the model counting in SMC with SAT formulae subject to randomized XOR constraints. Experiments on solving important SMC problems in AI for social good demonstrate that XOR-SMC finds solutions close to the true optimum, outperforming several baselines which struggle to find good approximations for the intractable model counting in SMC.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google