Pith. sign in

REVIEW 1 major objections 5 minor 1 cited by

Improved Sum-of-Squares Stability Verification of Neural-Network-Based Controllers

T0 review · 1 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Pith's one-line read A single sum-of-squares program can certify local asymptotic stability of a neural-network-controlled system and simultaneously produce an invariant set inside its region of attraction.

desk verdict Solid, honest extension of SOS verification for NN controllers; the new Lemma 4.1 and sequential RoA algorithm are the real contributions, and the REN gap is presentation-level rather than fatal. read the letter →

arxiv 2507.10352 v1 pith:U6NPZKY7 submitted 2025-07-14 eess.SY cs.SY

classification eess.SYcs.SY MSC 93D3093D0590C2293C5568T07
keywords sum-of-squaresprogrammingsemialgebraicsetsneuralnetworkcontrollersLyapunovstabilityregionofattractionrecurrentequilibriumnetworkssemidefinitediscrete-timebarrierfunctions
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper is trying to make sum-of-squares verification of neural-network controllers deliver more, with less manual work. It claims that a single semidefinite program can certify that a nonlinear closed loop is locally asymptotically stable and return an explicit invariant set inside its region of attraction, removing the separate sublevel-set search used in earlier work. It also widens the class of certifiable controllers to recurrent equilibrium networks and to smooth semialgebraic activations that mimic softplus and tanh. If the claim is right, stability certificates for trained recurrent or smooth-activation controllers become a direct output of one optimization, including a concrete region of guaranteed convergence.

What carries the argument

The load-bearing mechanism is Lemma 4.1, the strict-minimum-at-the-origin lemma: for a closed invariant set $X$ with $0 \in X$, any continuous nonnegative $V$ with $V(x)-V(x^+) \ge \|x\|^2$ on $X$ has $\arg\min V = \{0\}$, so $V$ is a valid Lyapunov function on $X$. Around this lemma, the machinery is the semialgebraic graph description of the network: lifting variables $\lambda$ plus polynomial equalities and inequalities describe the controller and the composed loop exactly, and SOS multipliers turn Lyapunov and invariance conditions into semidefinite constraints. Invariance of $Q$ is enforced by a discrete-time barrier-function constraint $q(x^+) \ge 0$ with fixed SOS multipliers, and the two-step alternating SDPs make the certified set $Q$ non-decreasing along the iteration.

What would settle it

A concrete test is to rerun the paper's counterexample system $x^+ = 2x$ with $Q = \{x : x^2 \le \frac14\}$ through optimization problem (50): the old SDP (15) admitted a spurious Lyapunov function there, so a feasible solution to (50) for that unstable closed loop would directly contradict Theorem 4.3, while infeasibility would confirm the new constraints close the gap.

Watch

Extended reading notes

Core claim

The paper's central claim is Theorem 4.3: under continuity assumptions on the lifting variables and local boundedness of the closed loop, any solution of optimization problem (50) certifies that the closed-loop system is locally asymptotically stable and that the set $Q$ defined by $q(x) = \alpha - \sigma_q(x)$ lies inside the region of attraction. The enabling result is Lemma 4.1, which shows that on a closed invariant set containing the origin, a continuous, nonnegative function $V$ satisfying $V(x) - V(x^+) \ge \|x\|^2$ must have its strict minimum at the origin; therefore the decrease condition alone makes $V$ a genuine Lyapunov function. From this, the paper derives two local-stability formulations: an explicit candidate-Lyapunov parameterization larger than previous classes, and a sequential algorithm that grows an invariant RoA estimate monotonically without prior knowledge of the system.

Load-bearing premise

The whole argument hinges on the assumption that the network's hidden variables can be chosen to vary continuously with the state; for recurrent equilibrium networks the paper assumes this follows from well-posedness and Lipschitz continuity, but it does not prove the continuous-selection step.

Editorial extensions

