A Robust Optimisation Perspective on Counterexample-Guided Repair of
  Neural Networks
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.
David Boetius, Stefan Leue, Tobias Sutter
# A Robust Optimisation Perspective on

###### 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, surpassing existing approaches.

## 1 Introduction

The success of artificial neural networks in such diverse domains as image recognition [40], natural language processing [9], predicting protein folding [50], and designing novel algorithms [20] sparks interest in applying them to more demanding tasks, including applications in safety-critical domains. Neural networks are proposed to be used for medical diagnosis [1], autonomous aircraft control [31, 34], and self-driving cars [7]. Since a malfunctioning of such systems can threaten lives or cause environmental disaster, we require mathematical guarantees on the correct functioning of the neural networks involved. Formal methods, including verification and repair, allow obtaining such guarantees [48]. As the inner workings of neural networks are opaque to human engineers, automated repair is a vital component for creating safe neural networks.

Alternating search for violations and removal of violations is a popular approach for repairing neural networks [4, 15, 23, 25, 27, 48, 57]. We study this approach under the name _counterexample-guided repair_. Counterexample-guided repair uses inputs for which a neural network violates the specification (counterexamples) to iteratively refine the network until the network satisfies the specification. While empirical results demonstrate the ability of counterexample-guided repair to successfully repair neural networks [4], a theoretical analysis of counterexample-guided repair is lacking.

In this paper, we study counterexample-guided repair from the perspective of robust optimisation. Viewing counterexample-guided repair as an algorithm for solving robust optimisation problems allows us to encircle neural network repair from two sides. On the one hand side, we are able to show termination and optimality for counterexample-guided repair of linear regression models and linear classifiers, as well as single ReLU neurons. Coming from the other side, we disprove termination for repairing ReLU networks to satisfy a specification with an unbounded input set. Additionally, we disprove termination of counterexample-guided repair when using generic
counterexamples without further qualifications, such as being most-violating. While we could not address termination for the precise robust program of neural network repair with specifications having bounded input sets, such as \(L_{\infty}\) adversarial robustness or the ACAS Xu safety properties [35], our robust optimisation framework provides, for the first time to the best of our knowledge, fundamental insights into the theoretical properties of counterexample-guided repair.

Our analysis establishes a theoretical limitation of repair with otherwise unqualified counter-examples and suggests most-violating counterexamples as a replacement. We empirically investigate the practical consequences of these findings by comparing _early-exit_ verifiers -- verifiers that stop search on the first counterexample they encounter -- and optimal verifiers that produce most-violating counterexamples. We complement this experiment by investigating the advantages of using falsifiers during repair [4, 15], which is another approach that leverages sub-optimal counterexamples.

These experiments do not reveal any practical limitations for repair using early-exit verifiers. In fact, using an early-exit verifier consistently yields faster repair for ACAS Xu networks [35] and an MNIST [40] network, compared to using an optimal verifier. While the optimal verifier often allows performing fewer iterations, this advantage is offset by its additional runtime cost most of the time. Our experiments with falsifiers demonstrate that they can provide a significant runtime advantage for neural network repair.

For repairing linear regression models, we use our theoretical insights to design an improved repair algorithm based on quadratic programming. We compare the new algorithm with the Ouroboros [57] and SpecRepair [4] repair algorithms. The new quadratic programming repair algorithm surpasses Ouroboros and SpecRepair, illustrating the practical value of our theoretical results.

We highlight the following main contributions of this paper:

* We formalise neural network repair as a robust optimisation problem and, therefore, view counterexample-guided repair as a robust optimisation algorithm.
* Using this framework, we prove termination of counterexample-guided repair for more restrained problems than neural network repair and disprove termination in a more general setting.
* We empirically investigate the merits of using falsifiers and early-exit verifiers during repair.
* Our theoretical insights into repairing linear regression models allow us to surpass existing approaches for repairing linear regression models using a new algorithm.

## 2 Related Work

Our investigation is concerned with viewing neural network repair through the lens of robust optimisation. Neural network repair relies on neural network verification and can make use of neural network falsification. We introduce related work from these fields in this section.

**Neural Network Verification**

Neural network repair relies on neural network verifiers for proving specification satisfaction. Techniques such as Satisfiability Modulo Theories (SMT) solving [17, 35] or Mixed Integer Linear Programming (MILP) [58] allow for formally proving whether a neural network satisfies a specification. Neural network verification benefits from bounds computed using linear relaxations [17], in particular, linear relaxations that are efficiently computable through forward or backward passes over a neural network [51, 64, 67]. A particularly fruitful technique from MILP is branch and
bound [10, 45, 62]. Approaches that combine branch and bound with multi-neuron linear relaxations [21] or extend branch and bound using cutting planes [66] form the current state-of-the-art [2].

Our experiments in Section 5 are concerned with using most-violating counterexamples for repair. Strong et al. [55] perform global optimisation of functions involving neural networks. Among other applications, this allows computing most-violating counterexamples. We follow a different approach than Strong et al. [55] by fully utilising the optimisation capabilities of the MILP-based ERAN verifier [53]. This is described in more detail in Section 5.1.1.

Falsifiers are designed to discover counterexamples fast at the cost of completeness -- they can not prove specification satisfaction. Falsifiers can be used during repair to reduce expensive verifier invocations [4]. We view adversarial attacks as falsifiers for adversarial robustness specifications. Falsifiers use generic local optimisation algorithms [25, 39, 42, 56], global optimisation algorithms [4, 60], or specifically tailored search and optimisation techniques [12, 46].

#### Neural Network Repair

Neural network repair is concerned with modifying a neural network such that it satisfies a formal specification. Many approaches make use of the counterexample-guided repair algorithm (Algorithm 1) while utilising different counterexample-removal algorithms. The approaches range from augmenting the training set [25, 48, 57], over specialised neural network architectures [15, 27], and neural network training with constraints [4], to using a verifier for computing network weights [23]. Counterexample-guided repair is also applied to support vector machines and linear regression models [28, 57].

An alternative to counterexample-guided repair is training against differentiable lower bounds on the minimum specification satisfaction as introduced in Equation (6). This approach is primarily applied to train provably adversarially robust neural networks. The applied techniques include interval arithmetic [26], semi-definite relaxations [49], linear relaxations [43], and duality [63]. However, it was observed that tighter relaxations do not surpass the certified robustness obtained using interval arithmetic [26, 32]. Designing improved relaxations proves to be challenging [32].

Compared to training against differentiable lower bounds, counterexample-guided repair can be conceived as using an upper bound on the minimum specification satisfaction. This upper bound stems from a finite set of counterexamples. Training against a differentiable lower bound is limited by the degree of tightness of the lower bound, with the potential of producing overly conservative neural networks. While counterexample-guided repair is not affected by this, it remains an open question whether counterexample-guided repair is guaranteed to terminate. This is the question we are concerned with in this paper.

Beyond the above approaches, specialised neural network architectures can increase the adversarial robustness of neural networks [14, 65] but are limited to robustness specifications. Using decoupled neural networks [54] provides optimality and termination guarantees for repair but is not applicable for typical neural network specifications, such as \(L_{\infty}\) adversarial robustness and the ACAS Xu safety specifications [35].

#### Robust and Scenario Optimisation

Robust optimisation is, originally, a technique for dealing with data uncertainty [5]. Unfortunately, robust optimisation problems are, in general, NP-hard [6]. Nevertheless, in many situations, one can derive a solution in polynomial time. However, the arsenal of classical robust optimisation methods is mainly restricted to the convex setting [5]. In practice, robust optimisation problems are often solved by considering various types of relaxations. One possible relaxation is via a _chance-constrained program_, where a family of inequalities is only required to be satisfied with probability \(1-\varepsilon\) for some parameter \(\varepsilon\in(0,1)\). While, in general, chance-constrained problems are still computationally intractable [5], in many settings, tractable approximations can be obtained through the scenario program, in which only finitely many uncertainty samples are considered.
Feasibility guarantees of a scenario solution with respect to the chance-constrained program can be obtained [11] and also a link to a modified (perturbed) robust program is available [19]. While the mentioned results hold for any distribution from which the constraints are sampled, the observed empirical performance highly depends on it [18].

Madry et al. [42] and Wong and Kolter [63] use robust optimisation to train adversarially robust neural networks. Fischer et al. [22] apply the approach of Madry et al. [42] for specifications beyond adversarial robustness. Here, we study a different robust optimisation formulation where the specification is modelled as constraints. This formulation is better suited for a general setting, as it properly captures the relationship between a safety specification and a loss function. We can accept a higher loss when it is the price for satisfying the specification, as satisfying the specification is absolutely essential for safety-critical applications. Our robust optimisation formulation of repair is introduced in the following section.

## 3 Preliminaries and Problem Statement

In this section, we introduce preliminaries on robust optimisation, neural networks, and neural network verification before progressing to neural network repair, counterexample-guided repair, and the problem statement of our theoretical analysis.

### Robust Optimisation

We consider general _robust optimisation problems_

\[P:\begin{cases}\underset{\mathbf{v}}{\text{minimise}}&f(\mathbf{v})\\ \text{subject to}&g(\mathbf{v},\mathbf{d})\geq 0\quad\forall\mathbf{d}\in \mathcal{D}\\ &\mathbf{v}\in\mathcal{V},\end{cases} \tag{1}\]

where \(\mathcal{V}\subseteq\mathbb{R}^{v}\), \(\mathcal{D}\subseteq\mathbb{R}^{d}\) and \(f:\mathcal{V}\rightarrow\mathbb{R}\), \(g:\mathcal{V}\times\mathcal{D}\rightarrow\mathbb{R}\). Both \(\mathcal{V}\) and \(\mathcal{D}\) contain infinitely many elements. Therefore, a robust optimisation problem has infinitely many constraints. The _variable domain_\(\mathcal{V}\) defines eligible values for the _optimisation variable_\(\mathbf{v}\). The set \(\mathcal{D}\) may contain, for example, all inputs for which a specification needs to hold. In this example, \(g\) captures whether the specification is satisfied for a concrete input. Elaborating this example leads to neural network repair, which we introduce in Section 3.4.

