Property-driven Training: All You (N)Ever Wanted to Know About

Neural networks are known for their ability to detect general patterns in noisy data. This makes them a popular tool for perception components in complex AI systems. Paradoxically, they are also known for being vulnerable to adversarial attacks. In response, various methods such as adversarial training, data-augmentation and Lipschitz robustness training have been proposed as means of improving their robustness. However, as this paper explores, these training methods each optimise for a different definition of robustness. We perform an in-depth comparison of these different definitions, including their relationship, assumptions, interpretability and verifiability after training. We also look at constraint-driven training, a general approach designed to encode arbitrary constraints, and show that not all of these definitions are directly encodable. Finally we perform experiments to compare the applicability and efficacy of the training methods at ensuring the network obeys these different definitions. These results highlight that even the encoding of such a simple piece of knowledge such as robustness in neural network training is fraught with difficult choices and pitfalls.


Introduction
From their inception in the first half of the 20th century, to their rise in computer vision and signal processing applications in the 90s, neural networks have made their way into modern AI applications, mostly as components responsible for perception tasks, e.g. processing signals, images, speech or text.
Unfortunately, neural networks lack properties known as explainability and interpretability: we usually deploy them in domains where the ideal data distribution is unknown or unattainable. Therefore, by definition, they are only approximately correct, only as good as the data is, and do not carry additional semantic meaning beyond a very general type R n → R m . In the absence of a clear specification, it becomes problematic to guarantee the absence of "bugs", or identify components that are responsible for deviations from the intended behaviour. The most famous instance of this problem is proving robustness against adversarial attacks (Szegedy et al. 2014;Goodfellow, Shlens, and Szegedy 2015). Adversarial robustness is a property that even very accurate neural networks fail to satisfy.
As safety and security are critical for some complex AI systems involving neural networks, their verification has be-come a hot topic, with several competing tools and methods on the market: ERAN (Gehr et al. 2018), Marabou (Katz et al. 2019), nnenum (Bak et al. 2020) to name a few. However, verification tools do not entirely solve the problem as they do not directly address the issue of an under-defined specification during training. To put it plainly, there is no reason to run a computationally expensive verifier if the neural network is not robust in the first place.
The proposed solution is to (re)train neural networks towards specified robustness properties. Such training can be seen as a way to impose a formal specification, and so may contribute to explainability as well as verification. This work considers four of the most prominent families of techniques: 1. Data augmentation (Shorten and Khoshgoftaar 2019) 2. Adversarial training (Goodfellow, Shlens, and Szegedy 2015;Madry et al. 2018) 3. Lipschitz robustness training (Anil, Lucas, and Grosse 2019;Pauli et al. 2021) 4. Training with logical constraints (Xu et al. 2018;Fischer et al. 2019) The last, training with logical constraints, is a more general approach that can train for not just robustness, but a wide range of properties expressed in variants of first-order logic.
Contributions In this work, we consider all of these approaches holistically under the prism of knowledge representation. We take classification problems as an example domain, interpreting f : R n → R m as a procedure that separates the n-dimensional data into m classes. We discuss how, although the first three families of methods all seek to represent the same high-level knowledge in the neural network (namely that the true function being modelled by the network is robust to small changes in the input), underneath they optimise for different definitions of robustness. We formally distinguish standard (SR), classification (CR), Lipschitz (LR), and approximate classification (ACR) robustness as key properties that encompass all four groups of methods. This enables the following findings: • From the security perspective, different definitions of robustness ultimately determine the nature of attack, thus giving rise to SR, CR, LR, ACR attacks. Thus, one can train for example with ACR constraint but attack with SR constraint. This raises questions about relative strengths of these different training methods and attacks. • Some property-driven training methods are special cases of others. For example, adversarial training known in the literature can be seen as a form of training with SR constraint, with certain amount of parameter tuning. But some training regimes do not yield generalisations. For example, the effect of data augmentation on training cannot be emulated by training with constraints. • We can order some robustness properties based on their strength, for example, we show that LR implies SR, and ACR implies CR. In this case, training with a stronger property (e.g. LR) will protect better against both kinds of attacks (in this case, both SR and LR attacks). • There are some properties that cannot be ordered by strength (e.g. SR and ACR, LR and ACR), and in this case, optimising training for a given property defends better only against attacks with this same target property. • Training with constraints defends against adversarial attacks better than data augmentation for any choice of robustness definition as a training constraint. • There are additional common criteria that can be used to qualitatively compare different modes of property-driven training, e.g. interpretability, global or local nature. For example. CR is the most interpretable, but not globally desirable, LR is least interpretable, but globally desirable.
These are the first results of this kind. Note that some of the previous work reported on unstable performance of constraint-driven training when it comes to defence against attacks (Ayers et al. 2020), which we do not observe in our experiments. No prior comparison between constraintdriven training and data augmentation existed. Some papers, such as (Fischer et al. 2019), listed and even implemented some kinds of robustness constraints that we study here, but gave no indication of their relative performance. We are not aware of any prior analysis of SR, LR, CR, ACR abstractly as logical properties. We are confident that this general method of initial abstract property analysis followed by subsequent application to training and evaluation of networks will be of broader use beyond just classification algorithms or just robustness properties.
To our knowledge, this is also the first systematic study of property-driven training from a general "knowledge representation" point of view. Although robustness was chosen as the property of interest in this paper, we aim to convincingly illustrate that training using logical constraints generally requires careful formal treatment, as many misconceptions and even errors arise on the boundary between logical constraints (such as the definitions of robustness expressed in first-order logic) and their machine-learning realisations (given by explicit or implicit translation into the language of loss functions and statistical optimisation). At the same time, this paper aims to convince the reader that conceptual clarity in this domain is possible; and thus aims to open new possibilities for a future community project on formally expressing and analysing other properties of machine-learning algorithms. The paper is organised as follows. Section 2 explains how different robustness properties arise from different machine learning approaches to property-driven training. Section 3 abstractly analysises these robustness definitions, establishing their relative strength, interpretability and applicability. Section 4 shows how these robustness properties determine different evaluation metrics and attacks, and provides a comprehensive empirical evaluation of the robustness properties deployed as training constraints and as attacks. Section 5 concludes the paper and outlines future work.

