Pith. sign in

REVIEW 4 major objections 4 minor 59 references

Neural Continuous-Time Supermartingale Certificates

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

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

Pith's one-line read This paper introduces the first neural-certificate framework that yields formally certified probability bounds for reachability, avoidance, and persistence in continuous-time stochastic systems.

desk verdict New continuous-time neural supermartingale framework, but the stay-property proof has a load-bearing gap that invalidates the stated persistence bound as written. read the letter →

arxiv 2412.17432 v1 pith:YOORMZ67 submitted 2024-12-23 eess.SY cs.AIcs.SY

Grigory Neustroev , Mirco Giacobbe , Anna Lukina This is my paper · ORCID
classification eess.SYcs.AIcs.SY MSC 60H1060G4668Q6093E15
keywords neuralcertificatessupermartingalecontinuous-timestochasticsystemsreach-avoid-stayformalverificationintervalboundpropagationdifferentialequationsprobabilisticcontrolguarantees
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 seeks to establish that a single learned function—a reach-avoid-stay certificate—can provide formally certified probability bounds for a continuous-time stochastic system: the probability that trajectories from a given initial set reach a target while avoiding unsafe states, and the probability that they stay in the target afterwards. This matters because existing neural certificates either assume discrete time or ignore stochasticity, so they cannot give sound guarantees for physical systems governed by stochastic differential equations. The authors propose a proof rule (Theorem 1) that connects six local conditions on the certificate and its infinitesimal generator to the specification probabilities $\varepsilon$ and $\delta$, and an algorithm that trains such a certificate by gradient descent and verifies it by interval bound propagation. They demonstrate the method on an inverted pendulum with a neural controller and on a bivariate geometric Brownian motion.

What carries the argument

The load-bearing object is the reach-avoid-stay certificate (RAS-C): a nonnegative, smooth function $V(t,x)$ whose infinitesimal generator $G_\pi V$ is forced to decrease outside the target and, inside the target, outside a small sublevel set, with four thresholds $\alpha_S < \beta_S < \alpha_{RA} < \beta_{RA}$. Around it the proof wraps a stopped process $Y_t = V(t \wedge \psi, X_{t\wedge\psi})$, where $\psi$ is the first time the certificate leaves $[\alpha_S,\beta_{RA})$; because the decrease and stay conditions make $\psi$ finite almost surely and $Y$ a nonnegative supermartingale, optional stopping bounds the certificate's expected value at stopping times and the maximal inequality converts that expectation into tail probabilities. The algorithmic counterpart is a neural network trained by a loss that penalizes violations of each condition, with the generator evaluated through analytic Hessian computations, and a verifier using interval bound propagation over axis-aligned cells that splits cells until the decrease condition is checked on a cover of the required region.

What would settle it

Run the trained certificate on the bivariate geometric Brownian motion example under many simulated trajectories, record the certificate value $V(\psi, X_\psi)$ at the first time it leaves $[\alpha_S,\beta_{RA})$, and compute the empirical average of those values. If the average exceeds $\alpha_S$, the maximal-inequality step of the stay proof fails and the claimed stay probability does not follow from the stated conditions.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: if a twice continuously differentiable function $V$ satisfies six conditions—nonnegativity, an upper bound $\alpha_{RA}$ on initial states, a lower bound $\beta_{RA}$ on unsafe states, a generator-decrease condition outside the target, a sub-$\beta_S$ goal set inside the target, and a generator-decrease condition inside the target outside a sub-$\alpha_S$ set—with constants ordered $\alpha_S < \beta_S < \alpha_{RA} < \beta_{RA}$, then the controlled process satisfies the reach-avoid-stay specification with reach-avoid probability at least $\varepsilon = 1 - \alpha_{RA}/\beta_{RA}$ and stay probability at least $\delta = 1 - \alpha_S/\beta_S$. The proof constructs the first time $\psi$ at which the certificate leaves the interval $[\alpha_S, \beta_{RA})$, shows that the stopped process is a supermartingale, and applies maximal and optional-stopping inequalities to turn the local decrease conditions into global probability bounds. The authors further claim that this is the first neural-certificate framework for continuous-time stochastic systems, and that the training-plus-verification pipeline produces sound lower bounds on the specification probabilities.

Load-bearing premise

