通过分支定界验证在环训练同时合成与验证神经控制障碍函数
系统与控制
2023-11-20 v1 系统与控制
摘要
提供形式化安全保证的控制障碍函数（CBFs）已广泛用于安全关键系统。然而，设计 CBF 并非易事。利用神经网络作为 CBF 已取得巨大成功，但这需要将其认证为 CBF。在本工作中，我们利用界传播技术和分支定界（Branch-and-Bound）方案，高效验证神经网络在连续状态空间上满足作为 CBF 的条件。为加速训练，我们进一步提出一个框架，将验证方案嵌入训练循环中，以同时合成并验证神经 CBF。具体而言，我们采用验证方案识别状态空间中不能保证满足 CBF 条件的划分，并通过从这些划分中纳入额外数据来扩展训练数据集。随后使用增广数据集优化神经网络以满足 CBF 条件。我们展示，对于一个非线性控制仿射系统，我们的框架能高效地将神经网络认证为 CBF，并比最先进的神经 CBF 工作给出更大的安全集。我们进一步使用所学习的神经 CBF 推导安全控制器，以说明我们框架的实际用途。
引用
@article{arxiv.2311.10438,
title = {Simultaneous Synthesis and Verification of Neural Control Barrier Functions through Branch-and-Bound Verification-in-the-loop Training},
author = {Xinyu Wang and Luzia Knoedler and Frederik Baymler Mathiesen and Javier Alonso-Mora},
journal= {arXiv preprint arXiv:2311.10438},
year = {2023}
}
备注
8 pages, 6 figures, under review for ECC 2024