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.

翻译：摘要：深度神经网络正逐渐成为各类系统的关键组件。然而，尽管取得了成功，它们仍时常出现严重错误——这激发了人们对形式化验证的浓厚兴趣。不幸的是，深度神经网络验证器作为复杂工具，本身也存在正确性缺陷。由于验证器的复杂性及被验证网络的规模，调试此类错误极具挑战性。本文提出名为DelBugV的新型工具，其核心思想是将自动化delta调试技术应用于深度神经网络验证器。给定存在故障的验证器与作为参考基准的正确验证器（在某些情况下仅需单个故障验证器），DelBugV能够生成显著简化的验证实例，这些实例仍能触发异常行为——从而大幅降低调试故障验证器的难度。该工具具备模块化与可扩展性，可便捷集成更多网络简化方法与策略。为评估性能，我们在2021年神经网络验证竞赛（VNN-COMP'21）中被观测到产生错误结果的4个验证引擎上运行DelBugV，成功简化了触发异常行为的大部分验证查询（简化幅度最高达99%）。我们认为，这项工作向着构建可靠可信的深度神经网络软件这一终极目标迈出了重要一步。