Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations
Formal verification of neural control barrier functions (NCBFs) remains challenging, especially for neural networks with nonlinear activations like \(\tanh\). Existing CROWN-based methods rely on conservative linear relaxations for Jacobian bounds, limiting scalability. We propose LightCROWN, which computes tighter Jacobian bounds by exploiting the analytical properties of activation functions. Experiments on nonlinear control systems including the inverted pendulum, Dubins car, and planar quadrotor demonstrate that LightCROWN improves verification success rates up to 100\%, while enhancing speed and scalability. Our approach provides a generalizable improvement for CROWN-based frameworks, enabling more efficient verification of complex NCBFs. The code can be found at github.com/Autonomous-Systems-and-Control-Lab/verify-neural-CBF.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Exact Verification of ReLU Neural Control Barrier Functions
Control Barrier Functions (CBFs) are a popular approach for safe control of nonlinear systems. In CBF-based control, the desired safety properties of the system are mapped to nonnegativity of a CBF, and the control input…
Safe Stabilization using Nonsmooth Control Lyapunov Barrier Function
This paper addresses the challenge of safe stabilization, ensuring the system state reach the origin while avoiding unsafe regions. Existing approaches relying on smooth Lyapunov barrier functions often fail to guarantee…
Learning Safe Neural Network Controllers with Barrier Certificates
We provide a novel approach to synthesize controllers for nonlinear continuous dynamical systems with control against safety properties. The controllers are based on neural networks (NNs). To certify the safety property …
Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation
Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems. Recently, CBFs represented as neural networks have shown great promise due to their expressiveness and …
Smooth Zone Barrier Lyapunov Functions for Nonlinear Constrained Control Systems
This paper introduces the Smooth Zone Barrier Lyapunov Function (s-ZBLF) for output and full-state constrained nonlinear control systems. Unlike traditional BLF methods, where control effort continuously increases as the…