A _scenario optimisation problem_ relaxes a robust optimisation problem by replacing the infinitely many constraints of \(P\) with a finite selection. For \(\mathbf{d}^{(i)}\in\mathcal{D}\), \(i\in\{1,\ldots,N\}\), \(N\in\mathbb{N}\), the scenario optimisation problem is

\[SP:\begin{cases}\underset{\mathbf{v}}{\text{minimise}}&f(\mathbf{v})\\ \text{subject to}&g\Big{(}\mathbf{v},\mathbf{d}^{(i)}\Big{)}\geq 0\quad \forall i\in\{1,\ldots,N\}\\ &\mathbf{v}\in\mathcal{V}.\end{cases} \tag{2}\]

The counterexample-guided repair algorithm that we study in this paper uses a sequence of scenario optimisation problems to solve a robust optimisation problem.

### Neural Networks

A neural network \(\text{net}_{\mathbf{\theta}}:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}\), with parameters \(\mathbf{\theta}\in\mathbb{R}^{p}\) is a function composition of affine transformations and non-linear activations. For our theoretical analysis, it suffices to consider fully-connected neural networks (FCNN). Our experiments in Section 5 also use convolutional
neural networks (CNN). We refer to Goodfellow et al. [24] for an introduction to CNNs. An FCNN with _\(L\) hidden layers_ is a chain of affine functions and activation functions

\[\mathrm{net}_{\mathbf{\theta}}=h^{(L+1)}\circ\sigma^{(L)}\circ h^{(L)}\circ\cdots \circ\sigma^{(1)}\circ h^{(1)}, \tag{3}\]

where \(h^{(i)}:\mathbb{R}^{n_{i-1}}\rightarrow\mathbb{R}^{n_{i}}\) and \(\sigma^{(i)}:\mathbb{R}^{n_{i}}\rightarrow\mathbb{R}^{n_{i}}\) with \(n_{i}\in\mathbb{N}\) for \(i\in\{0,\dots,L+1\}\) and, specifically, \(n_{0}=n\) and \(n_{L+1}=m\). Each \(h^{(i)}\) is an affine function, called an _affine layer_. It computes \(h^{(i)}(\mathbf{z})=\mathbf{W}^{(i)}\mathbf{z}+\mathbf{b}^{(i)}\) with _weight matrix_\(\mathbf{W}^{(i)}\in\mathbb{R}^{n_{i}\times n_{i-1}}\) and _bias vector_\(\mathbf{b}^{(i)}\in\mathbb{R}^{n_{i}}\). Stacked into one large vector, the weights and biases of all affine layers are the _parameters_\(\mathbf{\theta}\) of the FCNN. An _activation layer_\(\sigma^{(i)}\) applies a non-linear function, such as \(\mathrm{ReLU}\left[z\right]^{+}=\max(0,z)\) or the sigmoid function \(\sigma(z)=\frac{1}{1+e^{-z}}\) in an element-wise fashion.

### Neural Network Verification

Neural network verification is concerned with automatically proving that a neural network satisfies a formal specification.

**Definition 1** (Specifications).: A _specification_\(\Phi=\{\varphi_{1},\dots,\varphi_{S}\}\) is a set of _properties_\(\varphi_{i}\). A _property_\(\varphi=(\mathcal{X}_{\varphi},\mathcal{Y}_{\varphi})\) is a tuple of an _input set_\(\mathcal{X}_{\varphi}\subseteq\mathbb{R}^{n}\) and an _output set_\(\mathcal{Y}_{\varphi}\subseteq\mathbb{R}^{m}\).

We write \(\mathrm{net}_{\mathbf{\theta}}\vDash\Phi\) when a neural network \(\mathrm{net}_{\mathbf{\theta}}:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}\)_satisfies_ a specification \(\Phi\). Specifically,

\[\mathrm{net}_{\mathbf{\theta}}\vDash\Phi \Leftrightarrow\forall\varphi\in\Phi:\mathrm{net}_{\mathbf{\theta}}\vDash\varphi \tag{4a}\] \[\mathrm{net}_{\mathbf{\theta}}\vDash\varphi \Leftrightarrow\forall\mathbf{x}\in\mathcal{X}_{\varphi}:\mathrm{net} _{\mathbf{\theta}}(\mathbf{x})\in\mathcal{Y}_{\varphi}. \tag{4b}\]

Example specifications, such as \(L_{\infty}\) adversarial robustness or an ACAS Xu safety specification [35] are defined in Appendix A. _Counterexamples_ are at the core of the counterexample-guided repair algorithm that we study in this paper.

**Definition 2** (Counterexamples).: An input \(\mathbf{x}\in\mathcal{X}_{\varphi}\) for which a neural network \(\mathrm{net}_{\mathbf{\theta}}\) violates a property \(\varphi\) is called a _counterexample_.

To define verification as an optimisation problem, we introduce _satisfaction functions_. A satisfaction function quantifies the satisfaction or violation of a property regarding the output set. Definition 4 introduces the verification problem, also taking the input set of a property into account.

**Definition 3** (Satisfaction Function).: A function \(f_{\mathrm{Sat}}:\mathbb{R}^{m}\rightarrow\mathbb{R}\) is a _satisfaction function_ of a property \(\varphi=(\mathcal{X}_{\varphi},\mathcal{Y}_{\varphi})\) if

\[\mathbf{y}\in\mathcal{Y}_{\varphi}\Leftrightarrow f_{\mathrm{Sat}}(\mathbf{y}) \geq 0. \tag{5}\]

**Definition 4** (Verification Problem).: The _verification problem_ for a property \(\varphi=(\mathcal{X}_{\varphi},\mathcal{Y}_{\varphi})\) and a neural network \(\mathrm{net}_{\mathbf{\theta}}\) is

\[V:f_{\mathrm{Sat}}^{*}=\begin{cases}\underset{\mathbf{x}}{\text{minimise}}&f_{ \mathrm{Sat}}(\mathrm{net}_{\mathbf{\theta}}(\mathbf{x}))\\ \text{subject to}&\mathbf{x}\in\mathcal{X}_{\varphi}.\end{cases} \tag{6}\]

We call a specification a _linear specification_ when its properties have a closed convex polytope as an input set and an affine satisfaction function. Appendix A contains the satisfaction functions from SpecRepair [4] for several specifications. The following Proposition follows directly from the definition of a satisfaction function.

**Proposition 1**.: _A neural network \(\mathrm{net}_{\mathbf{\theta}}\) satisfies the property \(\varphi\) if and only if the minimum of the verification problem \(V\) is non-negative._
We now consider _counterexample searchers_ that evaluate the satisfaction function for concrete inputs to compute an upper bound on the minimum of the verification problem \(V\). Such tools can disprove specification satisfaction by discovering a counterexample. They can also prove specification satisfaction when they are _sound_ and _complete_.

**Definition 5** (Soundness and Completeness).: We call a counterexample searcher _sound_ if it computes valid upper bounds. A counterexample searcher is _complete_ if it is guaranteed to find a counterexample whenever a counterexample exists.

**Definition 6** (Verifiers and Falsifiers).: We call a sound and complete counterexample searcher a _verifier_. A counterexample searcher that is sound but not complete is a _falsifier_.

We additionally differentiate _optimal_ and _early-exit_ verifiers.

**Definition 7** (Optimal and Early-Exit Verifiers).: An _optimal_ verifier is a verifier that always produces a global minimiser of the verification problem -- a _most-violating counterexample_. Contrarily, an _early-exit_ verifier provides any counterexample when a property is violated, without further qualifications. It aborts on the first counterexample it encounters.

A technique that allows building a verifier is global optimisation. Performing global minimisation of the verification problem allows for attaining completeness. For ReLU-activated neural networks, this is possible, for example, using Mixed Integer Linear Programming (MILP) [13, 41]. On the other hand, a falsifier may perform local optimisation using projected gradient descent [39, 42] to become sound but not complete. We name this approach _BIM_, abbreviating the name _Basic Iterative Method_ used by Kurakin et al. [39].

### Neural Network Repair

Neural network repair means modifying a trained neural network so that it satisfies a specification it would otherwise violate. While the primary goal of repair is satisfying the specification, the key secondary goal is that the repaired neural network still performs well on the intended task. This secondary goal can be captured using a performance measure, such as the training loss function [4] or the distance between the modified and the original network parameters [23].

**Definition 8** (Repair Problem).: Given a neural network \(\mathrm{net}_{\mathbf{\theta}}\), a property \(\varphi=(\mathcal{X}_{\varphi},\mathcal{Y}_{\varphi})\) and a performance measure \(J:\mathbb{R}^{p}\rightarrow\mathbb{R}\), repair translates to solving the _repair problem_

\[R:\begin{cases}\underset{\mathbf{\theta}\in\mathbb{R}^{p}}{\text{minimise}}&J( \mathbf{\theta})\\ \text{subject to}&f_{\mathrm{Sat}}(\mathrm{net}_{\mathbf{\theta}}(\mathbf{x})) \geq 0\quad\forall\mathbf{x}\in\mathcal{X}_{\varphi}.\end{cases} \tag{7}\]

The repair problem \(R\) is an instance of a robust optimisation problem as defined in Equation (1). Checking whether a parameter \(\mathbf{\theta}\) is feasibility for \(R\) corresponds to verification. In particular, we can equivalently reformulate \(R\) using the verification problem's minimum \(f_{\mathrm{Sat}}^{*}\) from Equation (6) as

\[R^{\prime}:\begin{cases}\underset{\mathbf{\theta}\in\mathbb{R}^{p}}{ \text{minimise}}&J(\mathbf{\theta})\\ \text{subject to}&f_{\mathrm{Sat}}^{*}\geq 0.\end{cases} \tag{8}\]

We stress several characteristics of the repair problem that we relax or strengthen in Section 4. First of all, \(\mathrm{net}_{\mathbf{\theta}}\) is a neural network and we repair all parameters \(\mathbf{\theta}\) of the network jointly. Practically, \(\mathrm{net}_{\mathbf{\theta}}\) is a ReLU-activated FCNN or CNN, as these are the models most verifiers support. For typical specifications, such as \(L_{\infty}\) adversarial robustness or the ACAS Xu safety specifications [35], the property input set \(\mathcal{X}_{\varphi}\) is a hyper-rectangle. Hyper-rectangles are closed convex polytopes and, therefore, bounded.
### Counterexample-Guided Repair

