Verifying Probabilistic Regions of Attraction with Neural Lyapunov Functions for Stochastic Systems

Hans De Sterck; Jun Liu; Yun Su

REVIEW 3 major objections 4 minor 29 references

Verifying Probabilistic Regions of Attraction with Neural Lyapunov Functions for Stochastic Systems

T0 review · 3 major / 4 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read The paper claims that a physics-informed neural network solving the stochastic Zubov equation, combined with satisfiability-modulo-theories verification, certifies probabilistic regions of attraction that are larger than those obtained with

desk verdict Theorem 14 is false as stated — a deterministic 1D example satisfies its hypotheses yet violates the conclusion, so the two-Lyapunov verification claim is currently unsupported. read the letter →

arxiv 2508.21213 v1 pith:6DG52VLF submitted 2025-08-28 math.OC

Yun Su , Hans De Sterck , Jun Liu This is my paper

classification math.OC MSC 93D3093E1560H1068T07

keywords stochasticZubovequationprobabilisticregionofattractionneuralLyapunovfunctionsphysics-informednetworksSMTverificationstabilitydifferentialequations

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

The paper claims that a physics-informed neural network approximating the stochastic Zubov equation can produce a Lyapunov function whose probabilistic region of attraction is certified by SMT solvers, and that this certified region is larger than what sum-of-squares or quadratic Lyapunov functions give on a nonlinear stochastic example. The central move is to prove sufficient conditions under which a quadratic Lyapunov function handles the small neighborhood of the origin and a separately trained neural function handles the outer shell; nesting the two sublevel sets yields a pointwise lower bound on the probability of convergence. If the claim holds, engineers get a practical route from unverified neural candidates to formal stochastic stability guarantees, complete with a probability for each initial condition.

What carries the argument

Stochastic Zubov equation and the annulus-nesting condition. $W(x) = 1 - \mathbb{E}\left[\exp\left(-\int g(X_s(x))\,ds\right)\right]$ solves $LW = -g(1-W)$ and characterizes the probabilistic region of attraction as $\{W<1\}$. The theorem that carries the argument is the nesting $W^{\beta_1} \subseteq V^{c_1} \subseteq V^{c_2} \subseteq W^{\beta_2}$ with $LW \leq -\zeta$ on the annulus, which lets two Lyapunov functions cooperate: one local near the origin, one global on the shell, and yields the product lower bound on attraction probability.

What would settle it

On a stochastic system where the true Zubov solution can be computed accurately (dense Monte-Carlo or a fine numerical PDE solve), run the training-plus-SMT pipeline. If the solver reports no constants $\beta_1 < \beta_2$ and $c_1 < c_2$ satisfying $W^{\beta_1} \subseteq V^{c_1} \subseteq V^{c_2} \subseteq W^{\beta_2}$ with $L W_{NN} \leq -\zeta$ on the annulus, while the true probabilistic region of attraction is large, the claimed enlargement mechanism has failed. Alternatively, take a point inside the verified $W^{\beta_2}$ whose predicted bound from Proposition 15 is high and simulate many trajectories: an observed convergence frequency below that bound would contradict th

Watch

Extended reading notes

Core claim

The paper's discovery is a verification theorem (Theorem 14) plus a training pipeline. Training solves the stochastic Zubov equation $LW = -g(1-W)$ with $W(0)=0$; its viscosity solution's strict sublevel set $\{W<1\}$ is exactly the set of initial conditions attracted with positive probability. Verification does not try to check $LW<0$ everywhere. Instead, after a quadratic Lyapunov function $V$ has been certified on $V^{c_2}$, a neural $W$ is certified only on the annulus $W^{\beta_2} \setminus W^{\beta_1}$, with $W^{\beta_1} \subset V^{c_1} \subset V^{c_2} \subset W^{\beta_2}$. Then every $x_0 \in W^{\beta_2}$ converges with probability at least $\left(1 - \frac{c_1}{c_2}\right)\left(1 - \frac{W(x_0)}{\beta_2}\right)$. The numerical example on a reversed Van der Pol oscillator shows the verified neural sublevel set exceeding the

Load-bearing premise

The certification depends on the trained neural network being close enough to the true stochastic Zubov solution that some annulus $W^{\beta_2} \setminus W^{\beta_1}$ satisfies the stochastic Lyapunov inequality and nests around the verified quadratic region; the paper provides no error bound or training guarantee for this nearness.

