{"id":"ec6d179a-8e13-43a3-8937-a926e06126ba","arxiv_id":"2505.03493","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"Iteratively refining the tessellation and data converts locally failed piecewise affine Lyapunov certificates into nested level sets that jointly certify attraction to the equilibrium.","lead":"This paper presents an iterative, data-driven algorithm that refines a piecewise linear Lyapunov certificate together with the sampling mesh and data, so that each round certifies the region left uncertified by the previous round. The scheme is demonstrated on a damped pendulum where the original fixed-data method left a diagonal strip uncertified.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Algorithm 1's refinement loop is not proven to terminate; the abstract's 'whenever' overclaims because no existence theorem guarantees the required inclusions after restart.","rationale":"The reader's weakest_assumption identified the lack of assurance that iterative refinement always succeeds. I agree that this is the most load-bearing concern because the paper's abstract and stated contribution ('whenever certificates are violated locally, a refinement ... is produced, thus leading to an improvement') is exactly this algorithmic guarantee, yet no proof of termination or eventual success is supplied. The paper explicitly mentions failure modes and says to 'restart ... until a better and valid result is generated', which is an unsupported assumption. Moreover, the success of refinement is contingent on the uncertified regions being contained in the true region of attraction; if they are not, no data density or tessellation can help. This is a fundamental limitation that the pendulum example does not address, as its initial tessellation is derived from a known Lyapunov function. The conditional Theorem 1 itself appears sound, relying on the imported certificate property from [13, Appendix A], so the verdict should remain CONDITIONAL: the paper's results are correct under the stated assumptions, but the central algorithmic claim needs a termination proof or an explicit caveat. No reason to reject the paper outright, as the conditional contribution has value, but the overclaim in the abstract should be tempered.","tokens_in":8696,"tokens_out":17130,"duration_ms":152471,"concrete_test":"Run Algorithm 1 on the damped pendulum (5) with the initial set X = [-3.5, 3.5] × [-3.5, 3.5], which strictly contains the true region of attraction and includes the saddle equilibria at (±π, 0). If the algorithm does not terminate within kmax iterations (e.g., kmax = 20) or fails to produce a final C_K ⊂ A0, this confirms that the refinement loop is not guaranteed to succeed for sets that extend beyond the true ROA, directly testing the 'whenever' claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central contribution is the iterative refinement in Algorithm 1. The abstract claims that 'whenever' certificates are violated locally, a refinement is produced that improves the region of attraction. However, Algorithm 1 itself acknowledges failure modes: if no β_{k+1} ≥ 1 exists such that β_{k+1} C_k ⊂ L^{V_k}_{α_k}, or if no α_{k+1} with C_k ⊂ L^{V_{k+1}}_{α_{k+1}} exists, the iteration fails and must be restarted with a finer tessellation and richer data. No proof, argument, or bound is given that such restarts eventually succeed. In fact, success is only possible if every C_k is contained in the true region of attraction of the equilibrium. If the initial set X or any uncertified region C_k intersects the complement of the true ROA, then no amount of refinement can produce the required Lyapunov certificate, and the algorithm will loop indefinitely without satisfying the hypotheses of Theorem 1. The theorem is conditional and does not address termination; the single pendulum example, whose initial tessellation is informed by a known quadratic Lyapunov function, does not exercise the non-terminating regime. This gap between the advertised 'whenever' contribution and the proven conditional result is load-bearing.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper addresses data-driven certification of the region of attraction for an unknown continuous-time dynamical system, assuming only pointwise evaluations of the vector field and a known Lipschitz bound. It builds on the PWA Lyapunov-function construction of [13], in which an SOCP is solved over a tessellation, and proposes an iterative refinement scheme (Algorithm 1): when the optimization leaves some vertices uncertified, the algorithm forms a convex hull of the uncertified region, rescales it, refines the tessellation and dataset, and repeats until the uncertified set is absorbed into the known attracted neighborhood. Theorem 1 states a conditional inclusion-based guarantee for the nested sublevel sets, and the method is demonstrated on a damped pendulum example, including a briefly reported fully data-driven run.","tokens_in":8993,"tokens_out":9635,"duration_ms":89260,"significance":"If the iterative refinement can be guaranteed to make progress, the approach is valuable: it avoids semidefinite programming, produces patchy PWA certificates, and the numerical section includes a fully data-driven run that is independent of the model-seeded run, which is a genuine strength. However, the central contribution as advertised in the abstract is stronger than what is proven. Theorem 1 is a conditional statement that assumes the very nested inclusions that Algorithm 1 is supposed to produce, and no termination or progress guarantee is established for the refinement loop. The manuscript therefore provides a plausible algorithmic framework with a conditional certificate and one numerical demonstration, rather than the 'whenever' theorem promised in the abstract.","major_comments":[{"comment":"The abstract claims that 'whenever those certificates are violated locally, a refinement of the domain and the associated tessellation is produced, thus leading to an improvement'. In Algorithm 1, however, if no β_{k+1} exists with X_{k+1}=β_{k+1}C_k ⊂ L^{V_k}_{α_k}, or if no α_{k+1} exists with C_k ⊂ L^{V_{k+1}}_{α_{k+1}}⊂X_{k+1}, the iteration is declared failed and restarted with a finer tessellation and richer data. No argument, bound, or additional assumption is given that such restarts terminate. In fact, if any C_k intersects the complement of the true region of attraction, no amount of refinement can produce the required Lyapunov certificate, so the algorithm may loop indefinitely without ever satisfying the hypotheses of Theorem 1. This gap between the advertised contribution and the conditional theorem is load-bearing and needs to be addressed, either by proving a progress guarantee under explicit assumptions or by restricting the claims accordingly.","section":"Section 3.1 / Algorithm 1"},{"comment":"The statement 'By design of constraint (3e) (see [13, Appendix A] for details), we can certify that ∀x∈X\\C, ∇V(x)^T f(x)<0' is essential for Theorem 1 but is not justified in the manuscript. Since C is defined as the convex hull of A and the uncertified vertices, a simplex that has one uncertified vertex is not necessarily contained in C, and the implication from negative slacks at vertices to negativity of ∇V^T f on the whole set X\\C is nontrivial. The manuscript should either state the precise imported result from [13, Appendix A] and verify its hypotheses, or provide a self-contained proof; as written, the induction in Theorem 1 rests on an unstated and unchecked implication.","section":"Section 3.1, Eq. (7) and following paragraph"},{"comment":"Algorithm 1 is not well-posed in the first loop iteration. The pseudocode tests 'if C_{k−1} ⊈ L^{V_k}_{α_k}' and at k=0 this refers to C_{−1}, which is never defined or initialized. The figures label the first iteration as k=0, and the surrounding text describes a first iteration producing C_0. A base case or initialization must be supplied so that the algorithm can be executed, otherwise the pseudocode as written is ill-posed.","section":"Algorithm 1"},{"comment":"The theorem states that the base case is 'C_K = A_K (no non-negative slack variable)', but by equation (7), if no slack is nonnegative then N is empty and C_K = conv(A_K), which equals A_K only when A_K is convex. Assumption 3 only requires A to be a polyunion and does not assume convexity. The proof's statement 'Suppose that K=0. Then, C_0=A_0 i.e. all slack variables in problem (3) are negative' is therefore not valid as written. Either convexity of A must be added to the assumptions, or the theorem and proof must be rephrased to handle C_K = conv(A_K).","section":"Theorem 1"},{"comment":"The numerical validation is limited in two ways that affect the strength of the paper's central claim. First, the main simulation uses an initial tessellation informed by a known quadratic Lyapunov function for the exact model (Section 3.1), which is a model-based seed rather than a purely data-driven start. Second, the fully data-driven run is only mentioned in a single sentence and in Figure 7, without specifying its initialization, data counts, tessellation, or the number of iterations beyond 'one more iteration'. Since the paper's stated scope is the unknown-dynamics setting, the validation would be substantially stronger if the fully data-driven experiment were described and reported with the same detail as the model-informed run.","section":"Section 4"}],"minor_comments":[{"comment":"The abstract and conclusion use 'whenever' to describe the refinement guarantee, but Theorem 1 is conditional and Algorithm 1 contains failure branches that are handled heuristically. The wording should be aligned with the actual proven statements.","section":"Abstract and Section 5"},{"comment":"Assumption 3 states that 'a fixed dataset D of the system is available', while Algorithm 1 requires generating and refining datasets D_k at each iteration. This apparent inconsistency should be clarified: is the assumption about the initial dataset only, or is the dataset allowed to be augmented?","section":"Assumption 3 vs. Algorithm 1"},{"comment":"The sentence 'According to [13, Appendix B], a dataset and a tessellation providing enough covering of the set X\\A are bound to bring forth a certified Lyapunov function' is informal. Please state the precise theorem from [13, Appendix B] so that the reader can see exactly which sufficient condition is being invoked and in what sense it is not 'sufficient for the algorithm's convergence to optimality'.","section":"Section 2.3, last paragraph"}],"recommendation":"major_revision","confidential_remarks":"The paper's core idea is interesting and likely publishable after a substantive revision, but the current manuscript does not prove the advertised 'whenever' contribution. The termination issue is the main concern: without a progress guarantee, Algorithm 1 is a heuristic whose success is only demonstrated on one example. The authors should either prove termination under explicit hypotheses (e.g., that X is contained in the true region of attraction and that the data/tessellation refinement satisfies a quantified density condition) or clearly present the result as a conditional framework with a weaker claim. I would also encourage the authors to include the precise statements of the results imported from [13], since the proof of Theorem 1 depends on them."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The new thing here is the large-to-small iteration: when the SOCP certificate leaves an uncertified region, you scale up the convex hull of the non-certified vertices, refine the tessellation and data, and recompute. That is a genuine extension of Tacchi et al.'s fixed-data method, and the conditional Theorem 1 is correct: if the nested inclusions C_{k-1} ⊂ L^{V_k}_{α_k} ⊂ X_k ⊂ L^{V_{k-1}}_{α_{k-1}} hold, then the initial level set is in the region of attraction. The paper also does the right thing by reporting a fully data-driven run that converges without model-informed initialization, even if it takes one more iteration.\n\nThe soft spots are real but not fatal. The abstract says 'whenever those certificates are violated locally, a refinement is produced,' but Algorithm 1 explicitly allows failures: if no β_{k+1} or α_{k+1} exists, the iteration restarts with a finer tessellation and richer data. No proof is given that such restarts succeed, and in fact they cannot succeed if any uncertified region C_k intersects the complement of the true region of attraction. The theorem is conditional on inclusions the algorithm is not guaranteed to produce. The paper is honest about the failure modes in the body, so the gap is one between the advertised contribution and the proven result rather than a hidden error. The numerical validation is a single pendulum example with no error bars, no quantitative comparison, and no code; the model-informed initial tessellation is a sanity check, and the fully data-driven run helps, but the evidence is thin.\n\nDespite these gaps, the core idea is sound and the conditional theorem is a useful certificate structure. The termination/existence question is the main thing a referee should push on. I would send this to peer review, with the expectation that the authors either prove a reasonable existence condition for refinement or substantially soften the 'whenever' claim and present the restarts as heuristic. The paper is worth engaging with; it just needs to be more precise about what is guaranteed.","headline":"A useful iterative extension of the SOCP-based Lyapunov certification method, but the abstract overclaims: the refinement loop has no termination proof and can fail whenever the uncertified region leaves the true region of attraction.","tokens_in":9475,"tokens_out":2219,"would_cite":true,"duration_ms":22947,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93D05","93D30","93C10"],"pacs":[],"model":"deepseek-v4-flash","headline":"Data-driven Lyapunov certificates can be extended iteratively by refining tessellation and data wherever a local certificate failure appears.","keywords":["data-driven stability analysis","piecewise affine Lyapunov function","region of attraction","iterative refinement","tessellation","second-order cone programming","patchy Lyapunov functions","dataset refinement"],"falsifier":"Run the iterative loop on a system whose region of attraction is a known nonconvex set with a cusp or fractal boundary, for example a periodically forced pendulum, using a fixed Lipschitz bound and a coarse initial dataset; if the loop enters its \"iteration failed, restart with finer mesh\" branch indefinitely and never produces a finite chain satisfying $C_{k-1}\\subset L^{V_k}_{\\alpha_k}\\subset X_k$ for all $k$ up to $C_K\\subset A_0$, then the assumed eventual success of refinement under condition (4) would be disproved for that setting.","tokens_in":8521,"feed_emoji":"🔄","tokens_out":13948,"duration_ms":114402,"temperature":0.7,"pith_summary":"This paper claims that an unknown dynamical system's region of attraction can be certified sequentially from point evaluations of its right-hand side, even when a first data-driven Lyapunov certificate fails in part of the region. The proposed loop re-runs the same optimisation-based piecewise affine (PWA) Lyapunov construction on a smaller, refined domain: it identifies the uncertified polyunion, shrinks the working set around it, densifies the tessellation and dataset, and repeats until the leftover uncertified region lies inside the already-known attracted neighbourhood. Theorem 1 states that, under the nested-inclusion conditions produced by the loop, the outermost level set of the first Lyapunov function is attracted to the equilibrium along the unknown dynamics. A local failure therefore no longer forces a global restart; it becomes the trigger for a targeted local refinement.","feed_headline":"Refine where stability checks fail to certify regions of attraction","feed_subtitle":"Iterating on refined regions turns local Lyapunov failures into a certified region of attraction.","key_machinery":"The central mechanism is the nested-inclusion chain of sublevel sets. Each iteration builds a PWA Lyapunov candidate $V_k$ with affine pieces $g_c^T x+b_c$ on triangular cells, computes slack variables $s_{i,c}$ from the second-order cone problem, and forms an uncertified region $C_k$ as the convex hull of $A_k$ and all vertices whose slacks satisfy $s_{i,c}\\ge0$. The next iteration's upscaling factor $\\beta_{k+1}$ picks $X_{k+1}=\\beta_{k+1}C_k$ inside $L^{V_k}_{\\alpha_k}$, so the new level set contains the previous failure region and remains inside the previous certificate. This produces a decreasing sequence of invariant sets, and Theorem 1 carries the attractivity of the innermost set back to $L^{V_0}_{\\alpha_0}$.","core_discovery":"The central claim is an iterative nesting theorem: if each new Lyapunov candidate $V_k$ admits a level $\\alpha_k$ with $C_{k-1}\\subset L^{V_k}_{\\alpha_k}\\subset X_k\\subset L^{V_{k-1}}_{\\alpha_{k-1}}$ for all $k$, and the final uncertified set satisfies $C_K\\subset A_0$, then $L^{V_0}_{\\alpha_0}$ is attracted to $0$. The loop achieves these inclusions by setting $X_{k+1}=\\beta_{k+1}C_k$ with the largest $\\beta_{k+1}\\geq1$ that keeps $X_{k+1}$ inside $L^{V_k}_{\\alpha_k}$, choosing a smaller prior attracted set $A_{k+1}\\subset A_k$, refining the triangular tessellation and dataset, and recomputing the PWA Lyapunov function. The numerical section demonstrates the construction on the damped pendulum, where five iterations eliminate the previously uncertified diagonal band; a fully data-driven run that does not use the model to choose the tessellation also converges in one extra step.","pith_inferences":["The paper leaves discrete and controlled systems as future work, but the proof mechanism suggests the nesting argument extends to discrete-time systems under the analogous one-step Lyapunov inequality.","The maximal upscaling factor $\\beta_{k+1}$ could double as an adaptive step-size signal: if the best $\\beta_{k+1}$ is close to 1, the failure region is near the boundary of the current certificate, suggesting the next refinement should concentrate on that boundary.","In the pendulum example the failure is concentrated where large-magnitude data points dominate the optimisation, so one may read the algorithm as an active data-acquisition rule: points near the uncertified vertices matter more than global coverage.","A testable prediction is that the number of iterations scales with the geometric complexity of the basin boundary; systems with highly nonconvex or fractal boundaries should need more refinement rounds than systems with polytopic basins."],"forward_implications":["The method certifies the whole outer level set $L^{V_0}_{\\alpha_0}$ as attracted to the equilibrium using only point samples of $f$ and a known Lipschitz bound, not a model.","A local failure in the optimisation is reinterpreted as information: it identifies where the data or tessellation under-samples the dynamics, and the next iteration concentrates resources there.","Each iteration produces an invariant set strictly inside the previous one, so the certified region of attraction is built by inclusion rather than by one monolithic Lyapunov function.","For the damped pendulum, the previously uncertified diagonal band is eliminated after five iterations, and a fully data-driven run that does not use the model to choose the tessellation also converges in one extra step."],"supporting_citations":[{"why":"Supplies the optimisation problem (3), the data-dependent negativity certificate in its Appendix A, and Proposition 6/Theorem 8 that turn negative slacks into attractivity of sublevel sets.","marker":"[13]"},{"why":"Provides the patchy Lyapunov function concept that licenses assembling locally certified affine pieces into a global certificate.","marker":"[14]"},{"why":"Supplies the generic triangulation method used for the initial tessellation when the dynamics are unknown and no model-informed subdivision is available.","marker":"[15]"}],"fun_headline_variants":["Iterative refinement certifies basin of attraction from data","Data-driven Lyapunov refinement converges to region of attraction","Refining Lyapunov certificates grows certified basin of attraction","Sequential data refinement proves region of attraction","Data-driven iterative tessellation refines attraction region"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that whenever a certificate fails locally, the user can keep refining the mesh and data until the next certificate satisfies the required nesting; the paper instructs restarting with a finer mesh when no scaling factor exists, but it does not prove that this refinement will always succeed.","fun_headline_variants_meta":{"raw":{"variants":["Iterative refinement certifies basin of attraction from data","Data-driven Lyapunov refinement converges to region of attraction","Refining Lyapunov certificates grows certified basin of attraction","Sequential data refinement proves region of attraction","Data-driven iterative tessellation refines attraction region"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.0002,"raw_usage":{"total_tokens":1337,"prompt_tokens":872,"completion_tokens":465,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":488,"completion_tokens_details":{"reasoning_tokens":390}},"tokens_in":488,"tokens_out":465,"duration_ms":4874,"temperature":1.0,"reasoning_tokens":390,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T23:50:28.891487+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the iterative loop on a system whose region of attraction is a known nonconvex set with a cusp or fractal boundary, for example a periodically forced pendulum, using a fixed Lipschitz bound and a coarse initial dataset; if the loop enters its \"iteration failed, restart with finer mesh\" branch indefinitely and never produces a finite chain satisfying $C_{k-1}\\subset L^{V_k}_{\\alpha_k}\\subset X_k$ for all $k$ up to $C_K\\subset A_0$, then the assumed eventual success of refinement under condition (4) would be disproved for that setting.","supporting_citations":[{"cited_title":"Robustly learning regions of attraction from fixed data,","cited_arxiv_id":null,"evidence_quote":"Supplies the optimisation problem (3), the data-dependent negativity certificate in its Appendix A, and Proposition 6/Theorem 8 that turn negative slacks into attractivity of sublevel sets."},{"cited_title":"Stabilization by patchy feedbacks and robustness properties,","cited_arxiv_id":null,"evidence_quote":"Provides the patchy Lyapunov function concept that licenses assembling locally certified affine pieces into a global certificate."},{"cited_title":"Sur la sph` ere vide.`A la m´ emoire de Georges Vorono¨ ı,","cited_arxiv_id":null,"evidence_quote":"Supplies the generic triangulation method used for the initial tessellation when the dynamics are unknown and no model-informed subdivision is available."}],"review_version":1}