If this is right

  • Solving optimization problem (50) directly yields both a Lyapunov function and an invariant set $Q$ certified inside the region of attraction, so the second sublevel-set SDP of earlier frameworks becomes unnecessary.
  • Algorithm 1 produces a sequence of invariant sets $Q_A$ that never shrink, giving a systematic, heuristic-free way to enlarge an RoA estimate starting from a small initial guess.
  • Controllers built with the new semialgebraic softplus-like and tanh-like activations, including recurrent equilibrium networks and recurrent neural networks, fall within the same certification framework as ReLU feedforward networks.
  • In the MPC imitation example, the certified RoA includes points outside the MPC controller's feasible set, so the certificate can establish convergence beyond the region the controller was trained or designed for.
  • The explicit candidate-Lyapunov parameterization (41) guarantees, under Assumption 2, that any feasible $V$ already admits a sublevel set inside $Q$, directly proving local asymptotic stability and existence of a nontrivial RoA estimate.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A testable next step is to use the semialgebraic surrogates to over-approximate pretrained tanh and softplus networks, then run the same SDP; success would certify already-deployed smooth controllers, not only controllers synthesized with the surrogate activations.
  • The continuity requirement on the lifting variables is worth stress-testing: for a REN with a well-posed but only piecewise-continuous fixed-point map, the SDP may certify a set description that does not match the actual controller, so uniqueness and continuity should be checked before trusting the certificate.
  • The monotone growth of the certified sets is an ideal guarantee; the numerical example reports the final SDP infeasible at solver tolerance, suggesting practical termination may stop short of the maximal verifiable RoA, and tolerance-aware stopping rules are a natural refinement.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. The paper extends an existing sum-of-squares (SOS) framework for stability verification of discrete-time systems controlled by neural networks. It introduces two semialgebraic activation functions that mimic softplus and tanh, claims compatibility of the framework with Recurrent Equilibrium Networks (RENs), provides an alternative stability proof (Lemma 4.1), and proposes two ways to improve local stability analysis: an explicit parameterization of candidate Lyapunov functions and a combined optimization problem (50) that certifies local asymptotic stability and gives an invariant subset of the region of attraction. Two numerical examples illustrate the proposed techniques.

Significance. If the gaps identified below are closed, the paper would make a useful contribution to SOS-based verification of neural-network controllers. Lemma 4.1 is correct and conceptually clean: it gives a precise condition under which a positive semidefinite continuous Lyapunov candidate has a strict minimum at the origin, thereby justifying the elimination of the separate sublevel-set step. The proposed semialgebraic activations are simple, exact descriptions of smooth activation-like functions, and the one-shot certificate in Theorem 4.3 is a genuine algorithmic improvement over the two-step procedure in prior work. The theoretical results are parameter-free and the numerical examples are plausible, although no code or data is provided for independent verification.

major comments (1)
  1. [Section IV-C, Algorithm 1, problem B (54)] Problem B does not explicitly re-impose Assumption 3 on the updated sigma_q. The feasibility argument for constraint (53) shows sigma_q(zeta(x)) <= sigma_q^A(zeta(x)) on Q_A and, with nonnegativity, sigma_q(0)=0, but it does not ensure that the new sigma_q satisfies the continuity condition in Assumption 3. If the updated sigma_q is allowed to depend on lifting variables or controller outputs for which no continuous selection f_q^lambda exists, then q may cease to be a continuous function of x and Theorem 4.3 no longer applies to the set returned by the algorithm. The algorithm should either keep sigma_q within a parameterization that explicitly satisfies Assumption 3 or prove that constraint (53) preserves that property.