Existing training techniques
We will explain our main ideas by means of an example. Suppose we are given the MNIST data set (LeCun, Cortes, and Burges 2010) which contains 60, 000 images of handwritten digits 28 × 28 pixels each, and a trained neural network f MNIST : R 784 → R 10 , where 784 is the number of pixels in every input image, and 10 is the number of output classes from 0 − 9. We will assume for the sake of the argument, that f MNIST is an arbitrary network trained using the standard settings of the gradient descent algorithm with some standard loss function L : R 784 → R 10 → R, that indicates the magnitude of the network's error given a data point and its intended classification. The most common example is the cross entropy loss function. We assume also that f MNIST has a high accuracy on the training set (say 99%).
For the property that we want to ensure, let us take the -ball robustness widely used in the literature (Singh et al. 2019;Huang et al. 2017;Katz et al. 2019). Intuitively, an image is robust if, when you move no more than away from it in the input space, the output does not change much, or alternatively, the classification decision that the network gives does not change. To verify that the network is robust for the MNIST data set, we check that the network is robust in the vicinity of each of the given 60, 000 images.
Take the example image in Figure 1 which is labelled in the data set as a 7. The network being robust around that image implies that any small perturbation of the image should result in only a small perturbation of the output and hence the perturbation should also classify as 7.
The problem is that for an arbitrary f MNIST , even when the is reasonable, the odds of f MNIST satisfying this con-straint for every image in the data set are extremely low. For example, the network with 99% accuracy used in (Fischer et al. 2019) did not satisfy the -ball constraint around a single image in the data set.
Let us now look at the existing solutions to this problem from the knowledge representation point of view.

