search

eth-sri / eran

ETH Robustness Analyzer for Deep Neural Networks
Apache License 2.0
320 stars 103 forks source link

Floating point soundness for Kpoly and PRIMA #105

Closed JacksonZyy closed 2 years ago

JacksonZyy commented 2 years ago

Hi,

I read your recent paper PRIMA and also its predecessor version KPoly with great interest.

  1. I wonder if you have the floating-point soundness for PRIMA? If so, could you please provide some insight on how do you handle floating-point errors for the convex computation?
  2. I notice that you call cddlib for convex computation in Kpoly. May I know if Kpoly also has floating-point soundness? And if so, does this soundness relies on the numerical error handling of cddlib, or do you handle this error by yourself?

Thanks for your reply!

mnmueller commented 2 years ago

Hi @JacksonZyy,

In PRIMA we ensure floating-point soundness of the computed multi-neuron constraints by checking for and potentially correcting any floating-point unsoundness. However, the LP solver we use (GUROBI) is not floating-point sound. Hence, the obtained results/certificates when using PRIMA are not floating-point sound.

GUROBI is also used with k-Poly which also makes it not floating-point sound.

Cheers, Mark