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

Type of tool

Model checker

Expected input

Format:

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.
Neural network

Links

Repository: https://github.com/rcpsl/PeregriNN

Last commit date

5 May 2021

Related papers

https://doi.org/10.1007/978-3-030-81685-8_13 (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to in CAV '21 paper: Neurify, Venus, nnenum, Marabou

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.