Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systems

Bin Hu; Haoyu Li; Huan Zhang; Xiangru Zhong

REVIEW 3 major objections 5 minor 1 cited by

Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systems

T0 review · 3 major / 5 minor · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2504.17102 v1 pith:GTQDEAXE submitted 2025-04-23 math.OC cs.LGcs.SYeess.SY

Haoyu Li , Xiangru Zhong , Bin Hu , Huan Zhang This is my paper · ORCID

classification math.OCcs.LGcs.SYeess.SY MSC 37C7593C5593D30

keywords contractionmetricsformalverificationneuralnetworksdiscrete-timenonlinearsystemsnon-smoothdynamicsRiemannianlengthmetricregionofattractionboundpropagation

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

The 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.

That 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.

Other 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.

My 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.

Referee Report

3 major / 5 minor

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.

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 (3)

[Section 3, proof of Theorem 3, Eq. (12)-(14)] 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 3, Eq. (14)] 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 4.2, Theorem 6] 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.

minor comments (5)

[Section 2, notation] 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 4.2, first paragraph] The text says 'following our theory in Sec. 4' when referring to the contraction theory developed in Section 3; this should be corrected.
[Section 3, proof of Lemma 4] 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 5, Table 1 and Figure 1] 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 4.3, Theorem 7] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the local verification condition (4) is not identified with the geodesic-metric contraction conclusion by construction, and the learned metric is checked by an independent sound verifier.

full rationale

The central derivation is not circular. Theorem 3 assumes a local weighted chord inequality (4) and concludes a global contraction bound d(f(x),f(y)) ≤ ρ′ d(x,y) in the geodesic metric d(x,y)=inf_γ L(γ); these are different objects, and ρ′ is strictly between ρ and 1 rather than a relabeled input. The learned metric M(x)=μI+R(x)^T R(x) is trained by minimizing the violation loss L_violate, but the reported certificates are produced by a separate sound verification step using α,β-CROWN, so no fitted parameter is passed off as a prediction. The paper does cite prior work by overlapping authors, including Yang et al. (2024) for the forward-invariant-set theorem and several α,β-CROWN papers, but these are not load-bearing in a circular sense: the invariance certificate is a Lyapunov-level-set condition independent of contraction, and α,β-CROWN is a standard sound verifier whose correctness does not assume the target contraction result. One non-circular concern is that the proof of Theorem 3 contains an unproven regularity step: uniformly approximating f∘γ_u by an admissible γ_p via Lemma 4 does not, without an additional argument, transfer the infinitesimal bound (14), because uniform closeness does not control the derivative. That is a correctness gap, not a reduction of the conclusion to the hypothesis, so it does not raise the circularity score.

Assumptions & free parameters 4 free parameters · 6 assumptions · 0 invented entities

The central theorem is conditional on the existence of a metric satisfying the local condition (4); the learning algorithm searches for one using hand-chosen parameters. The proof also relies on standard Riemannian facts, on the external soundness of alpha,beta-CROWN, and on the Lyapunov certifier. No new physical entities are introduced.

free parameters (4)

rho (contraction rate) = per experiment, rho' = scale * rho_ROA
Chosen by hand in Algorithm 1 and used in verification condition (18); the final certificate depends on this value.
mu (metric lower bound) = not reported
M(x)=mu I + R^T R; the theorem requires a uniform lower bound, and the value affects the learned metric.
epsilon (neighborhood radius) = not reported
Local verification is performed over B(0;epsilon); contraction under Theorem 3 is only certified for this radius, and no sensitivity analysis is given.
theta (weights of R network) = not reported
Trained with PGD counterexamples; the existence of a valid metric in the experiments rests on this training run, and no architecture or initialization is given.

assumptions (6)

