pith. sign in

arxiv: 2605.26577 · v1 · pith:ZD2YZOM6new · submitted 2026-05-26 · 📡 eess.SY · cs.AI· cs.LG· cs.SY· math.OC

Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial

Haoyu Li , Xiangru Zhong , Hao Cheng , Bin Hu , Huan Zhang This is my paper

Pith reviewed 2026-06-29 16:16 UTC · model grok-4.3

classification 📡 eess.SY cs.AIcs.LGcs.SYmath.OC
keywords neural network verificationcontrol theoryLyapunov stabilityformal verificationalpha-beta-CROWNsafety-critical systemsreachability analysisneural controllers
0
0 comments X

The pith

α,β-CROWN verifier turns control problems into bound computations over state domains for scalable stability and safety checks.

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

The paper shows how the α,β-CROWN bounding engine can verify neural-network controller properties such as stability and safety without relying on special structural assumptions. It starts from the observation that many control tasks reduce to checking real-valued inequalities over a state domain, then uses tight certified bounds on the nonlinear functions to decide those inequalities. The engine also supports reachability analysis directly from the bounds and can recursively partition and prune subdomains to finish the check. GPU acceleration makes the approach scale to higher-dimensional systems where earlier methods slow down. The tutorial presents this as a general bridge between control theory and neural-network verification tools.

Core claim

α,β-CROWN is a general-purpose bounding engine for nonlinear functions given as computation graphs; given an input domain it returns certified bounds and explicit linear relaxations. These bounds suffice for reachability analysis on their own and, when combined with recursive partitioning and pruning of subdomains, allow satisfiability checking and optimization. Because Lyapunov stability, safety, and similar control conditions reduce to real-valued inequalities over state domains, the same engine verifies those conditions at scale.

What carries the argument

α,β-CROWN bounding engine that produces certified bounds and linear relaxations for nonlinear functions represented as computation graphs, then uses those bounds for recursive subdomain partitioning and pruning.

If this is right

  • Lyapunov stability conditions become checkable for arbitrary neural controllers by feeding the Lyapunov function into the bounding engine.
  • Reachability sets for closed-loop systems are obtained directly from the certified bounds without separate set-propagation code.
  • Optimization-based controller synthesis gains certified feasibility checks via the same bounding and pruning pipeline.
  • GPU-parallel bound computation removes the dimensionality bottleneck that limits traditional symbolic or SMT-based verifiers.
  • The same pipeline applies unchanged to safety invariants expressed as inequalities over the state.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach could be applied to verify other inequality-defined properties in dynamical systems, such as invariance or dissipativity.
  • Integration with controller synthesis loops would let the verifier guide gradient updates toward provably stable networks.
  • Real-time embedded deployment becomes plausible once the pruned-domain computation finishes within a fixed time budget.

Load-bearing premise

Control verification problems can be expressed as checking real-valued inequalities over a state domain that the bounding engine can process directly.

What would settle it

A concrete Lyapunov or safety certificate for a neural controller whose truth value cannot be settled by α,β-CROWN bounds even after exhaustive partitioning of the state domain.

Figures

Figures reproduced from arXiv: 2605.26577 by Bin Hu, Hao Cheng, Haoyu Li, Huan Zhang, Xiangru Zhong.

Figure 1
Figure 1. Figure 1: Computation graph of Equation (6). The abstraction above captures many models and specifi￾cations that are commonly used in learning and control. For example, it is clear that any standard feed-forward network or more complicated neural network structures, such as residual networks or transformers, can be specified in this form with an appropriate choice of nodes, edges, and operators. Furthermore, many in… view at source ↗
Figure 2
Figure 2. Figure 2: Computation graph of the Lyapunov condition. For illustration, [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 4
Figure 4. Figure 4: Overview structure of α,β-CROWN 1) Initial Falsification: The process begins with a falsi￾fier, where we typically apply a projected gradient descent (PGD) [96] to search for counterexamples to the verification condition. Concretely, PGD performs gradient-based mini￾mization on the violation objective (e.g., the margin in (5)) over a large batch of initial candidates, and after each step projects the candi… view at source ↗
read the original abstract

Learning-based methods for synthesizing controllers have gained popularity due to their high expressiveness and strong empirical performance. However, in safety-critical scenarios such as autonomous driving, robotics, and power systems, empirical performance alone is insufficient, and formal verification of controller properties such as stability and safety is highly desirable. Unfortunately, many prior verification approaches are either tied to specific structural assumptions on the system or the certificate, making them difficult to transfer across settings, or suffer from poor scalability on higher-dimensional neural network systems. In this tutorial, we present a unified framework that aims to mitigate this gap via bridging control with the state-of-the-art neural network verifier $\alpha,\!\beta$-CROWN (alpha-beta-CROWN). At its core, $\alpha,\!\beta$-CROWN is a general-purpose bounding engine for nonlinear functions represented as computation graphs: given an input domain, it can produce certified bounds and explicit linear relaxation of the nonlinear function. These certified bounds are useful on their own for tasks such as reachability analysis, and they also provide the foundation for more complex routines that perform satisfiability checking and optimization. More specifically, many control problems reduce to verifying real-valued inequalities over a state domain (e.g., Lyapunov theory). Consequently, $\alpha,\!\beta$-CROWN enables scalable verification of such conditions by computing tight bounds and recursively partitioning and pruning subdomains based on the bounds. Thanks to GPU parallelization, this pipeline demonstrates superior scalability on verification and optimization problems that are challenging for traditional approaches. In this tutorial, we discuss the basics of $\alpha,\!\beta$-CROWN and introduce its application to various control-related tasks.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript is a tutorial introducing the α,β-CROWN neural network verifier as a tool for control verification tasks. It describes reducing problems such as stability and safety certification (e.g., via Lyapunov inequalities) to real-valued inequality verification over state domains, then using the verifier's certified bounds, linear relaxations, recursive subdomain partitioning/pruning, and GPU parallelization to achieve scalable checking and optimization for learning-based controllers in high-dimensional systems.

Significance. If the explanations and examples are accurate and self-contained, the tutorial could modestly advance adoption of general-purpose neural-network verifiers within the control community by highlighting their applicability to inequality-based certificates without requiring problem-specific structural assumptions. Its primary contribution is expository rather than theoretical; no new derivations, proofs, or benchmarks are introduced, so significance rests on clarity of the bridge to existing α,β-CROWN capabilities.

minor comments (3)
  1. Abstract: the phrase 'unified framework' is used to describe the pipeline, yet the text appears to apply an existing external tool without defining new unifying theory, algorithms, or reductions; this wording may overstate novelty for a tutorial and should be revised to 'application framework' or similar.
  2. Abstract and §1 (inferred from description): the claim of 'superior scalability' relative to traditional approaches is asserted without any quantitative comparison, timing data, or new case studies inside the manuscript; readers are referred to prior α,β-CROWN literature, which reduces the tutorial's standalone evidentiary value.
  3. Notation: the special formatting α,β-CROWN (with thin spaces) appears inconsistently; a consistent textual rendering such as 'alpha-beta-CROWN' should be used alongside the math mode to improve readability across PDF and HTML versions.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the constructive summary and for recommending minor revision. The report accurately captures the tutorial's focus on applying the existing α,β-CROWN verifier to control verification tasks via bound computation and domain partitioning. No major comments were listed in the report.

Circularity Check

0 steps flagged

No circularity: tutorial applies established external verifier

full rationale

The paper is a tutorial describing the application of the pre-existing α,β-CROWN bounding engine to control verification tasks such as Lyapunov inequalities. No new derivations, equations, fitted parameters, or predictions are introduced that could reduce to self-definition or self-citation. The central statements restate standard uses of neural network verifiers (bound computation plus domain partitioning) without any load-bearing self-referential steps or imported uniqueness claims. The derivation chain is self-contained against external benchmarks and contains no reductions by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based solely on the abstract; the tutorial rests on one domain assumption from control theory and the capabilities of the pre-existing α,β-CROWN tool. No free parameters or invented entities appear.

axioms (1)
  • domain assumption Many control problems reduce to verifying real-valued inequalities over a state domain
    Stated directly in the abstract as the justification for applying the bounding engine to control tasks.

