aiqbench analysis
This research advances the formal verification of neural networks by introducing a method to construct verified quadratic characterizations that reduce conservatism in reachability analysis. By leveraging sum-of-squares certificates and exploiting neuron dependencies, the framework offers tighter bounds for both smooth activations like tanh and ReLU networks compared to generic analytical descriptions. This work directly enhances safety-critical applications where precise uncertainty quantification is essential for feedforward architectures.
Quadratic Characterizations for Reachability Analysis of Neural Networks
arXiv:2605.20482v2 Announce Type: replace Abstract: 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.
Abstract: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.
Machine Learning (cs.LG); Systems and Control (eess.SY)
arXiv:2605.20482 [cs.LG]
(or arXiv:2605.20482v2 [cs.LG] for this version)
https://doi.org/10.48550/arXiv.2605.20482 Focus to learn more arXiv-issued DOI via DataCite
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 308 words
Related coverage
Scaling Laws and Spectra of Shallow Neural Networks in the Feature Learning Regime
arXiv · Jun 6, 2026
Scaling Laws and Spectra of Shallow Neural Networks in the Feature Learning Regime
arXiv · Aug 7, 2026

PIRAMID: Progress and Plans
LessWrong · Jul 27, 2026

Exploding variance of means of exponentials: least-squares to the rescue – Machine Learning Research Blog
francisbach.com · Sep 27, 2026