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 →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
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.
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
- 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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)
- [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)
- [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.
- [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.
- [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.
- [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.
- [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
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
free parameters (3)
- c_sp =
e.g., ln(2)^2 in Section V-A
- c_tanh =
e.g., 1 in Section V-A
- k =
user-specified nonnegative integer in (49)
assumptions (6)
- domain assumption Assumption 1: continuous selection f^V_lambda exists so V(zeta(x)) is a continuous function of x
- domain assumption Assumption 2: Q is closed and contains the origin in its interior
- domain assumption Assumption 3: continuous selection for q, analogous to Assumption 1
- domain assumption REN well-posedness and Lipschitz continuity
- domain assumption Exact or over-approximating semialgebraic graph representations for all activation functions
- standard math Standard SOS and Positivstellensatz background
invented entities (2)
-
lambda_sp(x) = x/2 + sqrt(c_sp + (x/2)^2)
independent evidence
-
lambda_tanh(x) = c_tanh x / sqrt(1 + (c_tanh x)^2)
independent evidence
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.
Forward citations
Cited by 1 Pith paper
-
Synthesis and SOS-based Stability Verification of a Neural-Network-Based Controller for a Two-wheeled Inverted Pendulum
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
-
[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
2021
-
[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
1980
-
[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
1992
-
[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
2019
-
[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
arXiv 2024
-
[4]
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
work page 2021
-
[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
work page 2003
-
[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
work page 1999
Show all 31 references
-
[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
2022
-
[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
2020
-
[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
2022
-
[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
2023
-
[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
2016
-
[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
2023
-
[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
2020
-
[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
2022
-
[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
2017
-
[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
2024
-
[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
2021
-
[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
2003
-
[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
2020 arXiv
-
[22]
J. B. Rawlings, D. Q. Mayne, and M. Diehl, Model predictive control: Theory, Computation, and Design. Madison, WI: Nob Hill Publishing, 2017
2017
-
[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
1960
-
[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
2017
-
[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
2014
-
[26]
H. K. Khalil, Nonlinear Systems . Upper Saddle River, NJ: Pearson, 1996
1996
-
[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
2021 arXiv
-
[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
2023
-
[29]
Adam: A method for stochastic optimization,
D. P. Kingma and J. Ba, “Adam: A method for stochastic optimization,”
-
[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...
2005
-
[2017]
Available: https://arxiv.org/abs/1412.6980
[Online]. Available: https://arxiv.org/abs/1412.6980
Reviewed August 6, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.