In the previous section, we have seen that the repair problem includes the verification problem as a sub-problem. Using this insight, one approach to tackle the repair problem is to iterate running a verifier and removing the counterexamples it finds. This yields the counterexample-guided repair algorithm, that was first introduced by Goldberger et al. [23], in a similar form. Removing counterexamples corresponds to a scenario optimisation problem \(CR_{N}\) of the robust optimisation problem \(R\) from Equation (7), where

\[CR_{N}:\begin{cases}\underset{\mathbf{\theta}\in\mathbb{R}^{p}}{\text{minimise}}&J( \mathbf{\theta})\\ \text{subject to}&f_{\text{Sat}}\Big{(}\text{net}_{\mathbf{\theta}}\Big{(}\mathbf{x}^ {(i)}\Big{)}\Big{)}\geq 0\quad\forall i\in\{1,\dots,N\}.\end{cases} \tag{9}\]

Algorithm 1 defines the counterexample-guided repair algorithm using \(CR_{N}\) and \(V\) from Equation (6). In analogy to \(CR_{N}\), we use \(V_{N}\) to denote the verification problem in iteration \(N\). We call the iterations of Algorithm 1_repair steps_.

Algorithm 1 defines the counterexample-guided repair algorithm for repairing a single property. However, the algorithm extends to repairing multiple properties by adding one constraint for each property to \(CR_{N}\) and verifying the properties separately. While Algorithm 1 is formulated for the repair problem \(R\), it is easy to generalise it to any robust program \(P\) as defined in Equation (1). Then, solving \(CR_{N}\) corresponds to solving \(SP\) from Equation (2) and solving \(V_{N}\) corresponds to finding maximal constraint violations of \(P\).

The question we are concerned with in this paper is whether Algorithm 1 is guaranteed to terminate after finitely many repair steps. We investigate this question in the following section by studying robust programs that are similar to the repair problem for neural networks and typical specifications but more restrained or more general.

```
1\(N\gets 0\)do
2\(\mathbf{\theta}^{(N)}\leftarrow\text{local minimiser of }CR_{N}\)// counterexample-removal (9)
3\(N\gets N+1\)
4\(\mathbf{x}^{(N)}\leftarrow\text{global minimiser of }V\text{ for net}_{\mathbf{\theta}^{(N-1)}}\)// verification (6)
5while\(f_{\text{Sat}}\big{(}\text{net}_{\mathbf{\theta}^{(N-1)}}\big{(}\mathbf{x}^{(N)} \big{)}\big{)}<0\)
```

**Algorithm 1**Counterexample-Guided Repair

## 4 Termination of Counterexample-Guided Repair

The counterexample-guided repair algorithm (Algorithm 1) repairs neural networks by iteratively searching and removing counterexamples. In this section, we study whether Algorithm 1 is guaranteed to terminate and whether it produces optimally repaired networks. Our primary focus is on studying robust optimisation problems that are more restrained or more general than the repair problem \(R\) from Equation (7). We apply Algorithm 1 to such problems and study termination of the algorithm for these problems. On our way, we also address the related questions of optimality on termination and termination when using an early-exit verifier as introduced in Definition 7.

We start our investigation by proving that Algorithm 1 provides an optimal solution whenever it terminates. Following this, we look at the more general case of repairing a neural network to conform to a property with an unbounded input set. We disprove termination by example for this case. Next, we prove termination for more restricted problems that originate from repairing linear regression models, linear classifiers, and single ReLU neurons. Lastly, we disprove termination for repairing linear regression models when relying on an early-exit verifier.
Table 1 summarises the central problem and variable names that we use throughout this section. The iterations of Algorithm 1 are called _repair steps_. We count the repair steps starting from one but index the counterexample-removal problems starting from zero, reflecting the number of constraints. Hence, the minimiser of the counterexample-removal problem \(CR_{N-1}\) from Equation (9) in repair step \(N\) is \(\mathbf{\theta}^{(N-1)}\). The verification problem in repair step \(N\) is \(V_{N}\) with the global minimiser \(\mathbf{x}^{(N)}\). We use \(\mathbf{\theta}^{\dagger}\) for a minimiser of the repair problem \(R\) from Equation (7). We are usually satisfied with finding a local minimiser of \(R\), for example, when the objective function of \(R\) is a training loss function. However, in certain settings [23], we may also seek a global minimiser of \(R\). The difference is largely irrelevant for our analysis, as we are primarily concerned with feasibility.

### Optimality on Termination

We prove that when applied to any robust program \(P\) as defined in Equation (1), counterexample-guided repair produces a minimiser of \(P\) whenever it terminates. While Algorithm 1 is formulated for the repair problem \(R\), it is easy to generalise it to \(P\), as described in Section 3.5.

**Proposition 2** (Optimality on Termination).: _Whenever Algorithm 1 terminates after \(\overline{N}\) iterations, it holds that \(\mathbf{\theta}^{(\overline{N}-1)}=\mathbf{\theta}^{\dagger}\)._

Proof.: Assume Algorithm 1 has terminated after \(\overline{N}\) iterations for some robust program \(P\). Since Algorithm 1 has terminated, we know that \(\min V_{\overline{N}}\geq 0\). Hence, \(\mathbf{\theta}^{(\overline{N}-1)}\) is feasible for \(R\). As \(\mathbf{\theta}^{(\overline{N}-1)}\) also minimises \(CR_{\overline{N}-1}\), which is a relaxation of \(R\), it follows that \(\mathbf{\theta}^{(\overline{N}-1)}\) minimises \(R\). 

This proof is independent of whether we search for a local minimiser or a global minimiser of \(R\). Therefore, Proposition 2 holds regardless of the type of minimiser we are interested in.

### Non-Termination for General Robust Programs

In this section, we demonstrate non-termination and divergence of Algorithm 1 when we relax assumptions on the repair problem \(R\) that we outline in Section 3.4. In particular, we drop the assumption that the property's input set \(\mathcal{X}_{\varphi}\) is bounded. We disprove termination by example when \(\mathcal{X}_{\varphi}\) is unbounded. To simplify the proof, we use a non-standard neural network architecture. After the proof, we devise a fully-connected neural network (FCNN) that also leads to non-termination. However, here we also have to relax the assumption that we repair all parameters of a neural network jointly. Instead, we repair an individual parameter of the FCNN in isolation.

**Proposition 3** (General Non-Termination).: _Algorithm 1 does not terminate for \(J:\mathbb{R}\rightarrow\mathbb{R}\), \(f_{\mathrm{Sat}}:\mathbb{R}^{2}\rightarrow\mathbb{R}\) and \(\mathrm{net}_{\mathbf{\theta}}:\mathbb{R}\rightarrow\mathbb{R}^{2}\) where_

\[J(\mathbf{\theta}) =[-\mathbf{\theta}]^{+} \tag{10a}\] \[f_{\mathrm{Sat}}(\mathbf{y}) =\mathbf{y}_{2}+\mathbf{y}_{1}-1\] (10b) \[\mathrm{net}_{\mathbf{\theta}}(\mathbf{x}) =\left[\begin{pmatrix}-\mathbf{\theta}\\ \mathbf{\theta}-\mathbf{x}\end{pmatrix}\right]^{+}\] (10c) \[\mathcal{X}_{\varphi} =\mathbb{R}, \tag{10d}\]

_where \(\left[x\right]^{+}=\max(0,x)\) denotes the rectified linear unit (ReLU)._

\begin{table}
\begin{tabular}{l l l l}
**Symbol** & **Meaning** & **Symbol** & **Meaning** \\ \hline \(R\) & Repair Problem (7) & \(\mathbf{\theta}^{\dagger}\) & (Local) minimiser of \(R\) \\ \(CR_{N}\) & Counterexample Removal Problem (9) & \(\mathbf{\theta}^{(N)}\) & (Local) minimiser of \(CR_{N}\) \\ \(V_{N}\) & Verification Problem for \(\mathrm{net}_{\mathbf{\theta}^{(N-1)}}\) (6) & \(\mathbf{x}^{(N)}\) & Global minimiser of \(V_{N}\) \\ \end{tabular}
\end{table}
Table 1: **Symbol Overview**
Before we begin the proof of Proposition 3, we first give an intuition for the proof using Figure 0(a). The core of the proof is that Algorithm 1 generates parameter iterates \(\mathbf{\theta}^{(N)}\) and counter-examples \(\mathbf{x}^{(N)}\) that lie on the dark-red flat surface of Figure 0(a), where \(f_{\mathrm{Sat}}\) is negative. The combination of \(f_{\mathrm{Sat}}\) and the objective function \(J\) that prefers non-negative \(\mathbf{\theta}^{(N)}\) leads to \(\mathbf{\theta}^{(N)}\geq 0\) for every \(N\in\mathbb{N}\). As there is always a new counterexample \(\mathbf{x}^{(N)}\) for every \(\mathbf{\theta}^{(N-1)}\geq 0\), Algorithm 1 does not terminate.

Proof of Proposition 3.: Let \(J\), \(f_{\mathrm{Sat}}\), \(\mathrm{net}_{\mathbf{\theta}}\) and \(\mathcal{X}_{\varphi}\) be as in Proposition 3. Assembled into a repair problem, they yield

\[R:\begin{cases}\underset{\mathbf{\theta}\in\mathbb{R}}{\text{minimise}}&[-\mathbf{ \theta}]^{+}\\ \text{subject to}&[\mathbf{\theta}-\mathbf{x}]^{+}+[-\mathbf{\theta}]^{+}-1\geq 0 \quad\forall\mathbf{x}\in\mathbb{R}.\end{cases} \tag{11}\]

We now show that Algorithm 1 does not terminate when applied to \(R\).