Data augmentation
Data augmentation is one of the earliest and simplest methods of improving the robustness of a neural network via training (Shorten and Khoshgoftaar 2019). It is applicable to any transformation of the input (e.g. addition of noise, translation, rotation, scaling) that leaves it semantically unchanged. To make the network robust against such a transformation, one augments the data set with instances sampled via the transformation. For example, to improve the robustness of the network against simple noise, we can sample images from the -ball of the given image of 7, and add them to the data set with the label 7.
Although it may seem that this simple solution has nothing to do with knowledge representation, it imposes significant choices from the point of view of the property specification: c1 the choice of will reflect our assumptions about admissible range of perturbations; c2 the choice of the distance function that measures theproximity will reflect our assumptions on desirable geometric properties of the perturbations; c3 the choice of the sampling method (e.g. random sampling, or based on some attack, generative algorithm or prior knowledge of images) will ultimately determine the properties we optimise for. But, perhaps even more significantly for us, this method determines the exact definition of robustness that we optimise for when we train our neural network f : R n → R m . We call it classification robustness and formally define as follows: given a model inputx, for all inputs x within the -ball distance ofx, ensure that outputs f (x) yield arg max(f (x)) = c, where c is the class ofx as given in the training data. In other words: Definition 1 (Classification robustness) Used as a spec for training, this property does not account for possibility of having "uncertain" images in the data set, for which a small perturbation ideally should change the class. For data sets that contain a significant number of such images, it will lead to significant reduction in accuracy of the trained neural networks; and, as we show later it may even have a detrimental effect on a network's robustness.

Adversarial training
Adversarial training is the current state-of the-art method to robustify a neural network. Whereas standard training tries to minimise loss between the predicted value, f (x), and the true value, y, of each entry (x, y) in the training data set, adversarial training minimises the loss with respect to the the worst-case perturbation of each sample in the training data set. It therefore replaces the standard training objective L(x, y) with: max Algorithmic solutions to the maximisation problem that find the worst-case perturbation has been the subject of several papers. The earliest suggestion was the Fast Gradient Sign Method (FGSM) algorithm introduced by Goodfellow et al. (Goodfellow, Shlens, and Szegedy 2015): FGSM(x) = proj(x + · sign(∇ x L(x, y))) However, modern adversarial training methods usual rely on some variant of the Projected Gradient Descent (PGD) algorithm (Gu and Rigazio 2014) which iterates FGSM some number of times: ) It has been empirically observed that neural networks trained using this family of methods exhibit greater robustness at the expense of an increased generalization error Madry et al. 2018;Zhang et al. 2019), which is frequently referred to as the accuracy-robustness tradeoff for neural networks (although this effect has been observed to disappear as the size of the training dataset grows (Raghunathan et al. 2019)).
In logical terms what is the property that this procedure is trying to train for? Obviously it's unreasonable to expect that adversarial training will ever succeed in driving the loss of all perturbations down to zero. Therefore let us assume that there's some maximum distance, δ, that it is acceptable for the output to be perturbed given the size of perturbations in the input. This leads us to the desired property: Definition 2 (Standard robustness) SR( , δ) ∀x : ||x −x|| ≤ ⇒ ||f (x) − y|| ≤ δ where in this case of adversarial training the distance between the outputs is measured using L(x, y).
We note that, just as with data augmentation, choices c1 -c3 are still there to be made, although the sampling methods are usually given by special-purpose FGSM/PGD heuristics based on computing the loss function gradients.

Training for Lipschitz robustness
More recently, a third competing definition of robustness has been proposed: Lipschitz robustness (Balan, Singh, and Zou 2018). Inspired by the well-established concept of Lipschitz continuity, Lipschitz robustness asserts that the distance between the original output and the perturbed output is at most a constant, L, times the change in the distance between the inputs.
As will be discussed in Section 3, this is a stronger requirement than standard robustness. Techniques for training for Lipschitz robustness include formulating it as a semidefinite programming optimisation problem (Pauli et al. 2021) or including a projection step that restricts the weight matrices to those with suitable Lipschitz constants (Gouk et al. 2021).