Editorial extensions

If this is right

Formal certificates replace simulation checks: every verified sublevel set W^{β2} comes with a probability bound for every initial condition inside it.
The method's verified region can extend beyond the deterministic region of attraction: on the example, stochastic effects stabilize some points outside the deterministic limit cycle.
Because the neural function only needs a negative Lyapunov derivative on an annulus, PINN training is relieved of the hardest part of reproducing the equilibrium singularity.
Applying the same verification pipeline to SOS and quadratic candidates yields smaller certified regions, indicating the Zubov-based candidate carries more of the true probabilistic region of attraction.
Any improvement in SMT solvers or in PINN accuracy translates directly into larger certified probabilistic regions without changing the theorem.

Reading between the lines

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

Since no error bound links PINN training loss to the certified constants, one could interleave training with SMT queries: if the solver cannot find β1, β2, add collocation points inside the annulus and retrain, making the pipeline an anytime certification method; the paper does not explore this.
The same nesting could be iterated with a chain of Lyapunov functions, each certified on its own annulus, to enlarge the certified region further than two functions allow.
The probability lower bound in Proposition 15 is conservative; sampling from the certified region with rare-event estimators could tighten the practical p-ROA estimate, although the formal bound would remain the conservative certificate.
Theorem 13's exit-time argument is a supermartingale property that could be reused for finite-time reach-avoid or barrier-style specifications, not just asymptotic attraction.

Share X Bluesky LinkedIn Reddit HN

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 extends neural Lyapunov verification to stochastic systems by training a PINN on the stochastic Zubov equation and then using dReal to verify the learned function. The idea is timely and the combination is new as far as I can tell. Proposition 11, the local stability condition, looks sound. That said, the central contribution, Theorem 14, is not valid as stated. The proof invokes Theorem 13(ii)—which requires LV<0 on the entire sublevel set V^{c2}\{0}—but the theorem's hypotheses only give LV≤−ζ on the annulus V^{c2}\V^{c1}. I checked the stress-test counterexample and it holds up: for the deterministic scalar system dx=(x−2x^3)dt with V=W=x^2, c1=β1=0.75, c2=β2=1.5, all hypotheses are satisfied, yet trajectories starting inside V^{c1} converge to ±1/√2, not 0. The claimed lower bound of (1−c1/c2)(1−W(x0)/β2) is then ~1/3 for x0^2=0.5, while the true convergence probability to 0 is 0. Deterministic systems are a special case, so this is not a contrived edge case.

This is not a cosmetic gap: Theorem 14 is what enables the two-Lyapunov enlargement argument and the piecewise probability bound in Proposition 15. Without an additional assumption, e.g., that V also satisfies Theorem 13(ii) on V^{c2}, the paper's verification results are unsupported. The numerical section also gives only a single 2D example and no code or verification scripts, which makes it hard to reproduce. The abstract's "largest probabilistic ROA" language overstates what is actually certified, since the verified region is a sublevel set where the conditions hold, not the true C.

What the paper does well: the PINN training with data from (3) is a sensible extension of prior deterministic work, and the local verification via the stochastic Lyapunov equation seems correct. The writing is clear and the related work is well positioned.

Bottom line: this is a serious paper with a load-bearing flaw. It deserves peer review, but only with the expectation of major revision and a corrected theorem. I would not cite it in its current form.

Referee Report

3 major / 4 minor

Summary. The paper develops a physics-informed neural network (PINN) approach to approximate the value function of a stochastic Zubov equation, yielding a learned neural Lyapunov function for the probabilistic region of attraction (ROA) of stochastic nonlinear systems. It then derives sufficient conditions, checkable by SMT solvers, for stochastic stability and probabilistic ROA. The main theoretical result is Theorem 14, which combines a locally verified quadratic Lyapunov function V with a neural Lyapunov function W that satisfies a Lyapunov inequality on an annulus W^{β2}\W^{β1}, in order to certify a probability lower bound on convergence from an enlarged set W^{β2}. Numerical experiments on a reversed Van der Pol oscillator illustrate that the method yields larger verified probabilistic ROAs than SOS-based Lyapunov functions.