The stay-probability proof assumes, without derivation, that the expected certificate value at the stopping time $\psi$ is at most $\alpha_S$; if that expectation can exceed $\alpha_S$, the claimed persistence probability is unsupported.

Editorial extensions

If this is right

  • A successful verification run yields a sound lower bound on each specification probability, so a valid certificate gives an honest guarantee about every trajectory from the initial set.
  • Systems with non-polynomial drift or diffusion, including neural-network policies, become verifiable because the certificate is trained and checked without symbolically integrating the dynamics.
  • The same certificate covers reachability, avoidance, and persistence simultaneously, and omitting unused conditions certifies reach-avoid or stay alone.
  • The verified probabilities are set by the ratios $\alpha_{RA}/\beta_{RA}$ and $\alpha_S/\beta_S$, so choosing the four thresholds controls how strong each guarantee is.

Reading between the lines

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

  • Beyond the paper: because the generator includes $\partial/\partial t$ and the sets are allowed to depend on time, the same proof structure should extend to moving or growing target and unsafe sets.
  • Beyond the paper: the ratio form of the bounds suggests that optimizing the level thresholds, rather than fixing them, could improve certified probabilities without changing the network architecture.
  • Beyond the paper: since training only needs samples of drift and diffusion, the certificate could be trained jointly with the control policy, turning verification into a synthesis objective rather than a post-hoc check.
  • Beyond the paper: adding an explicit condition that the certificate's expected value at $\psi$ is below $\alpha_S$ would make the persistence bound self-contained and is directly testable on the two benchmarks.
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.

Referee Report

4 major / 4 minor

Summary. The paper proposes a framework for neural certificate-based verification of continuous-time stochastic dynamical systems against probabilistic reach-avoid-stay (RAS) specifications. The main theoretical contribution is Theorem 1, which states that a function V satisfying six conditions (nonnegativity, initial, safety, decrease, goal, stay) with constants αS < βS < αRA < βRA certifies the specification with avoidance probability ε = 1 - αRA/βRA and stay probability δ = 1 - αS/βS. The paper also presents a training algorithm that samples from the dynamics and an interval-bound-propagation (IBP) verifier, with experiments on an inverted pendulum and a bivariate geometric Brownian motion.

Significance. If the proof of Theorem 1 were correct, the paper would make a substantial contribution: it would extend neural supermartingale certificates to continuous-time SDEs, provide quantitative probabilistic guarantees, and include a reproducible prototype with code. The claimed first-ness of continuous-time neural supermartingale certification is plausible based on the related work review. However, the stay-property proof in the Technical Appendix contains a load-bearing gap, and the training and verification pipeline has internal inconsistencies. The central quantitative claim (the stay probability δ) is therefore not established as written.

major comments (4)
  1. [Technical Appendix, Proof of Theorem 1 (stay part)] The proof asserts P(sup_{t≥ψ} V(t,X_{π,t}) ≥ βS) ≤ (1/βS) E[V(0,X_{π,ψ})] ≤ αS/βS. The first inequality misapplies Proposition 5: after shifting time by ψ, the initial value of the shifted process is V(ψ,X_{π,ψ}), not V(0,X_{π,ψ}). The second inequality is not derived from Definition 2: optional stopping applied to the ψ-stopped supermartingale gives E[V(ψ,X_{π,ψ})] ≤ V(0,x0) ≤ αRA, and no condition in Definition 2 bounds this expectation by αS. Since ψ can exit the interval [αS,βRA) through the high side with probability only bounded by αRA/βRA, the contribution of that exit event to the expectation is not controlled by αS. Consequently, the stated stay probability δ = 1 - αS/βS is unsupported.
  2. [Technical Appendix, Proof of Theorem 1 (opposite event)] The decomposition of the complement of {sup_{t≥ψ} V ≥ βS} as {∀t≥ψ: V < βS} ∩ {∄γ < βS: ∀t≥ψ: V < γ} is false: the second clause is equivalent to sup_{t≥ψ} V ≥ βS, so the intersection is the null event {sup = βS}, not the complement. The intended conclusion P(∀t≥ψ: V < βS) ≥ 1 - αS/βS would follow directly from the maximal inequality, but the erroneous decomposition makes the argument invalid as written.
  3. [Eq. (13), Training] The goal loss L⋆ = Σ_{x∈B∩X⋆} (βS - Vθ(x))_+ penalizes the certificate for being below βS inside the target set. This is the reverse of the goal condition (Definition 2, condition 5), which requires the existence of a sublevel set L^-_{βS}(V) within X⋆, i.e., values V ≤ βS somewhere in X⋆. The intended penalty should be (Vθ(x) - βS)_+. As written, the training objective drives Vθ away from satisfying the goal condition, so Algorithm 1 cannot learn a certificate in the direction required by Theorem 1.
  4. [Eq. (18), Verification] The generator decrease/stay conditions are checked only on cells with Vlow(C) > αS and Vup(C) ≤ βRA. Cells that intersect the level set {V = αS} or {V = βRA} are excluded and never split, although Definition 2 requires GπV ≤ -ζ (and GπV ≤ -ξ) on the full sets L^-_{βRA}\int X⋆ and X⋆∩L^-_{βRA}\int L^-_{αS}. Thus a successful verification does not imply that the certificate conditions hold on the domains used in the proof of Theorem 1, so the formal guarantee is not discharged by the algorithm.
