Towards Formal Repair and Verification of Industry-scale Deep Neural Networks

There is a strong demand in the industry to update a deep neural network (DNN) as quickly, safely, and user-driven as possible for fixing critical prediction failure cases found in a safety-critical ML-enabled system for continuous quality assurance. DNN repair and equivalence verification (hereinafter called "verification") with formal methods are promising technologies for this demand because they can guarantee desirable properties, such as repair "locality (i.e., predictions do not degrade for known cases not subject to repair)" and verification "detectability (i.e., a degraded unknown case is found if it truly exists in the search space)". However, the industrial application of these technologies is difficult, mainly due to the increased computational load for mathematical optimization against a large number of DNN parameters. In this paper, we describe a challenge and new solution with our example to realize formal repair and verification of industry-scale DNNs. In this solution, repair and verification target only sparse parameter changes in a particular DNN layer and the space of inputs to that layer (i.e., feature space). By specializing mathematical optimization in repair and verification, the computational load is dramatically reduced. On the other hand, the solution also introduces new challenges regarding using feature space. We show in a practical and quantifiable way how to reasonably apply formal repair and verification and the specific challenges and issues involved, especially for the industry-scale DNN for image classification with live-action images.