minor comments (5)
  1. [Theorem 3.1] The theorem statement says solutions "can be expressed via a set as in (4)", but the proof only establishes that every solution lies in the constructed set, not the converse inclusion. A one-sided containment is sufficient for the SDP soundness argument, but the wording should be clarified.
  2. [Equation (53) and (54b)] In optimization problem B, sigma_B is used as a vector of SOS polynomials in (53), but (54b) states "sigma_B, sigma_q SOS polynomial" in the singular. Please clarify that sigma_B is a vector of SOS multipliers and state the componentwise interpretation.
  3. [Section IV-B, equations (42)-(43)] The notation in the products over subsets I and J is not introduced. Define g_I(zeta) = prod_{i in I} g_i(zeta) and make explicit that the union runs over nonempty subsets of I_0 and all subsets of the complement.
  4. [Lemma 4.1] In the proof, the sentence "This directly implies V(0) < ||x||^2 <= V(x) for all x in X2" is slightly confusing because V(0) < ||x||^2 is exactly the definition of X2. Rephrase to avoid the impression that it follows from the decrease condition.
  5. [Section VI] The conclusion says "two new optimization problems", but Section IV-B introduces a new parameterization of candidate Lyapunov functions within the existing SDP (15), not a distinct optimization problem. Consider rewording to "a new parameterization and a new optimization problem".

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the stability certificates are produced by SDP searches rather than fitted to data, and the central theorems are proven in-paper from explicit assumptions.

full rationale

The paper's derivation chain is self-contained and does not reduce any load-bearing result to its own inputs. Theorem 4.3 is proven directly from Lemma 4.1, and Lemma 4.1 is proven in the paper from the stated decrease and nonnegativity conditions together with closedness and invariance; it does not import an external uniqueness or Lyapunov theorem from the authors' prior work. The SDP constraints (14), (49), and (53) are certificate-search conditions: the optimization variables are SOS multipliers, Lyapunov candidates, and barrier functions, not parameters fitted to a target output. No quantity is fitted to a subset of data and then renamed a prediction. The new semialgebraic activation functions are explicitly defined by (20) and (21), and their set descriptions (22) and (23) are exact algebraic identities, not assumptions smuggled in by citation. The REN compatibility argument of Theorem 3.1 is constructive, and the cited well-posedness/Lipschitz condition from Revay et al. is an external hypothesis about the network, not an equivalent restatement of the stability conclusion. The monotonicity of Algorithm 1 is shown from constraint (53), not assumed. The main weakness is that Assumption 1 is asserted for REN implicit branches rather than proved, and problem B does not explicitly re-state Assumption 3; however, this is a rigor or soundness gap, not a circular reduction, because the offending assumption is not shown to be equivalent to the theorem's conclusion. Therefore the circularity score is 0.

Assumptions & free parameters 3 free parameters · 6 assumptions · 2 invented entities

The central claims rest on standard SOS/Positivstellensatz math, on the semialgebraic graph descriptions being exact or over-approximating, and on continuity assumptions (Assumptions 1-3). The activation scale constants are user choices. No hidden entities are introduced beyond the explicitly defined activation functions.

free parameters (3)
  • c_sp = e.g., ln(2)^2 in Section V-A
    Scale parameter of the softplus-mimic activation lambda_sp; sets the curvature and the gap between the asymptotes. Chosen by hand for the numerical examples.
  • c_tanh = e.g., 1 in Section V-A
    Scale parameter of the tanh-mimic activation lambda_tanh; sets the slope at the origin and the approach to saturation. Chosen by hand.
  • k = user-specified nonnegative integer in (49)
    Exponent on the fixed SOS multiplier in the discrete barrier constraint; affects conservatism of the invariance certificate.