minor comments (4)
  1. [Technical Appendix, Proposition 2 and Lemma 2] There are typos in this appendix: 'recurreny citerion' should be 'recurrence criterion', and the statement 'β ≤ ρ' in Lemma 2 should read 'αS ≤ βRA'.
  2. [Technical Appendix, Proof of Theorem 1 (opposite event)] The entire paragraph on the 'opposite event' could be removed, since the maximal inequality already gives the desired bound directly; as written it is confusing and mathematically incorrect.
  3. [Eq. (17), Verification] The goal-condition verification only checks V ≥ βS on cells intersecting ∂X⋆. To establish L^-_{βS} ⊆ X⋆ one needs a lower bound on V on all of X \ X⋆, or an explicit topological assumption ensuring that a sublevel set crossing outside X⋆ must intersect ∂X⋆.
  4. [Remark 3] The statement 'we can fix either αRA or βRA beforehand' is unclear, since the ratios are fixed by the specification; consider rewording to explain how the free scaling is used.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the probability bounds are derived from the certificate conditions and independently verified, with no fitted quantity or load-bearing self-citation.

full rationale

The paper's derivation is self-contained. Definition 2 states sufficient conditions on the certificate V, and Theorem 1 derives the reach-avoid and stay probability bounds from standard supermartingale maximal inequalities (Khasminskii 2011; Prajna et al. 2004). The certificate is trained by minimizing violation losses and then independently verified with interval bound propagation; the reported probabilities epsilon_hat and delta_hat are computed from verified cell bounds, not from the training loss or from a fitted parameter. The constants alpha_RA, beta_RA, alpha_S, and beta_S are chosen from the desired epsilon and delta, but the theorem's implication (conditions imply bounds) is not an equivalence, and the verification does not assume the conclusion. The authors' self-citations appear only in related-work context and are not load-bearing for Theorem 1. A genuine proof gap exists in the stay part of Theorem 1's appendix: the bound E[V(0,X_{pi,psi})] <= alpha_S is not implied by Definition 2, and the displayed equality for the complement of the staying event is algebraically false. This is a soundness and correctness defect in the paper as written, not a circular reduction: the missing bound is not an input to Definition 2, and no equation in the derivation reduces by construction to a fitted or assumed quantity. Therefore the circularity score is 0.

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

The central derivation relies on standard Itô calculus tools (generator, optional stopping, maximal inequality) and on the soundness of interval bound propagation. The threshold levels are user-set design parameters that define the guaranteed probabilities, not fitted values. No new physical entities are introduced.

free parameters (4)
  • κ (verification slack) = 4
    Chosen to force the training to find larger probabilities ε and δ, giving slack to the verification procedure. Affects the derived thresholds.
  • ζ (generator threshold) = 1.0
    Constant used in the decrease and stay conditions of Definition 2. Set by hand, not fitted to data.
  • λ (regularizer multiplier) = 0.1
    Weight-norm regularization term in the loss to keep network weights small and ease verification.
  • αRA, βRA, βS, αS = 1, 40, 0.9, 0.0225
    Threshold levels of the certificate, set by the user via ε, δ, and κ. They define the guaranteed probabilities ε = 1 - αRA/βRA and δ = 1 - αS/βS. Not fitted to data.
