基于微分动态逻辑的可证明安全神经网络控制器
摘要
尽管神经网络（NN）作为信息物理系统的自主控制器具有潜力，但验证基于神经网络的控制系统的安全性对其实际应用构成了重大挑战，尤其是在需要无限时间跨度安全性的情况下。原因之一在于分析神经网络、常微分方程（ODE）和混合系统的困难性。为此，我们提出了 VerSAILLE（Verifiably Safe AI via Logically Linked Envelopes）：首个允许将控制理论结果重用于 NNCS 验证的通用方法。通过联合发力，我们利用了 NN 验证工具的高效性，同时保留了微分动态逻辑的严密性。基于 dL 中可证明安全的控制包络，我们推导出通过 NN 验证来证明的 NN 规格。我们表明，NN 遵循该规格的证明由 NNCS 无限时间安全性的 dL 证明所映射。由混合系统导出的 NN 验证属性通常包含非线性算术和任意逻辑结构，而高效的 NN 验证仅支持线性约束。为克服这一鸿沟，我们提出了 Mosaic：一种针对分段线性神经网络多项式实数算术属性的高效、可靠且完备的验证方法。Mosaic 将复杂的验证查询划分为简单的查询，并通过将近似与反例区域的精确推理相结合，以保持完备性的方式将现成的线性约束工具提升至非线性场景。我们的评估展示了 VerSAILLE 和 Mosaic 的多功能性：我们在经典的垂直机载防撞 NNCS 验证基准上证明了两种场景的无限时间安全性，同时在不安全场景中（穷举地）枚举了反例区域。我们还表明，我们的方法在闭环 NNV 中显著优于现有技术工具。
引用
@article{arxiv.2402.10998,
title = {Provably Safe Neural Network Controllers via Differential Dynamic Logic},
author = {Samuel Teuber and Stefan Mitsch and André Platzer},
journal= {arXiv preprint arXiv:2402.10998},
year = {2025}
}
备注
39 pages (main paper has 10 pages), 13 figures; Accepted at the Thirty-Eighth Annual Conference on Neural Information Processing Systems (NeurIPS 2024)