Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911662624210944 |
|---|---|
| author | Zhang, Jun Zhang, Haibo Liu, Chun Wang, Xiaofan Xu, Liang |
| author_facet | Zhang, Jun Zhang, Haibo Liu, Chun Wang, Xiaofan Xu, Liang |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_07757 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations Zhang, Jun Zhang, Haibo Liu, Chun Wang, Xiaofan Xu, Liang Machine Learning 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. |
| title | Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations |
| topic | Machine Learning |
| url | https://arxiv.org/abs/2605.07757 |