NEUROSPF: A tool for the Symbolic Analysis of Neural Networks
This tool addresses the need for improved reliability in neural networks, particularly for software engineering applications, but it is incremental as it builds on existing symbolic execution methods.
The paper tackles the problem of analyzing neural networks for reliability by introducing NEUROSPF, a tool that translates trained models into a Java representation for symbolic execution, enabling applications such as coverage-based testing, adversarial example generation, and constraint-based repair to improve neural network reliability.
This paper presents NEUROSPF, a tool for the symbolic analysis of neural networks. Given a trained neural network model, the tool extracts the architecture and model parameters and translates them into a Java representation that is amenable for analysis using the Symbolic PathFinder symbolic execution tool. Notably, NEUROSPF encodes specialized peer classes for parsing the model's parameters, thereby enabling efficient analysis. With NEUROSPF the user has the flexibility to specify either the inputs or the network internal parameters as symbolic, promoting the application of program analysis and testing approaches from software engineering to the field of machine learning. For instance, NEUROSPF can be used for coverage-based testing and test generation, finding adversarial examples and also constraint-based repair of neural networks, thus improving the reliability of neural networks and of the applications that use them. Video URL: https://youtu.be/seal8fG78LI