PV3 ⊧ DNNV: Deep Neural Network Verificationverifies if a given property holds for a given neural network according to a given verifier

Framework that standardizes input and output formats, includes a DSL for specifying deep neural network (DNN) properties and provides simplification and reduction operations to facilitate the application, development and comparison of DNN verifiers.

Application domain/field

• Deep neural network (DNN)
• DNN verification

Type of tool

Framework?

Expected input

• Properties
• Neural network
• Verifier that should be used

Format:

• Properties: specified in their own property DSL (.prop file) called DNNP
• Neural network: Can be defined in the .prop file, in the ONNX format
• Verifier to be used: defined as a parameter when calling the DNNV tool

Expected output

sat if the property was falsified, unsat if the property was proven to hold, unknown if the verifier is incomplete and could not prove the property, or error if there was an error. If the result was sat, indicating that a violation of the property was found, then DNNV also returns a counterexample.

Internals

Supports the following verifiers: Reluplex, planet, MIPVerify.jl, Neurify, ERAN, PLNN, Marabou, nnenum, verinet

Comments

License: MIT