sisl / NeuralVerification.jl

Methods to soundly verify deep neural networks
MIT License
224 stars 50 forks source link

Conjuction of constraints on output #178

Open preritt opened 4 years ago

preritt commented 4 years ago

Hi The tool allows constraints to be specified in the following format

A = [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, -1.0, 0.0]'
b = [0.0]

Yc = HPolytope(A, b)

What if I want multiple constraints to be satisfied simultaneously? Can A have multiple rows and b be a column vector? For instance, can we have the following requirement on the outputs?

A = [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, -1.0, 0.0;
      1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, -1.0, 0.0]'
b = [0.0, 1.0]

Yc = HPolytope(A, b)

Thanks!

tomerarnon commented 4 years ago

Hi @preritt, The answer is yes, but depends on the solver. The restriction is that optimization-based solvers can find counterexamples only within convex sets, requiring that the complement of Y must be convex. The complement of Y being Yc, that means Yc must be convex. Therefore, your definition above would work for optimization based solvers. On the other hand, reachability based solvers can show set membership only for convex sets. That means Y itself must be convex for them to work. So the set Yc above is invalid for reachability methods. We have thoughts on relaxing these restrictions, but haven't yet taken steps to implement these ideas (e.g. #67)

preritt commented 4 years ago

Hi @tomerarnon
Thanks for your reply and the reference!