提出符号化方法高效验证神经控制屏障函数，提升机器人安全控制可靠性。
Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation
- 利用符号导数边界传播，结合激活函数阶梯形式推导梯度界。
- 在多种机器人模型上验证率与耗时均优于区间算术基线。
- 适合关注神经控制安全性的研究者与工业应用开发者。
控制屏障函数（CBFs）在安全关键系统和机器人控制中至关重要。近年来，神经网络被用于参数化复杂系统的有界控制输入的CBFs。然而，如何高效地以符号方式验证预训练的神经控制屏障函数（神经CBFs）仍具挑战。为此，本文提出一种针对基于ReLU的神经CBFs的新验证框架，通过结合线性有界非线性动态系统与神经CBFs的梯度边界，实现符号导数边界传播。具体地，利用激活函数导数的Heaviside阶跃函数形式，证明了符号边界可通过神经CBF雅可比矩阵与非线性系统动力学的内积进行传播。在不同机器人动力学上的大量实验表明，该方法在沿CBF边界的验证率和验证时间上均优于基于区间算术的基线方法，验证了所提方法的有效性与高效性。代码已开源：https://github.com/intelligent-control-lab/verify-neural-CBF。
原文摘要 · Abstract (English)
Control barrier functions (CBFs) are important in safety-critical systems and robot control applications. Neural networks have been used to parameterize and synthesize CBFs with bounded control input for complex systems. However, it is still challenging to verify pre-trained neural networks CBFs (neural CBFs) in an efficient symbolic manner. To this end, we propose a new efficient verification framework for ReLU-based neural CBFs through symbolic derivative bound propagation by combining the linearly bounded nonlinear dynamic system and the gradient bounds of neural CBFs. Specifically, with Heaviside step function form for derivatives of activation functions, we show that the symbolic bounds can be propagated through the inner product of neural CBF Jacobian and nonlinear system dynamics. Through extensive experiments on different robot dynamics, our results outperform the interval arithmetic based baselines in verified rate and verification time along the CBF boundary, validating the effectiveness and efficiency of the proposed method with different model complexity. The code can be found at https://github.com/intelligent-control-lab/ verify-neural-CBF.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。