assumptions (5)
  • domain assumption SDE (1) has a unique strong solution under Lipschitz and growth conditions, and the state process is a Feller-Dynkin process with infinitesimal generator (6).
    Invoked in 'Problem Statement' and 'A Primer on Stochastic Calculus' to justify the use of the generator and the recurrence criterion.
  • standard math Proposition 2 (recurrence criterion, Khasminskii) is valid: a generator bound with divergent integral implies almost-sure finite exit from a domain.
    Used in Lemma 2 to show ψ < ∞ a.s.
  • standard math Proposition 5 (maximal inequality for nonnegative supermartingales) and optional stopping apply to the stopped certificate process.
    Used in the proof of Theorem 1 to bound the probability of leaving sublevel sets.
  • ad hoc to paper The goal condition of Definition 2 implies that the sublevel set L^-_{βS}(V) is entirely contained in X⋆.
    The wording 'there exists a sub-βS set' is ambiguous, but the proof of Theorem 1 uses L^-_{βS}(V) ⊂ X⋆. This stronger interpretation is necessary for the proof.
  • domain assumption Interval bound propagation (IBP) yields sound upper and lower bounds on V and GπV over each axis-aligned cell, and the cell partition together with recursive splitting covers all points where the certificate conditions must hold.
    Assumed in Section 'Verification'. The algorithm's soundness depends on IBP providing valid interval bounds and on the cell covering being exhaustive, which is not fully established for cells straddling the αS or X⋆ boundaries.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Neural Continuous-Time Supermartingale Certificates." pith.science (2026). https://pith.science/paper/YOORMZ67

@misc{pith2026241217432,
  author       = {Pith},
  title        = {Pith review of: Neural Continuous-Time Supermartingale Certificates},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YOORMZ67}},
  note         = {Machine review of arXiv:2412.17432}
}
read the original abstract

We introduce for the first time a neural-certificate framework for continuous-time stochastic dynamical systems. Autonomous learning systems in the physical world demand continuous-time reasoning, yet existing learnable certificates for probabilistic verification assume discretization of the time continuum. Inspired by the success of training neural Lyapunov certificates for deterministic continuous-time systems and neural supermartingale certificates for stochastic discrete-time systems, we propose a framework that bridges the gap between continuous-time and probabilistic neural certification for dynamical systems under complex requirements. Our method combines machine learning and symbolic reasoning to produce formally certified bounds on the probabilities that a nonlinear system satisfies specifications of reachability, avoidance, and persistence. We present both the theoretical justification and the algorithmic implementation of our framework and showcase its efficacy on popular benchmarks.

Figures

Figures reproduced from arXiv: 2412.17432 by the authors.