The problem \(CR_{0}\) is minimising \(J(\mathbf{\theta})=[-\mathbf{\theta}]^{+}\) without constraints. The minimiser of \(J\) is not unique, but all minimisers satisfy \(\mathbf{\theta}^{(0)}\geq 0\). Let \(\mathbf{\theta}^{(0)}\geq 0\) be such a minimiser.

Searching for the global minimiser \(\mathbf{x}^{(1)}\) of \(V_{1}\), we find that this minimiser is non-unique as well. However, all minimisers satisfy \(\mathbf{x}^{(1)}\geq\mathbf{\theta}^{(0)}\). This follows since any minimiser of

\[g\Big{(}\mathbf{x},\mathbf{\theta}^{(0)}\Big{)}=\Big{[}\mathbf{\theta}^{(0)}-\mathbf{ x}\Big{]}^{+}+\left[-\mathbf{\theta}^{(0)}\right]^{+}-1 \tag{12}\]

minimises \(\big{[}\mathbf{\theta}^{(0)}-\mathbf{x}\big{]}^{+}\) as the remaining terms of Equation (12) are constant regarding \(\mathbf{x}\). The observation \(\mathbf{x}^{(1)}\geq\mathbf{\theta}^{(0)}\) applies analogously for later repair steps. Therefore, \(\mathbf{x}^{(N)}\geq\mathbf{\theta}^{(N-1)}\).

For any further repair step, we find that all non-negative feasible points \(\mathbf{\theta}\) of \(CR_{N}\) satisfy

\[\mathbf{\theta}\geq\max\Big{(}\mathbf{x}^{(1)},\ldots,\mathbf{x}^{(N)}\Big{)}+1. \tag{13}\]

This follows because \(g\big{(}\mathbf{x}^{(i)},\mathbf{\theta}\big{)}\geq 0\) has to hold for all \(i\in\{1,\ldots,N\}\) for \(\mathbf{\theta}\) to be feasible for \(CR_{N}\). Now, if \(\mathbf{\theta}\geq 0\), this condition simplifies to

\[g\Big{(}\mathbf{x}^{(i)},\mathbf{\theta}\Big{)}=\Big{[}\mathbf{\theta}-\mathbf{x}^{(i )}\Big{]}^{+}+[-\mathbf{\theta}]^{+}-1=\Big{[}\mathbf{\theta}-\mathbf{x}^{(i)}\Big{]} ^{+}-1\geq 0, \tag{14}\]

Figure 1: **Constraint Visualisations for Non-Termination Proofs.** We visualise the function \(f_{\mathrm{Sat}}(\mathrm{net}_{\mathbf{\theta}}(\mathbf{x}))\) from Proposition 3 and for the FCNN variant from Example 1. In both cases, the parameter iterates \(\mathbf{\theta}^{(N)}\) and the counterexamples \(\mathbf{x}^{(N)}\) diverge to \(\infty\) along the dark-red flat surface where the \(f_{\mathrm{Sat}}\) value is negative. This divergence implies non-termination of Algorithm 1. The black line represents an example sequence of diverging parameter and counterexample iterates.
for all \(i\in\{1,\ldots,N\}\). We see that Equation (14) is satisfied for all \(i\in\{1,\ldots,N\}\) only if \(\mathbf{\theta}\) is larger than the largest \(\mathbf{x}^{(i)}\) by at least one. This yields equivalence of Equations (14) and (13).

As Equation (13) always has a solution, there always exists a positive feasible point for \(CR_{N}\). Now, due to \(J\), any minimiser \(\mathbf{\theta}^{(N)}\) of \(CR_{N}\) is positive and hence satisfies Equation (13). Putting these results together, we obtain

\[\mathbf{\theta}^{(0)} \geq 0 \tag{15a}\] \[\mathbf{x}^{(N)} \geq\mathbf{\theta}^{(N-1)}\] (15b) \[\mathbf{\theta}^{(N)} \geq\mathbf{x}^{(N)}+1. \tag{15c}\]

Inspecting Equation (11) closely reveals that no positive value \(\mathbf{\theta}\) is feasible for \(R\) as there always exists an \(\mathbf{x}\geq\mathbf{\theta}\). However, it follows from Equations (15) that the iterate \(\mathbf{\theta}^{(N)}\) of Algorithm 1 is always positive and thus never feasible for \(R\). Since feasibility for \(R\) is the criterion for Algorithm 1 to terminate, it follows that Algorithm 1 does not terminate for this repair problem. 

We might be willing to accept non-termination for problems without a minimiser. However, \(R\) from Equation (11) has a minimiser. We have already seen in the proof of Proposition 3 that all positive \(\mathbf{\theta}\) are infeasible for \(R\). Similarly all \(\mathbf{\theta}\in(-1,0]\) are infeasible. However, all \(\mathbf{\theta}\leq-1\) are feasible as

\[[\mathbf{\theta}-\mathbf{x}]^{+}+[-\mathbf{\theta}]^{+}-1\geq[-\mathbf{\theta}]^{+}-1\geq 0, \tag{16}\]

for any \(\mathbf{x}\in\mathbb{R}\). For negative \(\mathbf{\theta}\), \(J\) prefers larger values. Because of this, the only minimiser of \(R\) is \(\mathbf{\theta}^{\dagger}=-1\). Indeed, Algorithm 1 not only fails to terminate but also moves further and further away from the optimal solution.

**Example 1** (Non-Termination for an FCNN).: The network in Proposition 3 fits our definition of a neural network but does not have a standard neural network architecture. However, Algorithm 1 also does not terminate for repairing only the parameter \(\mathbf{\theta}\) of the FCNN

\[\mathrm{net}_{\mathbf{\theta}}(\mathbf{x})=\left[\begin{pmatrix}-1&0\\ 1&-1\end{pmatrix}\left[\begin{pmatrix}0\\ 1\end{pmatrix}\mathbf{x}+\begin{pmatrix}\mathbf{\theta}\\ 2\end{pmatrix}\right]^{+}+\begin{pmatrix}2\\ 0\end{pmatrix}\right]^{+}, \tag{17}\]

when \(f_{\mathrm{Sat}}\) is as in Proposition 3 and \(J(\mathbf{\theta})=\mathrm{net}_{\mathbf{\theta}}(0)_{1}\). Figure 2 visualises this FCNN. The proof of non-termination for this FCNN is analogous to the proof of Proposition 3. Figure 0(b) visualises \(f_{\mathrm{Sat}}(\mathrm{net}_{\mathbf{\theta}}(\mathbf{x}))\) for the FCNN from Equation (17). Comparison with Figure 0(a) reveals that the key aspects of \(f_{\mathrm{Sat}}(\mathrm{net}_{\mathbf{\theta}}(\mathbf{x}))\) for the FCNN are identical to Proposition 3, except for being shifted. Most notably, there also is a flat surface with a negative \(f_{\mathrm{Sat}}\) value. As \(J\) also prefers non-negative \(\mathbf{\theta}\) in this example, Algorithm 1 diverges here as well.

### Termination for Robust Programs with Linear Constraints

In the previous section, we relax assumptions on neural network repair and show non-termination for the resulting more general problem. In this section, we look at a more restricted class of problems instead: robust problems with linear constraints. This class of problems encompasses, for example, repairing linear regression models to conform to a linear specification. Linear regression models can be understood as neural networks without hidden layers. As defined in Section 3.3, linear specifications consist only of properties with an affine satisfaction function and a closed convex polytope as an input set.
**Theorem 1** (Termination for Linear Constraints).: _Let \(g(\mathbf{\theta},\mathbf{x})=f_{\mathrm{Sat}}(\mathrm{net}_{\mathbf{\theta}}(\mathbf{x}))\) be bi-linear and let \(\mathcal{X}_{\varphi}\) be a closed convex polytope. Algorithm 1 computes a minimiser of_

