# Relational DNN Verification With Cross Executional Bound Refinement

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 32 of its 48 references that are in the map.
- First posted on arXiv 16 May 2024.

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

- [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)
- [Convex optimization](https://mlsanity.com/paper/2106.01946/) (2021)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Universal adversarial perturbations](https://mlsanity.com/paper/1610.08401/) (2016)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Adversarial camera stickers: A physical camera-based attack on deep learning systems](https://mlsanity.com/paper/1904.00759/) (2019)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation](https://mlsanity.com/paper/2009.09943/) (2020)
- [Double Sampling Randomized Smoothing](https://mlsanity.com/paper/2206.07912/) (2022)
- [Fast Geometric Projections for Local Robustness Certification](https://mlsanity.com/paper/2002.04742/) (2020)
- [Adversarial Music: Real World Audio Adversary Against Wake-word Detection System](https://mlsanity.com/paper/1911.00126/) (2019)
- [BagFlip: A Certified Defense against Data Poisoning](https://mlsanity.com/paper/2205.13634/) (2022)
- [CertiFair: A Framework for Certified Global Fairness of Neural Networks](https://mlsanity.com/paper/2205.09927/) (2022)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [Verification of Non-Linear Specifications for Neural Networks](https://mlsanity.com/paper/1902.09592/) (2019)
- [Abstract Neural Networks](https://mlsanity.com/paper/2009.05660/) (2020)
- [DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers](https://mlsanity.com/paper/2103.01629/) (2021)

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

- [Revisiting Differential Verification: Equivalence Verification with Confidence](https://mlsanity.com/paper/2410.20207/) (2024)
- [Support is All You Need for Certified VAE Training](https://mlsanity.com/paper/2504.11831/) (2025)
- [Hybrid Robustness Verification for Spatio-Temporal Neural Networks](https://mlsanity.com/paper/2606.09746/) (2026)
- [Branch and Bound for Relational Verification of Neural Networks](https://mlsanity.com/paper/2608.13118/) (2026)
- [Exploring Solver-Level Warmstarting for Neural Network Verification](https://mlsanity.com/paper/2609.25962/) (2026)

## Abstract (arXiv)

We focus on verifying relational properties defined over deep neural networks (DNNs) such as robustness against universal adversarial perturbations (UAP), certified worst-case hamming distance for binary string classifications, etc. Precise verification of these properties requires reasoning about multiple executions of the same DNN. However, most of the existing works in DNN verification only handle properties defined over single executions and as a result, are imprecise for relational properties. Though few recent works for relational DNN verification, capture linear dependencies between the inputs of multiple executions, they do not leverage dependencies between the outputs of hidden layers producing imprecise results. We develop a scalable relational verifier RACoon that utilizes cross-execution dependencies at all layers of the DNN gaining substantial precision over SOTA baselines on a wide range of datasets, networks, and relational properties.