Towards Repairing Neural Networks Correctly
This work addresses the problem of ensuring correctness in safety-critical neural network applications, particularly for scenarios where static verification is not scalable.
The paper proposes a runtime verification method to ensure the correctness of neural networks in safety-critical applications. It introduces additional gates at strategically identified locations to correct neural network behaviors at runtime, guaranteeing property satisfaction while maintaining consistency with the original network most of the time.
Neural networks are increasingly applied to support decision making in safety-critical applications (like autonomous cars, unmanned aerial vehicles and face recognition based authentication). While many impressive static verification techniques have been proposed to tackle the correctness problem of neural networks, it is possible that static verification may never be sufficiently scalable to handle real-world neural networks. In this work, we propose a runtime verification method to ensure the correctness of neural networks. Given a neural network and a desirable safety property, we adopt state-of-the-art static verification techniques to identify strategically locations to introduce additional gates which "correct" neural network behaviors at runtime. Experiment results show that our approach effectively generates neural networks which are guaranteed to satisfy the properties, whilst being consistent with the original neural network most of the time.