\[R:\left\{\begin{aligned} &\underset{\mathbf{\theta}\in\mathbb{R}^{p}}{ \text{minimise}}& J(\mathbf{\theta})\\ &\text{subject to}& g(\mathbf{\theta},\mathbf{x})\geq 0 \quad\forall\mathbf{x}\in\mathcal{X}_{\varphi}\end{aligned}\right. \tag{18}\]

_in a finite number of repair steps._

Proof.: We prove termination of Algorithm 1 for \(R\) from Theorem 1. Optimality then follows from Proposition 2. Let \(g:\mathbb{R}^{p}\times\mathbb{R}^{n}\to\mathbb{R}\) be bi-linear, that is, linear in each argument when the other one is fixed. Let \(\mathcal{X}_{\varphi}\) be a closed convex polytope. Given this, every \(V_{N}\) is a linear program and all \(V_{N}\) share the same feasible set \(\mathcal{X}_{\varphi}\). Because \(V_{N}\) is a linear program, its minimiser coincides with one of the vertices of the feasible set \(\mathcal{X}_{\varphi}\).

It follows that \(\forall N\in\mathbb{N}:\mathbf{x}^{(N)}\in\mathrm{vert}(\mathcal{X}_{\varphi})\), where \(\mathrm{vert}(\mathcal{X}_{\varphi})\) are the vertices of \(\mathcal{X}_{\varphi}\). Because \(\mathrm{vert}(\mathcal{X}_{\varphi})\) is finite, at some repair step \(\overline{N}\) of Algorithm 1, we obtain a minimiser that we already encountered in a previous repair step. Let \(\tilde{N}\) be that repair step, such that \(\mathbf{x}^{(\tilde{N})}=\mathbf{x}^{(\overline{N})}\). Since \(\mathbf{\theta}^{(\overline{N}-1)}\) is feasible for \(\mathit{CR}_{\overline{N}-1}\), it satisfies

\[g\Big{(}\mathbf{\theta}^{(\overline{N}-1)},\mathbf{x}^{(\tilde{N})}\Big{)}=g \Big{(}\mathbf{\theta}^{(\overline{N}-1)},\mathbf{x}^{(\overline{N})}\Big{)}=f_{ \mathrm{Sat}}\Big{(}\mathrm{net}_{\mathbf{\theta}^{(\overline{N}-1)}}\Big{(} \mathbf{x}^{(\overline{N})}\Big{)}\Big{)}\geq 0. \tag{19}\]

As this is the negation of the loop condition of Algorithm 1, the algorithm terminates in repair step \(\overline{N}\). 

Note that Theorem 1 holds without assumptions on the objective \(J\). Therefore, Theorem 1 encompasses such cases as training a linear regression model or a linear support vector machine under a linear specification. The insights from our proof enable a new repair algorithm for linear regression models based on quadratic programming. We discuss and evaluate this algorithm in Section 5.4.

### Termination for Element-Wise Monotone Constraints

Next, we study a different restricted class of repair problems that contains repairing single ReLU and sigmoid neurons to conform to linear specifications. This includes repairing linear classifiers, which are single sigmoid neurons. In this class of problems, the constraint \(g(\mathbf{\theta},\mathbf{x})=f_{\mathrm{Sat}}(\mathrm{net}_{\mathbf{\theta}}(\mathbf{ x}))\) is _element-wise monotone_ and continuous and \(\mathcal{X}_{\varphi}\) is a hyper-rectangle. Element-wise monotone functions are monotone in each argument, all other arguments being fixed at some value. We show termination for this class of repair problems.

Figure 2: **Fully-Connected Neural Network Variant of Proposition 3. This Figure visualises Equation (17). Empty nodes represent single ReLU neurons. Edge labels between nodes contain the network weights. Where edges are omitted, the corresponding weights are zero. Biases are written next to the incoming edge above the ReLU neurons.**
**Definition 9** (Element-Wise Monotone).: A function \(f:\mathcal{X}\to\mathbb{R}\), \(\mathcal{X}\subseteq\mathbb{R}^{n}\), is _element-wise monotone_ if

\[\forall i\in\{1,\ldots,n\}:\forall\mathbf{x}\in\mathcal{X}:\,f|_{\mathcal{X} \cap(\{\mathbf{x}_{1}\}\times\cdots\times\{\mathbf{x}_{i-1}\}\times\mathbb{R} \times\{\mathbf{x}_{i+1}\}\times\cdots\times\{\mathbf{x}_{n}\})}\text{ is monotone}. \tag{20}\]

_Remark_.: Affine transformations of element-wise monotone functions maintain element-wise monotonicity. This directly follows from affine transformations maintaining monotonicity.

Element-wise monotone functions can be monotonically increasing and decreasing in the same element but only for different values of the remaining elements. Examples of element-wise monotone functions include \(\big{[}\mathbf{w}^{\mathsf{T}}\mathbf{x}+\mathbf{b}\big{]}^{+}\) and \(\sigma\big{(}\mathbf{w}^{\mathsf{T}}\mathbf{x}+\mathbf{b}\big{)}\), where \([x]^{+}=\max(0,x)\) is the ReLU function and \(\sigma(x)=\frac{1}{1+e^{-x}}\) is the sigmoid function. These functions are also continuous.

**Theorem 2** (Termination for Element-Wise Monotone Constraints).: _Let \(g(\boldsymbol{\theta},\mathbf{x})=f_{\mathrm{Sat}}(\mathrm{net}_{\boldsymbol{ \theta}}(\mathbf{x}))\) be element-wise monotone and continuous. Let \(\mathcal{X}_{\varphi}\) be a hyper-rectangle. Algorithm 1 computes a minimiser of_

\[R:\begin{cases}\underset{\boldsymbol{\theta}\in\mathbb{R}^{p}}{ \text{minimise}}&J(\boldsymbol{\theta})\\ \text{subject to}&g(\boldsymbol{\theta},\mathbf{x})\geq 0\quad\forall \mathbf{x}\in\mathcal{X}_{\varphi}\end{cases} \tag{21}\]

_in a finite number of repair steps under the assumption that the algorithm prefers global minimisers of \(V_{N}\) that are vertices of \(\mathcal{X}_{\varphi}\)._

In this theorem, we make an assumption on the global minimisers that Algorithm 1 prefers when there are multiple global minimisers. In the proof of Lemma 1, we show that the assumption in Theorem 2 is a weak assumption. In particular, we show that it is easy to construct a global minimiser of \(V_{N}\) that is a vertex of \(\mathcal{X}_{\varphi}\) given any global minimiser of \(V_{N}\). Lemma 1 is a preliminary result for proving Theorem 2.

**Lemma 1** (Optimal Vertices).: _Let \(R\), \(g\) and \(\mathcal{X}_{\varphi}\) be as in Theorem 2. Then, for every \(N\in\mathbb{N}\) there is \(\tilde{\mathbf{x}}^{(N)}\in\mathrm{vert}(\mathcal{X}_{\varphi})\) that globally minimises \(V_{N}\), where \(\mathrm{vert}(\mathcal{X}_{\varphi})\) denotes the set of vertices of \(\mathcal{X}_{\varphi}\)._

Proof.: Let \(R\), \(g\), \(\mathcal{X}_{\varphi}\) be as in Lemma 1. Let \(N\in\mathbb{N}\). To prove the lemma we show that a) \(V_{N}\) has a minimiser and b) when there is a minimiser of \(V_{N}\), some vertex of \(\mathcal{X}_{\varphi}\) also minimises \(V_{N}\) and has the same \(f_{\mathrm{Sat}}\) value.

* As the feasible set of \(V_{N}\) is closed and bounded due to being a hyper-rectangle and the objective function is continuous, \(V_{N}\) has a minimiser.
* Let \(\mathbf{x}^{(N)}\in\mathbb{R}^{n}\) be a global minimiser of \(V_{N}\). We show that there is a \(\tilde{\mathbf{x}}^{(N)}\in\mathrm{vert}(\mathcal{X}_{\varphi})\) such that \(\tilde{\mathbf{x}}^{(N)}\) also minimises \(V_{N}\) since \[g\Big{(}\boldsymbol{\theta}^{(N-1)},\mathbf{x}^{(N)}\Big{)}\geq g\Big{(} \boldsymbol{\theta}^{(N-1)},\tilde{\mathbf{x}}^{(N)}\Big{)}.\] (22) Pick any dimension \(i\in\{1,\ldots,n\}\). As \(g\) is element-wise monotone, it is non-increasing in one of the two directions along dimension \(i\) starting from \(\mathbf{x}^{(N)}\). When \(\mathbf{x}^{(N)}\) does not already lie on a face of \(\mathrm{X}_{\varphi}\) that bounds expansion along the \(i\)-axis, we walk along the non-increasing direction along dimension \(i\) until we reach such a face of \(\mathrm{X}_{\varphi}\). As \(\mathrm{X}_{\varphi}\) is a hyper-rectangle and, therefore, bounded, it is guaranteed that we reach such a face. We pick the point on the face of \(\mathrm{X}_{\varphi}\) as the new \(\mathbf{x}^{(N)}\). While keeping dimension \(i\) fixed, we repeat the above procedure for a different dimension \(j\in\{1,\ldots,n\},i\neq j\). We iterate the procedure over all dimensions always keeping the value of \(\mathbf{x}^{(N)}\) in already visited dimensions fixed. In every step of this procedure, we restrict ourselves to a lower-dimensional face of \(\mathcal{X}_{\varphi}\) as we fix the value in one dimension. Thus, when we have visited every dimension, we have
reached a \(0\)-dimensional face of \(\mathcal{X}_{\varphi}\), that is, a vertex. Since we only walked along directions in which \(g\) is non-increasing and since \(g\) is element-wise monotone, the vertex \(\tilde{\mathbf{x}}^{(N)}\) that we obtain satisfies Equation (22). Since \(\mathbf{x}^{(N)}\) is a global minimiser, Equation (22) needs to hold with equality.

Together, a) and b) yield that there is always a vertex \(\tilde{\mathbf{x}}^{(N)}\in\operatorname{vert}(\mathcal{X}_{\varphi})\) that globally minimises \(V_{N}\). 

Proof of Theorem 2.: Again, we prove termination with optimality following from Proposition 2. Let \(R\), \(g\), \(\mathcal{X}_{\varphi}\) be as in Theorem 2. Also, assume that Algorithm 1 prefers vertices of \(\mathcal{X}_{\varphi}\) as global minimisers of \(V_{N}\). From Lemma 1 we know that there is always a vertex of \(\mathcal{X}_{\varphi}\) that minimises \(V_{N}\). From the proof of Lemma 1 we also know that it is easy to find such a vertex given any global minimiser of \(V_{N}\).

As Algorithm 1 always chooses vertices of \(\mathcal{X}_{\varphi}\) under our assumption, there is only a finite set of minimisers \(\mathbf{x}^{(N)}\), as a hyper-rectangle has only finitely many vertices. Given this, termination follows analogously to the proof of Theorem 1. 

As the class of continuous element-wise monotone functions includes single ReLU and sigmoid neurons, Theorem 2 provides a termination guarantee for repairing linear classifiers -- which are single sigmoid neurons -- to conform to linear specifications.

While we have proven termination for single neurons now, the facts that we used in our proof no longer hold when we consider neural networks of multiple neurons. Notably, for such networks, \(V_{N}\) can have a minimiser anywhere inside the feasible region and this minimiser may move when the network parameters are modified. Coming from the other side, the construction that we use in Section 4.2 relies on a diverging sequence of counterexamples. However, when counterexamples need to lie in a bounded set, as it is the case with common neural network specifications, it becomes intricate to construct a diverging sequence originating from a repair problem.

In summary, although we can not answer at this point whether Algorithm 1 terminates when applied to neural network repair for bounded property input sets, our methodology is useful for studying related questions. Our theoretical results in this paper may point in the direction in which the answer to our original question lies. In the following section, we continue our theoretical analysis, showing that early-exit verifiers are insufficient for guaranteeing termination of Algorithm 1.

### Counterexample-Guided-Repair with Early-Exit Verifiers

From a verification perspective, verifiers are not required to find most-violating counterexamples. Instead, it suffices to find any counterexample if one exists. In this section, we show that using just any counterexample is not sufficient for Algorithm 1 to terminate. We show that when using an _early-exit_ verifier that produces such otherwise unqualified counterexamples, repair may fail even for repairing linear regression models. As linear regression models are special neural networks without hidden layers, this result propagates to neural network repair.