standard math The geodesic distance d(x,y)=inf L(gamma) over admissible curves is a metric on X.
Invoked in proof of Theorem 3; the paper cites Lee (2018) without proving this property for continuous positive definite metrics.
standard math Every piecewise regular curve admits an arclength parametrization with unit speed almost everywhere.
Used in proof of Theorem 3 before constructing f(gamma_u).
domain assumption X is open, connected, forward invariant; f is continuous; M is uniformly continuous with a uniform lower bound; and the local condition (4) holds.
These are the hypotheses of Theorem 3; if M lacks uniform continuity or a uniform lower bound, the proof does not go through.
domain assumption alpha,beta-CROWN is a sound verifier for the disjunctive query (18).
The practical formal guarantee depends on the soundness of the external verifier and on the computation-graph encoding; no verifier certificate is included in the paper.
domain assumption The forward invariant set X={V<rho} intersect B is certified by the Lyapunov method of Yang et al. (2024).
Used in Sections 4.1 and 5 to define the domain; contraction is only meaningful on a certified invariant set.
ad hoc to paper There exists an admissible curve gamma_p uniformly close to f(gamma_u) whose pointwise M-speed satisfies inequality (13).
The proof of Theorem 3 asserts this after Lemma 4 and Eq. (12) without a rigorous error analysis; this is the main unproved step.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systems." pith.science (2026). https://pith.science/paper/GTQDEAXE

@misc{pith2026250417102,
  author       = {Pith},
  title        = {Pith review of: Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GTQDEAXE}},
  note         = {Machine review of arXiv:2504.17102}
}

abstract

Contraction metrics are crucial in control theory because they provide a powerful framework for analyzing stability, robustness, and convergence of various dynamical systems. However, identifying these metrics for complex nonlinear systems remains an open challenge due to the lack of scalable and effective tools. This paper explores the approach of learning verifiable contraction metrics parametrized as neural networks (NNs) for discrete-time nonlinear dynamical systems. While prior works on formal verification of contraction metrics for general nonlinear systems have focused on convex optimization methods (e.g. linear matrix inequalities, etc) under the assumption of continuously differentiable dynamics, the growing prevalence of NN-based controllers, often utilizing ReLU activations, introduces challenges due to the non-smooth nature of the resulting closed-loop dynamics. To bridge this gap, we establish a new sufficient condition for establishing formal neural contraction metrics for general discrete-time nonlinear systems assuming only the continuity of the dynamics. We show that from a computational perspective, our sufficient condition can be efficiently verified using the state-of-the-art neural network verifier $\alpha,\!\beta$-CROWN, which scales up non-convex neural network verification via novel integration of symbolic linear bound propagation and branch-and-bound. Built upon our analysis tool, we further develop a learning method for synthesizing neural contraction metrics from sampled data. Finally, our approach is validated through the successful synthesis and verification of NN contraction metrics for various nonlinear examples.

Figures

Figures reproduced from arXiv: 2504.17102 by the authors.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Tube MPC for Bilinear Koopman Models using Robust Control Contraction Metrics
math.OC 2026-07 conditional novelty 6.0 of 10

A tube MPC scheme for bilinear Koopman models with neural-network contraction metrics yields recursive feasibility, robust constraint satisfaction, and ISS guarantees.

Reference graph

Works this paper leans on

34 extracted references · 26 canonical work pages · cited by 1 Pith paper

[1]

A unified algebraic perspective on L ipschitz neural networks

Alexandre Araujo, Aaron J Havens, Blaise Delattre, Alexandre Allauzen, and Bin Hu. A unified algebraic perspective on L ipschitz neural networks. In International Conference on Learning Representations, 2023

work page 2023
[2]

Contraction theory for dynamical systems

Francesco Bullo. Contraction theory for dynamical systems. Francesco Bullo, 2022

work page 2022
[3]

Neural lyapunov control

Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural lyapunov control. Advances in neural information processing systems, 32, 2019

2019
[4]

Lyapunov-stable neural-network control

Hongkai Dai, Benoit Landry, Lujie Yang, Marco Pavone, and Russ Tedrake. Lyapunov-stable neural-network control. arXiv preprint arXiv:2109.14152, 2021

arXiv 2021
[5]

Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control

Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control. IEEE Transactions on Robotics, 39 0 (3): 0 1749--1767, 2023

2023
[6]

Drip: Domain refinement iteration with polytopes for backward reachability analysis of neural feedback loops

Michael Everett, Rudy Bunel, and Shayegan Omidshafiei. Drip: Domain refinement iteration with polytopes for backward reachability analysis of neural feedback loops. IEEE Control Systems Letters, 7: 0 1622--1627, 2023

work page 2023
[7]

Efficient and accurate estimation of L ipschitz constants for deep neural networks

Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George Pappas. Efficient and accurate estimation of L ipschitz constants for deep neural networks. Advances in neural information processing systems, 32, 2019

work page 2019
[8]

Computation and formal verification of neural network contraction metrics

