# Quadratic Characterizations for Reachability Analysis of Neural Networks

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 25 references that are in the map.
- First posted on arXiv 19 May 2026.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Stability Analysis using Quadratic Constraints for Systems with Neural Network Controllers](https://mlsanity.com/paper/2006.07579/) (2020)
- [A Complete Set of Quadratic Constraints for Repeated ReLU and Generalizations](https://mlsanity.com/paper/2407.06888/) (2024)
- [Adversarial Reinforcement Learning for Robust Control of Fixed-Wing Aircraft under Model Uncertainty](https://mlsanity.com/paper/2510.16650/) (2025)

## Abstract (arXiv)

Quadratic constraints (QCs) are widely used to characterize nonlinearities and uncertainties, but generic analytical characterizations can be conservative on bounded domains. This paper develops a framework for constructing verified quadratic characterizations of scalar relations in the two-dimensional real plane. Candidate quadratic inequalities are locally generated by solving convex quadratic programs using samples from the relation and exterior sample points. They are then verified globally using sum-of-squares certificates over an exact semialgebraic description or, in the case of nonpolynomial relations, over relaxed polynomial descriptions. The resulting verified constraints define a sound overapproximation of the scalar relations over the considered domains. These constraints are directly compatible with existing analysis frameworks based on QCs and pointwise integral quadratic constraints (IQCs) for static nonlinearities and uncertainties, and they can also be embedded in QC-based semidefinite programs for reachability and safety analysis of feedforward neural networks. For smooth activations such as tanh, the method yields domain-dependent quadratic characterizations that constitute an alternative to generic sector- or slope-based descriptions. For ReLU networks, we give methods to reduce conservatism in QC-based reachability analysis of feedforward networks by exploiting dependencies between neurons and tighter local bounds. Numerical examples demonstrate improved reachability results for smooth activations, reduced conservatism for ReLU networks, and applicability beyond neural networks through an example involving saturation.