Consider a modification of Algorithm 1, where we only search for a feasible point of \(V_{N}\) with a negative objective value instead of the global minimum. This corresponds to using an early-exit verifier during repair. The following proposition demonstrates that this modification can lead to non-termination even for robust optimisation problems with linear constraints.
**Proposition 4** (Non-Termination for Early-Exit Verifiers).: _Algorithm 1 modified to use an early-exit verifier is not guaranteed to terminate for_

\[J(\mathbf{\theta}) =|\mathbf{\theta}| \tag{23a}\] \[f_{\mathrm{Sat}}(\mathbf{y}) =\mathbf{y}\] (23b) \[\mathrm{net}_{\mathbf{\theta}}(\mathbf{x}) =\mathbf{\theta}-\mathbf{x}\] (23c) \[\mathcal{X}_{\varphi} =[0,1]. \tag{23d}\]

Proof.: Let \(J\), \(f_{\mathrm{Sat}}\), \(\mathrm{net}_{\mathbf{\theta}}\) and \(\mathcal{X}_{\varphi}\) be as in Proposition 4. When inserting these into Equation (7), we obtain the repair problem

\[R:\begin{cases}\underset{\mathbf{\theta}\in\mathbb{R}}{\text{minimise}}&|\mathbf{ \theta}|\\ \text{subject to}&\mathbf{\theta}-\mathbf{x}\geq 0\quad\forall\mathbf{x}\in[0,1]. \end{cases} \tag{24}\]

Assume the early-exit verifier generates the sequence \(\mathbf{x}^{(N)}=\frac{1}{2}-\frac{1}{N+2}\) as long as these points are counterexamples for \(\mathrm{net}_{\mathbf{\theta}^{(N-1)}}\). Otherwise, let it produce \(\mathbf{x}^{(N)}=1\), the global minimum of all \(V_{N}\). Minimising \(J\) without constraints yields \(\mathbf{\theta}^{(0)}=0\). The point \(\mathbf{x}^{(1)}=\frac{1}{2}-\frac{1}{3}\) is a valid result of the early-exit verifier for \(V_{1}\), as it is a counterexample. We observe that the constraint

\[f_{\mathrm{Sat}}(\mathrm{net}_{\mathbf{\theta}}(\mathbf{x}))=\mathbf{ \theta}-\mathbf{x}\geq 0 \tag{25}\]

is tight when \(\mathbf{\theta}=\mathbf{x}\). Smaller \(\mathbf{\theta}\) violate the constraint. Since \(J\) prefers values of \(\mathbf{\theta}\) closer to zero, it always holds for any minimiser of \(CR_{N}\) that

\[\mathbf{\theta}^{(N)}=\max\left(\mathbf{x}^{(1)},\dots,\mathbf{x}^{ (N)}\right)=\mathbf{x}^{(N)}. \tag{26}\]

The last equality is due to the construction of the points returned by the early-exit verifier. However, for these values of \(\mathbf{\theta}^{(N)}\), \(\frac{1}{2}-\frac{1}{N+2}\) always remains a valid product of the early-exit verifier for \(V_{N}\). Thus we obtain,

\[\mathbf{\theta}^{(N)}=\mathbf{x}^{(N)}=\frac{1}{2}-\frac{1}{N+2}. \tag{27}\]

The minimiser of \(R\) is \(\mathbf{\theta}^{\dagger}=1\). However, \(\mathbf{\theta}^{(N)}\) does not converge to this point but to the infeasible \(\lim_{N\to\infty}\mathbf{\theta}^{(N)}=\frac{1}{2}\). Since the iterates \(\mathbf{\theta}^{(N)}\) always remain infeasible for \(R\), the modified Algorithm 1 never terminates. 

This result concludes our theoretical investigation. Table 2 summarises our results regarding the termination of Algorithm 1. In the following section, we research empirical aspects of Algorithm 1, including the practical implications of the above result on using early-exit verifiers.

## 5 Experiments

_Optimal_ verifiers that compute most-violating counterexamples are theoretically advantageous but not widely available [55]. Conversely, _early-exit_ verifiers that produce plain counterexamples without further qualifications are readily available [3, 21, 36, 59, 66], but are theoretically disadvantageous, as apparent from Section 4.5. However, despite these theoretical findings, previous work reveals that practically it is possible to achieve repair while using early-exit verifiers [4, 15]. In this section, we empirically compare the effects of using most-violating counterexamples and sub-optimal counterexamples -- as produced by early-exit verifiers and falsifiers -- for repair. Additionally, we apply our insights from Section 4.3 for repairing linear regression models. Our experiments address the following questions regarding counterexample-guided repair:
* How does repair using an early-exit verifier compare quantitatively to repair using an optimal verifier?
* What quantitative advantages does it provide to use falsifiers during repair?
* Can we surpass existing repair algorithms for linear regression models using our theoretical insights?

### Experiment Design

In our experiments, we repair an MNIST [40] network, ACAS Xu networks [35], a CollisionDetection [17] network, and Integer Dataset Recursive Model Indices (RMIs) [57]. For repair, we make use of an early-exit verifier, an optimal verifier, the SpecAttack falsifier [4], and the BIM falsifier [39]. To obtain an optimal verifier, we modify the ERAN verifier [53] to compute most-violating counterexamples. We use the modified ERAN verifier both as the early-exit and as the optimal verifier in our experiments, as it supports both exit modes.

In all experiments, we use the SpecRepair counterexample-removal algorithm [4] unless otherwise noted. We use SpecRepair with a decreased initial penalty weight of \(2^{-4}\) and a satisfaction constant of \(10^{-4}\). We set up all verifiers and falsifiers to return a single counterexample. For SpecAttack, that produces multiple counterexamples, we select the counterexample with the largest violation. We make this modification to eliminate differences due to some tools returning more counterexamples than others, as we are interested in studying the effects of counterexample quality, not counterexample quantity.

#### 5.1.1 Modifying ERAN to Compute Most-Violating Counterexamples

The ETH Robustness Verifier for Neural Networks (ERAN) [53] combines abstract interpretation with Mixed Integer Linear Programming (MILP) to verify neural networks. For our experiments, we use the DeepPoly abstract interpretation [52]. ERAN leverages Gurobi [29] for MILP. To verify properties with low-dimensional input sets having a large diameter, ERAN implements the ReluVal

\begin{table}
\begin{tabular}{l l l l l} \multicolumn{1}{c}{**Problem Class**} & \multicolumn{1}{c}{**Model**} & \multicolumn{1}{c}{**Specification**} & \multicolumn{1}{c}{**Termination of**} \\ \hline \(f_{\text{Sat}}(\text{net}_{\mathbf{\theta}}(\mathbf{x}))\) bi-linear, & Linear Regression & Linear & ✓ & (Theorem 1) \\ \(\mathcal{X}_{\varphi}\) closed convex & Model, Linear & & & \\ polytope & Support Vector & & & \\  & Machine & & & \\ \(f_{\text{Sat}}(\text{net}_{\mathbf{\theta}}(\mathbf{x}))\) element- & Linear Classifier, & Linear & ✓ & (Theorem 2) \\ wise monotone and & ReLU Neuron & & & \\ continuous, & & & & \\ \(\mathcal{X}_{\varphi}\) hyper-rectangle & & & & \\ net\({}_{\mathbf{\theta}}(\mathbf{x})\) neural network, & Neural Network & Bounded Input &? \\ \(\mathcal{X}_{\varphi}\) bounded & & Set & & \\ net\({}_{\mathbf{\theta}}(\mathbf{x})\) neural network, & Neural Network & Unbounded & ✗(Proposition 3) \\ \(\mathcal{X}_{\varphi}\) unbounded & & Input Set & & \\ Using an early-exit & Any & Any & ✗(Proposition 4) \\ verifier & & & & \\ \end{tabular}
\end{table}
Table 2: **Termination Results Summary**
input splitting branch and bound procedure [61]. We employ this branch and bound procedure only for ACAS Xu.

The Gurobi MILP solver can be configured to stop optimisation when encountering the first point with a negative satisfaction function value below a small threshold. We use this feature for the early-exit mode. To compute most-violating counterexamples, we instead run the MILP solver until achieving optimality.

The input-splitting branch and bound procedure evaluates branches in parallel. In the early-exit mode, the procedure terminates when it finds a counterexample on any branch. As other branches may contain more-violating counterexamples, we search the entire branch and bound tree in the optimal mode.

#### 5.1.2 Datasets, Networks, and Specifications

We perform experiments with four different datasets. In this section, we introduce the datasets, as well as what networks we repair to conform to which specifications. The network architectures for each dataset are contained in Table 3.

#### Mnist

The MNIST dataset [40] consists of \(70\,000\) labelled images of hand-written Arabic digits. Each image has \(28\times 28\) pixels. The dataset is split into a training set of \(60\,000\) images and a test set of \(10\,000\) images. The task is to predict the digit in an image from the image pixel data. We train a small convolutional neural network achieving \(97\,\%\) test set accuracy (\(98\)% training set accuracy). Table 3 contains the concrete architecture.

We repair the \(L_{\infty}\) adversarial robustness of this convolutional neural network for groups of \(25\) input images. These images are randomly sampled from the images in the training set for which the network is not robust. Each robustness property has a radius of \(0.03\). Overall, we form \(50\) non-overlapping groups of input images. Thus, each repaired network is guaranteed to be locally robust for a different group of \(25\) training set images. While specifications of this size are not practically relevant, they make it feasible to perform several (\(50\)) experiments for each verifier variant. We formally define \(L_{\infty}\) adversarial robustness in Appendix A.1.

We train the MNIST network using Stochastic Gradient Descent (SGD) with a mini-batch size of \(32\), a learning rate of \(0.01\) and a momentum coefficient of \(0.9\), training for two epochs. Counterexample-removal uses the same setup, except for using a decreased learning rate of \(0.001\) and iterating only for a tenth of an epoch.

