VeRe: Verification Guided Fault Localization and Repair Synthesis of Deep Neural Networks
Neural network repair aims to fix the ‘bugs’ of neural networks by modifying the model's architecture or parameters. However, due to the data-driven nature of neural networks, it is difficult to explain the relationship between internal neurons and erroneous behaviors, making further repair challenging. While several work exists to identify responsible neurons based on gradient or causality analysis, their effectiveness heavily rely on the quality of available ‘bugged’ data and multiple heuristics. Consequently, achieving precise localization and targeted repair remains a significant challenge, particularly in data-scarce scenarios. In this work, we address the issue utilizing the power of formal verification. Specifically, we propose VeRe, a verification-guided repair framework that leverages linear relaxation to precisely and efficiently estimate the repair significance of neurons. Based on the linear bounds, VeRe synthesizes ideal intervals that provide sound guarantees for correct behaviors, thereby facilitating surgical and targeted adjustments of neuron parameters to rectify faulty behaviors. We evaluated VeRe on various repair tasks, and results show that VeRe consistently achieves superior repair success rates and high generalization with negligible impact on original performance. Notably, VeRe exhibits a significantly lower dependency on repair data than existing baselines, effectively removing faulty behaviors even in data-restricted scenarios.