提出新方法验证神经反馈系统的安全性和目标可达性。
BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems
- 用混合整数线性规划求解神经反馈系统的后向可达集
- 通过反向可达集严格验证系统能否达到目标状态
- 适合需要安全保证的智能控制系统验证
学习型规划与控制算法日益普及，但往往缺乏性能或安全性的严格保障。本文提出一种计算非线性离散时间神经反馈回路后向可达集的算法，并利用该可达集检验目标可达性。算法通过上界逼近系统动态函数，将后向可达集计算转化为混合整数线性规划问题求解。我们严格分析了算法的正确性，并在数值例子中进行了验证。本工作拓展了可验证的学习型系统的性质范围。
原文摘要 · Abstract (English)
Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based on overapproximating the system dynamics function to enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。