{"id":"2f4a1981-a4b3-4ddd-9202-45188423c583","arxiv_id":"2509.10118","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A CEGIS-based framework synthesizes and verifies discrete-time sISS certificates for neural controllers, giving formal string-stability guarantees for interconnected systems.","lead":"This paper shows how to synthesize and formally verify neural certificates that guarantee string stability, the property that disturbances do not amplify through a chain of agents, for interconnected systems such as vehicle platoons, drone formations, and microgrids. It introduces a discrete-time extension of scalable input-to-state stability and uses neural network verifiers to certify learned controllers with a safety margin for model error.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Formal sISS guarantee requires a sound Lipschitz constant L_fi for the true dynamics, yet the drone-formation experiments assume unknown dynamics with no valid estimator supplied.","rationale":"The reader's weakest assumption identifies exactly the load-bearing concern: Theorem 2's formal guarantee is conditional on a sound a priori Lipschitz constant L_fi for the true dynamics, and the paper's drone-formation scenario explicitly assumes unknown dynamics without providing such a constant. If L_fi is underestimated, the error bound ε_i is invalid, and the verified inequality on the surrogate does not transfer to the true system. This is a correctness issue for a stated primary application, not merely a practical gap. Other potential concerns, such as the mismatch between sISS and the empirical string-stability gain metric in Eq. (37) or the absence of released code, are secondary: sISS is explicitly defined as the paper's notion of string stability, and missing code affects reproducibility rather than the validity of the argument. Because the reader already issued a CONDITIONAL verdict based substantially on this assumption, my analysis does not move the verdict; it sharpens the condition under which the central claim holds. The paper could be accepted if the authors either supply a valid L_fi for every experiment (e.g., from physical bounds or formal range analysis of the simulator) or restrict the formal claim to systems with known Lipschitz constants.","tokens_in":29790,"tokens_out":10601,"duration_ms":125715,"concrete_test":"In the drone-formation benchmark, compute a certified upper bound on the Lipschitz constant of F_i from the simulator used to generate data (e.g., via interval arithmetic on the implementation), then re-run the verification pipeline with that certified bound replacing the assumed L_fi. If the sISS certificate no longer verifies, or if the margin δ_i becomes insufficient, then the published certificate used an underestimated L_fi and does not satisfy the hypotheses of Theorem 2. Conversely, if verification still succeeds with the certified bound, the concern is refuted in this benchmark.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central formal claim rests on Theorem 2, whose error bound ε_i = ε̂_i + 0.5(L_fi + L_f̃i)|Δ|2 (Section 3.2) is only an upper bound if L_fi is a genuine Lipschitz constant of the true dynamics fi on Z_i. The proof (Appendix A.2, Eq. A.13) explicitly uses this constant to bound |fi(z) − fi(z′)|. Remark 1 assumes L_fi is 'known a priori from physics/regularity,' but Section 5.1 states for drone formations that 'the true dynamic is unknown F_i, and we estimate it from data.' No sound estimator for L_fi is offered; finite-sample estimates are not upper bounds. If the L_fi used in verification is too low, ε_i and hence the required margin δ_i are underestimated. Then Eq. (9) can hold on the surrogate while the true decremental condition Eq. (5) is violated, so the certificate does not imply sISS for the actual system. This directly undermines the claim of 'formally guaranteeing' string stability under unknown dynamics, and the paper does not report how L_fi was obtained in the drone experiments.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a synthesis-and-verification pipeline for neural Lyapunov certificates — and in the controlled case, neural controllers — for discrete-time interconnected systems. The formal property is discrete-time scalable input-to-state stability (sISS), which the authors use as their notion of string stability. Theorem 1 gives a small-gain vector-Lyapunov sufficient condition for sISS; Theorem 2 extends it to the realistic case where only a neural surrogate of the true dynamics is available, using Lipschitz constants and a grid-based approximation-error bound to impose a robust margin; Section 4 gives the analogous sISS-VCLF result for neural controllers; Theorems 3–6 and Corollaries 3–5 support certificate reuse for substructure-isomorphic, structurally equivalent, parameter-affine, and decomposable networks. The experimental sections apply the pipeline to mixed-autonomy platoons, drone formations, and microgrids, reporting reduced training/verification time via the reuse strategies and error gains below one in Table 3.","tokens_in":30065,"tokens_out":15576,"duration_ms":172807,"significance":"If the formal claims are correct, the framework would be a useful contribution to a difficult area: it would provide a scalable, verifier-backed way to give learned controllers a Lyapunov-based stability certificate in networked systems. The robustification step in Theorem 2 is the most valuable part, since it explicitly propagates surrogate-model error through the certificate, and the node-equivalence/decomposability results are practically relevant. I found no obvious flaw in the core derivation of Theorem 2 under Assumptions 1–2. However, the paper currently overstates what is proved: the formal guarantee is sISS, not the classical string-stability gain of Eq. (37), and the experiments on unknown dynamics do not discharge the sound-Lipschitz-constant assumption that Theorem 2 requires. These points are substantive but addressable.","major_comments":[{"comment":"Section 5.1 says for drone formations 'the true dynamic is unknown F_i, and we estimate it from data'; the HDV model is also treated as unknown. Theorem 2/Remark 1 instead require a sound Lipschitz constant L_fi for the true dynamics. In the proof (Appendix A.2, Eq. (A.13)), L_fi enters epsilon_i = epsilon_hat_i + 0.5(L_fi + L_tilde_fi)|Delta|_2; if L_fi is underestimated, the margin delta_i is too small and Eq. (9) can hold for the surrogate while Eq. (5) fails for the true system. No sound estimator for L_fi is supplied or reported for the drone/HDV experiments. Please either provide verified Lipschitz bounds for the true models used in the experiments, or explicitly restrict the formal guarantee to settings where L_fi is known.","section":"Section 5.1 / Theorem 2 / Remark 1"},{"comment":"The abstract and conclusion claim a formal guarantee of 'string stability,' but the formal result is discrete-time sISS (Def. 1), a network-wide ISS estimate. The classical string-stability gain in Eq. (37), max_i ||v_i||_{L2}/||v_{i-1}||_{L2} <= 1, is used in Table 3 without a proof that sISS implies it. Thus Table 3 is an empirical check, not a formal certificate. Please prove the implication under stated assumptions, or revise the claims in the title/abstract/conclusion to say that the framework guarantees sISS and that Eq. (37) is an empirical performance metric.","section":"Section 5.4, Eq. (37)"},{"comment":"The certificate conditions Eqs. (3) and (9) are verified only on the bounded operating region R_i and Z_i, but no forward-invariance of R_i is stated or verified. In the proof of Theorem 1, the class-K∞ bounds are used at every time k (Eqs. (A.6)–(A.9)); if a trajectory leaves R_i, those bounds are no longer available and the sISS estimate is not established. The paper should either prove invariance of R_i, verify the conditions on an absorbing superset, or explicitly state the sISS result as conditional on trajectories remaining in R_i.","section":"Sections 3.1–3.2, Eqs. (3), (5), (9)"}],"minor_comments":[{"comment":"The quantifier in Eq. (9) is written 'for any tilde_x_{i,k} in R_i', but the condition involves the neighbor states {x_j,k} and d_i,k. It should quantify over z_i,k in Z_i. The same issue appears in Eq. (23) and Corollary 2.","section":"Section 3.2, Eq. (9)"},{"comment":"The proof says 'By Eq. (25)'; Eq. (25) belongs to Corollary 4. The affine dynamics of Theorem 5 are in Eq. (14). Please correct this cross-reference.","section":"Appendix A.5 (proof of Theorem 5)"},{"comment":"The entries '-' and 'TO' are not explained in the captions. Make explicit that 'Full R.' failed to complete within 4 hours and that '-' indicates no value is reported.","section":"Section 5.3, Tables 1–2"},{"comment":"Several typos and notation slips should be cleaned: 'representing its the admissible operating region' (Sec. 3.1), 'The true dynamic is unknown F i' (Sec. 5.1), and inconsistent use of tilde_x_{k+1,i} versus tilde_x_{i,k+1}. Also ensure figure axis labels render legibly in the final version.","section":"Throughout"},{"comment":"The proof of Theorem 6 assumes the remaining agents satisfy sISS conditions but does not explicitly assemble the combined gain matrix or verify the small-gain condition for the full system. This is likely fixable by setting gains on added edges to zero and checking row sums; please make that argument explicit.","section":"Section 3.4, Theorem 6 / Definition 4"}],"recommendation":"major_revision","confidential_remarks":"To the editor: the manuscript is potentially publishable after major revision. The core robustification proof is coherent, and the missing pieces are local rather than invalidating the method. The main risks are whether the authors can discharge the Lipschitz-constant assumption in the unknown-dynamics experiments and whether they can realign the 'string stability' terminology with what is actually proved. I do not see grounds for rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First: this is a solid paper and the theory mostly holds up. The authors extend sISS to discrete-time systems, give a vector-Lyapunov sufficient condition, and prove a robust verification theorem (Thm 2) that adds a margin δ_i to the decrement inequality so that a certificate verified on a neural surrogate remains valid for the true dynamics under Lipschitz assumptions. The scaling results—certificate reuse under substructure isomorphism, node equivalence, and modular decomposability—are genuinely useful and correctly proved. The control extension with an imitation loss is natural. I didn't find a circularity in the CEGIS loop; the verification is independent of training.\n\nThe main soft spot is the gap between the formal claim and one of the experiments. Theorem 2 needs a valid Lipschitz constant L_fi of the true dynamics (Assumption 1, Remark 1). The paper says this is known a priori. But Section 5.1 says for drone formations the true dynamics is unknown and estimated from data. No sound estimator for L_fi is offered; a finite-sample estimate is not an upper bound, and an underestimate would shrink ε_i and violate the margin. So the 'formal guarantee' for that experiment is conditional on an L_fi the authors don't report. That is fixable—either provide a certified Lipschitz bound or soften the claim—but as written it overclaims.\n\nSecond, smaller issue: the paper uses sISS as the formal notion of string stability and separately validates the classical gain metric (Eq. 37) empirically. That's not inconsistent, but the abstract's 'formally guarantee string stability' glosses over the fact that the formal property is sISS. The empirical gain check is not derived from the certificate.\n\nMinor: no code or data, and the class-K∞ bounds and the margins are not specified, so reproducibility is limited.\n\nWho is this for: researchers in formal verification for learning-based control, especially multi-agent and networked systems. Worth a serious referee—the theory advances the state of the art and the main issues are about aligning claims with assumptions and releasing artifacts.","headline":"Solid theory, but the formal guarantee for unknown dynamics depends on a Lipschitz constant the paper assumes without showing it holds in the drone experiment.","tokens_in":30572,"tokens_out":2713,"would_cite":true,"duration_ms":29802,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93D30","93A15","93C10"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims that string stability of large-scale interconnected systems with neural-network controllers can be formally guaranteed by training and verifying discrete-time scalable input-to-state stability certificates that explicitly","keywords":["neural certificates","string stability","interconnected systems","scalable input-to-state stability","neural network verification","vector Lyapunov functions","counterexample-guided inductive synthesis","large-scale control"],"falsifier":"In a drone formation where the true dynamics are estimated from data, collect a certificate using a Lipschitz constant 10% below the value estimated on a dense hold-out grid, then simulate a sinusoidal disturbance at a point between two grid nodes; if the maximum velocity error gain across the formation exceeds 1, the claimed formal sISS guarantee for the true system is refuted.","tokens_in":29653,"feed_emoji":"🔗","tokens_out":4788,"duration_ms":47660,"temperature":0.7,"pith_summary":"The paper aims to close the gap between learning-based control and formal guarantees by proving that discrete-time scalable input-to-state stability (sISS), a stronger, network-size-independent form of string stability, can be certified for interconnected systems even when the dynamics are neural surrogates of unknown true dynamics. Its central claim is that a vector Lyapunov function, verified with a margin that accounts for the discrepancy between true and approximate dynamics, suffices to guarantee string stability of the true closed-loop system. To make this practical, the paper proves structural reuse theorems that let certificates trained on small or symmetric systems be cheaply lifted to large ones, and validates the pipeline on platoons, drone formations, and microgrids. A sympathetic reader would care because it offers a path to deploy black-box RL controllers with formal safety guarantees in safety-critical networked systems.","feed_headline":"Neural controllers earn formal string-stability guarantees","feed_subtitle":"Certified string stability means local disturbances cannot amplify through the network.","key_machinery":"A discrete-time sISS vector Lyapunov certificate: a set of local neural-network Lyapunov functions V_i together with a coupling matrix Γ, satisfying a local decremental condition and a global small-gain condition max_i Σ_{j∈E_i∪{i}} γ_{i,j} ≤ 1−ε. The verification step uses off-the-shelf neural network verifiers to check these local conditions on the surrogate model with a robust margin, and the synthesis step uses counterexample-guided inductive synthesis (CEGIS) to alternately train the certificates and controllers against violating counterexamples.","core_discovery":"The paper establishes that discrete-time scalable input-to-state stability (sISS) provides a formal notion of string stability: it requires the maximum state deviation across agents to be bounded by a network-size-independent KL function of the initial deviation plus a K function of the sup-norm of disturbances. The central sufficient condition is a vector Lyapunov function {V_i} with class-K∞ bounds and a decremental inequality V_i(x_i,k+1) ≤ Σ_{j∈E_i∪{i}} γ_{i,j}V_j(x_j,k) + ψ|d_i,k|_2, coupled with a small-gain condition max_i Σ γ_{i,j} ≤ 1−ε. The paper's robust verification theorem shows that if these inequalities hold on a learned surrogate model with an added margin δ_i that covers the","pith_inferences":["The structural reuse theorems suggest that for highly symmetric networks, certification cost could become essentially independent of fleet size, which would make formal guarantees practical for real-time deployment.","The reliance on a priori Lipschitz bounds suggests a natural extension where these bounds are themselves verified or tightened online using set-membership identification, rather than assumed from physics.","The error bound depends on grid resolution; an adaptive grid that refines near counterexamples could yield tighter margins and less conservative controllers.","The same certificate-and-verify machinery could be adapted to other network effects such as safety or stochastic disturbances, provided the analogous approximation-error propagation can be bounded."],"forward_implications":["If the certificate verifies on the approximated model with the prescribed margin, the true system is guaranteed to be sISS, hence string-stable, independent of network size.","Certificates for a small or substructure-isomorphic system can be reused for a larger one without re-verification, reducing the cost of certification at scale.","For parameter-affine dynamics and convex Lyapunov functions, certifying only the vertices of a convex parameter region certifies the whole region.","Adding a new node to an already-verified subsystem only requires local verification of the coupling if the subsystem dynamics are independent of external states.","In closed-loop settings, the framework jointly synthesizes and verifies a controller and a certificate, preserving the original policy's performance via an imitation loss."],"fun_headline_variants":["Neural certificates prove string stability at scale","Scalable verification of string-stable neural controllers","Formal string-stability from neural certificates","Guaranteeing string stability with neural certificates","Neural certificates enforce string stability in networks"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The formal guarantee hinges on knowing a priori a valid Lipschitz constant for the true dynamics on the operating region; if that constant is underestimated, the robust margin is too small and the certificate may not imply string stability for the real system.","fun_headline_variants_meta":{"raw":{"variants":["Neural certificates prove string stability at scale","Scalable verification of string-stable neural controllers","Formal string-stability from neural certificates","Guaranteeing string stability with neural certificates","Neural certificates enforce string stability in networks"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000735,"raw_usage":{"total_tokens":3150,"prompt_tokens":799,"completion_tokens":2351,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":543,"completion_tokens_details":{"reasoning_tokens":2283}},"tokens_in":543,"tokens_out":2351,"duration_ms":20221,"temperature":1.0,"reasoning_tokens":2283,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T18:06:44.220250+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"In a drone formation where the true dynamics are estimated from data, collect a certificate using a Lipschitz constant 10% below the value estimated on a dense hold-out grid, then simulate a sinusoidal disturbance at a point between two grid nodes; if the maximum velocity error gain across the formation exceeds 1, the claimed formal sISS guarantee for the true system is refuted.","supporting_citations":[],"review_version":1}