SpEXplAIn is a tool that automatically generates Space Explanations of neural network classification. It gives provable guarantees of the behavior of the network in continuous areas of the input feature space. The tool leverages the OpenSMT solver compatible with a range of flexible Craig interpolation algorithms and unsatisfiable core generation. The computational engine can optionally also use the NN verifier Marabou to compute interval-like explanations (i.e., including abductive explanations). The development webpage of the tool, which also includes detailed instructions on how to build and run the tool, is located at GitHub: https://github.com/usi-verification-and-security/spexplain

Publications: