which pkg Ai2 rely on ?

[Student2Pro]

I'm a university student studying math and I'm trying to find a way to improve Ai2, and I could really use some help with this pkg. I'd like to know which Pkg I don't need when I focus on Ai2.

[Student2Pro]

I delete unnecessary part of this pkg because PicoSAT(if I remember it right) dosen't work on windows and I hope that by doing it the code would run faster.

[tomerarnon]

Hi @Student2Pro, I'm not sure why exactly your original error was happening. It's probably because our package hasn't kept up with changes in our dependencies. If you'd like help tracking down which dependency needs downgrading, and to which version, I'm happy to help.

If you're hacking up NV.jl for the purposes of focusing only on Ai2, you can throw out JuMP, GLPK, SCS, and PicoSAT. You can also comment out all of the include blocks in the topmost NeuralVerification.jl file except the reachability block.

I should note that our implementation of Ai2 really does not do the original algorithm justice. The original paper describes the algorithm using zonotopes rather than h-polytopes (which ostensibly makes a huge difference). At the time that we implemented Ai2 here, we did not have methods for handling zonotope intersect/union operations (the authors of LazySets have since kindly implemented that functionality for us!). At some point we intend to revisit the algorithm and implement the original authors' actual method.

[mforets]

Hi @Student2Pro and @tomerarnon,

I'm interested to help implementing AI2 using zonotopes. I'm beginning to work with student @SebastianGuadalupe in this regard, who has been doing Zonotope and Parallelotope related stuff with us in LazySets lately. He will also possibly apply for GSOC. There are several things to do. I would suggest at some point to coordinate so we don't step over each other; JuliaReach gitter channel is the usual communication channel we use, but you can also reach me by email.

@Student2Pro some comments:

• Your second comment seems to imply that removing packages from a module will make the code faster. This is not the case. The precompilation time of the package may be faster, but that is just a couple of seconds anyways and only once when you load the package.

• With respect to the error you reported before editing your OP, it is known and a fix has been found but we have not released it yet. As I commented in this PR, you can try setting the appropriate branch as a hot-fix,

julia> ] add LazySets#mforets/nverif

[tomerarnon]

The precompilation time of the package may be faster, but that is just a couple of seconds anyways and only once when you load the package

True. If you're making edits incrementally and reloading the package each time (and therefore paying the price of precomplication each time), look into using Revise.jl instead!

I'm interested to help implementing AI2 using zonotopes.

Awesome to hear! From 0 to 2 interested parties within a day 😄 The idea is relatively straightforward. Right now Ai2 relies on two core methods, forward_partition and convex_hull.

• forward_partition returns a vector containing the input set "rectified" (relu-ed) with respect to the axes. For HPolytopes, this is a simple intersection with a linear constraint. (LazySets has added the lazy Rectification, which may be able to serve as a stand-in for that operation, but right now we do everything concretely.) To extend this function to zonotopes, the same intersection process would still take place, but in a zonotope-over-approximate way. (This method is a stand-in for what the paper calls "meet")

• convex_hull is easy to imagine for general polytopes or hyperrectangles, etc.. For zonotopes, this operation is an over-approximate union-like operation. As I recall, the original paper cites a source for the method. (This method is a stand-in for what the paper calls "join")

I'm not sure whether both of these (overapproximate intersection and overapproximate convex-hull) are already implemented in LazySets, but if so, the extension of those two functions should be rather easy!

[Student2Pro]

Glad to hear from you @tomerarnon @mforets and thanks for your advices.

Hi @Student2Pro, I'm not sure why exactly your original error was happening. It's probably because our package hasn't kept up with changes in our dependencies. If you'd like help tracking down which dependency needs downgrading, and to which version, I'm happy to help.

I change the input from [-1.0, 1.0] to [-0.9, 0.9] and it worked and I got the correct result. Although I don't understand why. Maybe I made mistakes that I didn't realize. As for zonotopes, honestly I only know it's better than polytopes.

If you're hacking up NV.jl for the purposes of focusing only on Ai2, you can throw out JuMP, GLPK, SCS, and PicoSAT. You can also comment out all of the include blocks in the topmost NeuralVerification.jl file except the reachability block.

This is really helpful, appreciate it.

I'm interested to help implementing AI2 using zonotopes. I'm beginning to work with student @SebastianGuadalupe in this regard, who has been doing Zonotope and Parallelotope related stuff with us in LazySets lately. He will also possibly apply for GSOC. There are several things to do. I would suggest at some point to coordinate so we don't step over each other; JuliaReach gitter channel is the usual communication channel we use, but you can also reach me by email.

I haven't complete my code yet, but I can tell the idea. I'm combing ExactReach and Ai2, join sets before activation, so I only care 'abstract domian', and also because I know little about zonotopes. I misunderstood those packages and thank you for pointing it out.

I'll let you guys know once I finishing my code, you are also welcome check it in my repository called 'NVtest'.

[mforets]

The idea is relatively straightforward. Right now Ai2 relies on two core methods, forward_partition and convex_hull.

Thanks for your write-up! I have outsourced them to a separate issue (#87).

As for zonotopes, honestly I only know it's better than polytopes.

Affine transformations for polytopes in constraint representation are efficient only if the matrix is invertible; otherwise, the computational complexity is exponential in the dimension n, while for zonotopes, that operation is cheap (cheap as matrix-vector multiplications). On the other hand, computing the intersection of in H-representation can be easily done by concatenating the constraints (and removing redundant inequalities), while for zonotopes, they are not closed under intersection and overapproximations are often used -- in the case of the AI2 paper, the authors cite the method from this paper.