提出更精确的神经控制屏障函数验证方法，提升成功率与效率。
Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations
- 利用激活函数解析性质计算更紧的雅可比边界
- 在倒立摆等系统上验证成功率最高提升100%
- 适合需要高效形式化验证的复杂控制系统研究者
神经控制屏障函数（NCBF）的形式化验证仍具挑战性，尤其针对具有非线性激活函数（如tanh）的神经网络。现有基于CROWN的方法依赖保守的线性松弛来估计雅可比边界，限制了可扩展性。本文提出LightCROWN，通过利用激活函数的解析特性，计算出更紧的雅可比边界。在倒立摆、杜宾斯车和平面四旋翼等非线性控制系统上的实验表明，LightCROWN将验证成功率最高提升100%，同时显著提高速度与可扩展性。该方法为基于CROWN的框架提供了通用改进，使复杂NCBF的高效验证成为可能。代码可在github.com/Autonomous-Systems-and-Control-Lab/verify-neural-CBF获取。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。