# Neuro-Symbolic Verification of Deep Neural Networks

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

## Key facts

- Cited by 21 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 47 references that are in the map.
- First posted on arXiv 2 Mar 2022.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [The Neuro-Symbolic Concept Learner: Interpreting Scenes, Words, and Sentences From Natural Supervision](https://mlsanity.com/paper/1904.12584/) (2019)
- [Neural-Symbolic VQA: Disentangling Reasoning from Vision and Language Understanding](https://mlsanity.com/paper/1810.02338/) (2018)
- [Neurosymbolic AI: The 3rd Wave](https://mlsanity.com/paper/2012.05876/) (2020)
- [Neural-Symbolic Computing: An Effective Methodology for Principled Integration of Machine Learning and Reasoning](https://mlsanity.com/paper/1905.06088/) (2019)
- [Preventing Repeated Real World AI Failures by Cataloging Incidents: The AI Incident Database](https://mlsanity.com/paper/2011.08512/) (2020)
- [Right for the Right Concept: Revising Neuro-Symbolic Concepts by Interacting with their Explanations](https://mlsanity.com/paper/2011.12854/) (2020)
- [From Statistical Relational to Neuro-Symbolic Artificial Intelligence](https://mlsanity.com/paper/2003.08316/) (2020)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [Generative Neurosymbolic Machines](https://mlsanity.com/paper/2010.12152/) (2020)
- [Concolic Testing for Deep Neural Networks](https://mlsanity.com/paper/1805.00089/) (2018)
- [Conversational Neuro-Symbolic Commonsense Reasoning](https://mlsanity.com/paper/2006.10022/) (2020)

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

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Not All Neuro-Symbolic Concepts Are Created Equal: Analysis and Mitigation of Reasoning Shortcuts](https://mlsanity.com/paper/2305.19951/) (2023)
- [BEARS Make Neuro-Symbolic Models Aware of their Reasoning Shortcuts](https://mlsanity.com/paper/2402.12240/) (2024)
- [A Neuro-Symbolic Benchmark Suite for Concept Quality and Reasoning Shortcuts](https://mlsanity.com/paper/2406.10368/) (2024)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [Shortcuts and Identifiability in Concept-based Models from a Neuro-Symbolic Lens](https://mlsanity.com/paper/2502.11245/) (2025)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Value Functions are Control Barrier Functions: Verification of Safe Policies using Control Theory](https://mlsanity.com/paper/2306.04026/) (2023)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [On the verification of Embeddings using Hybrid Markov Logic](https://mlsanity.com/paper/2312.08287/) (2023)
- [Neuro-Symbolic AI for Cybersecurity: State of the Art, Challenges, and Opportunities](https://mlsanity.com/paper/2509.06921/) (2025)
- [Neuro-Symbolic Artificial Intelligence: A Task-Directed Survey in the Black-Box Models Era](https://mlsanity.com/paper/2603.03177/) (2026)
- [Modular design patterns for neural-symbolic integration: refinement and combination](https://mlsanity.com/paper/2206.04724/) (2022)
- [VeriFlow: Modeling Distributions for Neural Network Verification](https://mlsanity.com/paper/2406.14265/) (2024)
- [A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification](https://mlsanity.com/paper/2502.03274/) (2025)
- [NeuroShield: A Neuro-Symbolic Framework for Adversarial Robustness](https://mlsanity.com/paper/2601.13162/) (2026)
- [Probabilistic ML Verification via Weighted Model Integration](https://mlsanity.com/paper/2402.04892/) (2024)
- [Bridging the Gap: Representation Spaces in Neuro-Symbolic AI](https://mlsanity.com/paper/2411.04393/) (2024)
- [The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification](https://mlsanity.com/paper/2506.12084/) (2025)
- [Attack logics, not outputs: Towards efficient robustification of deep neural networks by falsifying concept-based properties](https://mlsanity.com/paper/2510.03320/) (2025)
- [Mining Verdict Boundaries for Neural Network Verification](https://mlsanity.com/paper/2607.28954/) (2026)

## Abstract (arXiv)

Formal verification has emerged as a powerful approach to ensure the safety and reliability of deep neural networks. However, current verification tools are limited to only a handful of properties that can be expressed as first-order constraints over the inputs and output of a network. While adversarial robustness and fairness fall under this category, many real-world properties (e.g., "an autonomous vehicle has to stop in front of a stop sign") remain outside the scope of existing verification technology. To mitigate this severe practical restriction, we introduce a novel framework for verifying neural networks, named neuro-symbolic verification. The key idea is to use neural networks as part of the otherwise logical specification, enabling the verification of a wide variety of complex, real-world properties, including the one above. Moreover, we demonstrate how neuro-symbolic verification can be implemented on top of existing verification infrastructure for neural networks, making our framework easily accessible to researchers and practitioners alike.