Counterexamples using SILVA
val-co opened this issue · 13 comments
Hello, thank you for sharing the code. Can you please share an example of how counterexamples can be generated using SILVA for an epsilon of 0.5 (for instance, the IRIS dataset)?
Also, can SILVA output counterexample ranges? For example if x = 1, and epsilon = 0.5, then all counterexamples lie in the intervals of [0.5, 0.9], and [1.1, 1.5]?
Thank you for using silva and for you question: the tool computes both a counterexample and a range (in the form of an hyper rectangle) as part of the verification process. To keep the command line interface simple, however, this information is not exported, we apologize for the inconvenience.
To obtain a single counterexample you can refer to the main function in src/silva.c: on line 158, when abstract_classifier_is_stable is called, if the classifier is unstable on given sample then status->sample_b will contain a counterexample, represented as an array of double.
Obtaining a range is a bit more involved as this information is only used internally by src/abstract_interpreters/forest_hyperrectangle.c and does not reach back to the main function. On lines 796 and 830, within the if bodies, sample is marked unstable and a counterexample is generated by taking the midpoint of the hyperrectangles x->x (line 798) o x_prime (line 832). Such hyper rectangles are built in way that guarantees they contain only counterexamples, so taking their midpoint was an arbitrary choice here.
In principle it should be possible to enrich the StabilityStatus structure by adding a counterexample hyper rectangle to propagate this information back to the main function where it can be exported.
Could that work? If so I think I can update the code in the next days.
Yes, that would be extremely helpful. Thank you for taking the time to update the code!
Can you also ensure the counterexample ranges outputted by SILVA are after an exhaustive search of the input space?
Not sure about what you mean by "exhaustive search": silva tries to avoid this as the number of states grows exponentially with the number of trees in the forest, so it stops after the first counterexample.
I mean exhaustively searching the input space for counterexamples. For example, for a simple 1-D input space, if x=1, and epsilon=0.5, then the sample is robust within [0.9, 1.1] and the counterexamples lie within [0.5, 0.89] and [1.11, 1.5]
I see, unfortunately that's not the case, silva won't compute every range of counterexamples due to aforementioned exponential complexity.
In the example you mentioned, silva could return something like [0.6, 0.75] (a subset of the first range), or [1.11, 1.5] (the whole second range), but not both. In general, no more than one. Maximality of the range is not guaranteed, although search strategy tends to explore larger regions first
Alright, but SILVA can return a whole range (like the [1.11, 1.5] in my example). If so, I think that could work! Is there a way to continue analysing the input space once the first whole range has been reported?
I updated silva by adding a --counterexamples <file path> option to the command line interface. This will create an output file with rows in the form
5: [[4.9,5.9],[3.4,4.4],[1.2,2.2],[0.8,0.9]]
where 5 is the index of the unstable sample in the dataset (starting from 0) and [[4.9,5.9],[3.4,4.4],[1.2,2.2],[0.8,0.9]] is the counter example hyper rectangle. This example is from iris, in R^4.
To reproduce this you can try the 5-5-gini forest on the iris dataset with the following command:
./silva 5-5-gini.silva data-set.csv --perturbation l_inf 0.5 --counterexamples counterexamples.dat
Let me know if this can work!
One more question - The counterexample hyperrectangle printed out per sample, does it only print out the largest violating region or does it print out all the violating regions?
Sorry for late reply, it prints only one region, not all the violating ones. It is not guaranteed to be the largest one, although this is likely to be the case due to how the search works.
Is there something that can be done on my end to make SILVA continue searching the remainder of the input space?
Not directly, but I guess you could run silva once on a sample to get one counterexample hyperrectangle, then manually compute narrower inputs and run silva on those to get more. The input hyperrectangle will eventually become so small that the classifier will become stable, and you will have found every counterexample.
For instance, in R^1 suppose you start with x = 0.5 (labeled as A), epsilon = 0.5, so input is [0.0, 1.0], and the classifier is unstable with [0.7, 0.9] as counterexample with label B. You can explore [0.0, 0.7] and [0.9, 1.0] to check what happens there, by crafting the inputs x_1 = 0.35, epsilon_1 = 0.35 and x_2 = 0.95, epsilon_2 = 0.05 and running silva two more times.
Let's say the classifier is stable over [0.9, 1.0] with label B, hence [0.9, 1.0] is another counterexample against initial x, while [0.0, 0.7] is marked unstable with counterexample [0.0, 0.4] labeled as B.
You can repeat the process on [0.4, 0.7], and see classifier is stable with label A, so no counterexample here and you'll have found every offending regions.
Bear in mind that this is going to be very expensive, as the number of regions to explore and check grows exponentially with the number of trees, their depth and the size of the feature space (which is why silva does not this out of the box).
That helps, thank you! :)
Completed