Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning

AbstractThis paper presents Verisig 2.0, a verification tool for closed-loop systems with neural network (NN) controllers. We focus on NNs with tanh/sigmoid activations and develop a Taylor-model-based reachability algorithm through Taylor model preconditioning and shrink wrapping. Furthermore, we provide a parallelized implementation that allows Verisig 2.0 to efficiently handle larger NNs than existing tools can. We provide an extensive evaluation over 10 benchmarks and compare Verisig 2.0 against three state-of-the-art verification tools. We show that Verisig 2.0 is both more accurate and faster, achieving speed-ups of up to 21x and 268x against different tools, respectively.

Download Full-text

Verification of Closed-loop Systems with Neural Network Controllers

10.29007/btv1 ◽

2019 ◽

Author(s):

Diego Manzanas Lopez ◽

Patrick Musau ◽

Hoang-Dung Tran ◽

Taylor T. Johnson

Keyword(s):

Neural Network ◽

Neural Networks ◽

Control Systems ◽

Closed Loop ◽

Closed Loop Control ◽

Feed Forward ◽

Loop Control ◽

Closed Loop Systems ◽

Feed Forward Neural Networks ◽

Neural Network Controllers

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 con- trollers 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.

Download Full-text

Efficient Reachability Analysis of Closed-Loop Systems with Neural Network Controllers

10.1109/icra48506.2021.9561348 ◽

2021 ◽

Author(s):

Michael Everett ◽

Golnaz Habibi ◽

Jonathan P. How

Keyword(s):

Neural Network ◽

Closed Loop ◽

Reachability Analysis ◽

Closed Loop Systems ◽

Neural Network Controllers

Download Full-text

Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming

2020 59th IEEE Conference on Decision and Control (CDC) ◽

10.1109/cdc42340.2020.9304296 ◽

2020 ◽

Author(s):

Haimin Hu ◽

Mahyar Fazlyab ◽

Manfred Morari ◽

George J. Pappas

Keyword(s):

Neural Network ◽

Semidefinite Programming ◽

Closed Loop ◽

Reachability Analysis ◽

Closed Loop Systems ◽

Neural Network Controllers

Download Full-text

Compositional Learning and Verification of Neural Network Controllers

ACM Transactions on Embedded Computing Systems ◽

10.1145/3477023 ◽

2021 ◽

Vol 20 (5s) ◽

pp. 1-26

Author(s):

Radoslav Ivanov ◽

Kishor Jothimurugan ◽

Steve Hsu ◽

Shaan Vaidya ◽

Rajeev Alur ◽

...

Keyword(s):

Neural Network ◽

Program Verification ◽

Controller Design ◽

Autonomous Systems ◽

Arbitrary Sequence ◽

Verification Tools ◽

Compositional Learning ◽

Lidar Observations ◽

Neural Network Controllers

Recent advances in deep learning have enabled data-driven controller design for autonomous systems. However, verifying safety of such controllers, which are often hard-to-analyze neural networks, remains a challenge. Inspired by compositional strategies for program verification, we propose a framework for compositional learning and verification of neural network controllers. Our approach is to decompose the task (e.g., car navigation) into a sequence of subtasks (e.g., segments of the track), each corresponding to a different mode of the system (e.g., go straight or turn). Then, we learn a separate controller for each mode, and verify correctness by proving that (i) each controller is correct within its mode, and (ii) transitions between modes are correct. This compositional strategy not only improves scalability of both learning and verification, but also enables our approach to verify correctness for arbitrary compositions of the subtasks. To handle partial observability (e.g., LiDAR), we additionally learn and verify a mode predictor that predicts which controller to use. Finally, our framework also incorporates an algorithm that, given a set of controllers, automatically synthesizes the pre- and postconditions required by our verification procedure. We validate our approach in a case study on a simulation model of the F1/10 autonomous car, a system that poses challenges for existing verification tools due to both its reliance on LiDAR observations, as well as the need to prove safety for complex track geometries. We leverage our framework to learn and verify a controller that safely completes any track consisting of an arbitrary sequence of five kinds of track segments.

Download Full-text

Symbolic-Numeric Reachability Analysis of Hybrid Systems

10.29007/249v ◽

2018 ◽

Author(s):

Sriram Sankaranarayanan

Keyword(s):

Hybrid Systems ◽

Closed Loop ◽

State Of The Art ◽

Reachability Analysis ◽

Operating Environment ◽

Plant Model ◽

Elegant Method ◽

Simulation Based ◽

Verification Tools ◽

Final System

We consider the problem of reachability analysis in hybrid systems defined by the closed-loop interaction of a complex, continuous time plant model with a software-based controller. In practice, the plant model is, often, a coarse approximation of the real-world operating environment of the software, whereas the software itself is the artifact that ends up being deployed in the final system. In this talk, we summarize the state-of-the-art techniques for purely symbolic and purely numeric approaches to reachability analysis of hybrid systems. We make the case for approaches that combine simulation-based exploration of the plant state-space with a corresponding symbolic exploration of the controller. We propose a simple yet elegant method to carry out this joint symbolic-numeric exploration based on an abstraction of the plant model, and present promising experimental results on software-in-the-loop setups that are beyond the scope of many existing verification tools.

Download Full-text

Hypernym Detection Using Strict Partial Order Networks

Proceedings of the AAAI Conference on Artificial Intelligence ◽

10.1609/aaai.v34i05.6263 ◽

2020 ◽

Vol 34 (05) ◽

pp. 7626-7633 ◽

Cited By ~ 2

Author(s):

Sarthak Dash ◽

Md Faisal Mahbub Chowdhury ◽

Alfio Gliozzo ◽

Nandana Mihindukulasooriya ◽

Nicolas Rodolfo Fauceglia

Keyword(s):

Neural Network ◽

Partial Order ◽

Network Architecture ◽

State Of The Art ◽

Soft Constraints ◽

Neural Network Architecture ◽

Strict Partial Order ◽

Generalize Type ◽

Extensive Evaluation ◽

Type Information

This paper introduces Strict Partial Order Networks (SPON), a novel neural network architecture designed to enforce asymmetry and transitive properties as soft constraints. We apply it to induce hypernymy relations by training with is-a pairs. We also present an augmented variant of SPON that can generalize type information learned for in-vocabulary terms to previously unseen ones. An extensive evaluation over eleven benchmarks across different tasks shows that SPON consistently either outperforms or attains the state of the art on all but one of these benchmarks.

Download Full-text

GATNNCDA: A Method Based on Graph Attention Network and Multi-Layer Neural Network for Predicting circRNA-Disease Associations

International Journal of Molecular Sciences ◽

10.3390/ijms22168505 ◽

2021 ◽

Vol 22 (16) ◽

pp. 8505

Author(s):

Cunmei Ji ◽

Zhihao Liu ◽

Yutian Wang ◽

Jiancheng Ni ◽

Chunhou Zheng

Keyword(s):

Neural Network ◽

Closed Loop ◽

State Of The Art ◽

Computational Method ◽

Circular Rnas ◽

Attention Network ◽

Initial Node ◽

New Class ◽

Disease Associations ◽

Non Coding Rnas

Circular RNAs (circRNAs) are a new class of endogenous non-coding RNAs with covalent closed loop structure. Researchers have revealed that circRNAs play an important role in human diseases. As experimental identification of interactions between circRNA and disease is time-consuming and expensive, effective computational methods are an urgent need for predicting potential circRNA–disease associations. In this study, we proposed a novel computational method named GATNNCDA, which combines Graph Attention Network (GAT) and multi-layer neural network (NN) to infer disease-related circRNAs. Specially, GATNNCDA first integrates disease semantic similarity, circRNA functional similarity and the respective Gaussian Interaction Profile (GIP) kernel similarities. The integrated similarities are used as initial node features, and then GAT is applied for further feature extraction in the heterogeneous circRNA–disease graph. Finally, the NN-based classifier is introduced for prediction. The results of fivefold cross validation demonstrated that GATNNCDA achieved an average AUC of 0.9613 and AUPR of 0.9433 on the CircR2Disease dataset, and outperformed other state-of-the-art methods. In addition, case studies on breast cancer and hepatocellular carcinoma showed that 20 and 18 of the top 20 candidates were respectively confirmed in the validation datasets or published literature. Therefore, GATNNCDA is an effective and reliable tool for discovering circRNA–disease associations.

Download Full-text