A Scalable Approach to Probabilistic Neuro-Symbolic Verification

要約

神経系シンボリック人工知能（NESY AI）は、神経学習を象徴的な推論と統合するための有望な方向として浮上しています。
このようなシステムの確率的バリアントでは、ニューラルネットワークは最初にサブシンボリック入力からシンボルのセットを抽出します。これは、記号コンポーネントによって使用され、クエリに答えるために確率的な方法で推論します。
この作業では、このような不気味な確率的推論システムの堅牢性を正式に検証する問題に対処し、したがって、重要なドメインでの安全な展開への道を開いています。
この問題を正確に解決することの複雑さを分析し、$ \ mathrm {np}^{\＃\ mathrm {p}} $-hardであることを示します。
この問題を克服するために、確率的な不気味なシステムのおおよそのリラクゼーションベースの検証のための最初のアプローチを提案します。
提案された方法は、ソルバーベースのソリューションよりも指数関数的に優れていることを実験的に実証し、手法を実際の自律運転データセットに適用し、そこで大規模な入力寸法とネットワークサイズの下で安全プロパティを確認します。

要約(オリジナル)

Neuro-Symbolic Artificial Intelligence (NeSy AI) has emerged as a promising direction for integrating neural learning with symbolic reasoning. In the probabilistic variant of such systems, a neural network first extracts a set of symbols from sub-symbolic input, which are then used by a symbolic component to reason in a probabilistic manner towards answering a query. In this work, we address the problem of formally verifying the robustness of such NeSy probabilistic reasoning systems, therefore paving the way for their safe deployment in critical domains. We analyze the complexity of solving this problem exactly, and show that it is $\mathrm{NP}^{\# \mathrm{P}}$-hard. To overcome this issue, we propose the first approach for approximate, relaxation-based verification of probabilistic NeSy systems. We demonstrate experimentally that the proposed method scales exponentially better than solver-based solutions and apply our technique to a real-world autonomous driving dataset, where we verify a safety property under large input dimensionalities and network sizes.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google