Training with logical constraints
Logically, this discussion leads one to ask whether a more general approach to property formulation may exist, and several attempts in the literature addressed this research question (Xu et al. 2018;Fischer et al. 2019), by proposing methods that can translate a first-order logical formula C into a constraint loss function L C . The loss function penalises the network when outputs do not satisfy a given Boolean property, and universal quantification is handled by a choice of sampling method. Our standard loss function L is substituted with: where α and β are weights that control how much a standard and the constraint loss contribute to training. This method looks deceivingly as a generalisation on the previous approaches. However, even given suitable choices for c1 -c3, the robustness definition (1) cannot be modelled via the constraint loss. For (1), it work as argmax is not differentiable. Instead (Fischer et al. 2019) define an alternative property we will call approximate classification robustness: Definition 4 (Approximate classification robustness) which only looks only at the prediction of the true class and checks whether it is greater than some value η (chosen to be 0.52 in their work).

Summary
We have just shown how non-trivial knowledge representation choices and problems arise on the boundary between logical form of the desired properties and their machinelearning realisations as loss functions. In the next section, we give analysis and explanation of the rationale for making a choice between these different kinds of robustness.

Comparison of definitions
In Section 2 we showed that there were a variety of different robustness definitions used by common training techniques. In this section we perform an in-depth comparison of the definitions, a summary of which is shown in Table 1.

Relationships
One of the most important aspects to discuss is the logical relationship between the various definitions, i.e. when the definitions agree and when they disagree.
Standard and Lipschitz robustness The easiest relationship to quantify is the one between standard robustness and Lipschitz robustness. In particular, the latter is a strictly stronger property than the former, in the sense that when a network satisfies LR( , L) then it also satisfies SR( , L). However, the converse does not hold, as standard robustness does not relate the distances between the inputs and the outputs. Consequently, there is no value of L such that if the network is SR( , δ) robust then the network is LR( , L) robust, as for any fixed L one can always make the distance ||x −x|| arbitrarily small in order to violate the Lipschitz inequality.
(Approximate) classification robustness The next relationship we study is between classification robustness and approximate classification robustness. As discussed in Section 2.4, the latter is designed to emulate the former whilst providing a logical loss function with a meaningful gradient. We work under the assumption that the last layer of the classification network is a softmax layer and therefore the output forms a probability distribution. When η > 0.5 then, as would be hoped, any network that satisfies ACR( , η) also satisfies CR( ). For η ≤ 0.5 this relationship breaks down as the true class may be assigned a probability greater than η but may still not be the class with the highest probability. We therefore recommended that one only uses value of η > 0.5 when using approximate classification robustness. For example η = 0.52 in (Fischer et al. 2019).
Given that LR is stronger than SR and ACR is stronger than CR, the obvious question is whether there is a relationship between these two groups? In short, the answer to this question is no. In particular, although the two sets of definitions agree whether a network is robust around images with high-confidence, they disagree over whether a network is robust around images with low confidence. We illustrate this with an example, comparing SR against CR. We note that similar analysis holds for any pairing from the two groups.

Standard vs classification robustness
The key insight is that standard robustness bounds the drop in confidence that a neural network can exhibit after a perturbation, whereas classification robustness does not. Figure 2 shows two hypothetical images from the MNIST dataset. Our network predicts that Figure 2a has an 85% chance of being a 7. Now consider adding a small perturbation to the image and consider two different scenarios. In the first scenario the output of the network for class 7 decreases from 85% to 83% and therefore the classification stays in the same. In the second scenario the the output of the network for class 7 decreases from 85% to 45%, and results in the classification changing from 7 to 9. When considering the two definitions, a small change in the output leads to no change in the classification and a large change in the output leads to a change in classification and so robustness and classification robustness both agree with each other.
However now consider Figure 2b with relatively high uncertainty. In this case our network is (correctly) less sure about the image, only very narrowly deciding that it's a 7. Again consider adding a small perturbation to it. In the first  scenario the prediction of the network changes dramatically with the probability of it being a 7 increasing from 51% to 91% but leaves the classification unchanged as 7. In the second scenario the output of the network only changes very slightly, decreasing from 51% to 49% flipping the classification from 7 to 9. Now, the definitions of robustness and classification robustness disagree. In the first case, adding a small amount of noise has erroneously massively increased the network's confidence and therefore the robustness definition correctly identifies that this is a problem. In contrast classification robustness has no problem with this massive increase in confidence as the classification remains unchanged.
Given this example, it is hopefully clear that although robustness and classification robustness agree on lowuncertainty examples, classification robustness breaks down and starts giving what we argue are both false positives and false negatives when considering examples with highuncertainty.

