A weird verification result about qnn_robustness_benchmarks HOT 3 CLOSED

Hi @zhangyedi

Here, it seems that the semantics of the BV encoding differs from the TF semantics (the text attacked image is predicted as X is generated from the prediction of the TF semantics, while the counterexample is generated with the BV semantics).

For me, it looks like the issue is caused by the summation of the self.output_vars. As the BV variables are only 6 bits, there is a high chance of an over/underflow happening here when they are summed up.
The TF semantics does not actually use integers but floats that are rounded, thus there cannot be an overflow in the TF semantics.

So in essence, I think that the counterexample generated by the BV encoding exploits some over/underflow that is not present in the TF semantics.
One thing to try is to extend the bit-width of the output_vars and see if this resolves the problem (though high-bit operations can make the SMT solver very slow)

from qnn_robustness_benchmarks.

Oh, yes! After I extend the bit-width, the verification result becomes normal. Thanks very much for your immediate reply!!! :)

from qnn_robustness_benchmarks.

Great. You are welcome

from qnn_robustness_benchmarks.