SEROAISE: Advancing ROA Estimation for ReLU and PWA Dynamics through Estimating Certified Invariant Sets

Hasan Poonawala; Pouya Samanipour

SEROAISE: Advancing ROA Estimation for ReLU and PWA Dynamics through Estimating Certified Invariant Sets

T0 review · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read SEROAISE estimates larger certified regions of attraction for PWA and ReLU dynamical systems by growing a certified invariant set via the NUGIS procedure and then solving a linear program for a Lyapunov-like function on that set.

desk verdict The NUGIS expansion idea is genuinely new, but the IISE certificate is not sound as written: the LP checks the barrier condition on the wrong partition, so the claimed RoA guarantees do not follow. read the letter →

arxiv 2504.12269 v1 pith:FZBTACT7 submitted 2025-04-16 eess.SY cs.SY

Pouya Samanipour , Hasan Poonawala This is my paper · ORCID

classification eess.SYcs.SY

keywords invariantcertifiedestimationiiseseroaiseconditionsderiveddynamics

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

To know whether a control system is safe, engineers need the region of attraction: the set of starting states that will eventually settle at the desired equilibrium. Computing this set exactly is hard, so methods compute guaranteed inner estimates. This paper works with systems whose dynamics are piecewise affine, including ReLU neural networks, which split the state space into linear regions.

The authors' approach, SEROAISE, has two steps. First, they find a large set of states that is forward invariant: if you start inside, you stay inside. They grow this set iteratively using a new rule called Non-Uniform Growth (NUGIS), which identifies boundary points where the dynamics push inward, and then they solve a linear program to expand the set around those points using barrier functions. Second, on this certified invariant set, they solve another linear program to find a Lyapunov-like function that strictly decreases along trajectories. If such a function exists on the invariant set, then every state in that set converges to the origin, so the set is an inner estimate of the region of attraction.

The paper reports larger estimates than two recent neural-network-based methods on three examples: path following, inverted pendulum, and cart-pole. However, the proof that the linear program actually certifies an invariant set has gaps. The constraints use a smaller slope for states outside the set, and some vertices that end up inside the set are still checked with that weaker slope, so the certificate may not be valid. The growth theorem also assumes away sliding behavior on cell boundaries, which is not stated in the theorem.

Extended reading notes

Core claim

The load-bearing claim is that the IISE algorithm produces certified invariant sets that grow monotonically and are systematically larger than those from the authors' prior work and from state-of-the-art methods, and that SEROAISE then certifies these sets as regions of attraction. The paper states: 'SEROAISE introduces a framework that finds a large RoA by identifying a large certified invariant subset and applying Lyapunov-like conditions to states inside this subset.' The certificate is grounded in optimization problem (35), where a barrier function h is found such that the barrier condition is satisfied at vertices, and in Remark 11, which asserts the solution is a certified invariant set when certain slack variables are zero.

Load-bearing premise

The LP certificate in Section 5.2 is valid only if the new barrier function's zero set aligns with the refined partition, so that checking the sign-dependent barrier constraint (35f)/(35g) at vertices is sufficient. The LP neither enforces this alignment nor reclassifies I_UC vertices after solving; a vertex that the solver places inside the set (h >= 0) is still checked with the alpha_m slope in (35g), which is weaker than the required alpha_0 slope. Additionally, Theorem 8's set-valued proof assumes 'absence of sliding behavior', a condition not stated in the theorem and not verified in examples. If the certificate is invalid, the claimed larger RoA estimates are not formally justified.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

This paper is worth a serious look, but not for the reason the authors hope. The NUGIS growth idea is genuinely new, and the IISE/SEROAISE pipeline—LP-based invariant set expansion plus a Lyapunov-like search restricted to that set—is a sensible engineering direction. The examples are nontrivial, the code is public, and the monotone growth plots are suggestive.