Significance. If correct, the paper would provide a formally verifiable, SMT-based certification procedure for probabilistic region-of-attraction estimates using neural Lyapunov functions, going beyond SOS methods and capturing larger regions in the demonstrated example. The verification approach is independent of the training procedure: the SMT solver checks the trained function itself, not the training objective, so there is no circularity of fitted constants. The numerical study is concrete and reproducible in principle. However, the central sufficient condition in Theorem 14 is false as stated; the proof silently uses a much stronger hypothesis than the theorem assumes. This is a load-bearing flaw that affects the main theoretical claim and the soundness of Proposition 15.

major comments (3)

[Section IV-B, Theorem 14] The theorem is false as stated because its proof upgrades the hypothesis without justification. The theorem assumes only that V satisfies Theorem 13 iii), i.e., LV ≤ -ζ on the annulus V^{c2}\V^{c1}. The proof, however, invokes Theorem 13 ii) to conclude convergence to 0 after the trajectory enters V^{c1}, which requires LV < 0 on all of V^{c2}\{0} and positive definiteness of V. These stronger properties are not implied by the stated assumptions. A deterministic counterexample satisfies all hypotheses but violates the conclusion: take dx = (x - 2x^3)dt, V=W=x^2, c1=β1=0.75, c2=β2=1.5. Then LV = 2x^2(1-2x^2) ≤ -0.75 on V^{c2}\V^{c1}, all sublevel inclusions hold, and all smoothness assumptions are met. But for x0 = 1/√2 (W(x0)=0.5), the claimed lower bound is (1-0.75/1.5)(1-0.5/1.5) ≈ 0.333, whereas the deterministic trajectory converges to ±1/√2, so the probability of convergence to 0 is
[Section IV-B, proof of Theorem 13 iii)] The proof contains an unjustified step: 'With a slightly modified argument as in the proof of part ii), we can show that P{Xt ∈ Vc2, ∀t ≥ t0} ≥ 1 - V(x0)/c2.' This conclusion does not follow from the assumptions, because LV may be positive inside Vc1, so the supermartingale argument of part i) is not available on the entire sublevel set Vc2. The proof needs a direct treatment of the exit probability, e.g., an optional-stopping argument applied only on the annulus, and a separate argument controlling the behavior after entering Vc1. As written, the proof is incomplete; the authors should either provide a correct proof of iii) or weaken the statement.
[Section IV-B, Proposition 15] The probability lower bound p(x0) is not supported by the results as stated. For W(x0) < β1, the proposition claims P(x0) ≥ 1 - V(x0)/c2, attributing this to Theorem 13 iii), but Theorem 13 iii) applies only to x0 ∈ Vc2\Vc1, whereas W(x0)<β1 places x0 inside Vc1. Moreover, the proof of Proposition 15 relies on Theorem 14, which is false as stated (see first major comment). After repairing Theorem 14 by adding the assumption that V satisfies Theorem 13 ii) on Vc2, Proposition 15 can be made valid, but it must be restated and reproved accordingly.

minor comments (4)

[Section V, Example 17] Typo: 'preform' should be 'perform'.
[Section IV-B, Proposition 15 proof] In the continuity argument, '1 − V (x0)' should read '1 − V (x0)/c2'.
[Figure 1 caption] The black curve is described as 'the region where the neural Lyapunov function is not well-trained'; as a curve it is presumably the boundary of such a region. Please clarify.
[Section II-B] The statement 'W(x) < 1 if and only if LW(x) < 0 when x ≠ 0' presumes W is positive definite and sufficiently smooth; the viscosity solution may not be C^2. This is used as intuition, but should be phrased more carefully.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: SMT verification checks the trained network independently; self-citations are not load-bearing.

full rationale

No circular step was found. The PINN training in Section III minimizes a squared PDE residual and a simulation-based data term; the formal verification in Section IV asks dReal to check inequalities (7) and (18) on the trained network W_NN. These are different logical statements (PDE residual versus sublevel-set Lyapunov inequalities), and the solver's answer is not forced by the training loss or by the fitted W values. Theorems 13 and 14 are proved from Itô/Dynkin supermartingale inequalities, so the probabilistic ROA bound is not equivalent to the assumptions by construction. The citations [7], [8], [13], [28] are methodological/tool citations by the same group, but the central claim does not reduce to any of them; the stochastic Zubov uniqueness is cited from Camilli–Grüne, not from the authors' own work. A separate soundness issue (not a circularity) exists in Theorem 14: the proof says 'By the assumptions on V and Theorem 13 ii), we obtain P(E2 | E1) ≥ 1 − V(Xτ(x0))/c2 = 1 − c1/c2', but the stated hypotheses on V only give Theorem 13 iii) (LV ≤ −ζ on V^{c2}\V^{c1}), whereas Theorem 13 ii) requires LV < 0 on all of V^{c2}\{0}; the proof silently assumes the missing condition inside V^{c1}. This is an unsupported inference that would make Theorem 14 unsound as stated, but it is not an input–output reduction and therefore does not count as circularity under the rubric.

