# Efficient Symbolic Reasoning for Neural-Network Verification

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

## 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 35 of its 71 references that are in the map.
- First posted on arXiv 23 Mar 2023.

## Placed in

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

## Builds on (most cited first, 30 of 35)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Distributed Representations of Words and Phrases and their Compositionality](https://mlsanity.com/paper/1310.4546/) (2013)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [FaceNet: A Unified Embedding for Face Recognition and Clustering](https://mlsanity.com/paper/1503.03832/) (2015)
- [The Limitations of Deep Learning in Adversarial Settings](https://mlsanity.com/paper/1511.07528/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Certified Defenses against Adversarial Examples](https://mlsanity.com/paper/1801.09344/) (2018)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [Sampling Matters in Deep Embedding Learning](https://mlsanity.com/paper/1706.07567/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Understanding Deep Neural Networks with Rectified Linear Units](https://mlsanity.com/paper/1611.01491/) (2016)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [On the Robustness of Vision Transformers to Adversarial Examples](https://mlsanity.com/paper/2104.02610/) (2021)
- [Multiscale Deep Equilibrium Models](https://mlsanity.com/paper/2006.08656/) (2020)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Globally-Robust Neural Networks](https://mlsanity.com/paper/2102.08452/) (2021)
- [Crafting Adversarial Input Sequences for Recurrent Neural Networks](https://mlsanity.com/paper/1604.08275/) (2016)
- [Exactly Computing the Local Lipschitz Constant of ReLU Networks](https://mlsanity.com/paper/2003.01219/) (2020)
- [Lipschitz constant estimation of Neural Networks via sparse polynomial optimization](https://mlsanity.com/paper/2004.08688/) (2020)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Training Certifiably Robust Neural Networks with Efficient Local Lipschitz Bounds](https://mlsanity.com/paper/2111.01395/) (2021)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [A Unified Algebraic Perspective on Lipschitz Neural Networks](https://mlsanity.com/paper/2303.03169/) (2023)
- [A Quantitative Geometric Approach to Neural-Network Smoothness](https://mlsanity.com/paper/2203.01212/) (2022)
- [Chordal Sparsity for Lipschitz Constant Estimation of Deep Neural Networks](https://mlsanity.com/paper/2204.00846/) (2022)
- [On the Tightness of Semidefinite Relaxations for Certifying Robustness to Adversarial Examples](https://mlsanity.com/paper/2006.06759/) (2020)

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

- [CTBENCH: A Library and Benchmark for Certified Training](https://mlsanity.com/paper/2406.04848/) (2024)

## Abstract (arXiv)

The neural network has become an integral part of modern software systems. However, they still suffer from various problems, in particular, vulnerability to adversarial attacks. In this work, we present a novel program reasoning framework for neural-network verification, which we refer to as symbolic reasoning. The key components of our framework are the use of the symbolic domain and the quadratic relation. The symbolic domain has very flexible semantics, and the quadratic relation is quite expressive. They allow us to encode many verification problems for neural networks as quadratic programs. Our scheme then relaxes the quadratic programs to semidefinite programs, which can be efficiently solved. This framework allows us to verify various neural-network properties under different scenarios, especially those that appear challenging for non-symbolic domains. Moreover, it introduces new representations and perspectives for the verification tasks. We believe that our framework can bring new theoretical insights and practical tools to verification problems for neural networks.