Implementation of NNV #186
Conversation
…LazySets with Stars and custom overapproximate and issubset functions
| @@ -161,3 +218,36 @@ end | |||
|
|
|||
| # Define overapproximate for SymbolicIntervalMasks and SymbolicIntervalGradients | |||
| LazySets.overapproximate(set::_SymIntOrGrad, ::Type{Hyperrectangle}) = Hyperrectangle(low=low(set), high=high(set)) | |||
| function temp_overapprox(set::Star; optimizer=GLPK.Optimizer) | |||
There was a problem hiding this comment.
temp_overapprox and issubset will be removed once the LazySets Star set PR finishes.
|
I'm hoping for some feedback on whether to more thoroughly integrate ExactReach and NNV. I could have the same forward_act functions for both (maybe living in reachability.jl), but in this case a reader who looks at NNV.jl or ExactReach.jl wouldn't get much of a sense of what the algorithm is doing under the surface. This tradeoff might be worth it to highlight their commonalities (both just repeatedly call forward_partition to go through a ReLU layer). I could also potentially unify the forward_partition function to be common to both. However, we would need to decide whether the trimming used to avoid splitting on some ReLUs for NNV should be applied to ExactReach as well. |
FYI that issue is now closed and there is a Star type in LazySets. If you have further concerns I'd be happy to discuss here (or on the Zulip OTOH in JuliaReach/LazySets.jl#2669 i'm exploring a generalization in which the predicate is a lazy intersection (say, of a polyhedron and a zonotope). That way, you can propagate such lazy intersection while storing intermediate constraints in the polyhedral part, and avoiding the (expensive) conversion of a zonotope to its hrep. |
Initial implementation of NNV. It depends on this PR in LazySets so this shouldn't be merged until that PR is closed.