search

stanleybak / nnenum

Neural Network Enumeration Tool
GNU General Public License v3.0
33 stars 17 forks source link

Returned counterexample is not correct #4

Closed dlshriver closed 2 years ago

dlshriver commented 2 years ago

Hi, I'm encountering an issue where nnenum reports that a network is unsafe an has a confirmed counterexample, but the counterexample that it returns is not a real violation for the problem. I have attached the model and run script I am using to get this result (reproduce.zip). The result should be UNSAFE, but I'm not sure why the counterexamples are incorrect. An example of a true violation is the input [[-1.1, 0.0]] (I print out the networks output for this input at the end of the run script to confirm).

Do you know why the counterexamples may be incorrect? Or am I maybe misinterpreting the results?

stanleybak commented 2 years ago

Thanks for reporting. This seems like a real bug... trying to look closer into what's the cause.

stanleybak commented 2 years ago

This should now be fixed on master.

The root cause was as follows. I had some code to compute which bounds on inputs to neurons in each layer decide when to branch (split sets) and which neurons are strictly negative (so their output is always zero). Since LP solving is used, this was based on a numeric tolerance defined in the settings: Settings.SPLIT_TOLERANCE = 1e-8.`

The code in prefiler.py was like this:

branching_neurons = np.nonzero(np.logical_and(
    self.layer_bounds[:, 0] < -Settings.SPLIT_TOLERANCE,
    self.layer_bounds[:, 1] > Settings.SPLIT_TOLERANCE))[0]
...
zero_indices = np.nonzero(self.layer_bounds[:, 1] < -Settings.SPLIT_TOLERANCE)[0]

Here layer_bounds is the input bounds for each neuron, column 0 is the min and column 1 is max.

The issue is that you had layers where the upper bound was exactly equal to zero, for example say the input to some neuron was in the range [-1.5, 0]. In this case, it wasn't considered a branching neuron since the upper bound 0 < 1e-8, but it also wasn't considered a zero neuron(!) since the code was checking if the upper bound 0 was less than -1e-8. Since it was never marked as a zero neuron, this input never got projected to zero (it was assumed to be a positive-only neuron), which is incorrect.

The correction was to change the zero_indices condition to:

zero_indices = np.nonzero(self.layer_bounds[:, 1] <= Settings.SPLIT_TOLERANCE)[0]

After that, the result was corrected. I suspect this wasn't noticed before as networks trained with data rarely have an upper bound of exactly zero (or between -1e-8 and 1e-8), which was necessary for this to occur. Was your network hand-made?

Please confirm this is fixed in the latest version.

dlshriver commented 2 years ago

Thank you! It looks like this did fix the issue.

Yes, this was a tiny hand-made network for testing DNNV. If I remember correctly, the network should compute N([x1, x2]) = [y1, y2] = [min(max(x2-x1, 1.0), 0.0), x2] and the property was something like forall x1,x2 \in [-1.1, 0]. (y2-y1 < 0.001). We can play with the value of 0.001 to make the property true or false.