Model Counting in the Wild

要約

モデルのカウントは、確率推論、ネットワークの信頼性、ニューラル ネットワーク検証などのアプリケーションを使用した自動推論における基本的な問題です。
モデル カウンティングは #P 完全性のため、理論的な観点からは計算で処理するのが困難ですが、スケーラビリティの課題に対処するための最先端のモデル カウンターの開発においては、過去 10 年間で大きな進歩が見られました。
この作業では、実際のモデル カウンターのスケーラビリティを厳密に評価します。
この目的を達成するために、11 のアプリケーション ドメインを調査し、これらのドメインから合計 2,262 のベンチマークを収集しました。
次に、これらのインスタンスで 6 つの最先端のモデル カウンターを評価し、スケーラビリティと実行時のパフォーマンスを評価しました。
私たちの経験的評価では、モデル カウンターのパフォーマンスがアプリケーション ドメインごとに大きく異なることが実証されており、エンド ユーザーが慎重に選択する必要があることが強調されています。
さらに、モデル計数コミュニティによって提案された 2 つのパラメーターに関してさまざまなカウンターの動作を調査しましたが、弱い相関関係しか見つかりませんでした。
私たちの分析は、モデルカウンティングにおけるポートフォリオベースのアプローチの課題と機会を浮き彫りにしています。

要約(オリジナル)

Model counting is a fundamental problem in automated reasoning with applications in probabilistic inference, network reliability, neural network verification, and more. Although model counting is computationally intractable from a theoretical perspective due to its #P-completeness, the past decade has seen significant progress in developing state-of-the-art model counters to address scalability challenges. In this work, we conduct a rigorous assessment of the scalability of model counters in the wild. To this end, we surveyed 11 application domains and collected an aggregate of 2262 benchmarks from these domains. We then evaluated six state-of-the-art model counters on these instances to assess scalability and runtime performance. Our empirical evaluation demonstrates that the performance of model counters varies significantly across different application domains, underscoring the need for careful selection by the end user. Additionally, we investigated the behavior of different counters with respect to two parameters suggested by the model counting community, finding only a weak correlation. Our analysis highlights the challenges and opportunities for portfolio-based approaches in model counting.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google