Figure 1
Figure 1. A neural supermartingale certificate for the [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. A (time-homogenous) example of the sets of Def [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Architecture of the neural certificate training and [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: An example of a neural supermartingale certificate [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: 0 5 10 15 20 25 30 35 40 45 50 0 5 10 X󰂏 σ = 0 X⊘ σ = 0.84 σ = 0.92 σ = 1 t x [PITH_FULL_IMAGE:figures/full_fig_p008_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

59 extracted references · 53 canonical work pages

  1. [1]

    , " * write output.state after.block = add.period write newline

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.a...

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

  3. [3]

    Abate, A.; Ahmed, D.; Giacobbe, M.; and Peruffo, A. 2021. Formal Synthesis of L yapunov Neural Networks. IEEE Control. Syst. Lett. , 5(3): 773--778

    work page 2021

  4. [4]

    Abate, A.; Edwards, A.; Giacobbe, M.; Punchihewa, H.; and Roy, D. 2023. Quantitative Verification with Neural Networks. In CONCUR , volume 279 of LIPIcs, 22:1--22:18. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik

    work page 2023

  5. [5]

    Abate, A.; Giacobbe, M.; and Roy, D. 2021. Learning Probabilistic Termination Proofs. In CAV (2) , volume 12760 of Lecture Notes in Computer Science, 3--26. Springer

    work page 2021

  6. [6]

    Abate, A.; Giacobbe, M.; and Roy, D. 2024. Stochastic Omega-Regular Verification and Control with Supermartingales. In CAV (3) , volume 14683 of Lecture Notes in Computer Science, 395--419. Springer

    work page 2024

  7. [7]

    E.; Botoeva, E.; Kouvaros, P.; and Lomuscio, A

    Akintunde, M. E.; Botoeva, E.; Kouvaros, P.; and Lomuscio, A. 2022. Formal verification of neural agents in non-deterministic environments. Auton. Agents Multi Agent Syst., 36(1): 6

    work page 2022

  8. [8]

    Anand, M.; and Zamani, M. 2023. Formally Verified Neural Network Control Barrier Certificates for Unknown Systems. IFAC-PapersOnLine, 56(2): 2431--2436

    work page 2023

Show all 59 references
  1. [9]

    A.; Lechner, M.; and Z ikeli\'c, D

    Ansaripour, M.; Chatterjee, K.; Henzinger, T. A.; Lechner, M.; and Z ikeli\'c, D. 2023. Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems. In ATVA (1) , volume 14215 of Lecture Notes in Computer Science, 357--379. Springer

    2023

  2. [10]

    Bacci, E.; Giacobbe, M.; and Parker, D. 2021. Verifying Reinforcement Learning up to Infinity. In IJCAI , 2154--2160. ijcai.org

    2021

  3. [11]

    Badings, T.; Koops, W.; Junges, S.; and Jansen, N. 2024. Learning-Based Verification of Stochastic Dynamical Systems with Neural Network Policies. arXiv:2406.00826

    2024 arXiv

  4. [12]

    Blumenthal, R.; and Getoor, R. 1968. Markov Processes and Potential Theory. Pure and applied mathematics : a series of monographs and textbooks. Academic Press. ISBN 9780121078508

    1968

  5. [13]

    Chang, Y.-C.; Roohi, N.; and Gao, S. 2019. Neural L yapunov Control. In NeurIPS , 3240--3249

    2019

  6. [14]

    A.; Lechner, M.; and Z ikeli\'c, D

    Chatterjee, K.; Henzinger, T. A.; Lechner, M.; and Z ikeli\'c, D. 2023. A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems. In TACAS (1) , volume 13993 of Lecture Notes in Computer Science, 3--25. Springer

    2023

  7. [15]

    J.; and Preciado, V

    Chen, S.; Fazlyab, M.; Morari, M.; Pappas, G. J.; and Preciado, V. M. 2021 a . Learning L yapunov functions for hybrid systems. In HSCC , 13:1--13:11. ACM

    2021

  8. [16]

    J.; and Preciado, V

    Chen, S.; Fazlyab, M.; Morari, M.; Pappas, G. J.; and Preciado, V. M. 2021 b . Learning Region of Attraction for Nonlinear Systems. In CDC , 6477--6484. IEEE

    2021

  9. [17]

    Dawson, C.; Gao, S.; and Fan, C. 2023. Safe Control With Learned Certificates: A Survey of Neural L yapunov, Barrier, and Contraction Methods for Robotics and Control. IEEE Trans. Robotics , 39(3): 1749--1767

    2023

  10. [18]

    Dawson, C.; Qin, Z.; Gao, S.; and Fan, C. 2021. Safe Nonlinear Control Using Robust Neural L yapunov-Barrier Functions. In CoRL, volume 164 of Proceedings of Machine Learning Research, 1724--1735. PMLR

    2021

  11. [19]

    Edwards, A.; Peruffo, A.; and Abate, A. 2023. A General Verification Framework for Dynamical and Control Models via Certificate Synthesis. CoRR, abs/2309.06090

    2023 arXiv

  12. [20]

    Gehr, T.; Mirman, M.; Drachsler-Cohen, D.; Tsankov, P.; Chaudhuri, S.; and Vechev, M. T. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In IEEE Symposium on Security and Privacy , 3--18. IEEE Computer Society

    2018

  13. [21]

    Giacobbe, M.; Kroening, D.; Pal, A.; and Tautschnig, M. 2024. Neural Model Checking. In NeurIPS

    2024

  14. [22]

    Giacobbe, M.; Kroening, D.; and Parsert, J. 2022. Neural termination analysis. In ESEC/SIGSOFT FSE , 633--645. ACM

    2022

  15. [23]

    E.; and Bertram, J

    Kalman, R. E.; and Bertram, J. E. 1959. Control system analysis and design via the second method of L yapunov: (I) continuous-time systems (II) discrete time systems. IRE Transactions on Automatic Control, 4(3): 112

    1959

  16. [24]

    W.; Dill, D

    Katz, G.; Barrett, C. W.; Dill, D. L.; Julian, K.; and Kochenderfer, M. J. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In CAV (1) , volume 10426 of Lecture Notes in Computer Science, 97--117. Springer

    2017

  17. [25]

    Khasminskii, R. 2011. Stochastic Stability of Differential Equations. Stochastic Modelling and Applied Probability. Springer

    2011

  18. [26]

    Z.; and Manek, G

    Kolter, J. Z.; and Manek, G. 2019. Learning Stable Deep Dynamics Models. In NeurIPS , 11126--11134

    2019

  19. [27]

    Kouvaros, P.; and Lomuscio, A. 2021. Towards Scalable Complete Verification of ReLU Neural Networks via Dependency-based Branching. In IJCAI, 2643--2650

    2021

  20. [28]

    Le Gall, J.-F. 2016. B rownian Motion, Martingales, and Stochastic Calculus . Graduate Texts in Mathematics. Springer

    2016

  21. [29]

    L.; Chen, R

    Li, X.; Wong, T.-K. L.; Chen, R. T. Q.; and Duvenaud, D. 2020. Scalable Gradients for Stochastic Differential Equations. In AISTATS , volume 108 of Proceedings of Machine Learning Research, 3870--3882. PMLR

    2020

  22. [30]

    Long, Y.; and Bayoumi, M. 1993. Feedback stabilization: control L yapunov functions modelled by neural networks. In CDC , 2812--2814. IEEE

    1993

  23. [31]

    L.; Ravaioli, U

    Mandal, U.; Amir, G.; Wu, H.; Daukantas, I.; Newell, F. L.; Ravaioli, U. J.; Meng, B.; Durling, M.; Ganai, M.; Shim, T.; Katz, G.; and Barrett, C. 2024. Formally Verifying Deep Reinforcement Learning Controllers with L yapunov Barrier Certificates. arXiv:2405.14058

    2024 arXiv

  24. [32]

    B.; Calvert, S

    Mathiesen, F. B.; Calvert, S. C.; and Laurenti, L. 2023. Safety Certification for Stochastic Systems via Neural Barrier Functions. IEEE Control. Syst. Lett. , 7: 973--978

    2023

  25. [33]

    Nadali, A.; Murali, V.; Trivedi, A.; and Zamani, M. 2024. Neural Closure Certificates. In AAAI , 21446--21453. AAAI Press

    2024

  26. [34]

    Noroozi, N.; Karimaghaee, P.; Safaei, F.; and Javadi, H. 2008. Generation of L yapunov functions by neural networks. In Proceedings of the World Congress on Engineering

    2008

  27. [35]

    Papachristodoulou, A.; and Prajna, S. 2002. On the construction of L yapunov functions using the sum of squares decomposition. In CDC , 3482--3487. IEEE

    2002

  28. [36]

    Petridis, V.; and Petridis, S. 2006. Construction of Neural Network Based L yapunov Functions. In IJCNN , 5059--5065. IEEE

    2006

  29. [37]

    Prajna, S.; Jadbabaie, A.; and Pappas, G. J. 2004. Stochastic safety verification using barrier certificates. In CDC , 929--934. IEEE

    2004

  30. [38]

    Prajna, S.; Jadbabaie, A.; and Pappas, G. J. 2007. A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates. IEEE Trans. Autom. Control. , 52(8): 1415--1428

    2007

  31. [39]

    Prokhorov, D. V. 1994. A L yapunov machine for stability analysis of nonlinear systems. In ICNN , 1028--1031. IEEE

    1994

  32. [40]

    Qin, Z.; Zhang, K.; Chen, Y.; Chen, J.; and Fan, C. 2021. Learning Safe Multi-agent Control with Decentralized Neural Barrier Certificates. In ICLR . OpenReview.net

    2021

  33. [41]

    M.; Berkenkamp, F.; and Krause, A

    Richards, S. M.; Berkenkamp, F.; and Krause, A. 2018. The L yapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems. In CoRL, volume 87 of Proceedings of Machine Learning Research, 466--476. PMLR

    2018

  34. [42]

    Serpen, G. 2005. Empirical approximation for L yapunov functions with artificial neural nets. In IJCNN , 735--740. IEEE

    2005

  35. [43]

    Singla, S.; and Feizi, S. 2020. Second-Order Provable Defenses against Adversarial Attacks. In ICML , volume 119 of Proceedings of Machine Learning Research, 8981--8991. PMLR

    2020

  36. [44]

    M.; and Shakarchi, R

    Stein, E. M.; and Shakarchi, R. 2009. Real analysis: measure theory, integration, and H ilbert spaces . Princeton University Press

    2009

  37. [45]

    Sun, D.; Jha, S.; and Fan, C. 2020. Learning Certified Control Using Contraction Metric. In CoRL, volume 155 of Proceedings of Machine Learning Research, 1519--1539. PMLR

    2020

  38. [46]

    Takeishi, N.; and Kawahara, Y. 2021. Learning Dynamics Models with Stable Invariant Sets. In AAAI , 9782--9790. AAAI Press

    2021

  39. [47]

    K.; and Seiler, P

    Topcu, U.; Packard, A. K.; and Seiler, P. J. 2008. Local stability analysis using simulations and sum-of-squares programming. Autom., 44(10): 2669--2675

    2008

  40. [48]

    M.; Musau, P.; Nguyen, L

    Tran, H.-D.; Yang, X.; Lopez, D. M.; Musau, P.; Nguyen, L. V.; Xiang, W.; Bak, S.; and Johnson, T. T. 2020. NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems. In CAV (1) , volume 12224 of Lecture Notes in Computer Sc...

    2020

  41. [49]

    L.; Kokke, W.; Refaeli, I.; Amir, G.; Julian, K.; Bassan, S.; Huang, P.; Lahav, O.; Wu, M.; Zhang, M.; Komendantskaya, E.; Katz, G.; and Barrett, C

    Wu, H.; Isac, O.; Zeljic, A.; Tagomori, T.; Daggitt, M. L.; Kokke, W.; Refaeli, I.; Amir, G.; Julian, K.; Bassan, S.; Huang, P.; Lahav, O.; Wu, M.; Zhang, M.; Komendantskaya, E.; Katz, G.; and Barrett, C. W. 2024. Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In...

    2024

  42. [50]

    Wu, J.; Clark, A.; Kantaros, Y.; and Vorobeychik, Y. 2023. Neural L yapunov Control for Discrete-Time Systems. In NeurIPS

    2023

  43. [51]

    Xu, K.; Shi, Z.; Zhang, H.; Wang, Y.; Chang, K.-W.; Huang, M.; Kailkhura, B.; Lin, X.; and Hsieh, C.-J. 2020. Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond. In NeurIPS

    2020

  44. [52]

    Yang, L.; Dai, H.; Shi, Z.; Hsieh, C.-J.; Tedrake, R.; and Zhang, H. 2024. L yapunov-Stable Neural Control for State and Output Feedback: A Novel Formulation. In ICML . OpenReview.net

    2024

  45. [53]

    Zhang, H.; Weng, T.-W.; Chen, P.-Y.; Hsieh, C.-J.; and Daniel, L. 2018. Efficient Neural Network Robustness Certification with General Activation Functions. In NeurIPS , 4944--4953

    2018

  46. [54]

    Zhang, H.; Wu, J.; Vorobeychik, Y.; and Clark, A. 2023 a . Exact Verification of ReLU Neural Control Barrier Functions. In NeurIPS

    2023

  47. [55]

    Zhang, J.; Zhu, Q.; and Lin, W. 2022. Neural Stochastic Control. In NeurIPS

    2022

  48. [56]

    Zhang, S.; Xiu, Y.; Qu, G.; and Fan, C. 2023 b . Compositional Neural Certificates for Networked Dynamical Systems. In L4DC , volume 211 of Proceedings of Machine Learning Research, 272--285. PMLR

    2023

  49. [57]

    Zhao, H.; Zeng, X.; Chen, T.; and Liu, Z. 2020. Synthesizing barrier certificates using neural networks. In HSCC , 25:1--25:11. ACM

    2020

  50. [58]

    A.; and Chatterjee, K

    Z ikeli\'c, D.; Lechner, M.; Henzinger, T. A.; and Chatterjee, K. 2023 a . Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees. In AAAI , 11926--11935. AAAI Press

    2023

  51. [59]

    Z ikeli\'c, D.; Lechner, M.; Verma, A.; Chatterjee, K.; and Henzinger, T. A. 2023 b . Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees. In NeurIPS

    2023

Pith tools

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