Our paper A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification received the best paper award at the 19th Conference on Neurosymbolic Learning and Reasoning (NeSy 2025).
The paper addresses formal verification of robustness in neuro-symbolic AI systems that combine neural perception with probabilistic symbolic reasoning. We show that a decision version of the core verification problem is NP^PP-complete, and propose the first relaxation-based approach for approximate verification, scaling exponentially better than exact solvers. We demonstrate the approach on a real-world autonomous driving domain under large input dimensionalities.