# Verification of Non-Linear Specifications for Neural Networks

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

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Feb 2019.

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

- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [HardNet: Hard-Constrained Neural Networks with Universal Approximation Guarantees](https://mlsanity.com/paper/2410.10807/) (2024)
- [Verification of Neural Networks' Global Robustness](https://mlsanity.com/paper/2402.19322/) (2024)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [Verified Safe Reinforcement Learning for Neural Network Dynamic Models](https://mlsanity.com/paper/2405.15994/) (2024)
- [Ensuring DNN Solution Feasibility for Optimization Problems with Convex Constraints and Its Application to DC Optimal Power Flow Problems](https://mlsanity.com/paper/2112.08091/) (2021)
- [Relational DNN Verification With Cross Executional Bound Refinement](https://mlsanity.com/paper/2405.10143/) (2024)
- [Learning Neural Networks under Input-Output Specifications](https://mlsanity.com/paper/2202.11246/) (2022)
- [A Primer on Multi-Neuron Relaxation-based Adversarial Robustness Certification](https://mlsanity.com/paper/2106.03099/) (2021)
- [Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization](https://mlsanity.com/paper/2405.17049/) (2024)
- [Parabolic Relaxation for Quadratically-constrained Quadratic Programming -- Part II: Theoretical & Computational Results](https://mlsanity.com/paper/2208.03625/) (2022)
- [Verification of Neural Networks Local Differential Classification Privacy](https://mlsanity.com/paper/2310.20299/) (2023)
- [A Scalable Approach for Safe and Robust Learning via Lipschitz-Constrained Networks](https://mlsanity.com/paper/2506.23977/) (2025)

## Abstract (arXiv)

Prior work on neural network verification has focused on specifications that are linear functions of the output of the network, e.g., invariance of the classifier output under adversarial perturbations of the input. In this paper, we extend verification algorithms to be able to certify richer properties of neural networks. To do this we introduce the class of convex-relaxable specifications, which constitute nonlinear specifications that can be verified using a convex relaxation. We show that a number of important properties of interest can be modeled within this class, including conservation of energy in a learned dynamics model of a physical system; semantic consistency of a classifier's output labels under adversarial perturbations and bounding errors in a system that predicts the summation of handwritten digits. Our experimental evaluation shows that our method is able to effectively verify these specifications. Moreover, our evaluation exposes the failure modes in models which cannot be verified to satisfy these specifications. Thus, emphasizing the importance of training models not just to fit training data but also to be consistent with specifications.