pith. sign in

arxiv: 2605.20482 · v1 · pith:EWKGMV5Snew · submitted 2026-05-19 · 💻 cs.LG · cs.SY· eess.SY

Quadratic Characterizations for Reachability Analysis of Neural Networks

Elias Khalife , Mazen Farhood , Pierre-Loic Garoche This is my paper

Pith reviewed 2026-05-21 07:02 UTC · model grok-4.3

classification 💻 cs.LG cs.SYeess.SY
keywords quadratic constraintsreachability analysisneural networkssum-of-squaressemidefinite programmingReLUtanhsafety verification
0
0 comments X

The pith

Verified quadratic inequalities from samples and sum-of-squares proofs yield tighter bounds for neural network reachability analysis.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper develops a method to create accurate quadratic descriptions of scalar relations over bounded domains, such as the input-output behavior of neural network activation functions. Candidate quadratic inequalities are first fitted locally by solving convex quadratic programs on sampled points from the relation and exterior points, then verified to hold globally using sum-of-squares certificates on exact semialgebraic sets or polynomial relaxations. When verified, the inequalities give sound overapproximations that plug directly into quadratic-constraint semidefinite programs, enabling reachability and safety analysis of feedforward networks. The resulting characterizations are less conservative than generic sector or slope bounds for tanh and allow exploitation of neuron dependencies to tighten bounds for ReLU networks.

Core claim

The authors develop a method to construct verified quadratic characterizations of scalar relations in the plane. They generate candidate quadratic inequalities locally via convex quadratic programs fitted to samples of the relation and exterior points, then verify them globally using sum-of-squares certificates on either exact semialgebraic sets or polynomial relaxations. These verified constraints form sound overapproximations that integrate directly into QC-based semidefinite programs for reachability and safety verification of feedforward neural networks, offering domain-specific improvements over generic bounds for activations like tanh and ReLU.

What carries the argument

The two-step construction of candidate quadratic inequalities via local convex quadratic programs on samples followed by global verification with sum-of-squares certificates over semialgebraic descriptions.

If this is right

  • For tanh activations, the method produces domain-dependent quadratic constraints that serve as alternatives to standard sector or slope bounds.
  • Exploiting dependencies between neurons in ReLU networks reduces conservatism in QC-based reachability analysis.
  • The verified constraints can be embedded in semidefinite programs to perform reachability and safety analysis of feedforward neural networks.
  • Numerical examples demonstrate improved reachability results for smooth activations and reduced conservatism for ReLU networks, with applicability to other nonlinearities such as saturation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same sample-plus-verification pipeline could be applied to nonlinearities in recurrent networks or hybrid dynamical systems to obtain tighter reachability sets.
  • Lower overapproximation error may allow certification of deeper or wider networks that remain out of reach with generic quadratic bounds.
  • The verified quadratic constraints could be combined with abstraction-refinement loops to further improve scalability of safety checks.

Load-bearing premise

The sum-of-squares certificates must succeed in proving that the candidate quadratic inequalities hold over the entire chosen domain for the given relations.

What would settle it

A concrete point inside the domain at which the scalar relation violates one of the generated quadratic inequalities, or a failure of the sum-of-squares solver to certify a valid inequality, would demonstrate that the overapproximation is unsound.

Figures

Figures reproduced from arXiv: 2605.20482 by Elias Khalife, Mazen Farhood, Pierre-Loic Garoche.