The soft spot is load-bearing. The certificate behind IISE does not go through as written. The LP in (35) checks the Leaky ReLU barrier condition only at vertices of a partition refined along the previous barrier function's zero set. But the new h solved at iteration m has its own zero set, which can cut through cell interiors. At those interior points the derivative condition uses the steeper alpha_0 slope when h is nonnegative and the flatter alpha_m slope when h is negative, but the LP assigns slopes by the vertex category from the previous iteration, not by the sign of the solved h. A vertex that was outside before but becomes inside after solving is still constrained with alpha_m in (35g), which is weaker than the required alpha_0. The stress-test note's 1D example is concrete and checks out: all vertex constraints are satisfied, yet the pointwise condition (7) fails at the new zero set. So Remark 11's claim that zero slack implies a certified invariant set is not established. Since every claimed RoA estimate inherits this gap, the central formal guarantee is missing.

There are smaller issues. Theorem 8's set-valued case assumes no sliding behavior without stating it in the theorem. The paper leans on the authors' own prior work for the initial invariant set and for Leaky ReLU feasibility, which is fine but should be clearly flagged. And the "systematically larger RoA" claim is demonstrated only by comparison to two baselines on three examples, not by a formal domination result.

The good news: the certificate gap looks fixable. A post-solve refinement that reclassifies vertices by the solved h's sign, or a formulation that enforces conditions across the new zero set, would likely close it. The NUGIS construction itself is independent and may be salvageable even if this particular LP needs patching.

Who is this for? Researchers working on LP/SOS-based invariant set computation for PWA/ReLU dynamics. It deserves a serious referee: the idea is new, the writing is mostly clear, and the flaw is a precise technical gap rather than a vague hand-wave. Send it to review, but be prepared to require the authors to fix the certificate or explicitly restrict the claims.

Assumptions & free parameters 6 free parameters · 5 assumptions · 0 invented entities

The method introduces no new physical entities. It does introduce the NUGIS growth rule and the IISE iteration, which are algorithmic constructs. The free parameters are tolerances and gains chosen by hand; the main assumptions are standard theorems, the bounded-polytope restriction, the no-sliding restriction in the NUGIS proof, and reliance on the authors' prior work for the initial invariant set and Leaky ReLU feasibility.

free parameters (6)

epsilon = 1e-4 in examples
Threshold in the NUGIS condition (11) and in the LP constraints; chosen small, not derived from data.
epsilon_1, epsilon_2, epsilon_3 = 1e-4 in examples
Tolerances in constraints (35a)-(35g) and (38); set by hand.
alpha_0 = not specified
Initial slope of the K-infinity function in (32); user-chosen.
gamma = not specified, < 1
Learning rate for updating alpha_m in (32); user-chosen, controls how quickly the barrier condition relaxes outside the invariant set.
Gamma = > 1
Penalty weight for non-UC slack variables in cost (34); user-chosen to prioritize certified slacks.
max_iter = not specified
Maximum iterations in Algorithm 1; termination relies on this when NUGIS condition remains true.

assumptions (5)

standard math LaSalle's theorem (Theorem 1) and Nagumo's theorem for forward invariance
Used to conclude asymptotic stability from a decreasing function on an invariant set and to verify forward invariance of constructed cells.
domain assumption Assumption 4: all cells are bounded polytopes and the vertex representation applies
Restricts the class of PWA dynamics; needed for the vertex-based LP formulations.
ad hoc to paper Absence of sliding behavior in set-valued vector fields for Theorem 8
Stated in the proof of the set-valued case (Section 4.2) but not in the theorem statement and not verified in the examples.
domain assumption Feasibility of Leaky ReLU as a K-infinity function is taken from [23, Theorem 1]
The update of alpha_m in (32) relies on the authors' prior result; not re-derived in this paper.
domain assumption The initial invariant set from [22] exists and is certified
Algorithm 1 requires a barrier function h(x,P0,alpha0) obtained using [22]; the guarantees of IISE inherit the validity of this starting point.

how reviews work

0 comments

Cite this review

Pith. "Pith review of SEROAISE: Advancing ROA Estimation for ReLU and PWA Dynamics through Estimating Certified Invariant Sets." pith.science (2026). https://pith.science/paper/FZBTACT7

@misc{pith2026250412269,
  author       = {Pith},
  title        = {Pith review of: SEROAISE: Advancing ROA Estimation for ReLU and PWA Dynamics through Estimating Certified Invariant Sets},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FZBTACT7}},
  note         = {Machine review of arXiv:2504.12269}
}

read the original abstract

