More Like this

1. Verification of Neural Network Compression of ACAS Xu Lookup Tables with Star Set Reachability

   https://doi.org/10.2514/6.2021-0995  

   Manzanas Lopez, Diego ; Johnson, Taylor ; Tran, Hoang-Dung ; Bak, Stanley ; Chen, Xin ; Hobbs, Kerianne L. ( January 2021 , AIAA Scitech 2021 Forum)

   null (Ed.)

   Neural network approximations have become attractive to compress data for automation and autonomy algorithms for use on storage-limited and processing-limited aerospace hard-ware. However, unless these neural network approximations can be exhaustively verified to be safe, they cannot be certified for use on aircraft. This manuscript evaluates the safety of a neural network approximation of the unmanned Airborne Collision Avoidance System (ACAS Xu). First, a set of ACAS Xu closed-loop benchmarks is introduced, based on a well-known open-loop benchmark, that are challenging to analyze for current verification tools due to the complexity and high-dimensional plant dynamics. Additionally, the system of switching and classification-based nature of the ACAS Xu neural network system adds another challenge to existing analysis methods. Experimental evaluation shows selected scenarios where the safety of the ownship aircraft’s neural network action selection is assessed with respect to an intruder aircraft over time in a closed loop control evaluation. Set-based analysis of the closed-loop benchmarks is performed using the Star Set representation using both the NNV tool and the nnenum tool, demonstrating that set-based analysis is becoming increasingly feasible for the verification of this class of systems. 

   more » « less
2. Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance

   https://doi.org/10.1109/DASC50938.2020.9256616  

   Irfan, Ahmed ; Julian, Kyle D. ; Wu, Haoze ; Barrett, Clark ; Kochenderfer, Mykel J. ; Meng, Baoluo ; Lopez, James ( October 2020 , Proceedings of the 39th Digital Avionics Systems Conference (DASC '20))

   The ACAS X family of aircraft collision avoidance systems uses large numeric lookup tables to make decisions. Recent work used a deep neural network to approximate and compress a collision avoidance table, and simulations showed that the neural network performance was comparable to the original table. Consequently, neural network representations are being explored for use on small aircraft with limited storage capacity. However, the black-box nature of deep neural networks raises safety concerns because simulation results are not exhaustive. This work takes steps towards addressing these concerns by applying formal methods to analyze the behavior of collision avoidance neural networks both in isolation and in a closed-loop system. We evaluate our approach on a specific set of collision avoidance networks and show that even though the networks are not always locally robust, their closed-loop behavior ensures that they will not reach an unsafe (collision) state. 

   more » « less
3. ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks

   https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_22  

   Lin, Xuankang ; Zhu, He ; Samanta, Roopsha ; Jagannathan, Suresh ( January 2020 , Formal Methods in Computer-Aided Design)

   Ivrii, Alexander ; Strichman, Ofer (Ed.)

   Artificial Neural Networks (ANNs) have demonstrated remarkable utility in various challenging machine learning applications. While formally verified properties of their behaviors are highly desired, they have proven notoriously difficult to derive and enforce. Existing approaches typically formulate this problem as a post facto analysis process. In this paper, we present a novel learning framework that ensures such formal guarantees are enforced by construction. Our technique enables training provably correct networks with respect to a broad class of safety properties, a capability that goes well-beyond existing approaches, without compromising much accuracy. Our key insight is that we can integrate an optimization-based abstraction refinement loop into the learning process and operate over dynamically constructed partitions of the input space that considers accuracy and safety objectives synergistically. The refinement procedure iteratively splits the input space from which training data is drawn, guided by the efficacy with which such partitions enable safety verification. We have implemented our approach in a tool (ART) and applied it to enforce general safety properties on unmanned aviator collision avoidance system ACAS Xu dataset and the Collision Detection dataset. Importantly, we empirically demonstrate that realizing safety does not come at the price of much accuracy. Our methodology demonstrates that an abstraction refinement methodology provides a meaningful pathway for building both accurate and correct machine learning networks. 

   more » « less
4. Verisig: verifying safety properties of hybrid systems with neural network controllers

   https://doi.org/10.1145/3302504.3311806  

   Ivanov, Radoslav ; Weimer, James ; Alur, Rajeev ; Pappas, George J. ; Lee, Insup ( April 2019 , HSCC 2019)

   This paper presents Verisig, a hybrid system approach to verifying safety properties of closed-loop systems using neural networks as controllers. We focus on sigmoid-based networks and exploit the fact that the sigmoid is the solution to a quadratic differential equation, which allows us to transform the neural network into an equivalent hybrid system. By composing the network's hybrid system with the plant's, we transform the problem into a hybrid system verification problem which can be solved using state-of-the-art reachability tools. We show that reachability is decidable for networks with one hidden layer and decidable for general networks if Schanuel's conjecture is true. We evaluate the applicability and scalability of Verisig in two case studies, one from reinforcement learning and one in which the neural network is used to approximate a model predictive controller. 

   more » « less
5. Building Verified Neural Networks for Computer Systems with Ouroboros

   Wei, T. ; Jia, Z. ; Liu, C. ; Tan, C ( May 2023 , Sixth Conference on Machine Learning and Systems)

   Neural networks are powerful tools. Applying them in computer systems—operating systems, databases, and networked systems—attracts much attention. However, neural networks are complicated black boxes that may produce unexpected results. To train networks with well-defined behaviors, we introduce ouroboros, a system that constructs verified neural networks. Verified neural networks are those that satisfy user-defined safety properties, known as specifications. Ouroboros builds verified networks by a training-verification loop that combines deep learning training and neural network verification. The system employs multiple techniques to fill the gap between today’s verification and the properties required for systems. Ouroboros also accelerates the training-verification loop by spec-aware learning. Our experiments show that ouroboros can train verified networks for five applications that we study and has a 2.8× speedup on average compared with the vanilla training-verification loop. 

   more » « less