Figure 3
Figure 3. Figure 3: Output reachable sets in the (y1, y2) and (y3, y4) planes. On average, over all projection directions, the reachable-set widths obtained with the proposed characterization are approx￾imately 6.4% tighter than those of NNV and approximately 1.2% tighter than those of α, β-CROWN in this example. The bounds obtained with the proposed method were also independently verified using α, β-CROWN. This illustrates t… view at source ↗
Figure 1
Figure 1. Figure 1: Verified characterizations of tanh(⋅) (left) and sat(⋅) (right) [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Projections of the state-invariant ellipsoids and simulations in the [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops a framework to construct verified quadratic characterizations of scalar relations (e.g., activation functions) by generating candidate quadratic inequalities via sample-based convex QPs and certifying them globally with sum-of-squares (SOS) over exact semialgebraic sets or relaxed polynomial descriptions. The resulting sound overapproximations are embedded in QC-based SDPs for reachability and safety analysis of feedforward neural networks, with specific methods for tanh (domain-dependent alternatives to sector bounds) and ReLU (exploiting inter-neuron dependencies to reduce conservatism). Numerical examples illustrate improved results for both smooth activations and ReLU networks, plus an application to saturation.

Significance. If the SOS certificates close as claimed, the approach supplies a systematic, sound method for obtaining tighter, domain-specific quadratic constraints that integrate directly with existing QC and IQC frameworks. This addresses a known source of conservatism in NN reachability analysis. The explicit use of SOS for verification and the sample-to-certificate pipeline are strengths that support reproducibility and soundness; the ReLU dependency exploitation is a concrete advance over pointwise bounds.

major comments (2)
  1. [§4] §4 (SOS verification): the claim that SOS certificates over the exact semialgebraic description or relaxed polynomial description successfully verify the candidate quadratic inequalities globally is load-bearing for soundness, yet the manuscript provides no explicit degree bounds, monomial basis size, or failure cases for the reported domains; without these it is impossible to assess whether the certificates are non-vacuous or merely reproduce the sample-based candidates.
  2. [§5.2] §5.2 (ReLU dependency exploitation): the joint constraints used to reduce conservatism are described at a high level, but the manuscript does not show how the resulting quadratic matrix is assembled into the overall QC-SDP or whether the dependency encoding preserves the block-diagonal structure required by standard pointwise IQC solvers.
minor comments (2)
  1. [Abstract] The abstract states that the method applies 'beyond neural networks through an example involving saturation,' but the corresponding numerical example is only summarized; a brief statement of the saturation relation and the achieved tightness improvement would strengthen the generality claim.
  2. [§2] Notation for the quadratic form (e.g., the matrix P in the inequality x^T P x + 2 q^T x + r ≥ 0) is introduced without an explicit reference to the standard QC literature; adding one sentence linking to the usual (M, N) or (P, q, r) parametrization would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and constructive feedback on our manuscript. We appreciate the recognition of the framework's potential to reduce conservatism in neural network reachability analysis. Below, we provide point-by-point responses to the major comments.

read point-by-point responses

  1. Referee: [§4] §4 (SOS verification): the claim that SOS certificates over the exact semialgebraic description or relaxed polynomial description successfully verify the candidate quadratic inequalities globally is load-bearing for soundness, yet the manuscript provides no explicit degree bounds, monomial basis size, or failure cases for the reported domains; without these it is impossible to assess whether the certificates are non-vacuous or merely reproduce the sample-based candidates.

    Authors: We agree that the manuscript would benefit from more explicit details on the SOS verification process to allow readers to fully evaluate the soundness and non-vacuous nature of the certificates. In the revised manuscript, we will include tables or text specifying the SOS polynomial degrees (e.g., degree 4 for tanh over [-1,1] and degree 2 for ReLU), the monomial basis sizes for each case, and any failure cases encountered during certification along with how they were resolved (e.g., by increasing degree or adjusting the relaxation). This will clarify that the certificates provide global verification independent of the samples. revision: yes

  2. Referee: [§5.2] §5.2 (ReLU dependency exploitation): the joint constraints used to reduce conservatism are described at a high level, but the manuscript does not show how the resulting quadratic matrix is assembled into the overall QC-SDP or whether the dependency encoding preserves the block-diagonal structure required by standard pointwise IQC solvers.

    Authors: The description in §5.2 is indeed at a high level, and we will expand it in the revision. We will add an explicit example or derivation showing how the joint quadratic constraints are combined into the overall quadratic form matrix for the QC-SDP. Regarding the block-diagonal structure, the dependency encoding is designed to preserve it by incorporating cross terms in a way that the per-layer or per-neuron blocks remain diagonal in the sense required by pointwise IQC solvers; we will provide a proof sketch or reference to the structure preservation in the revised text to confirm compatibility with standard solvers. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper constructs candidate quadratic inequalities via sample-based convex QPs, then certifies them globally using sum-of-squares over exact or relaxed semialgebraic sets. Soundness follows directly from the external SOS certificate implying the inequality holds on the relation; the verification step is independent of the candidate generation and does not reduce to a fitted parameter or self-citation. No load-bearing step equates a derived result to its own input by construction, and the method relies on standard external convex optimization and SOS solvers rather than re-deriving its premises.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract-only review; ledger populated from stated steps. The method assumes convex QP solutions yield useful candidates and that SOS can certify them globally; no explicit free parameters or invented entities are named.

axioms (1)
  • domain assumption Sum-of-squares certificates over semialgebraic or relaxed polynomial descriptions can verify candidate quadratic inequalities globally.
    Invoked in the verification step described in the abstract.

pith-pipeline@v0.9.0 · 5775 in / 1274 out tokens · 26529 ms · 2026-05-21T07:02:43.354374+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages

  1. [1]

    System analysis via integral quadratic constraints,

    A. Megretski and A. Rantzer, “System analysis via integral quadratic constraints,”IEEE Transactions on Automatic Control, vol. 42, no. 6, pp. 819–830, 1997

    work page 1997

  2. [2]

    Robust stability and performance analysis based on integral quadratic constraints,

    J. Veenman, C. W. Scherer, and H. Köro ˘glu, “Robust stability and performance analysis based on integral quadratic constraints,”European Journal of Control, vol. 31, pp. 1–32, 2016

    work page 2016

  3. [3]

    Computa- tion of invariant sets for discrete-time uncertain systems,

    E. Khalife, D. Abou Jaoude, M. Farhood, and P.-L. Garoche, “Computa- tion of invariant sets for discrete-time uncertain systems,”International Journal of Robust and Nonlinear Control, vol. 33, no. 14, pp. 8452– 8474, 2023

    work page 2023

  4. [4]

    Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming,

    M. Fazlyab, M. Morari, and G. J. Pappas, “Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming,”IEEE Transactions on Automatic Control, vol. 67, no. 1, pp. 1–15, 2022

    work page 2022

  5. [5]

    Reach-SDP: Reach- ability analysis of closed-loop systems with neural network controllers via semidefinite programming,

    H. Hu, M. Fazlyab, M. Morari, and G. J. Pappas, “Reach-SDP: Reach- ability analysis of closed-loop systems with neural network controllers via semidefinite programming,” in2020 59th IEEE Conference on Decision and Control (CDC), 2020, pp. 5929–5934

    work page 2020

  6. [6]

    Robustness analysis of uncertain time-varying systems using integral quadratic constraints with time-varying multipliers,

    J. M. Fry, D. Abou Jaoude, and M. Farhood, “Robustness analysis of uncertain time-varying systems using integral quadratic constraints with time-varying multipliers,”International Journal of Robust and Nonlinear Control, vol. 31, no. 3, pp. 733–758, 2021

    work page 2021

  7. [7]

    Positive polynomials on compact semi-algebraic sets,

    M. Putinar, “Positive polynomials on compact semi-algebraic sets,” Indiana Univ. Mathematics Journal, vol. 42, no. 3, pp. 969–984, 1993

    work page 1993

  8. [8]

    Exploiting algebraic structure in sum of squares programs,

    P. A. Parrilo, “Exploiting algebraic structure in sum of squares programs,” inPositive Polynomials in Control, D. Henrion and A. Garulli, Eds. Springer Berlin Heidelberg, 2005, pp. 181–194

    work page 2005

  9. [9]

    Stability analysis using quadratic constraints for systems with neural network controllers,

    H. Yin, P. Seiler, and M. Arcak, “Stability analysis using quadratic constraints for systems with neural network controllers,”IEEE Trans- actions on Automatic Control, vol. 67, no. 4, pp. 1980–1987, 2022

    work page 1980

  10. [10]

    A complete set of quadratic constraints for repeated ReLU and generalizations,

    S. V . Noori, B. Hu, G. Dullerud, and P. Seiler, “A complete set of quadratic constraints for repeated ReLU and generalizations,”IEEE Transactions on Automatic Control, pp. 1–14, 2025

    work page 2025

  11. [11]

    Satisfiability modulo theories,

    C. Barrett and C. Tinelli, “Satisfiability modulo theories,” inHandbook of Model Checking. Springer Intl. Publishing, 2018, pp. 305–343

    work page 2018

  12. [12]

    Code-level formal verification of ellipsoidal invariant sets for linear parameter-varying systems,

    E. Khalife, P.-L. Garoche, and M. Farhood, “Code-level formal verification of ellipsoidal invariant sets for linear parameter-varying systems,” inNASA Formal Methods, K. Y . Rozier and S. Chaudhuri, Eds. Cham: Springer Nature Switzerland, 2023, pp. 157–173

    work page 2023

  13. [13]

    Formally proving invariant systemic properties of control programs using ghost code and integral quadratic constraints,

    ——, “Formally proving invariant systemic properties of control programs using ghost code and integral quadratic constraints,” inNASA Formal Methods, A. Dutle, L. Humphrey, and L. Titolo, Eds. Cham: Springer Nature Switzerland, 2025, pp. 180–200

    work page 2025

  14. [14]

    Bertot and P

    Y . Bertot and P. Castéran,Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, ser. Texts in Theoretical Computer Science. Springer Verlag, 2004

    work page 2004

  15. [15]

    J. C. Mason and D. C. Handscomb,Chebyshev Polynomials. Chapman and Hall/CRC, 2002

    work page 2002

  16. [16]

    S. Boyd, L. El Ghaoui, E. Feron, and V . Balakrishnan,Linear Matrix Inequalities in System and Control Theory. SIAM, 1994

    work page 1994

  17. [17]

    Restructuring of deep neural network acoustic models with singular value decomposition,

    J. Xue, J. Li, and Y . Gong, “Restructuring of deep neural network acoustic models with singular value decomposition,” inInterspeech, 2013, pp. 2365–2369

    work page 2013

  18. [18]

    Frama-C,

    P. Cuoq, F. Kirchner, N. Kosmatov, V . Prevosto, J. Signoles, and B. Yakobowski, “Frama-C,” inSoftware Engineering and Formal Methods. Springer Berlin Heidelberg, 2012, pp. 233–247

    work page 2012

  19. [19]

    Z3: An efficient smt solver,

    L. de Moura and N. Bjørner, “Z3: An efficient smt solver,” in TACAS’08/ETAPS’08. Springer Berlin Heidelberg, 2008, pp. 337–340

    work page 2008

  20. [20]

    A collaborative framework for non-linear integer arithmetic reasoning in Alt-Ergo,

    S. Conchon, M. Iguernelala, and A. Mebsout, “A collaborative framework for non-linear integer arithmetic reasoning in Alt-Ergo,” in2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. IEEE, 2013, pp. 161–168

    work page 2013

  21. [21]

    Adversarial reinforcement learning for robust control of fixed-wing aircraft under model uncertainty,

    D. J. Marquis, B. Wilhelm, D. Muniraj, and M. Farhood, “Adversarial reinforcement learning for robust control of fixed-wing aircraft under model uncertainty,” inProceedings of the 2026 American Control Conference, 2026, arXiv preprint arXiv:2510.16650

    work page arXiv 2026

  22. [22]

    NNV: The neural network verification tool for deep neural networks and learning-enabled cyber- physical systems,

    H.-D. Tran, X. Yang, D. Manzanas Lopez, P. Musau, L. V . Nguyen, W. Xiang, S. Bak, and T. T. Johnson, “NNV: The neural network verification tool for deep neural networks and learning-enabled cyber- physical systems,” inComputer Aided Verification, S. K. Lahiri and C. Wang, Eds. Springer International Publishing, 2020, pp. 3–17

    work page 2020

  23. [23]

    An introduction to CORA 2015,

    M. Althoff, “An introduction to CORA 2015,” inProceedings of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems. EasyChair, 2015, pp. 120–151

    work page 2015

  24. [24]

    Beta-Crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification,

    S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter, “Beta-Crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification,”Advances in Neural Information Processing Sys., vol. 34, pp. 29 909–29 921, 2021

    work page 2021

  25. [25]

    Policy compression for aircraft collision avoidance systems,

    K. D. Julian, J. Lopez, J. S. Brush, M. P. Owen, and M. J. Kochenderfer, “Policy compression for aircraft collision avoidance systems,” in2016 IEEE/AIAA 35th Digital Avionics Systems Conference, 2016, pp. 1–10

    work page 2016

  26. [26]

    Reluplex: An efficient smt solver for verifying deep neural networks,

    G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient smt solver for verifying deep neural networks,” inComputer Aided Verification, R. Majumdar and V . Kun ˇcak, Eds. Springer International Publishing, 2017, pp. 97–117

    work page 2017