# A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification

arXiv: https://arxiv.org/abs/2502.03274 · HTML: https://mlsanity.com/paper/2502.03274/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 18 of its 36 references that are in the map.
- First posted on arXiv 5 Feb 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 18 of 18)

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Neural Probabilistic Logic Programming in DeepProbLog](https://mlsanity.com/paper/1907.08194/) (2019)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Scaling provable adversarial defenses](https://mlsanity.com/paper/1805.12514/) (2018)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [NeurASP: Embracing Neural Networks into Answer Set Programming](https://mlsanity.com/paper/2307.07700/) (2023)
- [From Statistical Relational to Neurosymbolic Artificial Intelligence: a Survey](https://mlsanity.com/paper/2108.11451/) (2021)
- [DeepStochLog: Neural Stochastic Logic Programming](https://mlsanity.com/paper/2106.12574/) (2021)
- [Certified Training: Small Boxes are All You Need](https://mlsanity.com/paper/2210.04871/) (2022)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [BEARS Make Neuro-Symbolic Models Aware of their Reasoning Shortcuts](https://mlsanity.com/paper/2402.12240/) (2024)
- [ROAD-R: The Autonomous Driving Dataset with Logical Requirements](https://mlsanity.com/paper/2210.01597/) (2022)
- [Expressive Losses for Verified Robustness via Convex Combinations](https://mlsanity.com/paper/2305.13991/) (2023)
- [Neuro-Symbolic Verification of Deep Neural Networks](https://mlsanity.com/paper/2203.00938/) (2022)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond](https://mlsanity.com/paper/2002.12920/) (2020)

## Built on by (most cited first, 1 of 1)

- [Does Reasoning Mitigate Backdoor Attacks? A Neuro-Symbolic Perspective](https://mlsanity.com/paper/2609.00464/) (2026)

## Abstract (arXiv)

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 NPPP-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.