提出新算法，提升神经反馈系统可达性验证的精度与效率
A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems
- 结合前向与后向分析，构建统一验证框架
- 可计算后向可达集的上下界逼近
- 适合需要高精度验证的智能控制系统研究者
前向可达性分析是验证神经反馈系统（由神经网络控制的动力系统）可达-避免性质的主流方法，主要因现有后向可达性方法扩展性差。本文提出新算法，能够计算此类系统后向可达集的上界和下界逼近。进一步将这些后向算法与成熟的前向分析技术融合，形成统一的验证框架，显著提升神经反馈系统的验证能力与适用范围。
原文摘要 · Abstract (English)
Forward reachability analysis is the predominant approach for verifying reach-avoid properties in neural feedback systems (dynamical systems controlled by neural networks). This dominance stems from the limited scalability of existing backward reachability methods. In this work, we introduce new algorithms that compute both over- and under-approximations of backward reachable sets for such systems. We further integrate these backward algorithms with established forward analysis techniques to yield a unified verification framework for neural feedback systems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。