Data set assumptions
A related question that we have found to be rarely discussed in the literature is what assumptions the different definitions are making about the distribution of the training data with respect to the data manifold of the true distribution of inputs.
For SR and LR it is, at minimum, desirable for the network to be robust over the entire data manifold. In the most domains the shape of the manifold is unknown and therefore it is necessary to approximate it by taking the union of the balls around the inputs in the training dataset. We are not particularly interested about whether the network is robust in regions of the input space that lie off the data manifold, but there is no problem if the network is robust in these regions. Therefore these definitions make no assumptions about the distribution of the training data set. This is in contrast to (A)CR. As discussed in the previous section, rather than requiring that there is only a small change in the output, they require that there is no change to the classification. This is only a desirable property when the region being considered does not contain a decision boundary. Consequently when one is training for some form of classification robustness, one is implicitly making the assumption that the training data points lie away from any decision boundaries within the manifold.
In practice, most datasets for classification problems assign a single label instead of an entire probability distribution to each input point, and so this assumption is usually valid. However, we feel it is important to note that classification robustness is not an appropriate definition to train for if the data set contains input points that may lie close to the decision boundaries.

Interpretability
One of the key selling points of training with logical constraints is that, by ensuring that the network obeys understandable properties, it improves the explainability of the neural network. Each of the robustness constraints encode that "small changes to the input only result in small changes to the output", but the interpretability of each definition also matters.
All of the definitions share the parameter which measures how much of a perturbation of the input is acceptable which is relatively interpretable. Despite its other drawbacks discussed so far, CR is inherently the most interpretable as it has no second parameter. In contrast, SR and ACR require extra parameters, δ and η respectively, which measures the allowable deviation in the output. While these second parameters still have a direct interpretation, their addition make these models less interpretable.
Finally we argue that, although LR is the most desirable property, it is also the least interpretable. Its second parameter L measures the allowable change in the output as a proportion of the allowable change in the input. It therefore requires us to not only have an interpretation of distance for both the input and output spaces, but to be able to relate them. In most domains, this relationship simply doesn't exist. Consider the MNIST dataset, both the commonly used notion of pixel-wise distance used in the input set, although crude, and the distance between the output distributions are both interpretable. However, the relationship between them is not. For example, what does allowing the distance between the output probability distributions being no more than twice the distance between the images actually mean? This therefore reflects the trade-off between complexity of the property and its interpretability.
Another aspect of interpretability that appears in logicalconstraint driven training, is the semantics of the parameters α and β which allow the users to decide how to weight the accuracy of the network vs the importance that it adheres to the constraint. Section 1 describes how the loss function used in logical-constraint training is split into two parts: where the first part is designed to maximise the accuracy of the predictions and the second encodes the constraint. However, in practice the properties (and therefore the derived loss functions) refer to the true label y rather than the current output of the network f (x), e.g.
This leads to scenarios where a network that is robust aroundx but gives the wrong prediction, being penalised by L C which on paper is designed to maximise robustness. Essentially L C is trying to maximise both accuracy and constraint adherence concurrently. Instead, we argue that to preserve the intended semantics of α and β it is important to instead compare against the current output of the network e.g. ∀x Of course, this doesn't work for ACR because in order to derive the most popular class from the output f (x) you need arg max, the very function ACR seeks to avoid using. This is yet another argument why using (A)CR should be avoided where possible.

