High dimensional Hrep-Vrep (Ai2/ExactReach)

[tomerarnon]

Ai2, ExactReach, Duality currently do not work in higher dimensions due to the scaling limitations of translating from H to V representation (for linear mapping, etc.).

Discussing a possible solution for this here.

[tomerarnon]

@changliuliu noted that Duality may by suffering from a different issue that has to do with solver time (fingers crossed).

[mforets]

Ai2, ExactReach currently do not work in higher dimensions due to the scaling limitations of translating from H to V representation (for linear mapping, etc.).

Would you mind pointing to one or more particular instances that could not be handled with the current implementation?

[tomerarnon]

Hi @mforets! As you can see, this issue has been neglected for quite a while. I'll come up with an example for you if I still can. As I recall, it was directly to do with the dimensionality of the conversion: JuliaPolyhedra/CDDLib.jl#34, but we never took the "lazier" approach in this library (still meaning to) like the one you developed in JuliaReach/LazySets.jl#966 which may side step a decent portion of the problem.

[mforets]

Hi @tomerarnon, thanks for the reply. Last week while visiting @schillic at IST Austria, we spent some time thinking about how to avoid the conversion from hrep to vrep completely, and we came up with a variation of AI2 using template polyhedra and implemented it. We also tried the ideas proposed earlier in the LazySets issue you mentioned (exploit lazy intersection operations), and also a new lazy Rectification operation with a method to compute its support function added in LazySets v1.16.0 (should be tagged this week). There are some other mathematical ideas left from the longer issue #1176 that we plan to tackle on a second stage.

In sum, we're eager to try a couple of different approaches, see if they work or not, and eventually contribute to NeuralVerification.jl. But as a first stage i'd appreciate if you can guide us through some particular problem instances from the test folder and the runtimeX.jl files.

[tomerarnon]

Wow, the stuff you guys have been up to in recent months is really cool!

But as a first stage i'd appreciate if you can guide us through some particular problem instances from the test folder and the runtimeX.jl files.

tagging @clazarus for any insights into those files beyond what I know. I know that in runtime1.jl which deals with Ai2 and ExactReach, the mnist tests certainly time out (I don't recall how many hours the termination condition was).

[tomerarnon]

Now that we don't use our own translate, affine_map, etc., this is no longer an issue.