{"id":"018a86e4-7240-46e3-9247-2e6989df9c47","arxiv_id":"2504.17102","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A continuity-only local contraction condition, verified with alpha,beta-CROWN, yields formally certified neural contraction metrics and the first verified metric for a ReLU-controlled inverted pendulum.","lead":"This paper proves a new sufficient condition for certifying contraction, a strong form of stability, in discrete-time nonlinear systems, assuming only that the dynamics are continuous rather than smooth. It pairs that condition with a neural network verifier to learn and formally check contraction metrics, including for non-smooth neural-network-controlled systems.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Proof of Theorem 3 has an unjustified C^0-perturbation step: uniform closeness of γ_p to f∘γ_u cannot control the derivative inequality (13), so the formal contraction guarantee is not established as written.","rationale":"The paper's headline contribution is a formal contraction certificate for discrete-time systems with only continuous dynamics. The reader's verdict pins the central weakness to the proof of Theorem 3, specifically the transition from the pointwise margin (10)–(11) to the approximated curve inequality (13). My independent reading reaches the same conclusion. The proof of Theorem 3 replaces f∘γ_u by an admissible curve γ_p that is uniformly close in C^0, but the subsequent inequality (13) is a statement about difference quotients and hence about derivatives. C^0 closeness does not control derivatives, and the margin in (10) is O(δt²), so a uniform perturbation error of size ε cannot be absorbed as δt→0. This is not a matter of missing constants; the argument as written cannot work without either a derivative-convergence construction for γ_p or a different proof strategy. The theorem itself is plausibly true: condition (4) applied termwise along a fine partition suggests that the M-length of f∘γ_u is bounded by ρ times the M-length of γ_u, and such a partition argument would avoid the problematic perturbation step. For that reason the appropriate outcome is not rejection of the paper but a conditional verdict requiring a repaired proof. The experimental results and α,β-CROWN integration are interesting but cannot substitute for the missing formal step, since the verification pipeline is only as sound as Theorem 3. I do not see an independent flaw in the numerical methodology that would change the verdict, and I agree with the reader that the missing error estimate is the single load-bearing concern.","tokens_in":11319,"tokens_out":11334,"duration_ms":115542,"concrete_test":"Prove or disprove the following replacement step: for any admissible γ, let η=f∘γ_u. Show that for every partition of [c,d] with mesh < ε, ∑_i ‖η(t_i)−η(t_{i+1})‖_{M(η(t_i))} ≤ ρ ∑_i ‖γ_u(t_i)−γ_u(t_{i+1})‖_{M(γ_u(t_i))}, using (4) termwise and uniform continuity of M. If this sum converges to the M-length of η as mesh→0, then d(f(x),f(y)) ≤ ρ L(γ) follows without the γ_p perturbation. If the identity fails, exhibit a continuous f and M satisfying (4) on a bounded X for which the contraction conclusion of Theorem 3 is false.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central formal result, Theorem 3, is not proved by the argument in Section 3. After arclength reparametrization, the proof applies the local condition (4) to obtain the strict inequality (10) with a margin of order δt². It then invokes Lemma 4 to replace f∘γ_u by an admissible curve γ_p with uniform error ε, and asserts that for small ε and δt the pointwise metric-speed inequality (13) survives. This does not follow: (12) only bounds the pointwise difference between the chords by 2ε, while the available margin in (10)–(11) scales like δt². For any fixed γ_p, the chord difference quotient is bounded below at a.e. t by ‖γ_p'(t)‖, which is independent of ε; a C^0-close polygonal curve can have arbitrarily large slopes. Even if (4) forces f∘γ_u to be Lipschitz on compacta, uniform C^0 approximation does not transfer the infinitesimal speed bound (14). Consequently the conclusion d(f(x),f(y)) ≤ ρ′ d(x,y) is not derived from the stated assumptions. This is load-bearing because Theorem 6 and the α,β-CROWN verification pipeline rest entirely on Theorem 3. The theorem may be salvageable by a partition argument that bounds the M-length of f∘γ_u directly, but that proof is not in the paper.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a Jacobian-free and matrix-inequality-free sufficient condition for certifying contraction of discrete-time nonlinear systems whose dynamics are only assumed continuous. The central object is a learned neural-network metric M(x); Theorem 3 states that a local pairwise inequality (4), holding for all x in an open, connected, forward-invariant set X and all y in B(x;epsilon)∩X, implies contraction of the system in the geodesic metric d(x,y)=inf L(gamma). The authors reformulate this condition as a disjunctive verification query for the neural-network verifier alpha,beta-CROWN, add a CEGIS-style learning procedure, and report experiments on a Van der Pol system, a polynomial system, a two-machine power system, and an inverted pendulum with a neural-network controller. The claimed contribution is a scalable formal verification pipeline for contraction certificates of nonsmooth discrete-time systems, including the first verified contraction metric for an NN-controlled state-feedback system.","tokens_in":11672,"tokens_out":5779,"duration_ms":58744,"significance":"If Theorem 3 is made fully rigorous, the paper would be a meaningful advance: contraction certification is extended to systems whose dynamics are merely continuous, removing both the differentiability requirement and the reliance on LMIs/Sylvester criteria that limit prior work. The use of alpha,beta-CROWN as an independent sound verifier is a genuine strength, and the reported experiments demonstrate that the learned metrics can certify substantially larger contraction regions than constant metrics. The authors also deserve credit for not passing off fitted constants as predictions: the learned metric is checked by an external verifier, and the contraction condition is a standalone mathematical statement. However, the central theorem's proof has a load-bearing gap, so the formal-guarantee claim is not currently established as written.","major_comments":[{"comment":"The step from Eq. (12) to Eq. (13) is not justified. Eq. (12) only bounds the Euclidean difference of the chords by 2epsilon, but the margin available in Eq. (10)-(11), after division by delta_t^2, is a constant independent of delta_t. To preserve the weighted inequality (13), one would need to control 2epsilon/delta_t in the metric M(gamma_p(t+delta_t)), and since delta_t is subsequently sent to 0, no fixed choice of epsilon can make the perturbation uniformly small in delta_t. Moreover, uniform C^0 approximation of f(gamma_u) by gamma_p does not control the derivative gamma_p'(t): a polygonal curve arbitrarily close in C^0 to a continuous curve can have arbitrarily large slopes. Consequently the pointwise speed bound (14) does not follow from the stated assumptions. This is load-bearing because Theorem 6 and the entire alpha,beta-CROWN verification pipeline rest on Theorem 3. The theorem may be salvageable, for example by first proving that f(gamma_u) is locally Lipschitz along compact subarcs using condition (4), and then constructing gamma_p with controlled chords, but that argument is absent from the manuscript.","section":"Section 3, proof of Theorem 3, Eq. (12)-(14)"},{"comment":"Even if Eq. (13) were available for some fixed epsilon, the passage 'send delta_t^2 to 0' is not a valid limiting argument as written. The inequality (13) is asserted only for all small enough delta_t, with the admissible range of delta_t possibly depending on the chosen epsilon, while epsilon itself would need to shrink with delta_t for the perturbation to vanish. No coupled error estimate between epsilon and delta_t is supplied, so the derivative inequality (14) is not derived from the hypotheses.","section":"Section 3, Eq. (14)"},{"comment":"Theorem 6 applies Theorem 3 to the set X={x: V(x)<rho}∩B, but Theorem 3 requires X to be open. If B is a closed box, which is the natural reading of the verification domain in Eq. (18), then X is generally not open in R^n. The manuscript should either define B as an open box or state a boundary-adapted version of Theorem 3 that avoids this mismatch.","section":"Section 4.2, Theorem 6"}],"minor_comments":[{"comment":"The definition of the infinity-norm ball contains a typo: it reads 'B(0;epsilon)={y : ||y-x||_infinity <= epsilon}', but the center should be x, i.e. B(x;epsilon)={y : ||y-x||_infinity <= epsilon}.","section":"Section 2, notation"},{"comment":"The text says 'following our theory in Sec. 4' when referring to the contraction theory developed in Section 3; this should be corrected.","section":"Section 4.2, first paragraph"},{"comment":"In the partition construction, the proof writes 'with gamma(t_1)=a and gamma(t_{N+1})=b', but t_1 and t_{N+1} are times, so the intended statement is gamma(a) and gamma(b); the notation should be fixed.","section":"Section 3, proof of Lemma 4"},{"comment":"The experiments do not report the verifier inputs needed to reproduce the formal claims, such as alpha,beta-CROWN tolerances, branch-and-bound settings, neural network widths, or the number of runs; no code is provided. The '100%' entries in Table 1 also appear without any sensitivity analysis or error bars, and Figure 1 does not specify the delta-grid used to visualize the contraction region.","section":"Section 5, Table 1 and Figure 1"},{"comment":"The phrase 'Except the condition x+delta in B, the rest of the verification condition (18) is equivalent to the following numerical condition' is slightly misleading: the condition x+delta in B is not part of the minimization in L_violate, so the sentence should clarify that x+delta in B is verified separately and that Eq. (20) characterizes the remaining disjuncts.","section":"Section 4.3, Theorem 7"}],"recommendation":"major_revision","confidential_remarks":"The central proof gap in Theorem 3 is serious but appears repairable within the paper's scope, likely by adding a Lipschitz argument along compact subarcs and replacing the C^0 perturbation step with a chord-controlled approximation. I therefore recommend major revision rather than rejection. The authors should also be asked to release verifier configurations and code if they wish the 'formally verified' claims to be independently checkable."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper has a genuinely new idea: a Jacobian-free, continuity-only sufficient condition for discrete-time contraction metrics, plus an encoding that makes verification practical with alpha,beta-CROWN. The learning pipeline and the first verified NN-controlled pendulum contraction metric are real artifacts, and the experimental numbers are good. This is a useful contribution to the certified-learning-control literature.\n\nThe problem is the proof of Theorem 3. The argument approximates f(gamma_u) uniformly by an admissible curve gamma_p and then claims that the metric-speed inequality (13) survives for small delta_t. That step does not follow. The original inequality (10) has a margin proportional to delta_t^2, while the uniform approximation error between the curves is a fixed epsilon. For any fixed epsilon, the discrepancy between the chord of gamma_p and the chord of f(gamma_u) is O(epsilon delta_t), which outpaces the O(delta_t^2) margin as delta_t tends to zero. You cannot absorb the approximation error into the margin and then send delta_t to zero. A C^0-close curve can have arbitrarily large derivative, so the bound on gamma_p' in (14) is not justified. The stress-test note is right on target here, and this is load-bearing: Theorem 6 and the entire verification pipeline inherit the gap.\n\nThat said, the theorem is very likely true and fixable, probably by a partition argument that bounds the M-length of f(gamma_u) directly using the local condition, or by a more careful two-step approximation that controls derivatives. But the proof as it stands does not establish the result.\n\nOther soft spots are minor by comparison: the experiments lack verifier inputs, code, and error bars, so the runtime claims are hard to audit; and the constant metric baseline is a stiff comparison. The citation pattern is fine; self-citation is to their own verifier tools, which is appropriate.\n\nMy view: this deserves a serious referee, but not acceptance as is. The theoretical gap must be closed and the experimental artifacts released. If the authors fix the proof, this is a solid within-subfield result with a strong practical component.","headline":"The verification pipeline is clever and the experiments are impressive, but Theorem 3 is not proved as written, and since everything rests on it, the paper's central guarantee is currently a conjecture.","tokens_in":12140,"tokens_out":3830,"would_cite":false,"duration_ms":36242,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["37C75","93C55","93D30"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper establishes a Jacobian-free sufficient condition for formal contraction metrics in discrete-time nonlinear systems, and shows it can be verified with a neural-network verifier and learned from data.","keywords":["contraction metrics","formal verification","neural networks","discrete-time nonlinear systems","non-smooth dynamics","Riemannian length metric","region of attraction","bound propagation"],"falsifier":"Search for a continuous map $f$ and a uniformly continuous positive-definite metric $M(x)$ that satisfy the local inequality (4) on every $\\epsilon$-neighborhood but violate $d(f(x),f(y))\\le \\rho' d(x,y)$ for some pair; a numerical counterexample would settle the theorem's validity, and a proof of the missing estimate connecting the curve-approximation error to the time step would settle it in the other direction.","tokens_in":11142,"feed_emoji":"📉","tokens_out":15887,"duration_ms":141845,"temperature":0.7,"pith_summary":"This paper aims to establish a way to certify contraction of a discrete-time system $x_{k+1}=f(x_k)$ without ever differentiating the dynamics. The sufficient condition is local and pointwise: for a state-dependent metric $M(x)$, every pair of nearby states satisfies $\\|f(x)-f(y)\\|_{M(f(x))}\\le \\rho\\|x-y\\|_{M(x)}$. If the condition holds on an $\\epsilon$-neighborhood of every point of a forward-invariant domain, the paper claims the system is contracting in the geodesic-type metric $d(x,y)=\\inf_{\\gamma} L(\\gamma)$. This matters because it extends formal contraction certificates to continuous, possibly ReLU-controlled, nonsmooth systems, where the classical Jacobian and matrix-inequality route is unavailable, and it gives an easy-to-verify format for bound-propagation neural-network verifiers. The paper reports that learned neural metrics certify contraction over 88.6% to 100% of the region of attraction on four benchmark systems, including the first certified contraction region for an NN-controlled state-feedback pendulum.","feed_headline":"Local metric inequality certifies contraction without Jacobians","feed_subtitle":"A verifier-friendly condition for ReLU-driven closed loops where matrix-inequality methods fail.","key_machinery":"The load-bearing object is the local pointwise inequality (4), checked on small balls rather than as a differential condition. It is paired with the length metric $d(x,y)=\\inf_{\\gamma}L(\\gamma)$, where $L(\\gamma)=\\int \\|\\gamma'(t)\\|_{M(\\gamma(t))}\\,\\mathrm{d}t$ is the length of a piecewise regular curve under $M$. The proof strategy is curve shortening: for any curve $\\gamma$ joining $x$ to $y$, the image curve $f\\circ\\gamma$ is approximated by an admissible curve, and the strict margin in (4) converts the local pointwise comparison into a comparison of derivative norms, hence of lengths. On the computational side, the same inequality becomes a set of constraints over a boxed domain, which is exactly the input format of the $\\alpha,\\beta$-CROWN verifier with symbolic linear bound propagation and branch-and-bound.","core_discovery":"The central discovery is Theorem 3: for a continuous map $f$ on an open, connected, forward-invariant set $X$ and a uniformly continuous matrix-valued metric $M(x)\\succeq \\mu I$, the local inequality $$\\|f(x)-f(y)\\|_{M(f(x))}\\le \\rho\\|x-y\\|_{M(x)}$$ for every $x\\in X$ and $y\\in B(x;\\epsilon)\\cap X$ implies contraction in the length metric $d(x,y)=\\inf_{\\gamma}\\int \\|\\gamma'(t)\\|_{M(\\gamma(t))}\\,\\mathrm{d}t$, with rate $\\rho'$ for any $\\rho'\\in(\\rho,1)$. This replaces the Jacobian-based criterion $F(x)^\\top F(x)-I\\preceq -\\mu I$ with a pure distance comparison, which remains meaningful for nonsmooth dynamics. The paper then turns the condition into a verification problem on a bounded computation graph (Theorem 6) and into a counterexample-guided training objective (Theorem 7), and demonstrates the full learn-and-verify pipeline on autonomous and neural-network-controlled examples.","pith_inferences":["Editorial extension: because the condition is local, an alternative certification route is to check (4) with interval-arithmetic bound propagation over a finite grid, which would supply formal contraction certificates for black-box dynamics without training a neural metric.","Editorial extension: the theorem's proof, if completed, would imply that contraction is a metric-topological property for continuous maps on length spaces, so the same local inequality might transfer to other distance-like objects such as control contraction metrics on nonlinear manifolds.","Editorial extension: the verified examples are low-dimensional; the practical ceiling is the verifier's branching on high-dimensional boxes, so a natural stress test is to combine the condition with zonotope or decomposed bound propagation to push past four state dimensions."],"forward_implications":["Formal contraction certificates become available for closed-loop dynamics with ReLU or LeakyReLU controllers, where the classical Jacobian-based criteria are undefined.","Contraction verification reduces to bounding a scalar function on a bounded box, so it can ride on GPU-accelerated neural-network verifiers instead of SMT or MIP solvers.","The same local condition can be used as a training loss, producing learned metrics that are then formally verified; on the four benchmarks the certified contraction region covers most or all of the region of attraction.","A verified contraction metric with rate $\\rho'$ implies that the distance between any two trajectories in the metric $d$ shrinks at rate $\\rho'$ each step, so the system has a unique trajectory inside the invariant set and all solutions converge to it.","The experiments include the first verified contraction region for a neural-network state-feedback inverted pendulum, showing the condition can absorb nonsmooth learned controllers."],"supporting_citations":[{"why":"Foundational contraction theory; supplies the classical differential contraction analysis that the paper generalizes.","marker":"Lohmiller and Slotine (1998)"},{"why":"Supplies the proof of the classical Jacobian-based criterion for discrete-time systems that the paper's condition bypasses.","marker":"Tran et al. (2018)"},{"why":"Provides the SMT-based verification baseline and several benchmark systems (polynomial, two-machine power, Van der Pol) used for comparison.","marker":"Fitzsimmons and Liu (2024)"},{"why":"Supplies the Riemannian length-metric construction and arclength parametrization used in the proof of Theorem 3.","marker":"Lee (2018)"},{"why":"Provides the Lyapunov-function invariant-set method and the ReLU-controlled inverted pendulum benchmark whose region of attraction is reused.","marker":"Yang et al. (2024)"},{"why":"Part of the alpha,beta-CROWN line of verifiers used to check the nonconvex verification condition.","marker":"Wang et al. (2021)"}],"fun_headline_variants":["Contraction proof via distance, not Jacobians","Distance inequality certifies nonsmooth contraction","No Jacobians? No problem for contraction","Neural contraction verified without derivatives","Local distance check proves contraction"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The result depends on an unstated error estimate: nudging the continuous curve $f(\\gamma)$ to a smooth curve must preserve the local contraction inequality with a fixed positive margin uniformly as the time step shrinks.","fun_headline_variants_meta":{"raw":{"variants":["Contraction proof via distance, not Jacobians","Distance inequality certifies nonsmooth contraction","No Jacobians? No problem for contraction","Neural contraction verified without derivatives","Local distance check proves contraction"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000336,"raw_usage":{"total_tokens":1897,"prompt_tokens":1020,"completion_tokens":877,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":636,"completion_tokens_details":{"reasoning_tokens":816}},"tokens_in":636,"tokens_out":877,"duration_ms":8174,"temperature":1.0,"reasoning_tokens":816,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T10:50:50.109867+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Search for a continuous map $f$ and a uniformly continuous positive-definite metric $M(x)$ that satisfy the local inequality (4) on every $\\epsilon$-neighborhood but violate $d(f(x),f(y))\\le \\rho' d(x,y)$ for some pair; a numerical counterexample would settle the theorem's validity, and a proof of the missing estimate connecting the curve-approximation error to the time step would settle it in the other direction.","supporting_citations":[{"cited_title":"On contraction analysis for non-linear systems","cited_arxiv_id":null,"evidence_quote":"Foundational contraction theory; supplies the classical differential contraction analysis that the paper generalizes."},{"cited_title":"o rn S R \\","cited_arxiv_id":null,"evidence_quote":"Supplies the proof of the classical Jacobian-based criterion for discrete-time systems that the paper's condition bypasses."},{"cited_title":"Introduction to Riemannian manifolds, volume 2","cited_arxiv_id":null,"evidence_quote":"Supplies the Riemannian length-metric construction and arclength parametrization used in the proof of Theorem 3."}],"review_version":1}