PV1 ⊧ PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifierchecks whether an image is always classified the same when it's perturbed

A tool to formally verifying the input/output behavior or ReLU neural networks.

Application domain/field

• Neural networks
• Model checking
• Safety verification
• Input-output behavior
• Adversarial inputs

Type of tool

Model checker

Expected input

• Rectified Linear Unit (ReLU) neural network
• Image file
• Max-norm perturbation $ϵ$

Format:

• Neural network: nnet format
• Comma-separated file that describes each pixel as a float between 0 and 1
• Max-norm perturbation: passed when calling the script, e.g. 0.02.

Expected output

Proves whether a particular input image always results in the same classification when it is subjected to a max-norm perturbation of at most some fixed size $ϵ$.

Internals

Uses Gurobi 9.1 convex optimizer for solving linear programs, Volesti to sample from the input polytope for the sampling inference block

Comments

License: MIT, however it relies on Gurobi which is a commercial tool. It is possible to get an academic license for Gurobi.