Racetrack
Racetrack
The work presented here is published in Automated Safety Verification of Programs Invoking Neural Networks.
Heterogeneous Software
Software is becoming increasingly heterogeneous. In other words, it consists of more and more diverse software components, implemented using different technologies such as neural networks, smart contracts, or web services. On the other hand, state-of-the-art program-analysis techniques are not yet able to effectively verify safety properties of heterogeneous systems. This is a fundamental limitation of prevalent program-analysis techniques, and as a result, we cannot effectively analyze the interaction between diverse components of a heterogeneous system to check system properties which depend on components correctly interacting with each other.
Neuro-Aware Program Analysis
In this project, we present Neuro-Aware Program Analysis, to make the first step in verifying safety properties on programs invoking neural networks in response to their prominent role in many upcoming application areas. Existing work on verification of neural networks has focused on the network itself, in contrast, our approach is designed for verifying safety of a C (or ultimately LLVM) program interacting with the network. More specifically, our approach proposes a symbiotic combination of a program and a neural-network analysis, both of which are based on abstract interpretation. As shown in the figure below, the two existing analyses are extended to pass information both from program analysis to neural network analysis.
Evaluation
We show the effectiveness of our approach in verifying goal reachability and crash avoidance for 33 Racetrack variants of varying complexity. These variants constitute a diverse set of verification tasks that differ both in the neural network itself and in how and for what purpose the program invokes the neural network. We use deep Q-learning to train a neural network for each racetrack variant and we user Crab program analyzer for the program part and employ DeepSymbol and ERAN neural network analyzers for the neural network part.
Below, we present effectiveness of Neuro-Aware Program Analysis on 3 Racetrack map. In the plots, cell colorings correspond whether the agent safely arrives one of goal states (green), crashs into walls (red) or hangs indefinitely (blue). Higher number of green cells require a precise analysis. Below plots demonstrate that Neuro-Aware Program Analysis is highly precise.
Below table illustrates the performance of Neuro-Aware Program Analysis on above Racetrack maps.
Summary
Many existing software systems are already heterogeneous, and we expect the number of such systems to grow further. In this project, we present a novel approach to verifying safety properties of such systems that symbiotically combines existing program and neural-network analyzers. Neuro-aware program analysis is able to effectively prove non-trivial system properties of programs invoking neural networks, such as the 33 variants of Racetrack benchmark.