Verification of Closed-loop Systems with Neural Network Controllers
Verification of Closed-loop Systems with Neural Network Controllers
复制标题
使用神经网络控制器验证闭环系统
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Taylor T. Johnson
中科院分区：
文献类型：
--
作者：
Diego Manzanas Lopez;Patrick Musau;Hoang;Taylor T. Johnson
该基准测试套件详细描述了一系列具有人工神经网络控制器的闭环控制系统。在许多应用中，前馈神经网络通过模型预测控制（MPC）和强化学习（RL）等多种方法学习和表示控制规律，从而大量参与控制器的实现。我们在本手稿中考虑的网络类型是前馈神经网络，由具有 ReLU 激活函数的多个隐藏层和输出层中的线性激活函数组成。虽然神经网络控制器已经能够在许多情况下实现理想的性能，但它们也提出了独特的挑战，因为很难对其行为的正确性或使用其使用的系统的稳定性提供任何保证。因此，从控制的角度来看，有必要将它们与闭环中相应的设备结合起来进行验证。尽管已经提出了一些针对使用前馈神经网络控制器验证闭环系统的工作，但该领域仍然缺乏关注和一套可以评估和比较验证技术的统一基准示例。因此，为此，我们提出了一系列从两个到六个状态变量的闭环控制系统，以及一系列在更复杂的系统中尺寸在十一个神经元到几百个神经元范围内的控制器。类别：学术难度：高度认可 本文中提供的材料基于美国国家科学基金会 (NSF) 资助号为 SHF 1736323、空军科学研究办公室 (AFOSR) 的合同号为 FA9550-15-1-0258、FA9550-16-10246 和 FA9550-18-1-0122 以及国防部支持的工作高级研究计划局 (DARPA)，合同号为 FA8750-18-C-0089。美国政府有权出于政府目的复制和分发重印本，无论其上有任何版权注释。本文包含的观点和结论属于作者的观点和结论，不应被解释为必然代表 AFOSR、DARPA 或 NSF G. Frehse 和 M. Althoff（编辑）的官方政策或认可（无论是明示还是暗示），ARCH19（EPiC 系列计算，第 61 卷），第 201–210 页 带神经网络控制器的闭环系统 Manzanas Lopez、Musau、Tran 和 Johnson 1 背景和起源。近年来，人工智能（AI）的进步催生了多种直接影响人们日常生活的技术[16]。特别是，在这个领域，深度学习（DL）等机器学习方法在模式和图像识别[12]、自然语言处理[7]以及知识表示和推理[15,22]等任务方面已经达到了与人类竞争或更好的准确性和性能水平。尽管取得了这些成就，但对于将它们纳入安全关键系统 [11] 仍存在保留，因为它们很容易因输入的轻微扰动而出现意外和错误行为 [18]。此外，神经网络通常被视为“黑匣子”，因为神经元激活的基本操作通常是难以辨别的[22]。鉴于这些挑战，人们在创建可以正式推理神经网络行为的方法和验证工具方面开展了大量工作[22]。然而，这些技术中的绝大多数只能处理具有分段线性激活函数的前馈神经网络 [4]。此外，这些方法中的大部分主要考虑了孤立地验证神经网络的输入输出属性[22]，并且只有少数工作明确解决了使用神经网络控制器验证闭环控制系统的问题[5,8,19-21]。验证神经网络控制系统的主要挑战之一是将现有方法应用于这些系统并不简单[9]，并且非线性常微分方程验证工具与神经网络可达性工具的简单组合会遭受严重的高估错误[5]。尽管如此，闭环神经网络系统的验证仍然非常重要，因为它们自然出现在安全关键系统 [5] 中，例如自动驾驶汽车，以及利用模型预测控制和强化学习的复杂控制系统 [16]。因此，迫切需要能够有效处理这些系统所表现出的复杂性的方法和先进的软件工具[5]。受研究文献中闭环神经网络控制系统验证方法缺乏的启发，本文的主要贡献是提供了一组使用强化学习[17]和模型预测控制[14]等方法合成的可执行基准。本文阐明的问题使用 Simulink/Stateflow (SLSF) 进行建模，可在以下 github 存储库中获取。我们的目标是提供全面的问题描述，可以评估和比较研究界中存在的众多用于非线性系统和神经网络验证的工具和方法[22]。如果研究界能够针对上述挑战设计出可接受的解决方案，他们将刺激稳健和智能系统的发展，并有可能为众多应用领域带来无与伦比的好处。 2 基准描述。在这篇手稿中，我们提出了一组线性和非线性闭环系统，其中包含连续时间工厂和前馈神经网络控制器，并使用不同的控制方案（例如强化学习或模型预测控制（MPC））进行训练。描述这些系统结构的典型架构如图 2.1 所示。所有神经网络1https://github.com/verivital/ARCH-2019
This benchmark suite presents a detailed description of a series of closed-loop control systems with artificial neural network controllers. In many applications, feed-forward neural networks are heavily involved in the implementation of controllers by learning and representing control laws through several methods such as model predictive control (MPC) and reinforcement learning (RL). The type of networks that we consider in this manuscript are feed-forward neural networks consisting of multiple hidden layers with ReLU activation functions and a linear activation function in the output layer. While neural network controllers have been able to achieve desirable performance in many contexts, they also present a unique challenge in that it is difficult to provide any guarantees about the correctness of their behavior or reason about the stability a system that employs their use. Thus, from a controls perspective, it is necessary to verify them in conjunction with their corresponding plants in closed-loop. While there have been a handful of works proposed towards the verification of closed-loop systems with feed-forward neural network controllers, this area still lacks attention and a unified set of benchmark examples on which verification techniques can be evaluated and compared. Thus, to this end, we present a range of closed-loop control systems ranging from two to six state variables, and a range of controllers with sizes in the range of eleven neurons to a few hundred neurons in more complex systems. Category: Academic Difficulty: High Acknowledgement The material presented in this paper is based upon work supported by the National Science Foundation (NSF) under grant number SHF 1736323, the Air Force Office of Scientific Research (AFOSR) through contract numbers FA9550-15-1-0258, FA9550-16-10246, and FA9550-18-1-0122, and the Defense Advanced Research Projects Agency (DARPA) through contract number FA8750-18-C-0089. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of AFOSR, DARPA, or NSF G. Frehse and M. Althoff (eds.), ARCH19 (EPiC Series in Computing, vol. 61), pp. 201–210 Closed-loop Systems with Neural Network Controllers Manzanas Lopez, Musau, Tran and Johnson 1 Context and Origins. In recent years, advances in Artficial Intelligence (AI) have enabled a diverse range of technologies that are directly impacting people’s everyday lives [16]. Particularly, within this space, machine learning methods such as Deep Learning (DL) have achieved levels of accuracy and performance that are competitive or better than humans for tasks such as pattern and image recognition [12], natural language processing [7], and knowledge representation and reasoning [15,22]. Despite these achievements, there have been reservations about incorporating them into safety critical systems [11] due to their susceptibility to unexpected and errant behavior from a slight perturbation in their inputs [18]. Furthermore, neural networks are often viewed as "black boxes" since the underlying operation of the neuron activations is often indiscernible [22]. In light of these challenges, there has been significant work towards the creation of methods and verification tools that can formally reason about the behavior of neural networks [22]. However, the vast majority of these techniques have only been able to deal with feed-forward neural networks with piecewise-linear activation functions [4]. Additionally, the bulk of these methods have primarily considered the verification of input-output properties of neural networks in isolation [22], and there are only a handful of works that have explicitly addressed the verification of closed-loop control systems with neural network controllers [5, 8, 19–21]. One of the central challenges in verifying neural network control systems is that applying existing methodology to these systems is not straightforward [9], and a simple combination of verification tools for non-linear ordinary differential equations along with a neural network reachability tool suffers from severe overestimation errors [5]. Still, the verification of closed loop neural network systems is deeply important as they naturally arise in safety critical systems [5] such as autonomous vehicles, and complex control systems that make use of model predictive control and reinforcement learning [16]. Thus, there is a compelling need for methods and advanced software tools that can effectively deal with the complexities exhibited by these systems [5]. Inspired by a shortage of verification methods for closed-loop neural network control systems in the research literature, the central contribution of this paper is the provision of a set of executable benchmarks that have been synthesized using methods such as reinforcement learning [17], and model predictive control [14]. The problems elucidated in the paper are modeled using Simulink/Stateflow (SLSF) and are available at the following github repository1. We aim to provide a thorough problem description to which the numerous tools and approaches for non-linear systems and neural network verification present in the research community can be evaluated and compared [22]. If the research community is able to devise acceptable solutions to the aformentioned challenges they will stimulate the development of robust and intelligent systems with the potential to bring unparalleled benefits to numerous application domains. 2 Description of benchmarks. In this manuscript, we present a set of linear and non-linear closed-loop systems with continuoustime plants and feedforward neural networks controllers trained using different controls schemes such as reinforcement learning or model predictive control (MPC). A typical architecture describing the structure of these systems is displayed in Figure 2.1. All the neural networks 1https://github.com/verivital/ARCH-2019