# VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 31 references that are in the map.
- First posted on arXiv 15 Dec 2023.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Adversarial examples in the physical world](https://mlsanity.com/paper/1607.02533/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Defensive Quantization: When Efficiency Meets Robustness](https://mlsanity.com/paper/1904.08444/) (2019)
- [Counterfactuals and Causability in Explainable Artificial Intelligence: Theory, Algorithms, and Applications](https://mlsanity.com/paper/2103.04244/) (2021)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [Unlocking Deterministic Robustness Certification on ImageNet](https://mlsanity.com/paper/2301.12549/) (2023)
- [Architecture-Preserving Provable Repair of Deep Neural Networks](https://mlsanity.com/paper/2304.03496/) (2023)
- [Verification of Neural Networks: Enhancing Scalability through Pruning](https://mlsanity.com/paper/2003.07636/) (2020)

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

- [Formal Local Implication Between Two Neural Networks](https://mlsanity.com/paper/2409.16726/) (2024)
- [Learning Robust Satellite Attitude Dynamics with Physics-Informed Normalising Flow](https://mlsanity.com/paper/2508.07841/) (2025)

## Abstract (arXiv)

Machine learning techniques often lack formal correctness guarantees, evidenced by the widespread adversarial examples that plague most deep-learning applications. This lack of formal guarantees resulted in several research efforts that aim at verifying Deep Neural Networks (DNNs), with a particular focus on safety-critical applications. However, formal verification techniques still face major scalability and precision challenges. The over-approximation introduced during the formal verification process to tackle the scalability challenge often results in inconclusive analysis. To address this challenge, we propose a novel framework to generate Verification-Friendly Neural Networks (VNNs). We present a post-training optimization framework to achieve a balance between preserving prediction performance and verification-friendliness. Our proposed framework results in VNNs that are comparable to the original DNNs in terms of prediction performance, while amenable to formal verification techniques. This essentially enables us to establish robustness for more VNNs than their DNN counterparts, in a time-efficient manner.