Distance functions and sampling
The one aspect that all the definitions of robustness have in common is the universal quantification over the set of perturbations that are "near" to the points in the dataset. Complete procedures that guarantee to find a perturbation that violates the robustness property if such a point exists, are too expensive to run during training. Consequently all the training algorithms we consider, translate this quantifier into a sampling problem over the domain. Given this commonality, one might assume that the sampling algorithms used would be similarly homogeneous across the different training methods. However, somewhat surprisingly, this does not appear to be the case. Adversarial training algorithms in the literature typically use sophisticated gradient-based methods like PGD. In contrast, the approach to sampling in data augmentation is much more varied. Some data augmentation practices do use guided attacks such as PGD after having partially trained the network on the original dataset, but they also frequently use much less guided sampling procedures which instead seek to generate samples that are representative of the targeted perturbation space rather than actively seek adversarial examples. Common such sampling procedures include adding uniform random noise and or transforming the images via rotations/scaling/translations/palette swaps. This leads us to hypothesise that there is significant potential of crosspollination between the different training techniques.
The space in which the sampling procedure operates is inherently determined by the choice of distance function. Although L p norms are commonly used for simplicity, it is common knowledge that they are not a good proxy for semantic similarity, so restricting the sampling domain according to such a norm can introduce undesirable invariances in the neural network. It is an active field of work coming up with sample spaces such that contain more realistic sets of perturbations.
However, another important consideration when choosing a distance function is verifiability, which often discourages the use of explicitly semantic-based distance functions. In general, the more complex the notion of distance, the more difficult it is to formally verify the conditions. At one end of the spectrum the L 1 or L ∞ norms can be verified by complete verifiers such as Marabou (Katz et al. 2019). Switching to the slightly more natural L 2 norm, or Euclidean distance, means that complete verification procedures are in general unable to verify the property, and instead one is forced to rely on incomplete verifiers such as ERAN (Gehr et al. 2018). At the far end of the spectrum, very few tools are capable of verifying robustness against even comparatively simple geometric transformations such as rotations, although some recent progress has been made (Singh et al. 2019).

Experiments
In this section we describe the results of some experiments designed to validate the conclusions from our previous sections and to compare the relative effectiveness of training with logical constraints against the other training techniques. However, before describing the experiment set up, we explain different choices for measuring success of propertydriven training. This is in line with our bigger purpose of setting up a comprehensive framework for different propertydriven approaches.

Evaluation metrics
Given a particular definition of robustness, a natural question is how to quantify how close a given network is to satisfying it? We have found the terminology in the literature both confusing and inconsistent, and therefore the following discussion is an attempt to clarify matters. We note that although we are only evaluating robustness properties, the definitions below easily generalise to any property that universally quantify over some set of inputs.
We argue that there are three different measures that one should be interested in: 1. Does the property hold? This is a binary measure and the answer is either true or false.
2. If the property doesn't hold, how easy is it for an attacker to find a violation?
3. If the property doesn't hold, how often does the average user encounter a violation?
Based off of these measures, we now define three concrete metrics: constraint satisfaction, constraint security, constraint accuracy. Let X be the training dataset, and B(x, ) {x ∈ R n | ||x −x|| ≤ } Figure 3: Experiments that show how the two networks trained with LR and SR constraints, respectively (with = 0.1, δ = 10, L = 10 and L ∞ distance) perform when evaluated against different definitions of robustness underlying the attack.
and P be the right hand side of the implication in each of the definitions of robustness. The I φ be the indicator function which is defined as follows: The constraint satisfaction metric measures the proportion of the training dataset for which the property holds.
Definition 5 (Constraint satisfaction) Unfortunately, depending on the network architecture and the property in question, the indicator function may not always be feasible to evaluate. In contrast, constraint security measures the proportion of inputs in the training dataset such that an attack A is unable to find an adversarial example for property P . Definition 6 (Constraint security) In our experiments we use the PGD attack for A, although in general any strong attack can be used. Finally constraint accuracy estimates the probability of a random user coming across a counter-example to the property. Let S(x, n) be a set of n elements randomly uniformly sampled from B(x, ). Then constraint accuracy follows: Definition 7 (Constraint accuracy) Note that there is no relationship between constraint accuracy and constraint security: an attacker may succeed in finding an adversarial example where random sampling fails and vice-versa. Our naming scheme differs from (Fischer et al. 2019) who use the term constraint accuracy (without explicitly defining it in the paper) to refer to what we term constraint security. We do not propose changing the name lightly, but the term constraint accuracy caused us significant confusion, and we hope that the reader will agree that the name constraint security is more appropriate given the use of an adversarial attack.
Note the role of sampling in this discussion and compare it to the discussion of the choice c3 in Section 2.1. Firstly, sampling procedures affect both training and evaluation of networks. But at the same time, their choice is orthogonal to choosing the verification property for which we optimise or evaluate. For example, we measure constraint security with respect to the PGD attack, and this determines the way we sample; but having made that choice still leaves us to decide which constraint, ACR, SR, LR, or other we will be measuring as we sample.
Choosing an evaluation metric. It is important to note that for all three metrics, one still has to make a choice for property P , namely SR, ACR or LR, as defined in Section 2. As constraint security always uses PGD to find input perturbations, the choice of SR, ACR and LR effectively amounts to us making a judgement what consists of an perturbation adversarial: is it a class change as defined by ACR, or is it a violation of the more nuanced metrics defined by SR and LR? Therefore, for constraint security, we will be talking about SR/ACR/LR attacks in the remainder of the section. This will be further analysed in the experiment E1 below.
For large search spaces in n dimensions, random sampling deployed in constraint accuracy fails to find the trickier adversarial examples, and usually has deceivingly high performance: we found 100% and > 98% constraint accuracy for SR and ACR, respectively. We will therefore not discuss these experiments in detail, but refer the reader to the project's GitHub page (Casadio et al. 2021).
Constraint satisfaction is different from constraint security and accuracy, in that it must evaluate properties over infinite domains rather than merely sampling from them. Verifiers such as Marabou or ERAN are built with this purpose in mind. It is out of scope for this paper to conduct experiments by this measure, and so we leave it for future work. Our preliminary experiments with Marabou confirm the generally accepted assumption that it is very hard for training tech-niques to achieve a high-score for constraint satisfaction.