This paper presents a novel framework for constructing the Region of Attraction (RoA) for dynamics derived either from Piecewise Affine (PWA) functions or from Neural Networks (NNs) with Rectified Linear Units (ReLU) activation function. This method, described as Sequential Estimation of RoA based on Invariant Set Estimation (SEROAISE), computes a Lyapunov-like PWA function over a certified PWA invariant set. While traditional approaches search for Lyapunov functions by enforcing Lyapunov conditions over pre-selected domains, this framework enforces Lyapunov-like conditions over a certified invariant subset obtained using the Iterative Invariant Set Estimator(IISE). Compared to the state-of-the-art, IISE provides systematically larger certified invariant sets. In order to find a larger invariant subset, the IISE utilizes a novel concept known as the Non-Uniform Growth of Invariant Set (NUGIS). A number of examples illustrating the efficacy of the proposed methods are provided, including dynamical systems derived from learning algorithms. The implementation is publicly available at: https://github.com/PouyaSamanipour/SEROAISE.git.

Figures

Figures reproduced from arXiv: 2504.12269 by the authors.

**Figure 2.** Because 0 ≤ ρ < 1, the convex polytope Xnew1 will always have a nonzero volume and it will be the subset of Xnew1 . The value of ρ for hyperplanes in (16) are set as follows: ρ = max k=2,...,n+1 u k u k + ǫ . (17) Once the simplex cell has been constructed, it can be checked to see if Forward invariance exists for this set. Step 2: Proving Forward Invariance To verify forward invariance of cell Xnew1 , we check Nag… view at source ↗

