提升神经控制屏障函数的安全验证效率
SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions
- 用新正则化减少安全边界处的激活区域数
- 通过紧致上界逼近降低每段验证开销
- 适用于需高安全保证的非线性系统控制
神经控制屏障函数（NCBF）在保障非线性自治系统的安全约束方面展现出巨大潜力。现有精确验证方法利用ReLU神经网络的分段线性结构，但仍需枚举靠近安全边界的全部激活区域，导致计算成本高。本文提出合成与高效精确验证框架（SEEV），包含两个部分：(i) 一种引入新型正则化的NCBF合成算法，以减少安全边界附近的激活区域数量；(ii) 一种利用安全条件紧致上界逼近的验证算法，降低每个分段线性片段的验证开销。仿真结果表明，SEEV在多种基准系统和神经网络结构下显著提升验证效率，同时保持了良好的CBF性能。代码已开源：https://github.com/HongchaoZhang-HZ/SEEV。
原文摘要 · Abstract (English)
Neural Control Barrier Functions (NCBFs) have shown significant promise in enforcing safety constraints on nonlinear autonomous systems. State-of-the-art exact approaches to verifying safety of NCBF-based controllers exploit the piecewise-linear structure of ReLU neural networks, however, such approaches still rely on enumerating all of the activation regions of the network near the safety boundary, thus incurring high computation cost. In this paper, we propose a framework for Synthesis with Efficient Exact Verification (SEEV). Our framework consists of two components, namely (i) an NCBF synthesis algorithm that introduces a novel regularizer to reduce the number of activation regions at the safety boundary, and (ii) a verification algorithm that exploits tight over-approximations of the safety conditions to reduce the cost of verifying each piecewise-linear segment. Our simulations show that SEEV significantly improves verification efficiency while maintaining the CBF quality across various benchmark systems and neural network structures. Our code is available at https://github.com/HongchaoZhang-HZ/SEEV.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。