{"id":"2815cdb4-6f69-4950-b710-f8d3906dbaeb","arxiv_id":"2507.10352","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"The authors extend an SOS-based stability verification framework to smooth semialgebraic activations and recurrent equilibrium networks, and introduce a sequential algorithm that grows certified regions of attraction.","lead":"This paper improves a method for proving that neural-network controllers keep nonlinear systems stable. It adds new smooth activation functions, extends the method to recurrent networks, and offers a systematic way to enlarge the certified region of attraction.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The main theorem is logically sound given its assumptions, but Assumption 1 is not proven for RENs: continuity of the implicit branch w_phi(x) is asserted from well-posedness/Lipschitzness without a supporting proof, and Algorithm 1's problem B does not explicitly re-impose Assumption 3 on the…","rationale":"The reader's weakest assumption correctly identifies the most fragile link in the paper: the passage from an SOS feasibility certificate to a genuine Lyapunov certificate requires V and q to be continuous functions of the state, and this is exactly what Assumption 1 provides. For the new REN extension, the paper shows that the implicit graph is semialgebraic (Theorem 3.1) but does not prove that the actual solution branch is continuous; well-posedness and Lipschitzness are cited from prior work but no theorem is stated showing that these imply Assumption 1 for the augmented state and lifting variables. Since the numerical examples include an implicit REN-like construction (Section V-A), this is not an idle technicality. I found no internal error in Lemma 4.1 or in the proof of Theorem 4.3 given the stated assumptions; the argument is conditional on Assumptions 1 and 3. The additional gap in Algorithm 1, where problem B does not explicitly re-impose (50d) for the updated sigma_q, reinforces the reader's conditional verdict without changing it: the mathematics is promising, but the paper needs an explicit continuity proof for the REN branch selection (and for updated q) before the certificates can be regarded as fully justified. Therefore the appropriate outcome remains conditional acceptance pending that proof, matching the reader's verdict. A concrete verification: analytically derive the continuity/Lipschitz property of the implicit fixed point from the well-posedness condition, or find a small REN counterexample with a discontinuous/multi-valued hidden branch under the stated assumptions.","tokens_in":20816,"tokens_out":29066,"duration_ms":348371,"concrete_test":"Prove or disprove the following analytic claim: for any REN satisfying the stated well-posedness condition (e.g. 2I-D11-D11^T ≻ 0, with semialgebraic slope-restricted activations), the unique solution w_phi(x) of (26) is Lipschitz continuous in x and admits a continuous selection of any additional lifting variables. Concretely, search over small randomly initialized RENs (n_phi=2,3; D11 with 2I-D11-D11^T ≻ 0 but ||D11||_2>1, e.g. skew D11) whether the fixed-point equation has multiple or discontinuous solutions as x varies. If a counterexample appears, restrict Theorem 3.1/Theorem 4.3 to contractive enough D11 or add an explicit continuity proof.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central certificate (Theorem 4.3 and its global analogue) rests on Assumption 1: V and q evaluated on the actual trajectory must be continuous functions of x, so that Lemma 4.1 can be applied. For feedforward ReLU networks this is established, but for RENs the paper only states that RENs are 'Lipschitz continuous and well-posed' (Section III-B) and proves in Theorem 3.1 that the implicit graph is a semialgebraic set (29). That set can contain all fixed-point branches of w = phi(D x + D11 w + b); it does not by itself show that the actual branch is unique and continuous, or that a continuous selection of the lifting variables exists. Uniqueness of a continuous fixed-point equation does not automatically imply continuity of the fixed point without a contraction or compactness argument. If the actual branch is discontinuous or the set description admits spurious branches, the SOS decrease (14) and barrier (49) are checked over a larger system than the true closed loop, and V/q may not be defined as continuous functions of the state, so Lemma 4.1 and Theorem 4.3 no longer apply. The same gap appears in Algorithm 1, problem B (54): the constraint (53) is argued to imply sigma_q in Q0 via nonnegativity and zero at the origin, but it does not enforce continuity-in-x of the updated sigma_q; (50d) is not re-imposed explicitly.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":21178,"tokens_out":12504,"duration_ms":145153,"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":[{"comment":"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.","section":"Section IV-C, Algorithm 1, problem B (54)"}],"minor_comments":[{"comment":"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.","section":"Theorem 3.1"},{"comment":"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":"Equation (53) and (54b)"},{"comment":"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.","section":"Section IV-B, equations (42)-(43)"},{"comment":"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":"Lemma 4.1"},{"comment":"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\".","section":"Section VI"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This paper is a genuine extension of the SOS verification framework for neural-network controllers, and the core math holds up. The new Lemma 4.1 is correct, and the sequential invariant-set algorithm (Algorithm 1) is a real practical improvement over the two-step state of the art. The REN compatibility proof is terse, but the gap the stress test flags is mostly a presentation issue, not a load-bearing flaw.\n\nWhat is actually new: two semialgebraic activation functions (softplus and tanh mimics) that fit naturally into the exact graph description; a proof that well-posed, Lipschitz RENs can be represented by semialgebraic sets; an alternate stability proof (Lemma 4.1) that gives a cleaner condition for when an SDP solution is a valid Lyapunov certificate; and two new local-stability SDPs, including the sequential algorithm that provably grows the region of attraction monotonically. These are useful contributions. The numerical examples are plausible and the MPC imitation example nicely demonstrates the point about certifying points outside the MPC feasible set.\n\nSoft spots, in order of severity:\n\n1. No code or data. The numerical claims (the P matrices, the phase portraits, the algorithm's convergence in 7 iterations) cannot be independently checked. This is a major reproducibility gap for a paper whose whole point is computational certification.\n\n2. Assumption 1 for RENs is not explicitly proven. The paper assumes Lipschitz continuity and well-posedness of the REN, which does imply continuity of the actual input-output map, so the stress test's worry about discontinuous branches is likely unfounded. But the paper never constructs the continuous selection of lifting variables lambda needed to satisfy Assumption 1. That is a fixable gap in exposition, but it should be fixed.\n\n3. In Algorithm 1 problem B, the constraint (53) plus sigma_q SOS and sigma_q^A(0)=0 does re-impose the essential part of (50d), so the stress test's concern there also does not fully land. However, the paper should explicitly state that if sigma_q is parameterized with lifting variables, Assumption 3 must be re-checked after the update. As written, the numerical example uses sigma_q(x) as a polynomial in x only, so it is fine, but the general case is left ambiguous.\n\n4. The claim that the candidate Lyapunov parameterization (41) is \"significantly larger than previous classes\" is plausible but not backed by a direct comparison. A short benchmark against the cited [13], [14] would help.\n\nThe citation pattern looks fair. The paper cites the relevant SOS and IQC literature, including the REN papers it builds on. The writing is clear, and the examples are well explained.\n\nWho this is for: researchers in verification of neural-network controllers, especially those working with SOS/SDP and RoA analysis. The paper deserves a serious referee. I would send it to peer review, with the request that the authors release code and tighten the REN/Assumption 1 argument.","headline":"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.","tokens_in":21707,"tokens_out":3144,"would_cite":true,"duration_ms":34100,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93D30","93D05","90C22","93C55","68T07"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["sum-of-squares programming","semialgebraic sets","neural network controllers","Lyapunov stability","region of attraction","recurrent equilibrium networks","semidefinite programming","discrete-time barrier functions"],"falsifier":"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.","tokens_in":20620,"feed_emoji":"🧠","tokens_out":10504,"duration_ms":111106,"temperature":0.7,"pith_summary":"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.","feed_headline":"One SDP certifies stability and an invariant region of attraction","feed_subtitle":"Neural-network controllers with smooth or recurrent activations can now be certified without a second sublevel-set search.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"provides the original global stability certificate (Theorem 2.3) and the semialgebraic description of ReLU networks that the extended framework builds on.","marker":"[7]"},{"why":"establishes the prior local stability framework with the two consecutive SDPs that this paper improves.","marker":"[16]"},{"why":"supplies the earlier SOS stability verification approach whose limitations motivate the new formulations.","marker":"[17]"},{"why":"defines recurrent equilibrium networks and their state-space representation, the architecture whose compatibility the paper proves.","marker":"[18]"},{"why":"gives the well-posedness and Lipschitz condition used to ensure an implicit REN has a unique continuous response.","marker":"[21]"},{"why":"supplies the Lyapunov-function definition and the theorem used to pass from a Lyapunov function in Q to local asymptotic stability and Q being in the region of attraction.","marker":"[22]"},{"why":"provides the discrete-time barrier-function concept behind the invariance constraint on Q.","marker":"[24]"},{"why":"supplies the linearization-based initialization and alternating-SDP strategy used to solve the nonconvex optimization problem (50).","marker":"[25]"},{"why":"supplies the result that a quadratic Lyapunov function for the linearized system gives an invariant sublevel set for the nonlinear system, used for the initial solution.","marker":"[26]"}],"fun_headline_variants":["SDP certifies invariant RoA for recurrent and smooth controllers","One SDP proves stability and invariant region of attraction","Alternate SDP proof expands Lyapunov candidates for local stability","Larger Lyapunov class and RoA certificate via SDP","SDP certifies stability for RENs and smooth activations"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["SDP certifies invariant RoA for recurrent and smooth controllers","One SDP proves stability and invariant region of attraction","Alternate SDP proof expands Lyapunov candidates for local stability","Larger Lyapunov class and RoA certificate via SDP","SDP certifies stability for RENs and smooth activations"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001128,"raw_usage":{"total_tokens":4687,"prompt_tokens":937,"completion_tokens":3750,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":553,"completion_tokens_details":{"reasoning_tokens":3663}},"tokens_in":553,"tokens_out":3750,"duration_ms":28565,"temperature":1.0,"reasoning_tokens":3663,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T17:35:17.840985+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Stability and performance verification of dynamical systems controlled by neural networks: Algorithms and complexity,","cited_arxiv_id":null,"evidence_quote":"provides the original global stability certificate (Theorem 2.3) and the semialgebraic description of ReLU networks that the extended framework builds on."},{"cited_title":"Recurrent equilibrium networks: Flexible dynamic models with guaranteed stability and robust- ness,","cited_arxiv_id":null,"evidence_quote":"defines recurrent equilibrium networks and their state-space representation, the architecture whose compatibility the paper proves."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"supplies the Lyapunov-function definition and the theorem used to pass from a Lyapunov function in Q to local asymptotic stability and Q being in the region of attraction."},{"cited_title":"Discrete control barrier functions for safety-critical control of discrete systems with application to bipedal robot navigation,","cited_arxiv_id":null,"evidence_quote":"provides the discrete-time barrier-function concept behind the invariance constraint on Q."},{"cited_title":"Region of attraction analysis via invariant sets,","cited_arxiv_id":null,"evidence_quote":"supplies the linearization-based initialization and alternating-SDP strategy used to solve the nonconvex optimization problem (50)."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"supplies the result that a quadratic Lyapunov function for the linearized system gives an invariant sublevel set for the nonlinear system, used for the initial solution."}],"review_version":1}