We have begun the process of selection and evaluation of benchmarks. The idea is to gather both convolutional and fully-connected Neural Networks together with their properties of interest. Ideally, these models will come from different domains of application.

ACAS XU Benchmark

Benchmarks based on the ACAS XU Neural Networks originally presented in the paper “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks“. The networks are in the ONNX format and the input/output values do not need to be normalized. The properties can be directly specified using the raw input/output values.

MNIST Fully Connected

Benchmarks based on the MNIST Neural Networks originally presented in the paper “Verification of Neural Networks: Enhancing Scalability through Pruning“. The networks are in the ONNX format and the input/output values are supposed to be normalized between (-1, 1).

Fashion MNIST Fully Connected

Benchmarks based on the FMNIST Neural Networks originally presented in the paper “Verification of Neural Networks: Enhancing Scalability through Pruning“. The networks are in the ONNX format and the input/output values are supposed to be normalized between (-1, 1).