pith-pipeline@v0.9.1-grok · 5848 in / 1108 out tokens · 50394 ms · 2026-06-29T16:16:41.145335+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

102 extracted references · 21 canonical work pages · 7 internal anchors

  1. [1]

    Champion-level drone racing using deep rein- forcement learning,

    E. Kaufmann, L. Bauersfeld, A. Loquercio, M. M ¨uller, V . Koltun, and D. Scaramuzza, “Champion-level drone racing using deep rein- forcement learning,”Nature, vol. 620, no. 7976, pp. 982–987, 2023

    2023

  2. [2]

    Applications of machine learning in real-time control systems: a review,

    X. Zhao, Y . Sun, Y . Li, N. Jia, and J. Xu, “Applications of machine learning in real-time control systems: a review,”Measurement Science and Technology, 2024

    2024

  3. [3]

    (deep) reinforcement learning for electric power system control and related problems: A short review and perspectives,

    M. Glavic, “(deep) reinforcement learning for electric power system control and related problems: A short review and perspectives,” Annual Reviews in Control, vol. 48, pp. 22–35, 2019

    2019

  4. [4]

    Reinforcement learning for control: Performance, stability, and deep approximators,

    L. Bus ¸oniu, T. De Bruin, D. Toli ´c, J. Kober, and I. Palunko, “Reinforcement learning for control: Performance, stability, and deep approximators,”Annual Reviews in Control, vol. 46, pp. 8–28, 2018

    2018

  5. [5]

    Verification approaches for learning-enabled autonomous cyber–physical systems,

    H.-D. Tran, W. Xiang, and T. T. Johnson, “Verification approaches for learning-enabled autonomous cyber–physical systems,”IEEE Design & Test, vol. 39, no. 1, pp. 24–34, 2020

    2020

  6. [6]

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

    C. Dawson, S. Gao, and C. Fan, “Safe control with learned certifi- cates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control,”IEEE Transactions on Robotics, vol. 39, no. 3, pp. 1749–1767, 2023

    2023

  7. [7]

    Neural lyapunov control,

    Y .-C. Chang, N. Roohi, and S. Gao, “Neural lyapunov control,” Advances in neural information processing systems, vol. 32, 2019

    2019

  8. [8]

    Formal synthesis of stochas- tic systems via control barrier certificates,

    P. Jagtap, S. Soudjani, and M. Zamani, “Formal synthesis of stochas- tic systems via control barrier certificates,”IEEE Transactions on Automatic Control, vol. 66, no. 7, pp. 3097–3110, 2020

    2020

  9. [9]

    Formally verified physics-informed neural control lyapunov functions,

    J. Liu, M. Fitzsimmons, R. Zhou, and Y . Meng, “Formally verified physics-informed neural control lyapunov functions,” in2025 Amer- ican Control Conference (ACC). IEEE, 2025, pp. 1347–1354

    2025

  10. [10]

    Physics-informed neural network lyapunov functions: Pde characterization, learning, and verification,

    J. Liu, Y . Meng, M. Fitzsimmons, and R. Zhou, “Physics-informed neural network lyapunov functions: Pde characterization, learning, and verification,”Automatica, vol. 175, p. 112193, 2025

    2025

  11. [11]

    Learning regions of attraction in unknown dynamical systems via zubov-koopman lifting: Regularities and convergence,

    Y . Meng, R. Zhou, and J. Liu, “Learning regions of attraction in unknown dynamical systems via zubov-koopman lifting: Regularities and convergence,”IEEE Transactions on Automatic Control, 2025

    2025

  12. [12]

    Tool lyznet: A lightweight python tool for learning and verifying neural lyapunov functions and regions of attraction,

    J. Liu, Y . Meng, M. Fitzsimmons, and R. Zhou, “Tool lyznet: A lightweight python tool for learning and verifying neural lyapunov functions and regions of attraction,” inProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, 2024, pp. 1–8

    2024

  13. [13]

    Actor-critic physics-informed neural lya- punov control,

    J. Wang and M. Fazlyab, “Actor-critic physics-informed neural lya- punov control,”IEEE Control Systems Letters, 2024

    2024

  14. [14]

    Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models,

    A. Edwards, A. Peruffo, and A. Abate, “Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models,” in Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, 2024, pp. 1–10

    2024

  15. [15]

    Towards learning and verifying maximal neural lyapunov functions,

    J. Liu, Y . Meng, M. Fitzsimmons, and R. Zhou, “Towards learning and verifying maximal neural lyapunov functions,” in2023 62nd IEEE Conference on Decision and Control (CDC). IEEE, 2023, pp. 8012–8019

    2023

  16. [16]

    dreal: An smt solver for nonlinear theories over the reals,

    S. Gao, S. Kong, and E. M. Clarke, “dreal: An smt solver for nonlinear theories over the reals,” inInternational conference on automated deduction. Springer, 2013, pp. 208–214

    2013

  17. [17]

    Z3: An efficient smt solver,

    L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” inIn- ternational conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337–340

    2008

  18. [18]

    Evaluating Robustness of Neural Networks with Mixed Integer Programming

    V . Tjeng, K. Xiao, and R. Tedrake, “Evaluating robustness of neural networks with mixed integer programming,”arXiv preprint arXiv:1711.07356, 2017

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  19. [19]

    Reluplex: An efficient smt solver for verifying deep neural net- works,

    G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient smt solver for verifying deep neural net- works,” inInternational conference on computer aided verification. Springer, 2017, pp. 97–117

    2017

  20. [20]

    The marabou framework for verification and analysis of deep neural networks,

    G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zelji´cet al., “The marabou framework for verification and analysis of deep neural networks,” inInterna- tional conference on computer aided verification. Springer, 2019, pp. 443–452

    2019

  21. [21]

    Stability and feasibility of neural network- based controllers via output range analysis,

    B. Karg and S. Lucia, “Stability and feasibility of neural network- based controllers via output range analysis,” in2020 59th IEEE Conference on Decision and Control (CDC). IEEE, 2020, pp. 4947– 4954

    2020

  22. [22]

    Lyapunov- stable neural-network control,

    H. Dai, B. Landry, L. Yang, M. Pavone, and R. Tedrake, “Lyapunov- stable neural-network control,”arXiv preprint arXiv:2109.14152, 2021

    work page arXiv 2021

  23. [23]

    Neural lyapunov control for discrete-time systems,

    J. Wu, A. Clark, Y . Kantaros, and Y . V orobeychik, “Neural lyapunov control for discrete-time systems,”Advances in neural information processing systems, vol. 36, pp. 2939–2955, 2023

    2023

  24. [24]

    A tutorial on sum of squares techniques for systems analysis,

    A. Papachristodoulou and S. Prajna, “A tutorial on sum of squares techniques for systems analysis,” inProceedings of the 2005, Amer- ican Control Conference, 2005.IEEE, 2005, pp. 2686–2700

    2005

  25. [25]

    Stability analysis using quadratic constraints for systems with neural network controllers,

    H. Yin, P. Seiler, and M. Arcak, “Stability analysis using quadratic constraints for systems with neural network controllers,”IEEE Trans- actions on Automatic Control, vol. 67, no. 4, pp. 1980–1987, 2021

    1980

  26. [26]

    Verification and synthesis of compatible control lyapunov and control barrier functions,

    H. Dai, C. Jiang, H. Zhang, and A. Clark, “Verification and synthesis of compatible control lyapunov and control barrier functions,” in 2024 IEEE 63rd Conference on Decision and Control (CDC). IEEE, 2024, pp. 8178–8185

    2024

  27. [27]

    Stability of non-linear neural feedback loops using sum of squares,

    M. Newton and A. Papachristodoulou, “Stability of non-linear neural feedback loops using sum of squares,” in2022 IEEE 61st Conference on Decision and Control (CDC). IEEE, 2022, pp. 6000–6005

    2022

  28. [28]

    Improved sum-of-squares stability verification of neural-network-based controllers,

    A. Detailleur, G. Ducard, and C. Onder, “Improved sum-of-squares stability verification of neural-network-based controllers,”arXiv preprint arXiv:2507.10352, 2025

    work page arXiv 2025

  29. [29]

    Imitation learning with stability and safety guarantees,

    H. Yin, P. Seiler, M. Jin, and M. Arcak, “Imitation learning with stability and safety guarantees,”IEEE Control Systems Letters, vol. 6, pp. 409–414, 2021

    2021

  30. [30]

    A semialgebraic framework for verification and synthe- sis of control barrier functions,

    A. Clark, “A semialgebraic framework for verification and synthe- sis of control barrier functions,”IEEE Transactions on Automatic Control, vol. 70, no. 5, pp. 3101–3116, 2024

    2024

  31. [31]

    Control contraction metric synthesis for discrete-time nonlinear systems,

    L. Wei, R. Mccloy, and J. Bao, “Control contraction metric synthesis for discrete-time nonlinear systems,”IFAC-PapersOnLine, vol. 54, no. 3, pp. 661–666, 2021

    2021

  32. [32]

    Lqr- trees: Feedback motion planning via sums-of-squares verification,

    R. Tedrake, I. R. Manchester, M. Tobenkin, and J. W. Roberts, “Lqr- trees: Feedback motion planning via sums-of-squares verification,” The International Journal of Robotics Research, vol. 29, no. 8, pp. 1038–1052, 2010

    2010

  33. [33]

    Safety index synthesis via sum-of-squares programming,

    W. Zhao, T. He, T. Wei, S. Liu, and C. Liu, “Safety index synthesis via sum-of-squares programming,” inAmerican Control Conference. IEEE, 2023, pp. 732–737

    2023

  34. [34]

    Verification of neural control barrier functions with symbolic derivative bounds propagation,

    H. Hu, Y . Yang, T. Wei, and C. Liu, “Verification of neural control barrier functions with symbolic derivative bounds propagation,” in Proceedings of The 8th Conference on Robot Learning, ser. Proceed- ings of Machine Learning Research, vol. 270. PMLR, 06–09 Nov 2025, pp. 1797–1814

    2025

  35. [35]

    Exact verification of relu neural control barrier functions,

    H. Zhang, J. Wu, Y . V orobeychik, and A. Clark, “Exact verification of relu neural control barrier functions,”Advances in neural information processing systems, vol. 36, pp. 5685–5705, 2023

    2023

  36. [36]

    Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

    N. Vertovec, F. B. Mathiesen, T. Badings, L. Laurenti, and A. Abate, “Scalable verification of neural control barrier functions using linear bound propagation,”arXiv preprint arXiv:2511.06341, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  37. [37]

    Real-time safe control of neural network dynamic models with sound approximation,

    H. Hu, J. Lan, and C. Liu, “Real-time safe control of neural network dynamic models with sound approximation,” inLearning for Dynamics and Control Conference, 2024. [Online]. Available: https://proceedings.mlr.press/v242/hu24a.html

    2024

  38. [38]

    Verifiable safety q-filters via hamilton-jacobi reachability and multiplicative q-networks,

    J. Li, H. Hu, Y . Yang, and C. Liu, “Verifiable safety q-filters via hamilton-jacobi reachability and multiplicative q-networks,” IEEE Control Systems Letters, 2025. [Online]. Available: https: //ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=11157757

    2025

  39. [39]

    Provable defenses against adversarial examples via the convex outer adversarial polytope,

    E. Wong and Z. Kolter, “Provable defenses against adversarial examples via the convex outer adversarial polytope,” inInternational conference on machine learning. PMLR, 2018, pp. 5286–5295

    2018

  40. [40]

    Certified defenses against adversarial examples,

    A. Raghunathan, J. Steinhardt, and P. Liang, “Certified defenses against adversarial examples,”arXiv preprint arXiv:1801.09344, 2018

    work page arXiv 2018

  41. [41]

    A unified view of sdp-based neural network verification through completely positive programming,

    R. A. Brown, E. Schmerling, N. Azizan, and M. Pavone, “A unified view of sdp-based neural network verification through completely positive programming,” inInternational conference on artificial in- telligence and statistics. PMLR, 2022, pp. 9334–9355

    2022

  42. [42]

    Ai2: Safety and robustness certification of neural networks with abstract interpretation,

    T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, “Ai2: Safety and robustness certification of neural networks with abstract interpretation,” in2018 IEEE symposium on security and privacy (SP). IEEE, 2018, pp. 3–18

    2018

  43. [43]

    Fast and effective robustness certification,

    G. Singh, T. Gehr, M. Mirman, M. P ¨uschel, and M. Vechev, “Fast and effective robustness certification,”Advances in neural information processing systems, vol. 31, 2018

    2018

  44. [44]

    Efficient Neural Network Robustness Certification with General Activation Functions

    H. Zhang, T.-W. Weng, P.-Y . Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,”Advances in Neural Information Processing Systems, vol. 31, pp. 4939–4948, 2018. [Online]. Available: https://arxiv.org/pdf/1811.00866.pdf

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  45. [45]

    Efficient interaction- aware interval analysis of neural network feedback loops,

    S. Jafarpour, A. Harapanahalli, and S. Coogan, “Efficient interaction- aware interval analysis of neural network feedback loops,”IEEE Transactions on Automatic Control, vol. 69, no. 12, pp. 8706–8721, 2024

    2024

  46. [46]

    Interval reachability of nonlinear dynamical systems with neural network controllers,

    ——, “Interval reachability of nonlinear dynamical systems with neural network controllers,” inLearning for Dynamics and Control Conference. PMLR, 2023, pp. 12–25

    2023

  47. [47]

    On the effectiveness of interval bound propagation for training verifiably robust models,

    S. Gowal, K. Dvijotham, R. Stanforth, R. Bunel, C. Qin, J. Uesato, R. Arandjelovic, T. Mann, and P. Kohli, “On the effectiveness of interval bound propagation for training verifiably robust models,” arXiv preprint arXiv:1810.12715, 2018

    work page arXiv 2018

  48. [48]

    A convex relaxation barrier to tight robustness verification of neural networks,

    H. Salman, G. Yang, H. Zhang, C.-J. Hsieh, and P. Zhang, “A convex relaxation barrier to tight robustness verification of neural networks,” Advances in Neural Information Processing Systems, vol. 32, pp. 9835–9846, 2019

    2019

  49. [49]

    Automatic perturbation analysis for scalable certified robustness and beyond,

    K. Xu, Z. Shi, H. Zhang, Y . Wang, K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh, “Automatic perturbation analysis for scalable certified robustness and beyond,”Advances in Neural Information Processing Systems, vol. 33, 2020

    2020

  50. [50]

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

    K. Xu, H. Zhang, S. Wang, Y . Wang, S. Jana, X. Lin, and C.-J. Hsieh, “Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers,” inInternational Conference on Learning Representations, 2021. [Online]. Available: https://openreview.net/forum?id=nVZtXBI6LNn

    2021

  51. [51]

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

    S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter, “Beta-CROWN: Efficient bound propagation with per- neuron split constraints for complete and incomplete neural network verification,”Advances in Neural Information Processing Systems, vol. 34, 2021

    2021

  52. [52]

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

    H. Zhang, S. Wang, K. Xu, L. Li, B. Li, S. Jana, C.-J. Hsieh, and J. Z. Kolter, “General cutting planes for bound-propagation-based neural network verification,”Advances in Neural Information Processing Systems, 2022

    2022

  53. [53]

    Prov- ably bounding neural network preimages,

    S. Kotha, C. Brix, J. Z. Kolter, K. Dvijotham, and H. Zhang, “Prov- ably bounding neural network preimages,” inAdvances in Neural Information Processing Systems, A. Oh, T. Neumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine, Eds., vol. 36. Curran Associates, Inc., 2023, pp. 80 270–80 290

    2023

  54. [54]

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

    D. Zhou, C. Brix, G. A. Hanasusanto, and H. Zhang, “Scalable neural network verification with branch-and-bound inferred cutting planes,” inThe Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024

    2024

  55. [55]

    Neural network verification with branch-and-bound for general nonlinearities,

    Z. Shi, Q. Jin, Z. Kolter, S. Jana, C.-J. Hsieh, and H. Zhang, “Neural network verification with branch-and-bound for general nonlinearities,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2025

    2025

  56. [56]

    Clip-and-verify: Linear constraint-driven domain clip- ping for accelerating neural network verification,

    D. Zhou, J. Chavez, H. Chen, G. A. Hanasusanto, and H. Zhang, “Clip-and-verify: Linear constraint-driven domain clip- ping for accelerating neural network verification,”arXiv preprint arXiv:2512.11087, 2025

    work page arXiv 2025

  57. [57]

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

    L. Yang, H. Dai, Z. Shi, C.-J. Hsieh, R. Tedrake, and H. Zhang, “Lyapunov-stable neural control for state and output feedback: A novel formulation,”arXiv preprint arXiv:2404.07956, 2024

    work page arXiv 2024

  58. [58]

    Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control

    Z. Shi, H. Li, C.-J. Hsieh, and H. Zhang, “Certified training with branch-and-bound for lyapunov-stable neural control,”arXiv preprint arXiv:2411.18235, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  59. [59]

    Neural contraction metrics with formal guarantees for discrete-time nonlinear dynamical systems.arXiv preprint arXiv:2504.17102, 2025

    H. Li, X. Zhong, B. Hu, and H. Zhang, “Neural contraction metrics with formal guarantees for discrete-time nonlinear dynamical sys- tems,”arXiv preprint arXiv:2504.17102, 2025

    work page arXiv 2025

  60. [60]

    Safe domains of at- traction for discrete-time nonlinear systems: Characterization and ver- ifiable neural network estimation,

    M. Serry, H. Li, R. Zhou, H. Zhang, and J. Liu, “Safe domains of at- traction for discrete-time nonlinear systems: Characterization and ver- ifiable neural network estimation,”arXiv preprint arXiv:2506.13961, 2025

    work page arXiv 2025

  61. [61]

    Two-stage learning of stabilizing neural controllers via zubov sampling and iterative domain expansion.arXiv preprint arXiv:2506.01356, 2025

    H. Li, X. Zhong, B. Hu, and H. Zhang, “Two-stage learning of stabilizing neural controllers via zubov sampling and iterative domain expansion,”arXiv preprint arXiv:2506.01356, 2025

    work page arXiv 2025

  62. [62]

    Flow*: An ana- lyzer for non-linear hybrid systems,

    X. Chen, E. ´Abrah´am, and S. Sankaranarayanan, “Flow*: An ana- lyzer for non-linear hybrid systems,” inInternational Conference on Computer Aided Verification. Springer, 2013, pp. 258–263

    2013

  63. [63]

    Set propagation techniques for reachability analysis,

    M. Althoff, G. Frehse, and A. Girard, “Set propagation techniques for reachability analysis,”Annual Review of Control, Robotics, and Autonomous Systems, vol. 4, no. 1, pp. 369–395, 2021

    2021

  64. [64]

    Nnv: the neural network verification tool for deep neural networks and learning-enabled cyber- physical systems,

    H.-D. Tran, X. Yang, D. Manzanas Lopez, P. Musau, L. V . Nguyen, W. Xiang, S. Bak, and T. T. Johnson, “Nnv: the neural network verification tool for deep neural networks and learning-enabled cyber- physical systems,” inInternational conference on computer aided verification. Springer, 2020, pp. 3–17

    2020

  65. [65]

    Reachability analysis of neural network control systems,

    C. Zhang, W. Ruan, and P. Xu, “Reachability analysis of neural network control systems,” inProceedings of the AAAI Conference on Artificial Intelligence, vol. 37, no. 12, 2023, pp. 15 287–15 295

    2023

  66. [66]

    Reachability analysis of neural network control systems with tunable accuracy and efficiency,

    Y . Zhang, H. Zhang, and X. Xu, “Reachability analysis of neural network control systems with tunable accuracy and efficiency,”IEEE Control Systems Letters, vol. 8, pp. 1697–1702, 2024

    2024

  67. [67]

    Safe reach set computation via neural barrier certificates,

    A. Abate, S. Bogomolov, A. Edwards, K. Potomkin, S. Soudjani, and P. Zuliani, “Safe reach set computation via neural barrier certificates,” IFAC-PapersOnLine, vol. 58, no. 11, pp. 107–114, 2024

    2024

  68. [68]

    Parallel differentiable reachability for learning and planning with certified neural dynamics and controllers,

    K. Shen and G. Chou, “Parallel differentiable reachability for learning and planning with certified neural dynamics and controllers,” in Proceedings of Robotics: Science and Systems (RSS), 2026

    2026

  69. [69]

    Efficient finite abstraction of mixed mono- tone systems,

    S. Coogan and M. Arcak, “Efficient finite abstraction of mixed mono- tone systems,” inProceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 2015, pp. 58–67

    2015

  70. [70]

    Finite abstraction of mixed monotone systems with discrete and continuous inputs,

    ——, “Finite abstraction of mixed monotone systems with discrete and continuous inputs,”Nonlinear Analysis: Hybrid Systems, vol. 23, pp. 254–271, 2017

    2017

  71. [71]

    Mixed monotonicity for reachability and safety in dynamical systems,

    S. Coogan, “Mixed monotonicity for reachability and safety in dynamical systems,” in2020 59th IEEE Conference on Decision and Control (CDC). IEEE, 2020, pp. 5074–5085

    2020

  72. [72]

    Specification-guided verification and abstraction refinement of mixed monotone stochastic systems,

    M. Dutreix and S. Coogan, “Specification-guided verification and abstraction refinement of mixed monotone stochastic systems,”IEEE Transactions on Automatic Control, vol. 66, no. 7, pp. 2975–2990, 2020

    2020

  73. [73]

    Overt: An algorithm for safety verification of neural network control policies for nonlinear systems,

    C. Sidrane, A. Maleki, A. Irfan, and M. J. Kochenderfer, “Overt: An algorithm for safety verification of neural network control policies for nonlinear systems,”Journal of Machine Learning Research, vol. 23, no. 117, pp. 1–45, 2022

    2022

  74. [74]

    Zubov-koopman learning of maximal lyapunov functions,

    Y . Meng, R. Zhou, and J. Liu, “Zubov-koopman learning of maximal lyapunov functions,” in2024 American Control Conference (ACC). IEEE, 2024, pp. 4020–4025

    2024

  75. [75]

    Towards learning and verifying maximal lyapunov-barrier functions with a zubov pde formulation,

    Y . Meng and J. Liu, “Towards learning and verifying maximal lyapunov-barrier functions with a zubov pde formulation,”arXiv preprint arXiv:2511.09523, 2025

    work page arXiv 2025

  76. [76]

    Formal verification of control lyapunov-barrier func- tions for safe stabilization with bounded controls,

    J. Liu, “Formal verification of control lyapunov-barrier func- tions for safe stabilization with bounded controls,”arXiv preprint arXiv:2511.10510, 2025

    work page arXiv 2025

  77. [77]

    Control barrier function based quadratic programs for safety critical systems,

    A. D. Ames, X. Xu, J. W. Grizzle, and P. Tabuada, “Control barrier function based quadratic programs for safety critical systems,”IEEE Transactions on Automatic Control, vol. 62, no. 8, pp. 3861–3876, 2016

    2016

  78. [78]

    Learning control barrier functions from expert demonstrations,

    A. Robey, H. Hu, L. Lindemann, H. Zhang, D. V . Dimarogonas, S. Tu, and N. Matni, “Learning control barrier functions from expert demonstrations,” in2020 59th IEEE Conference on Decision and Control (CDC). Ieee, 2020, pp. 3717–3724

    2020

  79. [79]

    Convex synthesis and verification of control-lyapunov and barrier functions with input constraints,

    H. Dai and F. Permenter, “Convex synthesis and verification of control-lyapunov and barrier functions with input constraints,” in 2023 American Control Conference (ACC). IEEE, 2023, pp. 4116– 4123

    2023

  80. [80]

    Safe nonlinear control using robust neural lyapunov-barrier functions,

    C. Dawson, Z. Qin, S. Gao, and C. Fan, “Safe nonlinear control using robust neural lyapunov-barrier functions,” inConference on Robot Learning. PMLR, 2022, pp. 1724–1735

    2022

Showing first 80 references.