# NEUROSPF: A tool for the Symbolic Analysis of Neural Networks

arXiv: https://arxiv.org/abs/2103.00124 · HTML: https://mlsanity.com/paper/2103.00124/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 24 references that are in the map.
- First posted on arXiv 27 Feb 2021.

## Builds on (most cited first, 9 of 9)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [DeepXplore: Automated Whitebox Testing of Deep Learning Systems](https://mlsanity.com/paper/1705.06640/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [DeepTest: Automated Testing of Deep-Neural-Network-driven Autonomous Cars](https://mlsanity.com/paper/1708.08559/) (2017)
- [DeepGauge: Multi-Granularity Testing Criteria for Deep Learning Systems](https://mlsanity.com/paper/1803.07519/) (2018)
- [Guiding Deep Learning System Testing using Surprise Adequacy](https://mlsanity.com/paper/1808.08444/) (2018)
- [Concolic Testing for Deep Neural Networks](https://mlsanity.com/paper/1805.00089/) (2018)
- [Repairing Deep Neural Networks: Fix Patterns and Challenges](https://mlsanity.com/paper/2005.00972/) (2020)
- [DeepFault: Fault Localization for Deep Neural Networks](https://mlsanity.com/paper/1902.05974/) (2019)

## Built on by (most cited first, 4 of 4)

- [NNrepair: Constraint-based Repair of Neural Network Classifiers](https://mlsanity.com/paper/2103.12535/) (2021)
- [FedDebug: Systematic Debugging for Federated Learning Applications](https://mlsanity.com/paper/2301.03553/) (2023)
- [Specifying and Testing k-Safety Properties for Machine-Learning Models](https://mlsanity.com/paper/2206.06054/) (2022)
- [DREAM: Debugging and Repairing AutoML Pipelines](https://mlsanity.com/paper/2401.00379/) (2023)

## Abstract (arXiv)

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