提出新算法验证神经反馈系统的安全边界，提升验证效率与精度。
The FABRIC Strategy for Verifying Neural Feedback Systems
- 结合前向与后向可达性分析，构建双向验证框架。
- 在多个基准测试中，显著优于现有最先进方法。
- 适合关注神经控制系统形式化验证的研究者。
前向可达性分析是验证神经反馈系统（即由神经网络控制的动力系统）满足避障规范的主流方法，已有多种研究方向。相比之下，针对此类系统的后向可达性分析关注度较低，部分原因在于现有技术可扩展性有限。本文首次填补这一空白，提出计算非线性神经反馈系统后向可达集的上界和下界近似的新算法，并将其与现有的前向分析技术集成。由此构建的算法称为前向与后向可达性融合认证（FaBRIC）。我们在一组代表性基准测试上评估了该方法，结果表明其显著优于现有最先进水平。
原文摘要 · Abstract (English)
Forward reachability analysis is a dominant approach for verifying reach-avoid specifications in neural feedback systems, i.e., dynamical systems controlled by neural networks, and a number of directions have been proposed and studied. In contrast, far less attention has been given to backward reachability analysis for these systems, in part because of the limited scalability of known techniques. In this work, we begin to address this gap by introducing new algorithms for computing both over- and underapproximations of backward reachable sets for nonlinear neural feedback systems. We also describe and implement an integration of these backward reachability techniques with existing ones for forward analysis. We call the resulting algorithm Forward and Backward Reachability Integration for Certification (FaBRIC). We evaluate our algorithms on a representative set of benchmarks and show that they significantly outperform the prior state of the art.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。