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.

翻译：反例引导修复旨在创建具有数学安全保障的神经网络，促进神经网络在安全关键领域的应用。然而，反例引导修复是否保证终止仍是一个悬而未决的问题。我们通过证明反例引导修复可被视为鲁棒优化算法来探讨该问题。尽管神经网络修复本身的终止保证仍无法实现，但我们证明了更受约束的机器学习模型的终止性，并在一般环境中否定了终止性。我们通过实证研究理论结果的实际意义，表明尽管理论结果不利，但通用验证器和反例生成器仍适用于修复。此外，我们利用理论洞察提出了一种基于二次规划的线性回归模型修复新算法，优于现有方法。