基于符号导数界传播的神经控制屏障函数验证

控制屏障函数 (CBF) 在安全关键系统和机器人控制应用中至关重要。神经网络被用于参数化和合成具有有界控制输入的 CBF 以适应复杂系统。然而，仍然具有挑战在符号效率地验证预训练的神经 CBF (神经 CBF)。为此，我们提出一种通过结合线性有界非线性动力系统和神经 CBF 梯度界的符号导数界传播来实现的高效验证框架。具体而言，借助激活函数导数的 Heaviside 步进函数形式，我们展示符号界可通过神经 CBF 雅可比矩阵与非线性系统动力学的内积来传播。通过在不同机器人动力学上的大量实验，我们的结果在 CBF 边界上的验证率和验证时间方面超过基于区间算术的基线，验证了所提出方法在不同模型复杂度下的有效性和效率。代码可在 https://github.com/intelligent-control-lab/verify-neural-CBF 查找。