assumptions (6)
  • domain assumption Assumption 1: continuous selection f^V_lambda exists so V(zeta(x)) is a continuous function of x
    Invoked in Section II-B and used in Theorems 4.2 and 4.3. Needed to interpret V as a Lyapunov function on the state space.
  • domain assumption Assumption 2: Q is closed and contains the origin in its interior
    Required for well-posedness of local stability SDPs (Section II-C).
  • domain assumption Assumption 3: continuous selection for q, analogous to Assumption 1
    Used in Theorem 4.3 so that Q defined by (48) is a closed set containing the origin.
  • domain assumption REN well-posedness and Lipschitz continuity
    Section III-B relies on [21] to ensure a unique output of the implicit network so the semialgebraic set represents the actual network.
  • domain assumption Exact or over-approximating semialgebraic graph representations for all activation functions
    Needed for the set descriptions Kphi and KL in (6)-(7) to capture the true network input-output relation.
  • standard math Standard SOS and Positivstellensatz background
    Used to convert nonnegativity constraints into SOS constraints in the SDPs, following Parrilo [20].
invented entities (2)
  • lambda_sp(x) = x/2 + sqrt(c_sp + (x/2)^2) independent evidence
    purpose: A semialgebraic, smooth, monotone activation function mimicking softplus, enabling exact set descriptions for SOS verification.
    Explicitly defined by (20) and its graph by (22). Its properties are checkable; no hidden postulate.
  • lambda_tanh(x) = c_tanh x / sqrt(1 + (c_tanh x)^2) independent evidence
    purpose: A semialgebraic, smooth, odd, bounded activation function mimicking tanh.
    Explicitly defined by (21) and its graph by (23). Fully specified.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Improved Sum-of-Squares Stability Verification of Neural-Network-Based Controllers." pith.science (2026). https://pith.science/paper/U6NPZKY7

@misc{pith2026250710352,
  author       = {Pith},
  title        = {Pith review of: Improved Sum-of-Squares Stability Verification of Neural-Network-Based Controllers},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/U6NPZKY7}},
  note         = {Machine review of arXiv:2507.10352}
}
read the original abstract

This work presents several improvements to the closed-loop stability verification framework using semialgebraic sets and convex semidefinite programming to examine neural-network-based control systems regulating nonlinear dynamical systems. First, the utility of the framework is greatly expanded: two semialgebraic functions mimicking common, smooth activation functions are presented and compatibility with control systems incorporating Recurrent Equilibrium Networks (RENs) and thereby Recurrent Neural Networks (RNNs) is established. Second, the validity of the framework's state-of-the-art stability analyses is established via an alternate proof. Third, based on this proof, two new optimization problems simplifying the analysis of local stability properties are presented. To simplify the analysis of a closed-loop system's Region of Attraction (RoA), the first problem explicitly parameterizes a class of candidate Lyapunov functions larger than in previous works. The second problem utilizes the unique guarantees available under the condition of invariance to further expand the set of candidate Lyapunov functions and directly determine whether an invariant set forms part of the system's RoA. These contributions are successfully demonstrated in two numerical examples and suggestions for future research are provided.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Synthesis and SOS-based Stability Verification of a Neural-Network-Based Controller for a Two-wheeled Inverted Pendulum

    eess.SY 2025-08 conditional novelty 6.0 of 10

    A neural network controller mimicking a tube-based MPC is certified locally asymptotically stable by SOS programming and outperforms an LQR on a physical inverted pendulum.

Reference graph

Works this paper leans on

