DelBugV: Delta-Debugging Neural Network Verifiers
Raya Elsaleh Guy Katz
Deep neural networks (DNNs) are becoming a key component in diverse systems
across the board. However, despite their success, they often err miserably; and
this has triggered significant interest in formally verifying them.
Unfortunately, DNN verifiers are intricate tools, and are themselves
susceptible to soundness bugs. Due to the complexity of DNN verifiers, as well
as the sizes of the DNNs being verified, debugging such errors is a daunting
task. Here, we present a novel tool, named DelBugV, that uses automated delta
debugging techniques on DNN verifiers. Given a malfunctioning DNN verifier and
a correct verifier as a point of reference (or, in some cases, just a single,
malfunctioning verifier), DelBugV can produce much simpler DNN verification
instances that still trigger undesired behavior -- greatly facilitating the
task of debugging the faulty verifier. Our tool is modular and extensible, and
can easily be enhanced with additional network simplification methods and
strategies. For evaluation purposes, we ran DelBugV on 4 DNN verification
engines, which were observed to produce incorrect results at the 2021 neural
network verification competition (VNN-COMP'21). We were able to simplify many
of the verification queries that trigger these faulty behaviors, by as much as
99%. We regard our work as a step towards the ultimate goal of producing
reliable and trustworthy DNN-based software.