Maxwell Fitzsimmons and Jun Liu. Computation and formal verification of neural network contraction metrics. IEEE Control Systems Letters, pages 1--1, 2024. doi:10.1109/LCSYS.2024.3478272

arXiv 2024

Show all 34 references

[9]

Construction of a contraction metric by meshless collocation

Peter Giesl and Holger Wendland. Construction of a contraction metric by meshless collocation. Discrete and Continuous Dynamical Systems-B, 24 0 (8): 0 3843--3863, 2019

2019
[10]

Review on contraction analysis and computation of contraction metrics

Peter Giesl, Sigurdur Hafstein, and Christoph Kawan. Review on contraction analysis and computation of contraction metrics. arXiv preprint arXiv:2203.01367, 2022

2022 arXiv
[11]

Contraction metric computation using numerical integration and quadrature

Peter Giesl, Sigurdur Hafstein, and Iman Mehrabinezhad. Contraction metric computation using numerical integration and quadrature. Discrete and Continuous Dynamical Systems-B, 29 0 (6): 0 2610--2632, 2024

2024
[12]

Training certifiably robust neural networks with efficient local L ipschitz bounds

Yujia Huang, Huan Zhang, Yuanyuan Shi, J Zico Kolter, and Anima Anandkumar. Training certifiably robust neural networks with efficient local L ipschitz bounds. Advances in Neural Information Processing Systems, 34: 0 22745--22757, 2021

2021
[13]

Introduction to Riemannian manifolds, volume 2

John M Lee. Introduction to Riemannian manifolds, volume 2. Springer, 2018

2018
[14]

On contraction analysis for non-linear systems

Winfried Lohmiller and Jean-Jacques E Slotine. On contraction analysis for non-linear systems. Automatica, 34 0 (6): 0 683--696, 1998

1998
[15]

The general problem of the stability of motion

Aleksandr Mikhailovich Lyapunov. The general problem of the stability of motion. International journal of control, 55 0 (3): 0 531--534, 1992

1992
[16]

Control contraction metrics: Convex and intrinsic criteria for nonlinear feedback design

Ian R Manchester and Jean-Jacques E Slotine. Control contraction metrics: Convex and intrinsic criteria for nonlinear feedback design. IEEE Transactions on Automatic Control, 62 0 (6): 0 3046--3053, 2017

2017
[17]

Construction of contraction metrics for discrete-time dynamical systems using meshfree collocation

Sareena Pokkakkillath and Peter Giesl. Construction of contraction metrics for discrete-time dynamical systems using meshfree collocation. Discrete and Continuous Dynamical Systems-B, 29 0 (4): 0 2043--2071, 2024

2024
[18]

Contraction theory on riemannian manifolds

John W Simpson-Porco and Francesco Bullo. Contraction theory on riemannian manifolds. Systems & Control Letters, 65: 0 74--80, 2014

2014
[19]

Learning certified control using contraction metric

Dawei Sun, Susmit Jha, and Chuchu Fan. Learning certified control using contraction metric. In Conference on Robot Learning, pages 1519--1539. PMLR, 2021

2021
[20]

o rn S R \

Duc N Tran, Bj \"o rn S R \"u ffer, and Christopher M Kellett. Convergence properties for discrete-time nonlinear systems. IEEE Transactions on Automatic Control, 64 0 (8): 0 3415--3422, 2018

2018
[21]

Neural contraction metrics for robust estimation and control: A convex optimization approach

Hiroyasu Tsukamoto and Soon-Jo Chung. Neural contraction metrics for robust estimation and control: A convex optimization approach. IEEE Control Systems Letters, 5 0 (1): 0 211--216, 2020

2020
[22]

Contraction theory for nonlinear stability analysis and learning-based control: A tutorial overview

Hiroyasu Tsukamoto, Soon-Jo Chung, and Jean-Jaques E Slotine. Contraction theory for nonlinear stability analysis and learning-based control: A tutorial overview. Annual Reviews in Control, 52: 0 135--169, 2021

2021
[23]

Actor-critic physics-informed neural lyapunov control

Jiarui Wang and Mahyar Fazlyab. Actor-critic physics-informed neural lyapunov control. arXiv preprint arXiv:2403.08448, 2024

2024 arXiv
[24]

Beta-CROWN : Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification

Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN : Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34, 2021

2021
[25]

On the scalability and memory efficiency of semidefinite programs for L ipschitz constant estimation of neural networks

