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

• URL: http://arxiv.org/abs/2605.26577v1
• Date: Tue, 26 May 2026 05:49:19 GMT
• Title: Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial
• Abstract summary: $,!$-CROWN is a general-purpose bounding engine for nonlinear functions represented as graphs.<n>In this tutorial, we discuss the basics of $,!$-CROWN and introduce its application to various control-related computation tasks.
• Score: 23.69448525306035
• License: http://creativecommons.org/licenses/by/4.0/
• 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 $α,\!β$-CROWN (alpha-beta-CROWN). At its core, $α,\!β$-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, $α,\!β$-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 $α,\!β$-CROWN and introduce its application to various control-related tasks.

Related papers

• Implicit Neural Networks as Static Controllers: Certificates and Performance Separation [0.8747606955991705]
  Implicit neural controllers (INCs) are static feedback laws that are evaluated through an algebraic fixed point equation<n>We propose a so-called implicit representation of neural networks as a key enabling device that exposes the controller as a trainable linear interconnection closed through a known static activation map.<n>For finite-dimensional LTI plants, we first develop a rigorous analysis theory for a given INC, including Perron--Frobenius and norm conditions for well posedness.<n>We then formulate as a certification synthesis search: training is carried out under explicit well-posedness constraints, implicit-differentiation formulas
  arXiv  Detail & Related papers  (2026-07-13T05:56:49Z)
• Hierarchical End-to-End Taylor Bounds for Complete Neural Network Verification [10.685380941330687]
  Reachability analysis of neural networks seeks to compute or bound the set of outputs attainable over a given input domain.<n>Existing approaches exploit at most second-order information and do not systematically leverage higher-order information.<n>We introduce textscHiTaB, a novel verification framework that exploits second-order smoothness through both the Hessian, $nabla2 f$, and its Lipschitz constant, $L_nabla2 f$.
  arXiv  Detail & Related papers  (2026-05-11T14:16:13Z)
• Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification [9.733843486234878]
  State-of-the-art neural network (NN) verifiers demonstrate that applying the branch-and-bound (BaB) procedure with fast bounding techniques plays a key role in tackling many challenging verification properties.<n>We introduce the linear constraint-driven clipping framework, a class of scalable and efficient methods designed to enhance the efficacy of NN verifiers.
  arXiv  Detail & Related papers  (2025-12-11T19:59:37Z)
• Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation [50.53301323864253]
  Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems.<n>We present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF.<n>Our approach scales to larger neural networks than state-of-the-art verification procedures for CBFs.
  arXiv  Detail & Related papers  (2025-11-09T11:51:15Z)
• A General Framework for Property-Driven Machine Learning [1.0485739694839669]
  We show that adversarial training can be used to improve robustness to small perturbations within $epsilon$-cubes.<n> domains other than computer vision may require more flexible input region specifications via generalised hyper-rectangles.<n>In this paper, we investigate how these two complementary approaches can be unified within a single framework for property-driven machine learning.
  arXiv  Detail & Related papers  (2025-05-01T11:33:38Z)
• Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
  Learning-based neural network (NN) control policies have shown impressive empirical performance in a wide range of tasks in robotics and control. Lyapunov stability guarantees over the region-of-attraction (ROA) for NN controllers with nonlinear dynamical systems are challenging to obtain. We demonstrate a new framework for learning NN controllers together with Lyapunov certificates using fast empirical falsification and strategic regularizations.
  arXiv  Detail & Related papers  (2024-04-11T17:49:15Z)
• Stable Nonconvex-Nonconcave Training via Linear Interpolation [51.668052890249726]
  This paper presents a theoretical analysis of linearahead as a principled method for stabilizing (large-scale) neural network training. We argue that instabilities in the optimization process are often caused by the nonmonotonicity of the loss landscape and show how linear can help by leveraging the theory of nonexpansive operators.
  arXiv  Detail & Related papers  (2023-10-20T12:45:12Z)
• Towards Practical Control of Singular Values of Convolutional Layers [65.25070864775793]
  Convolutional neural networks (CNNs) are easy to train, but their essential properties, such as generalization error and adversarial robustness, are hard to control. Recent research demonstrated that singular values of convolutional layers significantly affect such elusive properties. We offer a principled approach to alleviating constraints of the prior art at the expense of an insignificant reduction in layer expressivity.
  arXiv  Detail & Related papers  (2022-11-24T19:09:44Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety. We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior.
  arXiv  Detail & Related papers  (2021-11-18T23:21:00Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  Neural networks can learn complex, non- adversarial functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. We propose an approach that integrates the optimization process into the verification procedure, achieving better performance than the naive approach.
  arXiv  Detail & Related papers  (2020-10-07T08:19:48Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.