A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification

TL;DR

This paper introduces a scalable, approximate verification method for probabilistic neuro-symbolic AI systems, ensuring their robustness and safety in critical applications like autonomous driving.

Contribution

It provides the first relaxation-based approach for probabilistic NeSy verification, addressing computational complexity and demonstrating practical scalability.

Findings

The decision problem is NP^PP-complete.

The proposed method scales exponentially better than solver-based solutions.

Successfully verified safety properties in autonomous driving scenarios.

Abstract

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.