Zi Wang, Bin Hu, Aaron J Havens, Alexandre Araujo, Yang Zheng, Yudong Chen, and Somesh Jha. On the scalability and memory efficiency of semidefinite programs for L ipschitz constant estimation of neural networks. In International Conference on Learning Representations, 2024

2024
[26]

Control contraction metric synthesis for discrete-time nonlinear systems

Lai Wei, Ryan Mccloy, and Jie Bao. Control contraction metric synthesis for discrete-time nonlinear systems. IFAC-PapersOnLine, 54 0 (3): 0 661--666, 2021

2021
[27]

Discrete-time contraction-based control of nonlinear systems with parametric uncertainties using neural networks

Lai Wei, Ryan McCloy, and Jie Bao. Discrete-time contraction-based control of nonlinear systems with parametric uncertainties using neural networks. Computers & Chemical Engineering, 166: 0 107962, 2022

2022
[28]

Neural lyapunov control for discrete-time systems

Junlin Wu, Andrew Clark, Yiannis Kantaros, and Yevgeniy Vorobeychik. Neural lyapunov control for discrete-time systems. Advances in neural information processing systems, 36: 0 2939--2955, 2023

2023
[29]

Automatic perturbation analysis for scalable certified robustness and beyond

Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33, 2020

2020
[30]

Fast and Complete : Enabling complete neural network verification with rapid and massively parallel incomplete verifiers

Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and Complete : Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations, 2021

2021
[31]

Lyapunov-stable neural control for state and output feedback: A novel formulation

Lujie Yang, Hongkai Dai, Zhouxing Shi, Cho-Jui Hsieh, Russ Tedrake, and Huan Zhang. Lyapunov-stable neural control for state and output feedback: A novel formulation. In Forty-first International Conference on Machine Learning, 2024

2024
[32]

Neural-network-based online optimal control for uncertain non-linear continuous-time systems with control constraints

Xiong Yang, Derong Liu, and Yuzhu Huang. Neural-network-based online optimal control for uncertain non-linear continuous-time systems with control constraints. IET Control Theory & Applications, 7 0 (17): 0 2037--2047, 2013

2013
[33]

Efficient neural network robustness certification with general activation functions

Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Advances in Neural Information Processing Systems, 31: 0 4939--4948, 2018

2018
[34]

General cutting planes for bound-propagation-based neural network verification

Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. General cutting planes for bound-propagation-based neural network verification. Advances in Neural Information Processing Systems, 2022

2022

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.

[1] [1]

A unified algebraic perspective on L ipschitz neural networks

Alexandre Araujo, Aaron J Havens, Blaise Delattre, Alexandre Allauzen, and Bin Hu. A unified algebraic perspective on L ipschitz neural networks. In International Conference on Learning Representations, 2023

work page 2023

[2] [2]

Contraction theory for dynamical systems

Francesco Bullo. Contraction theory for dynamical systems. Francesco Bullo, 2022

work page 2022

[3] [3]

Neural lyapunov control

Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural lyapunov control. Advances in neural information processing systems, 32, 2019

2019

[4] [4]

Lyapunov-stable neural-network control

Hongkai Dai, Benoit Landry, Lujie Yang, Marco Pavone, and Russ Tedrake. Lyapunov-stable neural-network control. arXiv preprint arXiv:2109.14152, 2021

arXiv 2021

[5] [5]

Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control

Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control. IEEE Transactions on Robotics, 39 0 (3): 0 1749--1767, 2023

2023

[6] [6]

Drip: Domain refinement iteration with polytopes for backward reachability analysis of neural feedback loops

Michael Everett, Rudy Bunel, and Shayegan Omidshafiei. Drip: Domain refinement iteration with polytopes for backward reachability analysis of neural feedback loops. IEEE Control Systems Letters, 7: 0 1622--1627, 2023

work page 2023

[7] [7]

Efficient and accurate estimation of L ipschitz constants for deep neural networks

Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George Pappas. Efficient and accurate estimation of L ipschitz constants for deep neural networks. Advances in neural information processing systems, 32, 2019

work page 2019

[8] [8]

Computation and formal verification of neural network contraction metrics

Maxwell Fitzsimmons and Jun Liu. Computation and formal verification of neural network contraction metrics. IEEE Control Systems Letters, pages 1--1, 2024. doi:10.1109/LCSYS.2024.3478272

arXiv 2024