\begin{table}
\begin{tabular}{l l} \hline
**Dataset** & **Network Architecture** \\ \hline MNIST & In(1\(\times\)28\(\times\)28), Conv(out=8, kernel=3, stride=3, pad=1), ReLU, FC(out=80), ReLU] \(\times\) 6, FC(out=50) \\ ACAS Xu & In(5), [FC(out=50), ReLU] \(\times\) 6, FC(out=5) \\ CollisionDetection & In(6), [FC(out=10), ReLU] \(\times\) 2, FC(out=2) \\ RMI, First Stage & In(1), [FC(out=16), ReLU] \(\times\) 2, FC(out=1) \\ RMI, Second Stage & In(1), FC(out=1) \\ \hline \end{tabular}
\end{table}
Table 3: **Network Architectures. In(*) gives the dimension of the network input. Convolutional layers are denoted Conv(*), where out is the number of filters and kernel, stride, and pad are the kernel size, stride, and padding for all spatial dimensions of the layer input. Fully-connected layers are denoted FC(*), where out is the number of neurons. [-] \(\times\)\(n\) denotes the \(n\)-fold repetition of the block in square brackets. RMI stands for the Integer Dataset RMIs.**
#### ACAS Xu

The ACAS Xu networks [35] form a collision avoidance system for aircraft without on-board personnel. Each network receives five sensor measurements that characterise an encounter with another aircraft. Based on these measurements, an ACAS Xu network computes scores for five possible steering directions: Clear of Conflict (maintain course), weak left/right, and strong left/right. The steering direction advised to the aircraft is the output with the minimal score. Each of the \(45\) ACAS Xu networks is responsible for another class of encounter scenarios. More details on the system are provided by Julian et al. [34]. Each ACAS Xu network is a fully-connected ReLU network with six hidden layers of \(50\) neurons each.

Katz et al. [35] provide safety specifications for the ACAS Xu networks. Of these specifications, the property \(\phi_{2}\) is violated by the largest number of networks. We repair \(\phi_{2}\) for all networks violating it, yielding \(34\) repair cases. The property \(\phi_{2}\) specifies that the score for the Clear of Conflict action is never maximal (least-advised) when the intruder is far away and slow. The precise formal definition of \(\phi_{2}\) is given in Appendix A.2.

We repair the ACAS Xu networks following Bauer-Marquart et al. [4]. To replace the unavailable ACAS Xu training data, we randomly sample a training and a validation set and compare with the scores produced by the original network. As a loss function, we use the asymmetric mean square error loss of Julian and Kochenderfer [33]. We repair using the Adam training algorithm [37] with a learning rate of \(10^{-4}\). We terminate training on convergence, when the loss on the validation set starts to increase, or after at most \(500\) iterations.

For assessing the performance of repaired networks, we compare the accuracy and the Mean Absolute Error (MAE) between the predictions of the repaired network and the predictions of the original network on a large grid of inputs, filtering out counterexamples. For all networks, the filtered grid contains more than \(24\) million points.

#### CollisionDetection

The CollisionDetection dataset [17] is introduced for evaluating neural network verifiers. The task is to predict whether two particles collide based on their relative position, speed, and turning angles. The training set of \(7000\) samples and the test set of \(3000\) samples are obtained from simulating particle dynamics for randomly sampled initial configurations. We train a small fully-connected neural network with \(20\) neurons on this dataset. The full architecture is given in Table 3.

Similarly to MNIST, we repair the adversarial robustness of this network for \(100\) non-overlapping groups of ten randomly sampled inputs from the training set. Here we also include inputs that do not violate the specification to gather a sufficient number of groups. Each robustness property has a radius of \(0.05\).

The CollisionDetection network is trained for \(1000\) iterations using Adam [37] with a learning rate of \(0.01\). Repair uses Adam with a learning rate of \(0.001\), terminating training on convergence or when reaching \(5000\) iterations.

#### Integer Dataset RMIs

Learned index structures replace index structures, such as B-trees, with machine learning models [38]. Tan et al. [57] identify these models as prime candidates for neural network verification and repair due to the strict requirements of their domain and the small size of the models. We use _Recursive Model Indices_ (RMIs) [38] in our experiments. The task of an RMI is to resolve a key to a position in a sorted sequence.

We build datasets, RMIs and specifications following Tan et al. [57], with the exception that we create models of two sizes. While Tan et al. [57] build one RMI with a second-stage size of ten, we build ten RMIs with a second-stage size ten and \(50\) RMIs with a second-stage size of \(304\). Each RMI is constructed for a different dataset. We create models of two second-stage sizes because the smaller size does not yield unsafe first-stage models, while the larger second-stage size does not yield unsafe second-stage models. However, we want to repair models of both stages.
Each dataset is a randomly generated integer dataset consisting of a sorted sequence of \(190\,000\) integers. The integers are randomly sampled from a uniform distribution with the range \(\left[0,10^{6}\right]\). The task is to predict the index of an integer (key) in the sorted sequence.

We build an RMI for each dataset. Each RMI consists of two stages. The first stage contains one neural network. The second stage contains several linear regression models. In our case, the second stage contains either ten or \(304\) models. Each dataset is first split into several disjoint blocks, one for each second-stage model. Now, the first-stage network is trained to predict the block an integer key belongs to. The purpose of this model is to select a model from the second stage. Each model of the second stage is responsible for resolving the keys in a block to the position of the key in the sorted sequence. The architectures of the models are given in Table 3.

We train the first-stage model to minimise the Mean Square Error (MSE) between the model predictions and the true blocks. Training uses Adam [37] with a learning rate of \(0.01\) and a mini-batch size of \(512\). For an RMI with a second-stage size of ten, we train for one epoch. For the larger second-stage size of \(304\), we train for six epochs.

Minimising the MSE between the positions a second stage model predicts and the true positions can be solved analytically. We use the analytic solution for training the second stage models. In Section 5.4, we compare with Ouroboros [57] that also uses the analytic solution. SpecRepair [4] can not make use of the analytic solution. Instead, it repairs second-stage models using gradient descent with a learning rate of \(10^{-13}\), running for \(150\) iterations.

The specifications for the RMIs are error bounds on the predictions of each model. For a first-stage neural network, the specification is that it may not deviate by more than one valid block from the true block. The specification for a second-stage model consists of one property for each integer in the target block and one for all other integers that the first stage assigns to the second-stage model. The property for a key \(k_{i}\) specifies that the prediction for all keys between the previous key \(k_{i-1}\) and the next key \(k_{i+1}\) in the dataset may not deviate by more than \(\varepsilon\) from the position for \(k_{i}\). We use two sets of specifications, one with \(\varepsilon=100\) and one with \(\varepsilon=150\). The specifications express a guaranteed error bound for looking up both existing and non-existing keys [57]. The formal definitions of the specifications are given in Appendix A.3.

#### 5.1.3 Implementation and Hardware