31 extracted references · 15 canonical work pages · cited by 1 Pith paper

  1. [13]

    Linear systems with neural network nonlinearities: Improved stability analysis via acausal zames-falb multipliers,

    P. Pauli, D. Gramlich, J. Berberich, and F. Allgower, “Linear systems with neural network nonlinearities: Improved stability analysis via acausal zames-falb multipliers,” in 2021 60th IEEE Conference on Decision and Control (CDC) , Austin, TX, USA, Feb. 2022, pp. 3611– 3618

  2. [14]

    Stability analysis using quadratic con- straints for systems with neural network controllers,

    H. Yin, P. Seiler, and M. Arcak, “Stability analysis using quadratic con- straints for systems with neural network controllers,” IEEE Transactions on Automatic Control , vol. 67, pp. 1980–1987, Apr. 2022

  3. [1]

    Neural networks for control systems—a survey,

    K. J. Hunt, D. Sbarbaro, R. ˙Zbikowski, and P. J. Gawthrop, “Neural networks for control systems—a survey,” Automatica (Oxf.) , vol. 28, no. 6, pp. 1083–1112, Nov. 1992

  4. [2]

    Universal function approximation by deep neural nets with bounded width and ReLU activations,

    B. Hanin, “Universal function approximation by deep neural nets with bounded width and ReLU activations,” Mathematics, vol. 7, no. 10, p. 992, Oct. 2019

  5. [3]

    Neural networks for fast optimisation in model predictive control: A review,

    C. Gonzalez, H. Asadi, L. Kooijman, and C. P. Lim, “Neural networks for fast optimisation in model predictive control: A review,” arXiv preprint, 2024. [Online]. Available: https://arxiv.org/abs/2309.02668

  6. [4]

    Neural networks for control: A tutorial and survey of stability-analysis methods, properties, and discussions,

    G. Norris, G. Ducard, and C. Onder, “Neural networks for control: A tutorial and survey of stability-analysis methods, properties, and discussions,” in 2021 International Conference on Electrical, Computer, Communications and Mechatronics Engineering (ICECCME) , Mauri- tius, Mauritius, Oct. 2021, pp. 1–6

  7. [5]

    Liberzon, Switching in systems and control , ser

    D. Liberzon, Switching in systems and control , ser. Systems & Control: Foundations & Applications. New York, NY: Springer, 2003

  8. [6]

    Complexity of stability and control- lability of elementary hybrid systems,

    V . D. Blondel and J. N. Tsitsiklis, “Complexity of stability and control- lability of elementary hybrid systems,” Automatica (Oxf.), vol. 35, pp. 479–489, Mar. 1999