Experimental setup
Data sets. We use the two benchmark datasets: 1. The FASHION MNIST (or just FASHION) dataset (Xiao, Rasul, and Vollgraf 2017) consists of 28 × 28 greyscale images of clothing items; 60,000 for training and 10,000 for testing. It has 10 classes: T-shirt/top, Trouser, Pullover, Dress, Coat, Sandal, Shirt, Sneaker, Bag, Ankle boot. 2. The GTSRB dataset (Stallkamp et al. 2011) contains 50, 000 images of German traffic signs. There are 40 classes and image sizes vary between 15×15 to 250×250 pixels. We use a modified version here that contains 12, 660 training images and 4, 170 test images. These images are all centre-cropped, greyscaled, 48 × 48 pixel and belong to 10 classes. Each dataset represents a vision classification problem where the goal is to identify which class a given image belongs to.
Networks. For our baseline architecture, we use two fully connected layers: the first layer uses the ReLU activation function, and the second uses the clamp function to restrict each output to the range [−100, 100]. We use a clamp function instead of the traditional softmax function because the former is compatible with the property verification tools such as Marabou whereas the latter is not. The predicted classification is then taken as the output with the maximum score. For instance, f MNIST = F 0 • F 1 , where F 1 : R 784 → R 100 and F 0 : R 100 → R 10 , α 0 = ReLU and α 1 (x) = clamp(x, −100, 100).
Loss functions. Since our experiments look at classification problems, we will use the cross-entropy loss function as our baseline loss function: For the L C component of the loss function L * , we use the constraint-to-loss function translation of (Fischer et al. 2019). In all experiments, we use the Adam optimiser (Kingma and Ba 2015) with the following learning parameters: η = 0.0001, 100 epochs, a batch size of 128.
Settings. By taking the given architecture, we vary only the loss functions. Thus our Baseline network is trained just with cross-entropy. Data Augmentation adds 2 additional images in the 0.1--ball of each image, and it samples either randomly (RU) or using an FGSM attack. Adversarial training refers to the standard PGD attack, or alternatively a L * function where β = 0, and α = 1, with PGD sampling. In all other cases, we use a constraint loss function L C defined as in (Fischer et al. 2019), and we use the constraints SR, ACR, LR as defined in Section 2 with α = 1 and β = 0.2. Because the loss function translation given in (Fischer et al. 2019) is not uniquely defined in its base case, for the sake of further control experiment, we define the constraint adversarial robustness (AR) which uses cross entropy for L C . All networks trained with L * use sampling by the PGD attack, for efficiency (as well as comparability).