We build upon SpecRepair [4] for our experiments, leveraging the modified ERAN. SpecRepair and ERAN are implemented in Python. SpecRepair is based on PyTorch [47]. For repairing linear regression models, we also use an ERAN-based Python reimplementation of Ouroboros [57]. The original Ouroboros implementation is not publicly available. The quadratic programming repair algorithm for linear regression models is implemented in Python and leverages Gurobi [29]. Our source code is available at [https://github.com/sen-uni-kn/specrepair](https://github.com/sen-uni-kn/specrepair).

All experiments were conducted on Ubuntu 2022.04.1 LTS machines using Python 3.8. The ACAS Xu, CollisionDetection and Integer Dataset RMI experiments were run on a compute server with an Intel Xeon E5-2580 v4 2.4GHz CPU (28 cores) and 1008GB of memory. The MNIST experiments were run on a GPU compute server with an AMD Ryzen Threadripper 3960X 24-Core Processor and 252GB of memory, utilising an NVIDIA RTX A6000 GPU with 48GB of memory.

We limit the execution time for repairing each ACAS Xu network and each MNIST specification to three hours. For CollisionDetection and the Integer Dataset RMIs, we use a shorter timeout of one hour. Except for ACAS Xu, whenever we report runtimes, we repeat all experiments ten times and report the median runtime from these runs. This way, we obtain more accurate runtime measurments that are necessary for interpreting runtime differences below one minute. For ACAS Xu, the runtime differences are sufficiently large for all but one network, so that we can faithfully compare different counterexample searchers without repeating the experiments.
### Optimal vs. Early Exit Verifier

To evaluate how repair using an early-exit verifier compares to repair using an optimal verifier, we run repair using both verifiers for CollisionDetection, MNIST, ACAS Xu, and the first-stage models of the Integer Dataset RMIs with second-stage size \(304\). Our findings are two-fold:

* When verification is expensive, repair using the early-exit verifier is faster most of the time.
* For smaller networks, the two methods are typically similarly fast.

We observe only minimal variations regarding the performance of the repaired networks. These results are reviewed in Appendix B.

#### Larger Networks

Figure 3 depicts which verifier leads to repair fastest. The figure depicts this both for the absolute runtime of repair and the number of repair steps Algorithm 1 performs.

For the larger MNIST and ACAS Xu networks, we observe that repair using the early-exit verifier requires less runtime in most cases. Regarding the number of repair steps, we observe the opposite trend. Here, the optimal verifier yields repair in fewer repair steps more often than not. The additional runtime cost of computing most-violating counterexamples offsets the advantage in repair steps. In extreme cases, the early-exit verifier enables repair while the optimal verifier leads to a timeout. Due to this, using the early-exit verifier has a success rate of \(100\,\%\) for ACAS Xu, compared to \(82.5\,\%\) when using the optimal verifier (MNIST: \(100\,\%\) to \(96\,\%\)).

The finding that the optimal verifier leads to fewer repair steps aligns well with theoretical intuition. From a theoretical perspective, we expect that most violating counterexamples should better guide Algorithm 1 towards a repaired network. However, the fact that \(20\,\%\) of the cases defy our expectation means that our intuition is limited. This could be due to the counterexample-removal procedure, but neural network repair may also simply yield unintuitive structures.

#### Smaller Networks

For the smaller CollisionDetection and Integer Dataset networks, we primarily observe that, typically, both verifiers yield interchangeable runtime. Only infrequently repair using one verifier outperforms using the other by more than \(30\) seconds. This is apparent from Figure 2(a). While

Figure 3: **Optimal vs. Early-Exit Verifier: Runtime. We plot how frequently repair using the optimal verifier \(\boxplus\) or the early-exit verifier \(\boxplus\) is faster in terms of (a) runtime and (b) repair steps. Gray bars \(\boxplus\) depict how frequently both approaches are equally fast. We consider two runtimes equal when they deviate by at most \(30\) seconds. The figure contains data for four different datasets: CollisionDetection (CD), Integer Datasets (RMI), MNIST and ACAS Xu. Gaps to \(100\,\%\) are due to failing repairs.**
there is no variation regarding the number of repair steps for the Integer Dataset RMIs, Figure 2(b) shows the same trend for CollisionDetection as for ACAS Xu and MNIST.

#### A Note on Failing Repairs

We witness several failing repairs in our experiments. These are either due to timeout or due to failing counterexample-removal. There are no indications of non-termination regarding Algorithm 1 itself in these failing repairs. In other words, we do not observe exceedingly high repair step counts. This holds true both for the optimal verifier, for which termination remains an open question, and the early-exit verifier, for which we disprove termination in Section 4.5.

### Using Falsifiers for Repair

Falsifiers are sound but incomplete counterexample searchers that specialise in finding violations fast. In this section, we study how falsifiers can speed up repair. We find that using the BIM falsifier (Rasmari et al., 2017; Rasmari et al., 2018) can significantly accelerate repair of the MNIST network, demonstrating the potential of falsifiers for repair.

To study the advantages of falsifiers for repair, we repair an MNIST network and the ACAS Xu networks using the SpecAttack (Bimpoul et al., 2018) and BIM (Rasmari et al., 2017; Rasmari et al., 2018) falsifiers. We outline the approach of the BIM falsifier in Section 3.3. We start repair by searching counterexamples using one of the falsifiers. Only when the falsifier fails to produce further counterexamples we turn to the early-exit verifier. Ideally, we would want that the verifier is invoked only once to prove specification satisfaction. Practically, often several additional repair steps have to be performed using the verifier.

For ACAS Xu, we observe that BIM generally fails to find counterexamples. Therefore, we only report using SpecAttack for ACAS Xu. For the small CollisionDetection and Integer Dataset networks, the verifier is already comparably fast, so neither BIM nor SpecAttack can provide a runtime advantage. We also evaluated combining falsifiers with the optimal verifier, but this does not improve upon using the early-exit verifier.

We run SpecAttack using Sequential Least SQuares Programming (SLSQP) as network gradients are available. In spirit of Dong et al. (2019), we run BIM with Adam (Kingmaa et al., 2015) as optimiser. We find that using Adam yields the most powerful falsifier compared to using gradient descent with momentum and RMSprop (Rasmari et al., 2017). BIM performs local optimisation ten times from different random starting points.

Figure 4: **Falsifiers: Runtime. We plot the number of repaired instances that individually require less than a certain runtime. We plot this for repair using BIM, SpecAttack, only the optimal verifier and only the early-exit verifier. Both experiments use a timeout of three hours. Runtimes are given on a logarithmic scale.**
### Bim

The results of our experiments are summarised in Figure 4. For MNIST, we see that using the BIM falsifier can significantly accelerate repair. Repair using BIM is the fastest method in \(70\,\%\) of the repair cases, compared to \(26\,\%\) for only the early-exit verifier, \(2\,\%\) for SpecAttack and \(0\,\%\) for only the optimal verifier. In \(2\,\%\) of the cases, the runtime of the two best variants is within \(30\) seconds.

BIM is an order of magnitude faster than the early-exit verifier, yet it can find counterexamples with a larger violation than the early-exit verifier. Thus, BIM can sometimes provide the repair step advantage of the optimal verifier at a much smaller cost. Again, the breakdown of which method is fastest for each repair case shows that the figure is not as clear as we may wish it to be -- BIM provides a significant runtime advantage in \(70\,\%\) of the cases, but in \(26\,\%\) of the cases using only the early-exit verifier is faster.

### SpecAttack

For the MNIST network, using SpecAttack is inferior to using only the early-exit verifier. In our experiments, SpecAttack provides no significant runtime advantage for generating counterexamples over the early-exit verifier and tends to compute counterexamples with a smaller violation. SpecAttack's runtime scales well with the network size but exponentially in the input dimension. Thus, it is not surprising that it provides no advantage for our MNIST network, which is tiny compared to state-of-the-art image classification networks.

For ACAS Xu, we would expect that SpecAttack outperforms using only the early-exit verifier more clearly than apparent from Figure 4. Here, SpecAttack's runtime is an order of magnitude faster than the runtime of the early-exit verifier. SpecAttack can also provide an advantage in repair steps in many cases. However, at times using SpecAttack also increases the number of repair steps. Additionally, SpecAttack sometimes makes the final invocations of the early-exit verifier more costly than when only the verifier is used.

Our experiments using falsifiers demonstrate that they can give a substantial runtime advantage to repair, but they also show that speeding up repair traces back to more intricate properties beyond just falsifier speed. Understanding these properties better is a promising future research direction for designing better falsifiers for repair.

### Repairing Linear Regression Models

Our theoretical investigation into the repair of linear regression models in Section 4.3 provides us with a termination guarantee for repairing these models. The investigation also provides interesting insights that can be used to create a repair algorithm for linear regression models based on quadratic programming. In this section, we describe this algorithm and compare it to the Ouroboros [57] and SpecRepair [4] repair algorithms.

We repair the second-stage models of ten Integer Dataset RMIs with second-stage size ten. The specifications that we obtain for these models have a similar average size as reported by Tan et al. [57] (\(19\,426\) properties). This indicates that our reimplementation is faithful. Both Ouroboros and SpecRepair are counterexample-guided repair algorithms. Ouroboros performs repair by augmenting the training set with counterexamples and retraining the linear regression models using an analytic solution. SpecRepair uses the \(L_{1}\) penalty function method [44], training the linear regression models using gradient descent. We perform at most two repair steps for SpecRepair. For Ouroboros, we perform up to five repair steps following Tan et al. [57].

### Insights into Repairing Linear Regression Models

We recall from Section 4.3 that for repairing a linear regression model to conform to a linear specification, the most-violating counterexample for a property is always located at the vertices of the property's input set. This implies two conclusions for repairing the second-stage RMI models:
* To verify a linear regression model, it suffices to evaluate it on the vertices of the input set. As the input of the models is one-dimensional, these are just two points per property.
* As we can analytically solve the verification problem \(V\), we can rewrite \(R^{\prime}\) from Equation (8) using two constraints per property. The two constraints correspond to evaluating the satisfaction function for the two vertices of the property input set. We obtain an equivalent formulation of the repair problem \(R\) from Equation (7) with a finite number of constraints.

Repair using Quadratic ProgrammingConclusion b) from the previous paragraph gives us an equivalent formulation of the repair problem with finitely many linear constraints. We train and repair the second-stage models using MSE. Since MSE is a convex quadratic function and all constraints are linear, it follows that the repair problem is a quadratic program [8]. This allows applying a quadratic programming solver to repair the linear regression models directly. We use Gurobi [29] and report the results for this method under the name _Quadratic Programming_.

Due to the above theory, the quadratic programming repair algorithm is exact. That is, we obtain an infeasible problem if and only if the linear regression model can not satisfy the specification and otherwise obtain the optimal repaired regression model. To mitigate floating point issues, we require the satisfaction function to be at least \(10^{-2}\) in Equation (7) instead of requiring it to be just non-negative. That corresponds to applying a satisfaction constant as in SpecRepair.

ResultsThe results of repairing linear classifiers are summarised in Table 4. Our new quadratic programming repair algorithm achieves the highest success rate. As this method is successful if and only if repair is possible, this is not surprising. It is followed by SpecRepair. Ouroboros is the least successful method. This means that SpecRepair's counterexample-removal procedure is stronger than the Ouroboros' counterexample-removal procedure, not only theoretically but also practically. Nonetheless, there remains a significant gap between SpecRepair and Quadratic Programming. Our implementation of the different algorithms does not allow for a fair runtime comparison, but we remark that the runtime of Quadratic Programming is competitive in our experiments.

## 6 Conclusion

We view counterexample-guided repair as a robust optimisation algorithm. This approach provides a framework for studying neural network repair, including related but more restrained as well as more general problems. We are able to prove termination of counterexample-guided repair for simpler machine learning models, such as linear classifiers, assuming linear specifications. On the other hand, we show non-termination of repairing neural networks when the specification has an unbounded input set. As our results show, our methodology of viewing repair as robust optimisation is useful for studying the theoretical properties of counterexample-guided repair. We expect

\begin{table}
\begin{tabular}{l c c}  & \multicolumn{2}{c}{**Success Rate**} \\
**Algorithm** & \(\varepsilon=100\) & \(\varepsilon=150\) \\ \hline Ouroboros [57] & \(30\,\%\) & \(77\,\%\) \\ SpecRepair [4] & \(58\,\%\) & \(94\,\%\) \\ Quadratic Programming & \(72\,\%\) & \(97\,\%\) \\ \end{tabular}
\end{table}
Table 4: **Comparison of Algorithms for Repairing Linear Regression Models.** We report the success rates of repairing RMI second-stage linear regression models for two specifications with different error bounds \(\varepsilon\). The success rates include models that already satisfy their specification.
that our insights will eventually help to answer the question whether counterexample-guided repair of neural networks terminates when applied to specifications with bounded input sets, such as \(L_{\infty}\) adversarial robustness or the ACAS Xu safety specifications.

Empirically, we find that \(-\) despite a disadvantageous theoretical result \(-\) early-exit verifiers allow achieving repair and can give speed advantages. Similarly, falsifiers can significantly accelerate repair, but this is to be traced back to more intricate properties than just being faster than the verifier. Studying these properties more closely is a promising direction for future research, as it may allow for designing improved falsifiers tailored to repair.

Our empirical results on repairing linear regression models shows that robust optimisation is also practically useful for designing stronger repair algorithms. Overall, we believe that robust optimisation provides a rich arsenal of useful tools for studying and advancing repair.
