PV3 ⊧ DNNV: Deep Neural Network Verificationverifies if a given property holds for a given neural network according to a given verifierFramework 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.
- Deep neural network (DNN)
- DNN verification
Type of toolFramework?
- Neural network
- Verifier that should be used
- Properties: specified in their own property DSL (
.propfile) called DNNP
- Neural network: Can be defined in the
.propfile, in the ONNX format
- Verifier to be used: defined as a parameter when calling the DNNV tool
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.