A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks

TL;DR

This paper analyzes counterexample-guided neural network repair through the lens of robust optimization, providing theoretical insights on termination and introducing a new repair algorithm for linear models.

Contribution

It establishes a connection between neural network repair and robust optimization, proving termination in restricted cases and developing a novel quadratic programming-based repair method for linear regression.

Findings

Termination guaranteed for certain restricted models

Common verifiers are practically effective despite theoretical limitations

New quadratic programming algorithm outperforms existing linear regression repair methods

Abstract

Counterexample-guided repair aims at creating neural networks with mathematical safety guarantees, facilitating the application of neural networks in safety-critical domains. However, whether counterexample-guided repair is guaranteed to terminate remains an open question. We approach this question by showing that counterexample-guided repair can be viewed as a robust optimisation algorithm. While termination guarantees for neural network repair itself remain beyond our reach, we prove termination for more restrained machine learning models and disprove termination in a general setting. We empirically study the practical implications of our theoretical results, demonstrating the suitability of common verifiers and falsifiers for repair despite a disadvantageous theoretical result. Additionally, we use our theoretical insights to devise a novel algorithm for repairing linear regression models based on quadratic programming, surpassing existing approaches.