OLIVE is an abstract execution tool for deep neural networks verification. Olive can accelerate the verification of a new neural network N* by leveraging existing verification results (templates) from a similar network N_0.
[This website aims to provide supplementary materials for the paper titled:"Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality" with more details and discussion, which could not be fully included in the original submission due to the page limits. ]
In particular, these materials includes:
15 DNN-based alternations benchmark models;
A running demonstration.
Detailed and additional experimental results for each research question;
Comprehensive discussion for experimental results with nice visualization (e.g., figures, plots, tables);
Additional discussion on benchmarks and source code.
Olive can accelerate the verification of a new neural network N* by leveraging existing verification results (templates) from a similar network N0. Branch and Bound technique first verifies an original network N0 through AppVerifier to generate templates T, then uses the templates to speed up the verification process when checking a modified network N*, achieving faster verification while maintaining correctness.
Key features of Olive:
Addresses a gap in current approaches: While existing methods focus on identifying whether each sub-problem should be reassessed, Olive introduces a novel prioritization strategy based on how necessary each reassessment is.
Eager to Falsification-Driven exploration: The approach explores sub-problems of verifying N* based on N0, which rechecks the most suspicious historical sub-problems first.
Olive reuses information across different subtrees of the template (represented previous verification subproblem space). Rather than treating each subtree independently, as in verification from scratch, Olive leverages insights and refinements from templates, which reduces redundant exploration with similar subproblems. Olive achieves greater efficiency in robustness verification.