mlech26l / qnn_robustness_benchmarks Goto Github PK

Hi, @mlech26l

When I read your code, I'm confused about the reason why you set "quantization_config" in your "QuantizedModel" class as follows,
"int_bits_weights": 1, # Signed, +-0.3
"int_bits_bias": 2, # Signed, +-1.2
"int_bits_activation": 2, # Unsigned (relu), +1.3
"int_bits_input": 0, # Unsigned (relu), +1.3"?

1. Does it have anything to do with the way you trained the benchmark? Or, it is only designed for computing the minimal amount of bits more conveniently? :)
2. And what does the comment mean? like, +-0.3, +-1.2, +1.3

Yedi

Hi @mlech26l,

In readme file you mentioned that the network size should be 784-64-32-10.

But in the check_mnist_robustness file, why the model is defined by:QuantizedModel([64, 32], ....
Where is the 10 dim output layer?

George

Hi, @mlech26l

I change your encoding.arg_not_max function into another property as follows,

def assert_not_argmax(self, max_index):
    lte_func = self.btor.Slte if self._last_layer_signed else self.btor.Ulte
    if max_index == 9:
        tmp = 0
        for i in range(9):
            tmp = self.btor.Add(tmp, self.output_vars[i])
        disjunction = lte_func(9 * self.output_vars[int(max_index)], tmp_smt)  # sat
        self.btor.Assert(disjunction)
    else:
        exit(0)

, which means the 9*output[9]<=output[0]+...+output[8]. In other words, if the property holds, then we must find an adversarial example for the input instance (we only process the input instance 9 which is correctly predicted). When I run the instance 151(whose prediction is image-9) in MNIST with eps=1, i.e. --sample_id 151 --eps 1 --dataset mnist, the verification result looks weird: mnist test sample 151 is NOT robust! Predicted original class is 9, vs attacked image is predicted as 9. It seems that the model returned from smt-formula is not a real solution for this verification problem of the network (input_bits=8, quantization_bits=6), since the model satisfying this property must be predicted as another class with this QNN. Also I print the output of the last layer for the solution returned from boolector as follows: [-2. -2. -2. -0.875 -2. -2. -2. -2. 1.1875 1.5625 -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. -2. ] In fact, the property 9*output[9]<=output[0]+...+output[8] does not hold for this solution. Is it possible that there is a problem with the implementation of smt-bv encoding, or I miss something?

Yedi