{"id":"815b513e-e289-4cb5-886c-c5e6662b7c96","arxiv_id":"2502.04551","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A Jordan recurrent network estimator is shown to have input-to-state stable error dynamics, with stability certified by SMT-verified Lyapunov functions and demonstrated on three example systems.","lead":"This paper trains Jordan recurrent neural networks as state estimators and analyzes the stability of their estimation error using input-to-state stability and SMT-verified Lyapunov functions. The authors report lower root mean square error than extended and unscented Kalman filters on two nonlinear examples and comparable performance to the Kalman filter on a linear example.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The nonlinear stability verification is local and not self-contained: Theorem 3.6 needs a global ISS Lyapunov certificate, but Section V reports only a [-2,2]^2 box check and defers the origin region to an unstated linearization argument.","rationale":"I read the paper as making a methodological contribution: an ISS framework for JRN-based state estimators. Theorem 3.6 is a standard and correct cascade result, and the linear-system treatment is conventional. The soft spot is the verification that the trained nonlinear JRN error dynamics satisfy the ISS Lyapunov inequalities globally. The paper's own Section III admits that the SMT approach excludes a neighborhood of the origin and delegates that region to an unshown linearization argument; Section V reports only a bounded-box certificate for one of the two nonlinear examples. The numerical comparisons may be sound, but they do not by themselves establish the stability theorem as stated. A local Lyapunov certificate plus a compact-box check can be a legitimate route if the box is invariant or part of the basin of attraction and the linearization covers the excluded region; none of these ingredients are demonstrated in the text. This is a question of missing support rather than a detected contradiction in the theorem, so the reader's CONDITIONAL verdict remains appropriate and no verdict change is needed.","tokens_in":9430,"tokens_out":6952,"duration_ms":80117,"concrete_test":"Inspect the GitHub repository for the dReal SMT scripts and the local linearization argument, then independently re-run the SMT verification for the down-pendulum Lyapunov function on an expanding box [-R,R]^2 for R = 4, 8, 16 with both e and x in the box, and require an explicit positive-definite matrix P for the linearized error dynamics near the origin. If the learned V violates the ISS inequalities for any R > 2, or if no local P is provided, the claimed global asymptotic stability is not supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim requires the error system (5) to be ISS over the full state space, since Theorem 3.6 concludes global asymptotic stability of the cascade. The nonlinear verification in Sections III and V does not deliver this. The text concedes that SMT solvers exclude a small neighborhood of the origin and that the linearized model is used there, but no local Lyapunov computation is reported for any nonlinear example. Furthermore, the only concrete nonlinear certificate is the down-pendulum Lyapunov function checked on [-2,2] x [-2,2] for the error states; neither the corresponding region for the state input nor any verification details for the reversed Van der Pol example are given. A Lyapunov inequality verified on a bounded box is insufficient to conclude ISS unless the box is shown to contain all relevant trajectories and the excluded region is covered by a separate certificate. As written, Theorem 3.6 does not license the claim that the learned estimator's error dynamics are asymptotically stable; the omitted steps are load-bearing.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes the use of Jordan recurrent neural networks (JRNs) for state estimation of nonlinear discrete-time systems and studies the stability of the resulting estimation error. The error dynamics are written as a cascade in which the nominal state trajectory x(t) acts as an input to the error system (5). Theorem 3.6 states that if the error system is input-to-state stable (ISS) and the origin of the nominal system (3) is globally asymptotically stable, then the origin of the cascade is globally asymptotically stable. For linear systems, a quadratic ISS-Lyapunov function is obtained from a discrete Lyapunov equation. For nonlinear systems, the authors train a neural-network Lyapunov function and verify the required inequalities with the SMT solver dReal, reporting the down pendulum and reversed Van der Pol oscillator as examples. The paper also compares the JRN estimator with KF, EKF, and UKF in terms of RMSE.","tokens_in":9651,"tokens_out":9503,"duration_ms":104554,"significance":"If the main claim were fully established, the paper would provide a useful stability guarantee for a class of learned recurrent-neural-network estimators. The cascade theorem itself is correct and elementary, and the linear mass-spring example is essentially complete. The authors also deserve credit for providing a reproducible code link and for using machine-checked SMT verification on the reported box. The practical significance of the paper, however, rests on the nonlinear verification, and that verification is not currently global: the paper verifies only a bounded box for the error states and explicitly defers the region near the origin to an unstated linearization argument. The reversed Van der Pol example has no verification details at all. Thus the central claimed contribution, the stability of the JRN error dynamics for nonlinear systems, is not yet established as written.","major_comments":[{"comment":"The only concrete nonlinear certificate reported in the paper is the statement that a learned ISS Lyapunov function was verified by dReal on a [-2,2] x [-2,2] region \"for the error states.\" No verification box for the nominal state x is given, and no invariant-set argument shows that the trajectories of the nominal system remain within any verified region. Since Definition 3.5 requires the Lyapunov inequalities for all e in E and all x in X, and Theorem 3.6 concludes global asymptotic stability of the cascade, a check on a bounded error box does not by itself establish the claimed asymptotic stability of the JRN error dynamics. This is the load-bearing gap between the SMT verification and the theorem's conclusion.","section":"Section V, down pendulum example"},{"comment":"The text acknowledges that SMT solvers require excluding a small region around the origin, that \"the linearization of the nonlinear system dominates\" there, and that the linear method is applied to provide stability guarantees. However, no linearized error system, no local Lyapunov matrix, no quantitative radius for the excluded region, and no proof of domination is given for either nonlinear example. Local linear stability near the origin does not imply the ISS Lyapunov inequality on the remaining unbounded set. The transition from a local linear certificate to the global stability claim is an omitted, load-bearing step.","section":"Section III, Nonlinear systems paragraph"},{"comment":"The text says that \"for both nonlinear systems\" an ISS Lyapunov function was learned and verified by an SMT solver, but only the down pendulum is described. For the reversed Van der Pol oscillator, no Lyapunov function, comparison functions, verification box, or even an explicit statement that the origin of the nominal system is globally asymptotically stable is presented. Since Theorem 3.6 requires the nominal system to be globally asymptotically stable and the error system to be ISS, the stability claim for the reversed Van der Pol example is currently unsupported.","section":"Section V, reversed Van der Pol example"}],"minor_comments":[{"comment":"Equation (17) appears to contain a typo: the discrete Lyapunov equation should presumably be A^T P A - P + Q = 0, not \"A^T P A - A + Q = 0\" as printed.","section":"Section III, Linear systems"},{"comment":"The symbol A is used both for the state matrix in (13) and later for WxaWax in the error dynamics, which makes the Lyapunov equation (17) confusing. Please use distinct symbols for these two matrices.","section":"Section III, Linear systems"},{"comment":"The definitions use |e| and |x| without formally defining the norm on R^n, and the same notation is reused for different quantities. It would be clearer to use \\|\\cdot\\| throughout.","section":"Definitions 3.4 and 3.5"},{"comment":"The displayed falsification formula (19) should be checked: as printed, the conjunction and disjunction structure does not appear to express a standard falsification query for the Lyapunov conditions on the specified valid region. Please provide the exact SMT formula that was used.","section":"Section III, Nonlinear systems, Eq. (19)"},{"comment":"In Table III, the header \"E(KF)\" should likely read \"EKF\", and the text occasionally refers to figures in an inconsistent order (e.g., \"Figures 2d and 2a\"). These should be corrected for clarity.","section":"Section V"}],"recommendation":"major_revision","confidential_remarks":"The cascade theorem is sound and the linear example is complete, but the nonlinear verification is not global and the reversed Van der Pol example is missing entirely. These are fixable within the paper's scope if the authors provide full verification details, including the state-space region, the local linearization argument with quantitative bounds, and the missing reversed Van der Pol certificate. I would not recommend acceptance in the current form."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this paper has a modestly novel core—deriving an ISS characterization for the error dynamics of a Jordan recurrent network estimator, then checking it with SMT-verified Lyapunov functions—but the nonlinear verification as written does not meet the bar of the theorem it invokes. The gap is load-bearing but repairable.\n\nThe new bit is Section III: rewriting the JRN estimator error as e(t+1)=g(e(t),x(t)) and exploiting the output-to-hidden recurrence so the error dynamics become a discrete-time system with x as input. Theorem 3.6 is the standard cascade ISS + GAS statement, and the proof is correct. The linear case is clean and self-contained: the quadratic Lyapunov function from the discrete Lyapunov equation is genuinely verified. The authors also provide code on GitHub and use an external SMT solver, which counts as real evidence.\n\nThe soft spot is the nonlinear story. For the down pendulum, the ISS-Lyapunov inequality is verified on [-2,2]^2 for the error states only, and no verification details are shown for the reversed Van der Pol example. But Theorem 3.6 concludes global asymptotic stability of the cascade, which needs the ISS property on the whole error state space. The text says a small neighborhood of the origin is excluded and the linearization dominates, with the linear method applied there—but no local Lyapunov computation is reported. That is not a cosmetic omission; it is the step that connects a bounded-box SMT check to a global conclusion. Until that is filled, the claim that the nonlinear JRN estimator errors are asymptotically stable is not established.\n\nThe performance comparison is also thinner than the abstract suggests: JRN beats EKF/UKF on the two nonlinear examples by small margins, and it is slightly worse than KF on the linear mass-spring system. The stability analysis is deterministic, so the noisy RMSE tables are supportive but not the proof. None of this invalidates the core idea; the approach is plausible and the missing pieces are likely in the repository. As written, the paper deserves a serious referee but needs substantial revision: either provide the local linearization details and a global or invariant-region certificate, or honestly restate the contribution as regional stability. I would send it to review, not desk reject, with explicit instructions to check the nonlinear verification.\n\nRecommendation: engage with it, but do not accept until the nonlinear verification is made self-contained.","headline":"The JRN error-dynamics stability analysis is a real but incomplete contribution: the cascade theorem is fine, and the linear case is clean, but the nonlinear verification only checks a bounded box and leaves the excluded-origin linearization argument unstated.","tokens_in":10176,"tokens_out":2498,"would_cite":false,"duration_ms":29630,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93D25","93D30","93B53","93C55","68T07"],"pacs":[],"model":"deepseek-v4-flash","headline":"A Jordan recurrent neural network state estimator is proved to have stable error dynamics—input-to-state stable with the plant state as input—so that when the plant is stable the estimation error converges to zero.","keywords":["Jordan recurrent neural network","state estimation","input-to-state stability","Lyapunov function","error dynamics","neural network verification","SMT solver","nonlinear filtering"],"falsifier":"Sample the decrease condition $V(g(e,x))-V(e)+\\alpha_3(\\|e\\|)-\\gamma(\\|x\\|)\\le 0$ on the down-pendulum example at points outside $[-2,2]^2$ for $e$ and $x$, and run the trained JRN from an initial error larger than 2; a single persistent violation, or a trajectory whose error fails to converge, would refute the claim.","tokens_in":9213,"feed_emoji":"📉","tokens_out":7982,"duration_ms":73716,"temperature":0.7,"pith_summary":"State estimators for nonlinear systems are usually judged by optimality, but a filter that is not stable is useless. This paper argues that a Jordan recurrent neural network (a recurrent net whose feedback path runs from its output back into the hidden layer) is a natural estimator architecture because its error dynamics admit a rigorous input-to-state stability analysis. The central theorem states that if the error system is input-to-state stable with the plant state as input, and the origin of the noise-free plant is globally asymptotically stable, then the cascade's origin is globally asymptotically stable—so the estimation error converges to zero. The paper demonstrates on a linear and two nonlinear examples that the JRN's error dynamics satisfy this condition, verified for the nonlinear cases by a learned ISS-Lyapunov function checked with an SMT solver, and that the JRN matches or outperforms extended and unscented Kalman filters on these examples.","feed_headline":"Neural estimator error provably decays on stable nonlinear systems","feed_subtitle":"JRN beats EKF and UKF on three tests, with an ISS-Lyapunov certificate for convergence.","key_machinery":"The Jordan recurrent network defined by $a(t+1)=\\sigma(W_{ay}y(t+1)+W_{ax}\\hat{x}(t))$ and $\\hat{x}(t+1)=W_{xa}a(t+1)$, whose recurrent connection goes from the previous output to the next hidden layer, is the central object. Substituting the plant and measurement equations turns the estimation error into the discrete-time system $e(t+1)=g(e(t),x(t))$ with $x(t)$ as an input. The paper's main instrument is the ISS-Lyapunov function $V$, satisfying $\\alpha_1(\\|e\\|)\\le V(e)\\le \\alpha_2(\\|e\\|)$ and $V(g(e,x))-V(e)\\le -\\alpha_3(\\|e\\|)+\\gamma(\\|x\\|)$; together with the cascade theorem, this converts a certificate on the error system plus stability of the noise-free plant into a global asymptotic stability certificate for the estimator error.","core_discovery":"The main contribution is an input-to-state stability analysis of the error dynamics of JRN-based estimators. The paper derives the error system $e(t+1)=g(e(t),x(t))$ from the Jordan network's forward propagation and treats the plant state $x(t)$ as an input. Theorem 3.6 shows that if this error system is ISS and the origin of the nominal plant (3) is globally asymptotically stable, then the origin of the combined cascade is globally asymptotically stable. For linear plants the ISS property is certified by a quadratic Lyapunov function obtained from a discrete Lyapunov equation; for nonlinear plants the authors synthesize an ISS-Lyapunov function with a neural network and verify its decrease and bounds constraints with SMT solvers, using linearization near the origin. The conclusion is that the trained JRN estimator, on the tested stable systems, has error dynamics that are asymptotically stable, not merely optimized.","pith_inferences":["The cascade argument would transfer to any recurrent estimator architecture that can be written with state-as-input error dynamics; an LSTM variant would inherit the same stability guarantee if its error system can be shown ISS, which may be harder than for JRNs because of hidden-state recurrence.","The nonlinear examples' numerical verification is carried out on the box $[-2,2]^2$ for the error states and linearized near the origin; a natural stress test is to verify the decrease condition on larger boxes or with a global method, since the paper does not provide a global numerical certificate for the nonlinear cases.","The comparison uses only three benchmark systems, so the observed advantage over EKF and UKF may be particular to low-dimensional, smooth dynamics; testing on higher-order or stiff systems would clarify whether the architecture's structural advantage persists.","The trained ISS-Lyapunov function itself could be reused as a monitoring tool: evaluating $V(e(t))$ online gives a quantitative confidence bound on the estimation error."],"forward_implications":["For any stable plant, a trained bias-free JRN estimator provably drives the estimation error to zero in the noiseless case, rather than merely giving a low mean-square error.","Small process or measurement disturbances produce a bounded error whose size scales with the disturbance level, because the error system is input-to-state stable.","On the three test systems, the JRN achieves lower or comparable root-mean-square error than EKF and UKF while having a much lower online testing cost.","The linear and nonlinear Lyapunov verification procedure supplies a formal stability certificate that can be produced as part of estimator design, not just checked after training.","The same theorem applies to any estimator whose error dynamics are ISS with the plant state as input, so the argument is not limited to the exact network architecture."],"supporting_citations":[{"why":"Provides the discrete-time ISS definitions, the ISS-Lyapunov function characterization, and the quadratic Lyapunov formulas used in the linear case.","marker":"[25]"},{"why":"Supplies the SMT-verified neural Lyapunov function method and algorithm that the paper adapts for nonlinear error dynamics.","marker":"[21]"},{"why":"The SMT solver used to verify the learned ISS-Lyapunov function on the error-state box.","marker":"[27]"},{"why":"Inspires the one-hidden-layer network representation used for the Lyapunov function candidate.","marker":"[26]"},{"why":"Introduces the input-to-state stability property that motivates and frames the main analysis.","marker":"[16]"}],"fun_headline_variants":["ISS proof: Jordan recurrent estimators have stable error dynamics","JRN beats EKF/UKF and gets stability guarantee","Stable nonlinear estimation via Jordan networks with Lyapunov proof","Input-to-state stability certified for Jordan neural estimators","Provable stability of error in Jordan recurrent state estimators"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The nonlinear examples' stability certificate is verified only on a finite box ([-2,2] for the error states) with linearization near the origin; if a violation of the stability condition hides in the unverified region or the linearization argument is incomplete, the claimed asymptotic stability of the JRN error is not established.","fun_headline_variants_meta":{"raw":{"variants":["ISS proof: Jordan recurrent estimators have stable error dynamics","JRN beats EKF/UKF and gets stability guarantee","Stable nonlinear estimation via Jordan networks with Lyapunov proof","Input-to-state stability certified for Jordan neural estimators","Provable stability of error in Jordan recurrent state estimators"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000448,"raw_usage":{"total_tokens":2237,"prompt_tokens":900,"completion_tokens":1337,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":516,"completion_tokens_details":{"reasoning_tokens":1258}},"tokens_in":516,"tokens_out":1337,"duration_ms":12029,"temperature":1.0,"reasoning_tokens":1258,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-08T22:21:21.819542+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Sample the decrease condition $V(g(e,x))-V(e)+\\alpha_3(\\|e\\|)-\\gamma(\\|x\\|)\\le 0$ on the down-pendulum example at points outside $[-2,2]^2$ for $e$ and $x$, and run the trained JRN from an initial error larger than 2; a single persistent violation, or a trajectory whose error fails to converge, would refute the claim.","supporting_citations":[{"cited_title":"Input-to-state stability for discrete-time nonlinear systems,","cited_arxiv_id":null,"evidence_quote":"Provides the discrete-time ISS definitions, the ISS-Lyapunov function characterization, and the quadratic Lyapunov formulas used in the linear case."},{"cited_title":"Physics-informed neural network Lyapunov functions: PDE characterization, learning, and verification,","cited_arxiv_id":null,"evidence_quote":"Supplies the SMT-verified neural Lyapunov function method and algorithm that the paper adapts for nonlinear error dynamics."},{"cited_title":"dreal: An SMT solver for nonlinear theories over the reals,","cited_arxiv_id":null,"evidence_quote":"The SMT solver used to verify the learned ISS-Lyapunov function on the error-state box."},{"cited_title":"FOSSIL: a software tool for the formal synthesis of Lyapunov func- tions and barrier certificates using neural networks,","cited_arxiv_id":null,"evidence_quote":"Inspires the one-hidden-layer network representation used for the Lyapunov function candidate."},{"cited_title":"On the input-to-state stability property,","cited_arxiv_id":null,"evidence_quote":"Introduces the input-to-state stability property that motivates and frames the main analysis."}],"review_version":1}