ReLU 神经控制障碍函数的精确验证
机器学习
2023-10-17 v1
摘要
控制障碍函数(CBFs)是非线性系统安全控制的一种流行方法。在基于 CBF 的控制中,系统期望的安全属性被映射为 CBF 的非负性,并选择控制输入以确保 CBF 在所有时刻保持非负。近来,将 CBF 表示为神经网络(神经控制障碍函数,NCBFs)的机器学习方法因神经网络的通用表示能力而展现出巨大前景。然而,验证所学 CBF 能保证安全性仍是一个具有挑战性的研究问题。本文提出了用于验证具有 ReLU 激活函数的前馈 NCBF 安全性的新颖精确条件与算法。这样做的关键挑战在于,由于 ReLU 函数的分段线性, NCBF 在某些点不可微,从而使假设障碍函数光滑的传统安全验证方法失效。我们通过利用 Nagumo 定理对具有非光滑边界集合不变性的推广,推导安全性的充要条件来解决此问题。基于此条件,我们提出了一种 NCBF 安全验证算法,该算法首先将 NCBF 分解为分段线性段,然后求解非线性规划以验证每一段以及线性段交集的安全性。我们通过仅考虑安全区域边界并使用区间界限传播(IBP)和线性松弛修剪分段来降低复杂度。我们通过数值研究评估了我们的方法,并与最先进的基于 SMT 的方法进行比较。我们的代码可在 https://github.com/HongchaoZhang-HZ/exactverif-reluncbf-nips23 获取。
引用
@article{arxiv.2310.09360,
title = {Exact Verification of ReLU Neural Control Barrier Functions},
author = {Hongchao Zhang and Junlin Wu and Yevgeniy Vorobeychik and Andrew Clark},
journal= {arXiv preprint arXiv:2310.09360},
year = {2023}
}