{"id":"a0cbe0fd-4ed6-4273-87ee-432dadc1ba9b","arxiv_id":"2508.15616","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":10,"one_line_summary":"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.","lead":"This paper trains a small neural network to imitate a robust model predictive controller for a two-wheeled inverted pendulum, then uses sum-of-squares optimization to prove local stability and to compute a region of attraction. It is the first claimed hardware demonstration that this type of neural-network stability certificate can be obtained for a real control system.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"SOS certificate covers only the nominal LTI model with full-state feedback; the implemented estimator loop and unmodeled nonlinearities are not certified.","rationale":"The reader's weakest_assumption correctly identifies that the SOS certificate is for the nominal LTI model with full-state feedback, not the implemented estimator-based loop or the nonlinear plant. This is the most load-bearing concern because the paper's central contribution—the practical value of SOS verification for real-world control—rests on the certificate governing the actual hardware. The paper provides no formal link between the certified model and the physical loop: no estimation-error bound, no robustness margin for the unmodeled nonlinearities (backlash, yaw, deadband residual), and no analysis of the output modifications. The hardware experiments are valuable empirical support, but they do not substitute for a formal transfer argument. The SOS machinery itself appears sound: the exact ReLU graph description (Section VI-A) and the SOS conditions (54)–(56) are standard, and the postprocessing enforcing φ(0)=0 addresses an important subtlety. My read agrees with the reader's conditional verdict: the technical verification is plausible but the claim as stated is too broad, and the missing artifacts further hinder reproduction. The proposed simulation test would provide a direct check of whether the certified RoA is meaningful for the actual closed loop.","tokens_in":23655,"tokens_out":8584,"duration_ms":98557,"concrete_test":"Simulate the full nonlinear closed loop: the nonlinear plant (1)–(5), the state estimator of Section III with Table II parameters, the trained NNC with postprocessing and saturation, and the output modifications (40)–(41). Choose initial true states whose corresponding estimated states lie inside the certified sublevel set L_γ(V) (γ=1.95). If any simulated trajectory leaves L_γ(V) or fails to converge to the origin, the certificate does not transfer to the implemented loop. Alternatively, evaluate the certified Lyapunov function V along the recorded experimental estimated-state trajectories from Section VII-C; failure of V to strictly decrease along any run would cast direct doubt on the transfer.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim—that the physical two-wheeled inverted pendulum is proven locally asymptotically stable under the NNC (Section VIII)—overstates what the certificate actually establishes. The SOS verification in Section VI is performed on the scaled linear time-invariant model x̄⁺ = Āx̄ + B̄φ(x̄) (Eq. 44) with exact full-state feedback x̄. In the implemented loop, the NNC is fed the estimated state x̂ from the complementary-filter-based estimator of Section III (Fig. 3), and the plant includes nonlinear dynamics, backlash, deadband residual, and yaw dynamics that are absent from model (20). The controller output modifications in Section V-D (feedforward, active yaw control, deadband compensation) are likewise not part of the certified system. The paper asserts (Section V-D) that these modifications 'allow the assumptions of the control-oriented model of (20) to be met,' but no bound on the estimation error ||x̂−x|| or on the unmodeled dynamics is provided, and no argument shows that trajectories of the true closed loop remain within the certified RoA L_γ(V). Consequently, the formal certificate does not apply to the implemented control loop; the experimental results provide empirical evidence but do not close this gap. This is the load-bearing weakness because the paper's primary contribution is the practical value of the SOS verification, and that value hinges on the certificate describing the real system.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents an end-to-end pipeline for a two-wheeled inverted pendulum (the Sigi platform): a nonlinear model (1)-(5), a state estimator (Section III), parameter identification and linearization to a control-oriented LTI model (20), and the synthesis of an LQR, a robust tube-based MPC, and a neural-network controller (NNC) that imitates the MPC (Section V). The main claimed contribution is an SOS-based verification of local asymptotic stability and an inner estimate of the region of attraction for the closed-loop system consisting of the NNC and the model (Section VI). The authors report a feasible SOS certificate with parameters α=1.5 and γ=1.95 (Section VII-B), and they provide experimental comparisons showing that the NNC outperforms a baseline LQR in regulation and reference-tracking tasks.","tokens_in":24060,"tokens_out":5779,"duration_ms":74211,"significance":"If the stability certificate applied to the physical closed-loop demonstrator, this would be a valuable first demonstration of SOS-based verification of a neural-network controller on a real-world problem. The paper has notable strengths: the ReLU network is modeled exactly through its semialgebraic graph, the SOS problems are solved with standard tools (SOSTOOLS/MOSEK), the identified model parameters are reported, and the experimental protocol is transparent. However, the certificate is computed for the scaled linearized model with exact full-state feedback, not for the implemented loop with the state estimator, yaw control, deadband compensation, and unmodeled nonlinearities. This gap is load-bearing because the paper's central claim—that the physical two-wheeled inverted pendulum is proven LAS under the NNC—is stronger than what the formal analysis establishes. The theoretical backing also depends on an unreviewed preprint [29], which supplies the two-step SOS Lyapunov argument. The experimental results are useful empirical evidence but do not close the formal gap.","major_comments":[{"comment":"The SOS certificate is obtained for the scaled LTI system x̄⁺ = Āx̄ + B̄φ(x̄) with exact full-state feedback x̄. In the implemented loop, the controller receives the estimated state x̂ from the estimator of Section III, and the control signal is modified by feedforward, active yaw control, and deadband compensation as in Eqs. (40)-(41) and Fig. 3. The statement in Section V-D that these modifications 'allow the assumptions of the control-oriented model of (20) to be met' is not supported by any quantitative bound on ||x̂−x||, any model of the residual deadband/backlash/yaw dynamics, or any argument that trajectories of the true closed loop remain inside L_γ(V). Consequently, the formal certificate does not apply to the implemented loop, and the conclusion in Section VIII that 'the two-wheeled inverted pendulum is proven to be LAS under this NNC' overstates what is proved.","section":"Section VI, Eq. (44); Section V-D; Fig. 3"},{"comment":"The verified closed-loop system is autonomous and regulation-oriented: x⁺ = f(x, φ(x)). The experimental reference-tracking task, however, uses a nonzero feedforward u_ff(k) and an active yaw controller that are not part of the certified dynamics. Even if the certificate correctly covers the nominal model, it does not certify stability or performance of the time-varying tracking loop. The empirical tracking results are not backed by the formal RoA result, and the paper should either extend the analysis to the tracking loop or clearly separate the verified claim (regulation of the nominal model) from the empirical demonstration.","section":"Section V-D; Section VII-C"},{"comment":"The proof that solving SDP (55) and then SDP (57) in succession yields a valid Lyapunov function in the sense of Definition 6.3 is delegated to the authors' unpublished preprint [29]. In particular, the text acknowledges in Section VI-B that functions parameterized by (53) 'are not necessarily candidate Lyapunov functions satisfying (42a) and (42b)', but the conditions under which the chosen bases of Table IV ensure V(0)=0 and positive definiteness are not stated. For a journal submission, the relevant theorem or a complete proof sketch should be included, or the dependency on [29] should be made explicit with the exact propositions used.","section":"Section VI, paragraphs after Eq. (57); Reference [29]"}],"minor_comments":[{"comment":"There are typographical artifacts in the numerical entries, e.g. '1.68eee−2' and 'e−2' formatting. Please ensure all table entries are rendered consistently.","section":"Tables V and VI"},{"comment":"The description of the two additional ReLU neurons implementing the ±2.0 V saturation is too terse; the reader cannot reconstruct the exact network weights or verify that the saturation is exactly min(max(u,−2),2). Please provide the layer equations or explicitly state the construction.","section":"Section V-C.3"},{"comment":"The two-step SOS procedure's computational cost is not reported. Since one of the paper's claims is practical value, a statement of solver times and problem sizes would strengthen the exposition.","section":"Section VI-D"},{"comment":"The notation B⃗ω B/I in (7) is used before its precise relation to the gyroscope measurement and the calibration procedure is described; consider reordering for clarity.","section":"Section III-A, Eq. (7)"},{"comment":"Only five runs per controller are reported, with no statistical variability measures such as standard deviation or confidence intervals. Given the hardware variability, a brief statement of run-to-run variation would help interpret the RMSE/MAE comparisons.","section":"Section VII-C"}],"recommendation":"major_revision","confidential_remarks":"The paper is a competent application of the authors' prior SOS framework, and the experimental work appears careful. However, the central claim is currently broader than the formal certificate: the certificate covers a nominal LTI model with full-state feedback, while the implemented demonstrator includes an estimator, yaw dynamics, and deadband compensation. This gap is fixable by either (i) restricting all formal claims to the nominal model and presenting experiments as empirical validation, or (ii) adding a robustness analysis (e.g., an estimation-error bound, an ISS or input-to-state argument, or explicit accounting for the unmodeled terms). The dependence on the unreviewed preprint [29] should also be made self-contained enough for a journal reader to check the Lyapunov argument. I do not see a fundamental flaw in the SOS computations themselves, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bottom line: the new thing here is a first hardware application of the exact-ReLU SOS verification framework, and as an applied paper it mostly holds together. The certificate itself is for the scaled LTI model with perfect full-state feedback; the claim that the physical Sigi robot is proven locally asymptotically stable goes beyond the math.\n\nWhat's good: the synthesis pipeline is sensible and described in enough detail to follow — MPC-informed sampling with 30% of samples in the invariant set, softened constraints, the postprocessing that forces φ(0)=0, and the output-layer fix. The SOS procedure, while mostly from Korda and Newton/Papachristodoulou, is adapted cleanly, and they report the actual numbers (α=1.5, γ=1.95) rather than hiding them. The hardware experiments are a useful empirical check, and they are honest about the mixed performance: better position tracking, worse velocity and pitch-rate errors. The approximation error between NNC and MPC is also shown and is consistent with the assumed disturbance bound.\n\nThe weak spots, in order. First, the certificate covers x̄⁺ = Āx̄ + B̄φ(x̄), Eq. (44), under exact full-state feedback. The real loop of Fig. 3 uses the estimator, the yaw controller, deadband compensation, and the plant has backlash and unmodeled dynamics. Section V-D asserts these modifications 'allow the assumptions' of (20) to be met, but that is an engineering statement, not a theorem, and no estimation-error bound is provided. So the formal result is narrower than the abstract and conclusion suggest. Since the body is fairly transparent about this, it is an overstatement rather than a fraudulent claim. Second, the method leans on companion preprint [29], unreviewed, for the improved formulation, and no weights, code, or SDP artifacts are released, so exact reproduction isn't possible. Both are addressable in revision. I would not call the nominal-model certificate into question; the mathematics seems coherent.\n\nThis is a paper for control-theory and safe-autonomy readers who want to see how exact-ReLU verification scales to a physical problem. It deserves a serious referee: send it out, but require a clear statement about [29] and ideally the artifacts.","headline":"A solid first hardware application of exact-ReLU SOS verification, but the certificate covers the linearized full-state model, not the estimator loop that actually ran, so the abstract's 'proven LAS' overstates the formal result.","tokens_in":24507,"tokens_out":3131,"would_cite":true,"duration_ms":37925,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93D30","90C22","93D05"],"pacs":[],"model":"deepseek-v4-flash","headline":"A neural network controller trained to imitate a tube-based MPC is proven locally asymptotically stable by sum-of-squares verification, and on a physical two-wheeled inverted pendulum it stabilizes the system and outperforms a baseline LQR.","keywords":["closed-loop stability","neural-network-based controllers","sum of squares (SOS)","semidefinite programming (SDP)","region of attraction","ReLU activation","tube-based model predictive control","two-wheeled inverted pendulum"],"falsifier":"Replace the linearized model (20) in the SOS loop description with the full nonlinear closed loop of Section II, including the deadband (5), backlash residual, and the estimator of Section III, and re-run programs (55) and (57): infeasibility, or any simulated trajectory starting inside the certified sublevel set L_γ(V) with γ = 1.95 that exits it, would show the certificate does not apply to the physical demonstrator. A hardware-compatible version: start the robot inside the certified RoA with a deliberately biased attitude estimate and observe whether the state leaves the certified set.","tokens_in":1849,"feed_emoji":"🤖","tokens_out":2308,"duration_ms":156115,"temperature":0.7,"pith_summary":"This paper reports the first application of an SOS-based stability verification procedure for neural-network controllers to a real control problem: balancing a two-wheeled inverted pendulum. The authors build a state estimator and a control-oriented linear model of the platform, synthesize a baseline LQR and a robust, tube-based MPC, and train a small ReLU network to imitate the MPC. Two SOS programs then produce a Lyapunov function that certifies the closed loop (linearized model plus network) is locally asymptotically stable, together with a sublevel-set inner estimate of its region of attraction. Experiments on the physical demonstrator show the neural controller stabilizes the system and improves position tracking over the LQR in both regulation and reference-tracking tasks. The practical stakes: heavy online optimization is replaced by a cheap, formally verified network.","feed_headline":"Neural controller proven stable, then beats LQR on real robot","feed_subtitle":"SOS verification gives the learned controller a proven region of attraction; on the robot it beats the LQR baseline.","key_machinery":"The load-bearing mechanism is the exact semialgebraic encoding of the ReLU network. A single ReLU neuron y = max(0, wᵀx + b) has a graph described by three polynomial (in)equalities (y ≥ 0, y − wᵀx − b ≥ 0, and y(y − wᵀx − b) = 0), and composing these across layers yields an exact description of the network's input-output relation on the set Q̄, plus of the composed loop L = φ ∘ f̄ ∘ (id, φ). Because these sets are semialgebraic, the Lyapunov decrease condition becomes a constraint enforceable by sum-of-squares polynomials, i.e., by a semidefinite program. The same encoding lets the second program certify that the found sublevel set L_γ(V) lies inside Q̄. This exactness is what distinguishes","core_discovery":"On its own terms: the SOS-based stability verification of Refs. [12], [13], which models the ReLU network's input-output map exactly as a semialgebraic set, can certify useful stability properties for a practically implemented NNC. For the closed loop x̄⁺ = Āx̄ + B̄φ(x̄) (scaled linearized model (20) plus trained ReLU network φ), two SOS programs find a Lyapunov function V with strict decrease over Q̄ = {x̄ : α − x̄ᵀQ̄x̄ ≥ 0} and then the largest sublevel set L_γ(V) ⊆ Q̄. With α = 1.5 and γ = 1.95, V certifies local asymptotic stability, and L_γ(V) is a certified inner estimate of the region of attraction. Experiments on the physical robot show the NNC stabilizes the demonstrator and outperf","pith_inferences":["A step the paper leaves open: the certificate covers only the nominal linearized plant with the true state as input, so folding the estimator and an error bound into the semialgebraic loop model is the natural path to a guarantee for the implemented loop.","Because the SOS problem size scales with the number of ReLU neurons and their lifted activations, a plausible trade-off emerges between imitation fidelity (more piecewise-linear regions) and verifiability (smaller networks); retraining the same MPC with different widths and comparing the certified γ would test this.","The comparison on the robot is against an LQR, but the certificate itself is never exercised at the RoA boundary in the experiments; a deliberate boundary-disturbance test would probe whether the certified set is tight under the unmodeled dynamics.","The synthesis recipe (softened feasible set for data generation, output-layer correction enforcing φ(0) = 0, ReLU saturation layers) reads as a general template: any expensive stabilizing policy that can be sampled could seed a certified cheap network, including policies found by reinforcement learning."],"forward_implications":["A small ReLU network can replace a tube-based MPC that is too computationally demanding for the embedded hardware, and the replacement carries a formal certificate of local asymptotic stability plus an inner region-of-attraction estimate.","The certified region (γ = 1.95 for α = 1.5) is large enough to cover the states used in the physical experiments, giving the guarantee practical rather than symbolic value.","In five regulation and five reference-tracking runs, the NNC improves average RMSE of position and CoG position over the LQR (e.g., xw RMSE drops from 2.79e−2 to 1.68e−2 m in regulation), while velocity and pitch-rate RMSE are larger, consistent with the learned MPC's more aggressive nonlinear behavior.","The a posteriori comparison of Fig. 10 shows the NNC's deviation from the MPC law mostly stays within the 0.075 V disturbance bound assumed during tube-MPC design, supporting the validity of that design parameter.","The controller output modifications (deadband compensation, active yaw control, feedforward) are what allow the real platform to match the planar, deadband-free model that the certificate applies to."],"supporting_citations":[{"why":"Introduces the SOS-based verification approach that models the neural network's input-output relation exactly via semialgebraic sets; the paper adapts this as its core certificate procedure.","marker":"[12]"},{"why":"The sum-of-squares stability verification for neural feedback loops that the authors apply to the closed-loop system of Section VI.","marker":"[13]"},{"why":"Supplies the Lyapunov-function definition (Def. B.12) and the tube-based MPC guarantee that the nominal system is robustly stabilized to the set E.","marker":"[21]"},{"why":"Theory used to compute the robust positive invariant ellipsoid E that defines the tube-based MPC's constraint tightening.","marker":"[22]"},{"why":"Linear-matrix-inequality background used to solve the semidefinite program yielding Ktube, Ptube, and δtube.","marker":"[23]"},{"why":"The optimization-based method for computing the largest sublevel set of V inside Q̄, used as the second SOS program.","marker":"[28]"},{"why":"The authors' improved SOS formulation, which supplies the basis-vector selection and minimum-at-origin construction used in SDPs (55) and (57).","marker":"[29]"},{"why":"Establishes the equivalence between SOS polynomials and positive-semidefinite Gram matrices, turning the Lyapunov conditions into a tractable SDP.","marker":"[30]"}],"fun_headline_variants":["SOS-verified neural controller beats LQR on real robot","Certified stable neural net outdoes LQR on inverted pendulum","Stability proof for learned controller, then real-world outperformance","Neural controller gets stability certificate, beats LQR on robot","SOS proof says NN stable, robot shows it beats LQR"],"cache_read_input_tokens":26240,"weakest_assumption_plain":"The stability proof applies to a simplified linear model of the robot with perfect state information; the real robot's controller gets an estimated state, and unmodeled backlash, voltage deadband, and yaw motion could carry the system outside the certified region.","fun_headline_variants_meta":{"raw":{"variants":["SOS-verified neural controller beats LQR on real robot","Certified stable neural net outdoes LQR on inverted pendulum","Stability proof for learned controller, then real-world outperformance","Neural controller gets stability certificate, beats LQR on robot","SOS proof says NN stable, robot shows it beats LQR"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00036,"raw_usage":{"total_tokens":1819,"prompt_tokens":814,"completion_tokens":1005,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":558,"completion_tokens_details":{"reasoning_tokens":918}},"tokens_in":558,"tokens_out":1005,"duration_ms":8770,"temperature":1.0,"reasoning_tokens":918,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T17:47:56.524222+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Replace the linearized model (20) in the SOS loop description with the full nonlinear closed loop of Section II, including the deadband (5), backlash residual, and the estimator of Section III, and re-run programs (55) and (57): infeasibility, or any simulated trajectory starting inside the certified sublevel set L_γ(V) with γ = 1.95 that exits it, would show the certificate does not apply to the physical demonstrator. A hardware-compatible version: start the robot inside the certified RoA with a deliberately biased attitude estimate and observe whether the state leaves the certified set.","supporting_citations":[{"cited_title":"Stability and performance verification of dynamical systems controlled by neural networks: Algorithms and complexity,","cited_arxiv_id":null,"evidence_quote":"Introduces the SOS-based verification approach that models the neural network's input-output relation exactly via semialgebraic sets; the paper adapts this as its core certificate procedure."},{"cited_title":"Stability of non-linear neural feedback loops using sum of squares,","cited_arxiv_id":null,"evidence_quote":"The sum-of-squares stability verification for neural feedback loops that the authors apply to the closed-loop system of Section VI."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the Lyapunov-function definition (Def. B.12) and the tube-based MPC guarantee that the nominal system is robustly stabilized to the set E."},{"cited_title":"Theory and computation of dis- turbance invariant sets for discrete-time linear systems,","cited_arxiv_id":null,"evidence_quote":"Theory used to compute the robust positive invariant ellipsoid E that defines the tube-based MPC's constraint tightening."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Linear-matrix-inequality background used to solve the semidefinite program yielding Ktube, Ptube, and δtube."},{"cited_title":"Stability and performance verification of optimization-based controllers,","cited_arxiv_id":null,"evidence_quote":"The optimization-based method for computing the largest sublevel set of V inside Q̄, used as the second SOS program."},{"cited_title":"Semidefinite programming relaxations for semialgebraic problems,","cited_arxiv_id":null,"evidence_quote":"Establishes the equivalence between SOS polynomials and positive-semidefinite Gram matrices, turning the Lyapunov conditions into a tractable SDP."}],"review_version":1}