Show all 31 references
  1. [7]

    Stability and performance verification of dynamical systems controlled by neural networks: Algorithms and complexity,

    M. Korda, “Stability and performance verification of dynamical systems controlled by neural networks: Algorithms and complexity,” IEEE Con- trol Systems Letters , vol. 6, pp. 3265–3270, June 2022

  2. [8]

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

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

  3. [9]

    A comparison of verification methods for neural-network controllers using mixed-integer programs,

    M. Dubach and G. Ducard, “A comparison of verification methods for neural-network controllers using mixed-integer programs,” in 2022 7th International Conference on Robotics and Automation Engineering (ICRAE), Singapore, Nov. 2022, pp. 43–48

  4. [10]

    Strengthened circle and Popov criteria for the stability analysis of feedback systems with ReLU neural networks,

    C. R. Richardson, M. C. Turner, and S. R. Gunn, “Strengthened circle and Popov criteria for the stability analysis of feedback systems with ReLU neural networks,” IEEE Control Systems Letters, vol. 7, pp. 2635– 2640, June 2023

  5. [11]

    Stability analysis of model predictive controllers using mixed integer linear programming,

    D. Simon and J. Lofberg, “Stability analysis of model predictive controllers using mixed integer linear programming,” in 2016 IEEE 55th Conference on Decision and Control (CDC), Las Vegas, NV , USA, Dec. 2016, pp. 7270–7275

  6. [12]

    Stability verification of neural network controllers using mixed-integer programming,

    R. Schwan, C. N. Jones, and D. Kuhn, “Stability verification of neural network controllers using mixed-integer programming,” IEEE Transac- tions on Automatic Control , vol. 68, pp. 7514–7529, June 2023

  7. [15]

    A convex parameterization of robust recurrent neural networks,

    M. Revay, R. Wang, and I. R. Manchester, “A convex parameterization of robust recurrent neural networks,” IEEE Control Systems Letters, vol. 5, pp. 1363–1368, Nov. 2020

  8. [16]

    Stability of non-linear neural feedback loops using sum of squares,

    M. Newton and A. Papachristodoulou, “Stability of non-linear neural feedback loops using sum of squares,” in 2022 IEEE 61st Conference on Decision and Control (CDC), Cancun, Mexico, Dec. 2022, pp. 6000– 6005

  9. [17]

    Stability and performance verification of optimization-based controllers,

    M. Korda and C. N. Jones, “Stability and performance verification of optimization-based controllers,” Automatica (Oxf.), vol. 78, pp. 34–45, Jan. 2017

  10. [18]

    Recurrent equilibrium networks: Flexible dynamic models with guaranteed stability and robust- ness,

    M. Revay, R. Wang, and I. R. Manchester, “Recurrent equilibrium networks: Flexible dynamic models with guaranteed stability and robust- ness,” IEEE Transactions on Automatic Control, vol. 69, pp. 2855–2870, May 2024

  11. [19]

    Neural network verification using polynomial optimisation,

    M. Newton and A. Papachristodoulou, “Neural network verification using polynomial optimisation,” in 2021 60th IEEE Conference on Decision and Control (CDC) , Austin, TX, USA, Dec. 2021, pp. 5092– 5097

  12. [20]

    Semidefinite programming relaxations for semialgebraic problems,

    P. A. Parrilo, “Semidefinite programming relaxations for semialgebraic problems,” Mathematical Programming , vol. 96, pp. 293–320, May 2003

  13. [21]

    Lipschitz bounded equilibrium networks,

    M. Revay, R. Wang, and I. R. Manchester, “Lipschitz bounded equilibrium networks,” arXiv, 2020. [Online]. Available: https: //arxiv.org/abs/2010.01732

  14. [22]

    J. B. Rawlings, D. Q. Mayne, and M. Diehl, Model predictive control: Theory, Computation, and Design. Madison, WI: Nob Hill Publishing, 2017

  15. [23]

    Control system analysis and design via the ’second method’ of Lyapunov,

    R. E. Kalman and J. E. Bertram, “Control system analysis and design via the ’second method’ of Lyapunov,” J. Basic Eng., vol. 82, pp. 371–393, June 1960

  16. [24]

    Discrete control barrier functions for safety-critical control of discrete systems with application to bipedal robot navigation,

    A. Agrawal and K. Sreenath, “Discrete control barrier functions for safety-critical control of discrete systems with application to bipedal robot navigation,” in Proceedings of Robotics: Science and Systems , Cambridge, Massachusetts, July 2017

  17. [25]

    Region of attraction analysis via invariant sets,

    G. Valmorbida and J. Anderson, “Region of attraction analysis via invariant sets,” in 2014 American Control Conference, Portland, Oregon, USA, June 2014

  18. [26]

    H. K. Khalil, Nonlinear Systems . Upper Saddle River, NJ: Pearson, 1996

  19. [27]

    Papachristodoulou, J

    A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, P. A. Parrilo, M. M. Peet, and D. Jagt, SOSTOOLS: Sum of squares optimization toolbox for MATLAB, http://arxiv.org/abs/1310.4716, 2021, available from https://github.com/oxfordcontrol/SOSTOOLS

  20. [28]

    MOSEK Optimization Toolbox for MATLAB - Release 10.0.47 , MOSEK ApS, MOSEK ApS, Fruebjergvej 3, Symbion Science Park, Box 16, 2100 Copenhagen O, Denmark, 2023

  21. [29]

    Adam: A method for stochastic optimization,

    D. P. Kingma and J. Ba, “Adam: A method for stochastic optimization,”

  22. [30]

    Invariant approximations of the minimal robust positively invariant set,

    S. V . Rakovic, E. C. Kerrigan, K. I. Kouramas, and D. Q. Mayne, “Invariant approximations of the minimal robust positively invariant set,” IEEE Transactions on Automatic Control , vol. 50, pp. 406–410, Mar. 2005. Alvaro Detailleur received the master’s degree in Robotics, Sys...

  23. [2017]

    Available: https://arxiv.org/abs/1412.6980

    [Online]. Available: https://arxiv.org/abs/1412.6980

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.