Update verinet

[MarcelBulpr]

This PR changes the install method of the verinet verifier, from pulling a fixed version from the dnnv github to installing it from pipenv. This will allow dnnv to always get the newest version of verinet (as long as there are no major API changes). It takes the verinet implementation provided by https://github.com/vas-group-imperial/VeriNet.

Some caveats:

1. The installer reports that the installation fails, even if it succeeded and verinet can be used. But I also had the same issue before the change and with other verifiers
2. Other verifiers install a specific commit as supposed to the most up-to-date version, this can be done here also if required.
3. This verinet version uses a different optimizer, Xpress instead of Gurobi.

[codecov[bot]]

Codecov Report

Patch coverage has no change and project coverage change: -12.18 :warning:

Comparison is base (f71c983) 89.90% compared to head (5c84bce) 77.72%.

Additional details and impacted files

@@             Coverage Diff              @@
##           develop     #107       +/-   ##
============================================
- Coverage    89.90%   77.72%   -12.18%     
============================================
  Files          140      140               
  Lines         7982     7982               
  Branches      1440     1440               
============================================
- Hits          7176     6204      -972     
- Misses         579     1634     +1055     
+ Partials       227      144       -83     

see 51 files with indirect coverage changes

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Do you have feedback about the report comment? Let us know in this issue.

[MarcelBulpr]

The code I provided to execute the new Verinet version does not quite work. I am currently trying to get it to work, but I have a question, if you have time @dlshriver .

How does DNNV change the networks before passing them to the verifiers? I am testing with image classification networks on MNIST. The original model correctly classifies the image as 1 and gives a corresponding (10,1) output. The model given to Verinet produces [16.436, 0], which I understand comes from the property using np.argmax(). But I do not understand a) why it has 2 outputs; and b) why does it not return only 0 or 1 due to the comparison in the property. I provided the property I am working with below.

from dnnv.properties import *
import numpy as np

N = Network("N")
x = Image("properties/0015/mnist/image2.npy")
x = x.reshape(N.input_shape[0])

true_class = 1

epsilon = 0.015

Forall(
    x_, Implies(x - epsilon <= x_ <= x + epsilon, np.argmax(N(x_)) == true_class)
)

I hope I provided enough information.

[dlshriver]

Hi Marcel, thanks for the PR. This is something I've needed to update for a while, and I appreciate your effort to do so. The reduction used should be the same as the one used by DNNF as described in this paper. The negation of the property is converted to DNF, then each disjunct is converted to a halfspace polytope representation which is used to construct two new layers for the output. The new output of the network has 2 values, the second of which is always 0 and the first of which is strictly greater than 0 if and only if the encoded disjunct is false.

Hopefully that helps a bit. Let me know if you have more questions.