Results
We start with noting the standard test set accuracy of the resulting neural networks in Table 2, making sure that our different training regimes do not deteriorate networks' general performance too drastically. Most notable accuracy drop is noticed for adversarial training. We now highlight groups of experiments that confirm or extend our main theoretical conclusions; the complete experiment description is available in (Casadio et al. 2021).
Experiment set E1. Comparable properties. In Section 3, we established that LR as a property is stronger than SR, and both are not strictly comparable to ACR. This would suggest that, if we train two neural networks, one with the SR, and the other with the LR constraint, then the latter should always have higher constraint security against both SR and LR attacks than the former. This is indeed confirmed by the experiment shown in Figure 3. We also discussed that depending on the properties of the data set, SR may not guarantee ACR, and Figure 3 shows exactly that case. It also confirms that generally, stronger properties are harder to obtain: whether a network is trained with SR or LR constraint, it is less robust for LR attack than any other attack.
Experiment set E2. Incomparable properties. The results in Figure 4 tell us that using the ACR constraint for training does not help to increase defences against SR attacks. A similar picture, but in reverse, can be seen when we optimise for SR but attack with ACR, see (Casadio et al. 2021).
Experiment set E3. Constraint training versus other modes of property-driven training. Next, we confirm our assumptions about relative inefficiency of using data augmentation compared to adversarial training or training with constraints, see Figure 5. We show this only for SR attack, but graphs for SL and ACR attacks show the same trends, see (Casadio et al. 2021). Surprisingly, neural networks trained with data augmentation give worse results than even the baseline network. The fact that Constraint Loss (SR) generally performs better than Constraint Loss (AR) shows that the custom-made loss function of (Fischer et al. 2019) has comparable performance to cross entropy. It is also encouraging to see that Constraint Loss (SR) is almost as good as standard adversarial training while the latter also gives 11 percentage point drop in terms of the networks accuracy (Table 2).  Experiment set E4. Role of other parameters. As already discussed, random uniform sampling struggles to find adversarial inputs in large searching spaces. It is logical to expect that using random uniform sampling when training will be less successful than training with sampling that uses FGSM or PGD as heuristics. Indeed, Figure 5 shows this effect for data augmentation, but similar trends are expected for any form of training.
Finally, one may ask whether the trends just described would be replicated for more complex architectures of neural networks. In particular, data augmentation is known to require larger networks. By replicating the results of Figure 5 with a large 18 layer convolutional network of (Fischer et al. 2019) indeed confirms that larger networks handle data augmentation better, and data augmentation improves robustness compared to the baseline. Nevertheless, data augmentation still lags behind all other modes of property driven training, and thus this major trend remains stable across network architectures, see (Casadio et al. 2021).

Conclusions, Related and Future Work
We have presented a comprehensive study of propertydriven training from the knowledge representation point of view. Taking robustness as a representative property, we ab-stractly studied different forms of robustness; and showed how the existing literature on property-driven training can be understood through this prism. Moreover, we proposed a method that separates out the logical study of properties from their implementation as loss functions for training on the one hand, and their use as evaluation methods and attacks on the other. We showed that this method allows to make general conclusions about relations of different modes of property-driven training that were not possible before.
For translation of constraints into loss functions, we used the implementation from (Fischer et al. 2019); thus our results are compatible and comparable with that prior study. In particular we have identified that the method of (Fischer et al. 2019) is not a strict generalisation of the other techniques and that significant trade-offs and decisions have to be made in order to represent some of the robustness definitions.
The main line of our future work is to extend our methods and conclusions to verification (or constraint satisfaction) frameworks such as Marabou (Katz et al. 2019) or DeepPoly (Singh et al. 2019); and obtain more flexible and general programming interaces for continuous verification (Komendantskaya, Kokke, and Kienitz 2020) that incorporates neural network verification and training.