**Figure 2.** Non-uniform Growth of the invariant set for points wi [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

Figures from the paper (5 more)

**Figure 4.** Figure 4: Vertex categorization for IISE, where blue region de [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]

**Figure 5.** Figure 5: The process of updating the K∞ function αm(x) in each iteration with learning rate γ. where α0 > 0 and σ [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]

**Figure 6.** Figure 6: Using IISE to expand the certified invariant set ob [PITH_FULL_IMAGE:figures/full_fig_p011_6.png]

**Figure 7.** Figure 7: RoA for the Path-following Example 14 determined usi [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]

**Figure 8.** Figure 8: RoA for the inverted pendulum in Example 15 with LQR co [PITH_FULL_IMAGE:figures/full_fig_p013_8.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 21 canonical work pages

[1]

Formal synthesis of lyapunov neural networks

Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruﬀo. Formal synthesis of lyapunov neural networks. IEEE Control Systems Letters, 5(3):773–778, 2020

work page 2020
[2]

Control barrier functions: Theory and applications

Aaron D Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada. Control barrier functions: Theory and applications. In 2019 18th European control conference (ECC), pages 3420–3431. IEEE, 2019

2019
[3]

Piecewise linear optimal controllers for hybrid systems

Alberto Bemporad, Francesco Borrelli, and Manfred Mora ri. Piecewise linear optimal controllers for hybrid systems. I n Proceedings of the 2000 American Control Conference. ACC (IEEE Cat. No. 00CH36334) , volume 2, pages 1190–1194. IEEE, 2000

work page 2000
[4]

Neural lyapunov control

Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural lyapunov control. Advances in neural information processing systems, 32, 2019

2019
[5]

Learning lyapunov functions for hybrid systems

Shaoru Chen, Mahyar Fazlyab, Manfred Morari, George J Pappas, and Victor M Preciado. Learning lyapunov functions for hybrid systems. In Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control , pages 1–11, 2021

2021
[6]

Taylor, Ugo Rosolia, and Aaron D

Noel Csomay-Shanklin, Andrew J. Taylor, Ugo Rosolia, and Aaron D. Ames. Multi-rate planning and control of uncertain nonlinear systems: Model predictive control and control lyapunov functions. In 2022 IEEE 61st Conference on Decision and Control (CDC) , pages 3732–3739, 2022

work page 2022
[7]

Lyapunov-stable neural-network control

Hongkai Dai, Benoit Landry, Lujie Yang, Marco Pavone, and Russ Tedrake. Lyapunov-stable neural-network control . arXiv preprint arXiv:2109.14152 , 2021

arXiv 2021
[8]

Safe nonlinear control using robust neural lyapunov-barri er functions

Charles Dawson, Zengyi Qin, Sicun Gao, and Chuchu Fan. Safe nonlinear control using robust neural lyapunov-barri er functions. In Conference on Robot Learning , pages 1724–

work page

Show all 29 references

[9]

Fossil 2.0: Formal certiﬁcate synthesis for the veriﬁcatio n and control of dynamical models

Alec Edwards, Andrea Peruﬀo, and Alessandro Abate. Fossil 2.0: Formal certiﬁcate synthesis for the veriﬁcatio n and control of dynamical models. arXiv preprint arXiv:2311.09793, 2023

2023 arXiv
[10]

A general veriﬁcation framework for dynamical and control models via certiﬁcate synthesis

Alec Edwards, Andrea Peruﬀo, and Alessandro Abate. A general veriﬁcation framework for dynamical and control models via certiﬁcate synthesis. arXiv preprint arXiv:2309.06090, 2023

2023 arXiv
[11]

Safety veriﬁcation and robustness analysis of neural netwo rks via quadratic constraints and semideﬁnite programming

Mahyar Fazlyab, Manfred Morari, and George J Pappas. Safety veriﬁcation and robustness analysis of neural netwo rks via quadratic constraints and semideﬁnite programming. IEEE Transactions on Automatic Control , 2020

2020
[12]

Generalized approxim ation theorem and computational capabilities of neural networks

Aleksandr Nikolaevich Gorban’. Generalized approxim ation theorem and computational capabilities of neural networks . Sibirskii zhurnal vychislitel’noi matematiki, 1(1):11–24, 1998

1998
[13]

Gurobi Optimizer Reference Manual, 2024

Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2024

2024
[14]

Robust estimations of the region of attraction using invari ant sets

Andrea Iannelli, Andr´ es Marcos, and Mark Lowenberg. Robust estimations of the region of attraction using invari ant sets. Journal of the Franklin Institute , 356(8):4622–4647, 2019. 14

2019
[15]

Asymptotic stability of piecewise aﬃne systems with ﬁlippo v solutions via discontinuous piecewise lyapunov functions

Raﬀaele Iervolino, Stephan Trenn, and Francesco Vasca . Asymptotic stability of piecewise aﬃne systems with ﬁlippo v solutions via discontinuous piecewise lyapunov functions . IEEE Transactions on Automatic Control , 66(4):1513–1528, 2020

2020
[16]

Nonlinear control, volume 406

Hassan K Khalil. Nonlinear control, volume 406. Pearson New York, 2015

2015
[17]

Stability and performance veriﬁcation of dynamical systems controlled by neural networks: algorith ms and complexity

Milan Korda. Stability and performance veriﬁcation of dynamical systems controlled by neural networks: algorith ms and complexity. IEEE Control Systems Letters , 2022

2022
[18]

Numb a: A llvm-based python jit compiler

Siu Kwan Lam, Antoine Pitrou, and Stanley Seibert. Numb a: A llvm-based python jit compiler. In Proceedings of the Second Workshop on the LL VM Compiler Infrastructure in HPC, pages 1–6, 2015

2015
[19]

Tool lyznet: A lightweight python tool for learning an d verifying neural lyapunov functions and regions of attract ion

Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. Tool lyznet: A lightweight python tool for learning an d verifying neural lyapunov functions and regions of attract ion. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Contr...

2024
[20]

Soft-minimum and soft-maximum barrier functions for safety with actuation constraints

Pedram Rabiee and Jesse B Hoagg. Soft-minimum and soft-maximum barrier functions for safety with actuation constraints. arXiv preprint arXiv:2305.10620 , 2023

2023 arXiv
[21]

Learni ng lyapunov (potential) functions from counterexamples and demonstrations

Hadi Ravanbakhsh and Sriram Sankaranarayanan. Learni ng lyapunov (potential) functions from counterexamples and demonstrations. arXiv preprint arXiv:1705.09619 , 2017

2017 arXiv
[22]

Invariant set estimation for piecewise aﬃne dynamical systems using piecewise aﬃne barrier function

Pouya Samanipour and Hasan Poonawala. Invariant set estimation for piecewise aﬃne dynamical systems using piecewise aﬃne barrier function. European Journal of Control, page 101115, 2024

2024
[23]

Replacing k- inﬁnity function with leaky relu in barrier function design : A union of invariant sets approach for relu-based dynamical systems

Pouya Samanipour and Hasan Poonawala. Replacing k- inﬁnity function with leaky relu in barrier function design : A union of invariant sets approach for relu-based dynamical systems. arXiv preprint arXiv:2502.03765 , 2025

2025 arXiv
[24]

Poonawala

Pouya Samanipour and Hasan A. Poonawala. Automated stability analysis of piecewise aﬃne dynamics using vertices. In 2023 59th Annual Allerton Conference on Communication, Control, and Computing (Allerton) , pages 1–8, 2023

2023
[25]

Poonawala

Pouya Samanipour and Hasan A. Poonawala. Stability analysis and controller synthesis using single-hidden-la yer relu neural networks. IEEE Transactions on Automatic Control, pages 1–12, 2023

2023
[26]

Neural lyapunov control for discrete-time systems

Junlin W u, Andrew Clark, Yiannis Kantaros, and Yevgeni y Vorobeychik. Neural lyapunov control for discrete-time systems. Advances in neural information processing systems , 36:2939–2955, 2023

2023
[27]

Lyapunov-stable neural control for state and output feedback: A novel formulation

Lujie Yang, Hongkai Dai, Zhouxing Shi, Cho-Jui Hsieh, R uss Tedrake, and Huan Zhang. Lyapunov-stable neural control for state and output feedback: A novel formulation. In Forty- ﬁrst International Conference on Machine Learning , 2024

2024
[28]

Neural lyapunov control of unknown nonlinear systems with stability guarantees

Ruikun Zhou, Thanin Quartz, Hans De Sterck, and Jun Liu. Neural lyapunov control of unknown nonlinear systems with stability guarantees. arXiv preprint arXiv:2206.01913 , 2022

2022 arXiv
[29]

Analysing region of attract ion of load balancing on complex network

Mengbang Zou and W eisi Guo. Analysing region of attract ion of load balancing on complex network. Journal of Complex Networks, 10(4):cnac025, 2022. 15

2022

Pith tools

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

[1] [1]

Formal synthesis of lyapunov neural networks

Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruﬀo. Formal synthesis of lyapunov neural networks. IEEE Control Systems Letters, 5(3):773–778, 2020

work page 2020

[2] [2]

Control barrier functions: Theory and applications

Aaron D Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada. Control barrier functions: Theory and applications. In 2019 18th European control conference (ECC), pages 3420–3431. IEEE, 2019

2019

[3] [3]

Piecewise linear optimal controllers for hybrid systems

Alberto Bemporad, Francesco Borrelli, and Manfred Mora ri. Piecewise linear optimal controllers for hybrid systems. I n Proceedings of the 2000 American Control Conference. ACC (IEEE Cat. No. 00CH36334) , volume 2, pages 1190–1194. IEEE, 2000

work page 2000

[4] [4]

Neural lyapunov control

Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural lyapunov control. Advances in neural information processing systems, 32, 2019

2019

[5] [5]

Learning lyapunov functions for hybrid systems

Shaoru Chen, Mahyar Fazlyab, Manfred Morari, George J Pappas, and Victor M Preciado. Learning lyapunov functions for hybrid systems. In Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control , pages 1–11, 2021

2021

[6] [6]

Taylor, Ugo Rosolia, and Aaron D

Noel Csomay-Shanklin, Andrew J. Taylor, Ugo Rosolia, and Aaron D. Ames. Multi-rate planning and control of uncertain nonlinear systems: Model predictive control and control lyapunov functions. In 2022 IEEE 61st Conference on Decision and Control (CDC) , pages 3732–3739, 2022

work page 2022

[7] [7]

Lyapunov-stable neural-network control

Hongkai Dai, Benoit Landry, Lujie Yang, Marco Pavone, and Russ Tedrake. Lyapunov-stable neural-network control . arXiv preprint arXiv:2109.14152 , 2021

arXiv 2021

[8] [8]

Safe nonlinear control using robust neural lyapunov-barri er functions

Charles Dawson, Zengyi Qin, Sicun Gao, and Chuchu Fan. Safe nonlinear control using robust neural lyapunov-barri er functions. In Conference on Robot Learning , pages 1724–

work page