A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification
This addresses the need for safe deployment of neuro-symbolic AI in critical domains, though it is incremental as it builds on existing verification challenges.
The paper tackles the problem of formally verifying the robustness of probabilistic neuro-symbolic reasoning systems, showing that exact verification is NP^PP-complete and proposing an approximate method that scales exponentially better than solver-based solutions, as demonstrated on a standard benchmark and a real-world autonomous driving domain.
Neuro-Symbolic Artificial Intelligence (NeSy AI) has emerged as a promising direction for integrating neural learning with symbolic reasoning. Typically, 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 a decision version of the core computation is $\mathrm{NP}^{\mathrm{PP}}$-complete. In the face of this result, we propose the first approach for approximate, relaxation-based verification of probabilistic NeSy systems. We demonstrate experimentally on a standard NeSy benchmark that the proposed method scales exponentially better than solver-based solutions and apply our technique to a real-world autonomous driving domain, where we verify a safety property under large input dimensionalities.