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

David Boetius, Stefan Leue, Tobias Sutter
Proceedings of the 40th International Conference on Machine Learning, PMLR 202:2712-2737, 2023.

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.

Cite this Paper

BibTeX
@InProceedings{pmlr-v202-boetius23a, title = {A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks}, author = {Boetius, David and Leue, Stefan and Sutter, Tobias}, booktitle = {Proceedings of the 40th International Conference on Machine Learning}, pages = {2712--2737}, year = {2023}, editor = {Krause, Andreas and Brunskill, Emma and Cho, Kyunghyun and Engelhardt, Barbara and Sabato, Sivan and Scarlett, Jonathan}, volume = {202}, series = {Proceedings of Machine Learning Research}, month = {23--29 Jul}, publisher = {PMLR}, pdf = {https://proceedings.mlr.press/v202/boetius23a/boetius23a.pdf}, url = {https://proceedings.mlr.press/v202/boetius23a.html}, 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.} }
Endnote
%0 Conference Paper %T A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks %A David Boetius %A Stefan Leue %A Tobias Sutter %B Proceedings of the 40th International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2023 %E Andreas Krause %E Emma Brunskill %E Kyunghyun Cho %E Barbara Engelhardt %E Sivan Sabato %E Jonathan Scarlett %F pmlr-v202-boetius23a %I PMLR %P 2712--2737 %U https://proceedings.mlr.press/v202/boetius23a.html %V 202 %X 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.
APA
Boetius, D., Leue, S. & Sutter, T.. (2023). A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks. Proceedings of the 40th International Conference on Machine Learning, in Proceedings of Machine Learning Research 202:2712-2737 Available from https://proceedings.mlr.press/v202/boetius23a.html.

Related Material