Assumptions & free parameters 3 free parameters · 5 assumptions · 0 invented entities

The paper introduces no new physical or mathematical entities. Its central derivation rests on the stochastic Zubov characterization from prior work, standard stochastic calculus, and the unverified assumption that the PINN training produces a useful Lyapunov function. The verification constants are free parameters chosen to maximize the certified region.

free parameters (3)

verification constants (c1, c2, beta1, beta2) = example: c=2.3151, beta2=0.86437, c1 and beta1 not reported
Chosen by hand/search to satisfy nested inclusions and Lyapunov inequalities; they determine the size of the certified ROA and are selected after training.
Zubov PDE weighting g(x)=0.1||x||^2 = 0.1
Arbitrary positive-definite function; the theoretical set C is independent of g, but the trained W_NN and its sublevel sets depend on this choice.
neural network architecture = 3 hidden layers, 10 neurons per layer
Architecture chosen without provided ablation or justification; affects the quality of the trained Lyapunov function.

assumptions (5)

domain assumption Stochastic Zubov equation characterization (from [17, Theorem 2.2]): W is the unique viscosity solution and C = {x: W(x) < 1}.
The entire training target relies on this external theorem, which is cited but not proven in the paper. Used in Section II-B.
domain assumption Assumption 1: f and sigma are twice continuously differentiable, f(0)=0, sigma(0)=0.
Stated in Section II-A; ensures the linearization and the stochastic Lyapunov equation are well-defined.
standard math Standard stochastic calculus results: Ito's formula, strong Markov property, Doob's optional stopping.
Used throughout the proofs of Theorems 13 and 14.
standard math Stochastic Lyapunov stability theorems (Theorem 6 and 7 from [25]).
Used to establish stochastic stability and asymptotic stability in Theorem 13 ii).
domain assumption The linearized stochastic system is mean-square stable, so the stochastic Lyapunov equation (6) has a positive definite solution P.
Assumed in Proposition 11 and the numerical example; not proven in the paper.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Verifying Probabilistic Regions of Attraction with Neural Lyapunov Functions for Stochastic Systems." pith.science (2026). https://pith.science/paper/6DG52VLF

@misc{pith2026250821213,
  author       = {Pith},
  title        = {Pith review of: Verifying Probabilistic Regions of Attraction with Neural Lyapunov Functions for Stochastic Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6DG52VLF}},
  note         = {Machine review of arXiv:2508.21213}
}

read the original abstract

Leveraging a stochastic extension of Zubov's equation, we develop a physics-informed neural network (PINN) approach for learning a neural Lyapunov function that captures the largest probabilistic region of attraction (ROA) for stochastic systems. We then provide sufficient conditions for the learned neural Lyapunov functions that can be readily verified by satisfiability modulo theories (SMT) solvers, enabling formal verification of both local stability analysis and probabilistic ROA estimates. By solving Zubov's equation for the maximal Lyapunov function, our method provides more accurate and larger probabilistic ROA estimates than traditional sum-of-squares (SOS) methods. Numerical experiments on nonlinear stochastic systems validate the effectiveness of our approach in training and verifying neural Lyapunov functions for probabilistic stability analysis and ROA estimates.

Figures

Figures reproduced from arXiv: 2508.21213 by the authors.

