一句话：提出 VeRe，用形式验证引导的故障定位与参数优化来自动修复神经网络错误行为，可去后门并修复安全属性。
神经网络修复通过修改模型架构或参数来消除网络中的“bug”，但由于神经网络的数据驱动特性，内部神经元与错误行为之间的关系难以解释，修复十分困难。已有工作多基于梯度或因果分析定位责任神经元，其效果严重依赖“带 bug”数据的质量和层/神经元选择中的多重启发式。本文借助（面向神经网络的）形式验证能力，提出验证引导的神经网络修复框架 VeRe：基于线性松弛符号化地计算各神经元的修复重要度以完成故障定位，并进一步优化问题神经元的参数以修复错误行为。作者在多种修复任务上评估 VeRe，结果表明它能高效修复所有神经网络且不降低模型性能：在去除后门任务中，平均将攻击成功率从 98.47% 降至 0.38%，平均性能仅下降 0.9%；在安全属性修复任务中成功修复全部 36 个任务，平均泛化率达 99.87%。
Neural network repair aims to fix the 'bugs'1 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 the 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 in layer or neuron selection. In this work, we address the issue utilizing the power of formal verification (in particular for neural networks). Specifically, we propose VeRe, a verification-guided neural network repair framework that performs fault localization based on linear relaxation to symbolically calculate the repair significance of neurons and furthermore optimize the parameters of problematic neurons to repair erroneous behaviors. We evaluated VeRe on various repair tasks, and our experimental results show that VeRe can efficiently and effectively repair all neural networks without degrading the model's performance. For the task of removing backdoors, VeRe successfully reduces attack success rate from 98.47% to 0.38% on average, while causing an average performance drop of 0.9%. For the task of repairing safety properties, VeRe successfully repairs all the 36 tasks and achieves 99.87% generalization on average.
@inproceedings{paperbot11349,
title = {VeRe: Verification Guided Synthesis for Repairing Deep Neural Networks},
author = {Jianan Ma and Pengfei Yang and Jingyi Wang and Youcheng Sun and Cheng-Chao Huang and Zhen Wang},
booktitle = {ICSE},
year = {2024},
doi = {10.1145/3597503.3623332}
}