论文标题
随机神经网络动态模型的形式控制合成
Formal Control Synthesis for Stochastic Neural Network Dynamic Models
论文作者
论文摘要
神经网络（NNS）正在作为强大的工具出现，以代表具有复杂物理或黑盒组件的控制系统的动力学。但是，由于NNS的复杂性，现有方法无法通过保证NN动态模型（NNDMS）来综合复杂行为。这项工作引入了具有性能保证的随机NNDM的控制综合框架。重点是在有限痕迹（LTLF）上解释的线性时间逻辑中表达的规范，该方法基于有限的抽象。具体而言，我们利用了最新技术来凸出NNS，将NNDM正式抽象为Markov决策过程（IMDP）。然后，在IMDP上合成了满足给定规范的可能性的最大概率的策略，并将其映射回基础NNDM。我们表明，将NNDMs抽象为IMDP的过程减少到一组凸优化问题，从而确保效率。我们还提出了一种自适应改进程序，使框架可扩展。在一些案例研究中，我们说明了我们的框架能够为NNDM提供非平凡的保证，其架构最多为5个隐藏层和数百个神经元。
Neural networks (NNs) are emerging as powerful tools to represent the dynamics of control systems with complicated physics or black-box components. Due to complexity of NNs, however, existing methods are unable to synthesize complex behaviors with guarantees for NN dynamic models (NNDMs). This work introduces a control synthesis framework for stochastic NNDMs with performance guarantees. The focus is on specifications expressed in linear temporal logic interpreted over finite traces (LTLf), and the approach is based on finite abstraction. Specifically, we leverage recent techniques for convex relaxation of NNs to formally abstract a NNDM into an interval Markov decision process (IMDP). Then, a strategy that maximizes the probability of satisfying a given specification is synthesized over the IMDP and mapped back to the underlying NNDM. We show that the process of abstracting NNDMs to IMDPs reduces to a set of convex optimization problems, hence guaranteeing efficiency. We also present an adaptive refinement procedure that makes the framework scalable. On several case studies, we illustrate the our framework is able to provide non-trivial guarantees of correctness for NNDMs with architectures of up to 5 hidden layers and hundreds of neurons per layer.