**Figure 2.** The probabilistic ROA Heatmap visualizes the attraction probability [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

29 extracted references · 28 canonical work pages

[1]

Neural Lyapunov control

Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov control. Advances in NeurIPS , 32, 2019

work page 2019
[2]

Neural Lyapunov control of unknown nonlinear systems with stability guar- antees

Ruikun Zhou, Thanin Quartz, Hans De Sterck, and Jun Liu. Neural Lyapunov control of unknown nonlinear systems with stability guar- antees. Advances in NeurIPS , 35, 2022

work page 2022
[3]

Region of attraction in a power system with discrete LTCs

Costas D V ournas and Nikos G Sakellaridis. Region of attraction in a power system with discrete LTCs. IEEE Transactions on Circuits and Systems I: Regular Papers , 53(7):1610–1618, 2006

work page 2006
[4]

Regions of attraction for hybrid limit cycles of walking robots

Ian R Manchester, Mark M Tobenkin, Michael Levashov, and Russ Tedrake. Regions of attraction for hybrid limit cycles of walking robots. IFAC Proceedings Volumes, 44(1):5801–5806, 2011

work page 2011
[5]

Region of attraction estimation of biological continuous boolean models

Megan Leigh Matthews and Cranos M Williams. Region of attraction estimation of biological continuous boolean models. In Proc. of IEEE SMC, pages 1700–1705. IEEE, 2012

work page 2012
[6]

Maximal Lyapunov functions and domains of attraction for autonomous nonlinear systems

Anthony Vannelli and Mathukumalli Vidyasagar. Maximal Lyapunov functions and domains of attraction for autonomous nonlinear systems. Automatica, 21(1):69–80, 1985

1985
[7]

Towards learning and verifying maximal neural Lyapunov functions

Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. Towards learning and verifying maximal neural Lyapunov functions. In Proc. of CDC , pages 8012–8019. IEEE, 2023

work page 2023
[8]

Physics-informed neural network Lyapunov functions: PDE charac- terization, learning, and verification

Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. Physics-informed neural network Lyapunov functions: PDE charac- terization, learning, and verification. Automatica, 175:112193, 2025

work page 2025

Show all 29 references

[9]

Data-driven computational methods for the domain of attraction and Zubov’s equation

Wei Kang, Kai Sun, and Liang Xu. Data-driven computational methods for the domain of attraction and Zubov’s equation. IEEE Transactions on Automatic Control , 69(3):1600–1611, 2023

2023
[10]

Formal synthesis of Lyapunov neural networks

Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. Formal synthesis of Lyapunov neural networks. IEEE Control Systems Letters, 5(3):773–778, 2020

2020
[11]

Lyapunov-net: A deep neural network architecture for lyapunov function approximation

Nathan Gaby, Fumin Zhang, and Xiaojing Ye. Lyapunov-net: A deep neural network architecture for lyapunov function approximation. In Proc. of CDC , pages 2091–2096. IEEE, 2022
[12]

Learning control Lyapunov functions from counterexamples and demonstrations

Hadi Ravanbakhsh and Sriram Sankaranarayanan. Learning control Lyapunov functions from counterexamples and demonstrations. Au- tonomous Robots, 43:275–307, 2019

2019
[13]

Tool LyZNet: A lightweight python tool for learning and verifying neural Lyapunov functions and regions of attraction

Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. Tool LyZNet: A lightweight python tool for learning and verifying neural Lyapunov functions and regions of attraction. In Proc. of HSCC, pages 1–8, 2024

2024
[14]

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

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

2023
[15]

Methods of AM Lyapunov and their application, volume 4439

Vladimir Ivanovich Zubov. Methods of AM Lyapunov and their application, volume 4439. US Atomic Energy Commission, 1961

1961
[16]

A characterization of the domain of attraction for a locally exponentially stable stochastic system

Fabio Camilli and Paola Loreti. A characterization of the domain of attraction for a locally exponentially stable stochastic system. Quaderno IAC, n:25, 2000

2000
[17]

Characterizing attraction probabilities via the stochastic zubov equation

Fabio Camilli and Lars Grüne. Characterizing attraction probabilities via the stochastic zubov equation. Discrete and Continuous Dynamical Systems-B, 3(3):457–468, 2003

2003
[18]

Zubov’s method for stochastic control systems

Fabio Camilli, Lars Grüne, and Fabian Wirth. Zubov’s method for stochastic control systems. IFAC Proceedings Volumes , 38(1):259– 264, 2005

2005
[19]

Lyapunov function computation for autonomous linear stochastic differential equations using sum-of-squares programming

Sigurdur Hafstein, Skuli Gudmundsson, Peter Giesl, Enrico Scalas, et al. Lyapunov function computation for autonomous linear stochastic differential equations using sum-of-squares programming. Discrete and Continuous Dynamical Systems-B , 23(2):939–956, 2018

2018
[20]

Neural stochastic control

Jingdong Zhang, Qunxi Zhu, and Wei Lin. Neural stochastic control. Advances in NeurIPS , 35, 2022

2022
[21]

Stability verification in stochastic control systems via neural network supermartingales

Mathias Lechner, Ðor ¯de Žikeli ´c, Krishnendu Chatterjee, and Thomas A Henzinger. Stability verification in stochastic control systems via neural network supermartingales. In Proc. of AAAI , volume 36(7), pages 7326–7336, 2022

2022
[22]

Learning control policies for region stabilization in stochastic systems

Matin Ansaripour, Mathias Lechner, Ðorde Žikelic, Krishnendu Chat- terjee, and Thomas A Henzinger. Learning control policies for region stabilization in stochastic systems. arXiv:2210.05304, 2022

2022 arXiv
[23]

dReal: An SMT solver for nonlinear theories over the reals

Sicun Gao, Soonho Kong, and Edmund M Clarke. dReal: An SMT solver for nonlinear theories over the reals. In Proc. of CADE , pages 208–214. Springer, 2013

2013
[24]

Stochastic stability of differential equations , volume 66

Rafail Khasminskii. Stochastic stability of differential equations , volume 66. Springer Science & Business Media, 2011

2011
[25]

Stochastic Differential Equations and Applications

Xuerong Mao. Stochastic Differential Equations and Applications . Elsevier, 2007

2007
[26]

A generalization of Zubov’s method to perturbed systems

Fabio Camilli, Lars Grüne, and Fabian Wirth. A generalization of Zubov’s method to perturbed systems. SIAM Journal on Control and Optimization, 40(2):496–515, 2001

2001
[27]

Local Lyapunov functions for nonlinear stochastic differen- tial equations by linearization

Hjörtur Björnsson, Peter Giesl, Skuli Gudmundsson, and Sigurdur F Hafstein. Local Lyapunov functions for nonlinear stochastic differen- tial equations by linearization. In Proc. of ICINCO , pages 589–596, 2018

2018
[28]

Stochastic Lyapunov-barrier functions for robust probabilistic reach-avoid-stay specifications

Yiming Meng and Jun Liu. Stochastic Lyapunov-barrier functions for robust probabilistic reach-avoid-stay specifications. IEEE Transactions on Automatic Control , 2024

2024
[29]

Scalable neural network verification with branch-and-bound inferred cutting planes

Duo Zhou, Christopher Brix, Grani A Hanasusanto, and Huan Zhang. Scalable neural network verification with branch-and-bound inferred cutting planes. arXiv:2501.00200, 2024

2024

Pith tools

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

[1] [1]

Neural Lyapunov control

Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov control. Advances in NeurIPS , 32, 2019

work page 2019

[2] [2]

Neural Lyapunov control of unknown nonlinear systems with stability guar- antees

Ruikun Zhou, Thanin Quartz, Hans De Sterck, and Jun Liu. Neural Lyapunov control of unknown nonlinear systems with stability guar- antees. Advances in NeurIPS , 35, 2022

work page 2022

[3] [3]

Region of attraction in a power system with discrete LTCs

Costas D V ournas and Nikos G Sakellaridis. Region of attraction in a power system with discrete LTCs. IEEE Transactions on Circuits and Systems I: Regular Papers , 53(7):1610–1618, 2006

work page 2006

[4] [4]

Regions of attraction for hybrid limit cycles of walking robots

Ian R Manchester, Mark M Tobenkin, Michael Levashov, and Russ Tedrake. Regions of attraction for hybrid limit cycles of walking robots. IFAC Proceedings Volumes, 44(1):5801–5806, 2011

work page 2011

[5] [5]

Region of attraction estimation of biological continuous boolean models

Megan Leigh Matthews and Cranos M Williams. Region of attraction estimation of biological continuous boolean models. In Proc. of IEEE SMC, pages 1700–1705. IEEE, 2012

work page 2012

[6] [6]

Maximal Lyapunov functions and domains of attraction for autonomous nonlinear systems

Anthony Vannelli and Mathukumalli Vidyasagar. Maximal Lyapunov functions and domains of attraction for autonomous nonlinear systems. Automatica, 21(1):69–80, 1985

1985

[7] [7]

Towards learning and verifying maximal neural Lyapunov functions

Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. Towards learning and verifying maximal neural Lyapunov functions. In Proc. of CDC , pages 8012–8019. IEEE, 2023

work page 2023

[8] [8]

Physics-informed neural network Lyapunov functions: PDE charac- terization, learning, and verification

Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. Physics-informed neural network Lyapunov functions: PDE charac- terization, learning, and verification. Automatica, 175:112193, 2025

work page 2025