{"id":"5a71f763-c01b-48d8-94ec-2b5af7fce020","arxiv_id":"2412.02807","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":6,"one_line_summary":"A Koopman-generator framework jointly learns an unknown continuous-time vector field and a Lyapunov function, then formally verifies a less conservative region of attraction using an SMT solver.","lead":"This paper learns a model of an unknown nonlinear system and a Lyapunov stability certificate from low-frequency trajectory data, then verifies the certificate with a formal SMT solver. The same data and dictionary are reused for both tasks, and the resulting certified safe regions are larger than those from quadratic certificates on the two test systems.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The certificate for the true system requires oracle knowledge: the true Lipschitz constant K_f and the sampled model error alpha are not obtainable from trajectory data, so the advertised formal guarantee for genuinely unknown systems is not realized as presented.","rationale":"The reader's verdict identifies Assumption 4.1 as the weakest assumption and mentions the known Lipschitz constant as a related premise. My reading agrees that the local ROA assumption is asserted rather than proved, but the more load-bearing issue is the global verification step in Proposition 4.2: the inequality that bridges the learned model and the true system requires K_f and alpha, both properties of the unknown vector field. These quantities appear directly in the margin condition (11), so without data-driven bounds or explicit prior knowledge the advertised formal certificate cannot be executed for a truly unknown system. The numerical examples sidestep this by using the benchmark's true equations to set K_f and alpha, which is legitimate for a proof of concept but not for the paper's stated claim. The paper otherwise has independent support: the resolvent-type generator learning is based on prior work with convergence guarantees, and the SMT-based verification of the learned Lyapunov function against the identified model is concrete and reproducible via the provided code. The central construction is coherent, but the guarantee for the true system is conditional on unverified oracle inputs. This supports the reader's CONDITIONAL verdict; no change is needed.","tokens_in":11232,"tokens_out":7838,"duration_ms":78860,"concrete_test":"Re-run the reversed Van der Pol experiment with K_f and alpha estimated entirely from trajectory data: estimate K_f via pairwise Lipschitz bounds on sampled trajectories and estimate alpha from held-out trajectory prediction errors of f_hat, instead of evaluating the true f. Then check whether the published V and beta still satisfy ((K_f + K_f_hat)*delta + alpha)*nu < beta and whether (9) remains verifiable over the same annulus. If the inequality fails or the certified ROA shrinks below the quadratic baseline, the advertised guarantee depends on oracle knowledge; if it passes with margin, the concern is largely resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Proposition 4.2's error propagation in (10)-(11) requires three quantities that the pipeline cannot extract from trajectory data alone: the true vector field's Lipschitz constant K_f, the pointwise model error alpha = max_{y in Y} ||f(y) - f_hat(y)|| at sampled states, and, via Assumption 4.1, the guarantee that the quadratic sublevel set O from the identified linearization is a true ROA for the unknown system. Section VI-A explicitly states 'We assume that the Lipschitz constant K_f is known,' and Tables I and II set K_f equal to K_f_hat; alpha is computed from the true vector field at samples. For a genuinely unknown system, none of these values is available. If K_f or alpha are underestimated, the inequality ((K_f + K_f_hat)*delta + alpha)*nu < beta may fail, and the SMT verification of (9) is performed only against the learned model f_hat, not against the true f. Assumption 4.1 is the local instance of the same gap: it asserts, without proof, that identification near the origin is accurate enough for O to be a true ROA. Thus the central claim of formally verified certificates for unknown systems is contingent on unobservable oracle information; this is not an internal inconsistency but a missing component in the data-driven guarantee.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript presents an integrated data-driven framework for simultaneously identifying the vector field of an unknown continuous-time nonlinear system and constructing Lyapunov/Zubov functions, using a learned finite-dimensional approximation of the Koopman generator. The identified generator is used both to approximate the vector field and to solve the Lyapunov and Zubov PDEs in a least-squares sense. The learned Lyapunov function is then verified with SMT solvers, and Proposition 4.2 is stated as the formal bridge: under Assumption 4.1 and bounds on mesh size, model error, Lipschitz constants, and verification margin, a sublevel set of the learned candidate is claimed to be a region of attraction for the true system. Numerical experiments on the reversed Van der Pol oscillator and a two-machine power system report less conservative certified ROAs than quadratic and neural-network baselines.","tokens_in":11545,"tokens_out":5003,"duration_ms":50834,"significance":"The paper addresses a genuine gap: existing Koopman-based Lyapunov constructions either lack formal verification or cannot be integrated with system identification. The proposed reuse of a common dictionary for generator learning and PDE solving is elegant, and the explicit error-propagation statement in Proposition 4.2 is a useful template for data-driven certificates. The authors ship code and use SMT verification, which is a strength. However, the advertised guarantee for unknown systems is conditionally formulated: the certificate requires quantities that the pipeline does not compute from trajectory data (Assumption 4.1, K_f, alpha), and the SMT checks are performed against the learned model rather than the true system. The value of the contribution will be realized once these oracle quantities are replaced by data-driven, verifiable bounds or the claims are reframed accordingly.","major_comments":[{"comment":"Assumption 4.1 is the anchor of Proposition 4.2 and is asserted rather than established. The text states that the assumption 'can typically be satisfied' by collecting data around the origin, and Section VI-A only says 'we verified that Assumption 4.1 indeed holds in this case' without giving a procedure. Because Proposition 4.2's conclusion is convergence to O, not to the origin, failure of Assumption 4.1 would leave only a certificate of convergence to a neighborhood. The paper needs a verifiable data-driven condition (or a rigorous numerical check) that O is a ROA for the true system, or the theorem should be restated with this as an explicit hypothesis and the main claim adjusted.","section":"§IV, Assumption 4.1"},{"comment":"The formal guarantee for the true system requires quantities that are not available from trajectory data alone. The proof of (10)-(11) uses the true Lipschitz constant K_f and the sampled model error alpha = max_y ||f(y) - f_hat(y)||; Section VI-A states 'We assume that the Lipschitz constant K_f is known,' and Tables I and II set K_f equal to K_f_hat. For a genuinely unknown system these values are oracle information, and underestimating either can violate the inequality ((K_f + K_f_hat)delta + alpha)nu < beta. The paper should provide certified upper bounds on K_f and alpha from the finite trajectory data, or explicitly characterize the theorem as conditional on these data-independent quantities.","section":"§IV, Prop. 4.2; §VI-A, Tables I-II"},{"comment":"The SMT verification in the experiments checks inequality (9) for the learned vector field f_hat, not for the true f. The proof bridges to the true system only through (11), which depends on the global bound on ||f - f_hat|| over the relevant domain. Without a certified bound on that model error, the SMT certificate does not transfer to the unknown system; the experiments therefore demonstrate a certificate for the identified model, not for the true system as claimed in the abstract.","section":"§VI-A, Eq. (9)"},{"comment":"The paper does not propagate the approximation error from the Koopman generator (Theorem 3.1) and the dictionary truncation to the identified vector field. Theorem 3.1 bounds ||L_{lambda,tau_s} - L_lambda|| on C^1(X), but no corresponding bound on alpha = max ||f - f_hat|| is derived in terms of the number of samples M, the dictionary size N, or the quadrature error. As a result, the main theorem's assumption on alpha is not connected to the actual learning pipeline, and the numerical values of alpha in Tables I-II are computed from the true model.","section":"§III, Theorem 3.1 and Eq. (8)"}],"minor_comments":[{"comment":"There is a typo in 'Lyapunov euqation'; it should read 'Lyapunov equation'.","section":"Assumption 4.1"},{"comment":"The statement 'Then D = D if and only if' is circular as written; one of the two D symbols should refer to the domain of attraction explicitly, e.g., 'D = D_A'.","section":"Theorem 2.5"},{"comment":"The caption says 'red dot-dashed circle' for the set X, but the experimental domain X = [-1.2,1.2]^2 is a square; the caption should say 'rectangle' or 'boundary of X' as appropriate.","section":"§VI-A and Figure 1"},{"comment":"The claim that 'beta is reduced by a factor of 1/10' is stated without a comparison baseline; please specify the baseline value and the context so the reader can interpret the improvement.","section":"§VI-A"},{"comment":"The first numerical example uses a monomial dictionary selected with prior knowledge that the system is polynomial, which is a form of model information; the paper should clarify that the 'unknown' setting still permits structural priors, otherwise the claim of identifying a fully unknown system is overstated.","section":"§V-C and §VI-A"}],"recommendation":"major_revision","confidential_remarks":"The paper is well structured and the core methodology is promising, but the abstract and introduction overstate the formal guarantee by omitting that the certificate depends on oracle quantities (K_f, alpha, and Assumption 4.1). I recommend major revision rather than rejection because the missing data-driven bounds may be addable in a revision. The comparison with [30] also uses different data regimes and priors, so the efficiency and generality claims should be contextualized."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing you should know: this is a sensible integration of three existing pieces—resolvent-based Koopman generator learning [18], PDE-based Lyapunov/Zubov solving [11], and SMT verification [10]—and the authors reuse the same observable dictionary and data subset for both identification and certificate search. That is a genuine contribution, more than a trivial combination, because the PDE solving is designed around the learned generator. The numerical results on two 2D systems are plausible and show larger certified ROAs than quadratic baselines and one neural baseline. Prop 4.2 is a correct error-propagation argument: given a mesh size delta, a pointwise model error alpha, a global gradient bound nu, and a decay margin beta, the true Lyapunov derivative is negative on the annulus. So the internal logic is fine.\n\nThe soft spot is exactly where the stress test lands. The certificate for the true system requires quantities that the pipeline never extracts from trajectory data. K_f, the true Lipschitz constant, is assumed known and set equal to K_f_hat in both tables. alpha is computed using the true vector field at sample points. And Assumption 4.1—that the quadratic sublevel set from the identified linearization is a true ROA—is asserted and only 'verified' informally in Section VI-A. All three are unobservable for a genuinely unknown system. If you do not know f, you cannot compute alpha or K_f, and you cannot certify Assumption 4.1. So the central claim of formally verified certificates for unknown systems is not realized as stated. The paper would be honest if it framed this as: given a priori bounds on K_f and alpha, and given enough data to satisfy Assumption 4.1, the SMT check against f_hat plus the error bound yields a true ROA. That is a meaningful conditional result, but it is not what the abstract promises.\n\nOne more thing: the experiments are only 2D, no error bars, and no comparison against the closest baseline [16], which is a missed opportunity. The code is available, and the parameter tables are explicit, so the work is reproducible, and that counts.\n\nWho gets value: researchers in Koopman-based learning and Lyapunov verification who want a concrete pipeline and a clean statement of what is missing to close the loop. It deserves a serious referee, but the author team should be pushed to either remove the oracle assumptions by estimating bounds from finite data, or reposition the contribution as a conditional certificate with prior bounds. I would not cite this for 'formal guarantees for unknown systems' as it now stands; I would cite it as a well-executed integration that clarifies the gap.","headline":"The integration is real and the error-propagation argument is sound, but the advertised formal guarantee for unknown systems rests on oracle quantities (K_f, alpha, and Assumption 4.1) that the pipeline never actually obtains from data.","tokens_in":12061,"tokens_out":2088,"would_cite":false,"duration_ms":19823,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93D30","93B30","93D20","37N35"],"pacs":[],"model":"deepseek-v4-flash","headline":"One pipeline learns unknown dynamics, proves stability from data","keywords":["Koopman generator","Lyapunov function learning","region of attraction","Zubov equation","system identification","SMT verification","continuous-time nonlinear systems","trajectory data"],"falsifier":"Run the framework on a known benchmark system where the true vector field and its Lipschitz constant are known, and deliberately sample too sparsely near the origin so that the identified linearization's sublevel set is not a true region of attraction. If the SMT-verified $\\Omega_{c_2}$ still passes verification but simulated trajectories from points inside it do not converge to the origin, the certificate chain has a hole at Assumption 4.1. Alternatively, compare the certified region of attraction with the true domain of attraction on a system with a known maximal Lyapunov function: the ratio of their volumes is a direct quantitative check.","tokens_in":11009,"feed_emoji":"📈","tokens_out":6652,"duration_ms":64463,"temperature":0.7,"pith_summary":"This paper proposes a framework that, from trajectory data collected at a relatively low sampling frequency, simultaneously learns the vector field of an unknown continuous-time nonlinear system and learns a Lyapunov function certifying its stability. The key idea is to learn the Koopman generator—the infinitesimal generator of the flow—and use that same learned operator both to reconstruct the dynamics and to solve stability-related PDEs, specifically the Zubov equation, whose solution encodes the domain of attraction. The learned Lyapunov function is then checked with an SMT solver, giving a formal guarantee that a certain sublevel set is a genuine region of attraction for the true, unknown system. If the framework works as claimed, a user with modest data can obtain a certified region of attraction for a black-box system without knowing its equations.","feed_headline":"One pipeline learns unknown dynamics, proves stability from data","feed_subtitle":"Low-frequency trajectory data can yield a formally certified region of attraction for a black-box system.","key_machinery":"The load-bearing object is the Koopman generator $L$, defined by $Lh = \\nabla h \\cdot f$, whose finite-sample approximation is built through a resolvent-type least-squares problem. Because the coordinate functions $x_i$ are included in the dictionary, rows of the same learned generator directly give the identified vector field $\\hat{f}$; the same generator and dictionary are reused to solve the linear PDEs $LV = -\\eta$ and $LW = -\\eta(1-W)$, where the latter is the Zubov equation. Proposition 4.2 is the bridge turning the approximate PDE solution into a certificate: it converts a bound on the residual of the Lyapunov derivative into a bound on the true derivative via the triangle inequality, so the annular condition together with Assumption 4.1 yields a true region of attraction.","core_discovery":"The central claim is that a single data-driven pipeline can replace separate system identification and stability analysis: with a shared dictionary of observable functions, the Koopman generator learned from trajectory snapshots yields both an identified vector field and a solution of the Zubov equation. Proposition 4.2 states the precise certificate: if the sample mesh spacing $\\delta$, the identification error $\\alpha$ on the samples, the Lipschitz constants $K_f$ and $K_{\\hat{f}}$ of the true and learned vector fields, and the gradient bound $\\nu$ satisfy $((K_f + K_{\\hat{f}})\\delta + \\alpha)\\nu < \\beta$ on the annular region $c_1 \\leq V(x) \\leq c_2$, and the learned Lyapunov function $V$ satisfies $\\nabla V \\cdot \\hat{f} \\leq -\\beta$ there, then the sublevel set $\\Omega_{c_2} = \\{V \\leq c_2\\}$ is a region of attraction for the true system, provided Assumption 4.1 holds—that the identified linearization's quadratic sublevel set is already a true region of attraction near the origin. The paper demonstrates on two examples, a reversed Van der Pol oscillator and a two-machine power system, that the certified regions of attraction are less conservative than those from quadratic Lyapunov functions and from a prior neural-network approach, while using far fewer samples.","pith_inferences":["If the certified region of attraction is to be trusted for a truly black-box system, the true Lipschitz constant $K_f$ must be estimated or bounded from data, since the paper treats it as known; a practical extension would supply a data-driven Lipschitz bound with its own confidence interval.","The gap between the verified condition and the true Lyapunov inequality is controlled by $\\beta$, which is reduced by an order of magnitude in the examples; pushing this margin smaller is a quantitative target for data collection and dictionary design.","The modular separation suggests a testable comparison: using the learned generator for the Zubov equation versus solving the same PDE directly with a separately identified vector field, to isolate which component gives the larger certified region of attraction.","The method's ability to certify outside the sampled region suggests that dictionary choice, not sample count, may be the dominant factor in region-of-attraction quality."],"forward_implications":["Low-frequency trajectory data suffice: in the polynomial example, 100 sampled initial conditions replace millions of labeled samples used by a neural benchmark.","The same learned generator serves two purposes, so identification and stability certification share one computation and one dictionary.","Formal SMT verification of the learned function yields a certified region of attraction for the unknown system, not just for the fitted model.","Because the Zubov equation is solved rather than only the Lyapunov inequality, the certified region of attraction can approach the true domain of attraction as approximation improves.","The framework is modular: if the vector field is identified by another technique, the learned generator can still be used purely for solving the stability PDEs."],"supporting_citations":[{"why":"Supplies the resolvent-type method for learning the Koopman generator and identifying the vector field that the framework reuses and extends.","marker":"[18]"},{"why":"Provides the PDE characterization of Lyapunov functions, the residual and boundary-condition formulation, and the learning and verification pipeline adapted here.","marker":"[11]"},{"why":"Gives Zubov's theorem, the equation whose solution encodes the domain of attraction and is solved with the learned generator.","marker":"[31]"},{"why":"The toolbox used to find and verify polynomial and neural Lyapunov functions; supplies the SMT-based verification of the Lyapunov derivative condition.","marker":"[10]"},{"why":"A neural-network method for unknown systems with formal closed-loop guarantees; used as the baseline for sample count, region-of-attraction size, and computational time.","marker":"[30]"},{"why":"A prior Zubov-Koopman approach for learning regions of attraction that requires a smoothing step and lacks verification, motivating the integrated framework.","marker":"[16]"},{"why":"The SMT solver used for interval analysis to compute the Lipschitz and gradient bounds and for formal verification.","marker":"[5]"}],"fun_headline_variants":["Data-driven Koopman pipeline certifies stability from sparse trajectories","Learn dynamics and Lyapunov functions from low-frequency data","Koopman generator plus neural Lyapunov gives formal stability proofs","Certified region of attraction from sparse trajectory data alone","Single pipeline learns unknown dynamics and proves stability"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The guarantee rests on Assumption 4.1: the data-driven model must already be accurate enough near the origin that the quadratic sublevel set of its linearization is a true region of attraction for the real system, and the paper also treats the true Lipschitz constant as known; if either gives way, the certificate only proves convergence to that inner set, not to the origin.","fun_headline_variants_meta":{"raw":{"variants":["Data-driven Koopman pipeline certifies stability from sparse trajectories","Learn dynamics and Lyapunov functions from low-frequency data","Koopman generator plus neural Lyapunov gives formal stability proofs","Certified region of attraction from sparse trajectory data alone","Single pipeline learns unknown dynamics and proves stability"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000574,"raw_usage":{"total_tokens":2726,"prompt_tokens":979,"completion_tokens":1747,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":595,"completion_tokens_details":{"reasoning_tokens":1667}},"tokens_in":595,"tokens_out":1747,"duration_ms":11804,"temperature":1.0,"reasoning_tokens":1667,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T23:05:15.332935+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the framework on a known benchmark system where the true vector field and its Lipschitz constant are known, and deliberately sample too sparsely near the origin so that the identified linearization's sublevel set is not a true region of attraction. If the SMT-verified $\\Omega_{c_2}$ still passes verification but simulated trajectories from points inside it do not converge to the origin, the certificate chain has a hole at Assumption 4.1. Alternatively, compare the certified region of attraction with the true domain of attraction on a system with a known maximal Lyapunov function: the ratio of their volumes is a direct quantitative check.","supporting_citations":[{"cited_title":"Resolvent- type data-driven learning of generators for unknown continuous-time dynamical systems","cited_arxiv_id":null,"evidence_quote":"Supplies the resolvent-type method for learning the Koopman generator and identifying the vector field that the framework reuses and extends."},{"cited_title":"Tool LyZNet: A lightweight Python tool for learning and verifying neural Lyapunov functions and regions of attraction","cited_arxiv_id":null,"evidence_quote":"The toolbox used to find and verify polynomial and neural Lyapunov functions; supplies the SMT-based verification of the Lyapunov derivative condition."},{"cited_title":"Neural lyapunov control of unknown nonlinear systems with stability guaran- tees","cited_arxiv_id":null,"evidence_quote":"A neural-network method for unknown systems with formal closed-loop guarantees; used as the baseline for sample count, region-of-attraction size, and computational time."},{"cited_title":"Learning Regions of Attraction in Unknown Dynamical Systems via Zubov-Koopman Lifting: Regularities and Convergence","cited_arxiv_id":"2311.15119","evidence_quote":"A prior Zubov-Koopman approach for learning regions of attraction that requires a smoothing step and lacks verification, motivating the integrated framework."},{"cited_title":"dReal: An SMT Solver for Nonlinear Theories over the Reals","cited_arxiv_id":null,"evidence_quote":"The SMT solver used for interval analysis to compute the Lipschitz and gradient bounds and for formal verification."}],"review_version":1}