Property-Driven Training

Note

This section contains a lot of theory. For implementation details, please skip to Logical Loss Functions In Vehicle.

Motivation

We will begin this chapter with a question: how can we train a neural network to be more robust within a desirable ? The long tradition of robustifying neural networks in machine learning has a few methods ready. For example, we can re-train the networks with new data that was augmented using images within the desired -balls, or generate adversarial examples (sample images closest to the boundary of the -ball) during training. Let us breifly explore these approaches.

Current Approaches

Data Augmentation works by generating additional data within the -balls of the original training data points, usually done using methods such as rotation, cropping, flipping, random sampling, etc. The augmented data points are assigned the same label as the original ones they were augmented from. We can then use our usual training methods with this augmented dataset with the hope that it will improve the network’s average-case robustness (Shorten & Khoshgoftaar, 2019) Shorten, C., & Khoshgoftaar, T. M. (2019). A survey on image data augmentation for deep learning. J. Big Data, 6(60). .

Unfortunately, this approach has its problems. Firstly, if our original sampled data point is already very close to the decision boundary, there is a chance that an augmented data point will actually lie on the wrong side, even though it is still within the -ball. This means it will have been assigned the wrong label:

In the case where two data points’ -balls overlap, there is a chance we generate two new data points with the same position in the input space. Furthermore, if the two original data points lie both close to (and on opposite sides of) the decision boundary, the augmented data points may have different labels, despite occupying the same location in the input space:

These inconsistencies mean this approach is generally unviable for network robustification.

Adversarial Training also involves generating new data to train the network, but unlike data augmentation where perturbations are sampled randomly, adversarial training aims to find the worst-case perturbation within -distance to a data point from the training dataset. Whilst data augmentation can be done using worst-case examples, it is still subtely different to adversarial training. Most notably, adversarial training is a process integrated into the network’s training loop, so perturbations are regenerated at every iteration. This means the worst-case examples will always be worst case, which is not true for data augmentation, as after a certain number of iterations the network will have learnt to account for these examples. The goal of adversarial training is to improve the network’s worst-case robustness; it is a form of prophylaxis against adversarial attacks.

The main limitation of adversarial training turns out to be the logical property it optimises for. Recall that we may encode an arbitrary property in Vehicle. However, as was discovered in (Casadio et al., 2022) Casadio, M., Komendantskaya, E., Daggitt, M. L., Kokke, W., Katz, G., Amir, G., & Refaeli, I. (2022). Neural Network Robustness as a Verification Property: A Principled Case Study. In S. Shoham & Y. Vizel (Eds.), Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I (Vol. 13371, pp. 219–231). Springer. https://doi.org/10.1007/978-3-031-13185-1\_11 , projected gradient descent can only optimise for one concrete property. Recall the property of -ball robustness was defined as: . It turns out that adversarial training determines the definition of to be .

Beyond -Balls

In the previous chapter, we learnt how to prove properties of neural networks, with a specific focus on -ball robustness. It is of course nice that we can prove this property is true for a given neural network, but as we have seen above, it is not novel to be able to train for it; this can be done with relative ease simply by using adversarial training.

However, something that adversarial training cannot do is teach a network to abide by any arbitrary logical property. This is where Vehicle comes in: we can define arbitrary properties in our specifications, and use Vehicle’s built-in functionality to compile these into a loss function to train a neural network. We can escape the world of -balls and train our networks to satisfy any property we may desire. Nonetheless, -ball robustness is a useful and intuitive property to understand, and we will continue to use it for our running example throughout the rest of this section, as well as in the exercises at the end.

Before we explore exactly how we train a network on logical properties in practice, those uninitiated into the cults of machine learning and logic may appreciate some theoretical background of how this is possible. This we cover in the following few sections.

Loss Functions

Humans learn by making mistakes. The same is true of neural networks. Loss functions are a way of measuring the “magnitude” of a mistake made by a neural network. For a given training input, loss functions compute a penalty proportional to the difference between the output of the network and the true output (i.e., the training label). Formally, this is written as follows:

The function represents the network, whose optimisation parameters are , and and represent the sizes of the input and output tensors respectively.

One of the simplest (yet usable) loss functions is called mean squared error, defined as:

where is the total number of data points, is the label for data point , and is the model’s predicted value for . I.e., we find the difference between the prediction and the actual value, square it, and take the average across the training dataset.

Models learn by iteratively tweaking their optimsation parameters with the goal of minimising the ouptut of the loss function. The most common way to do this is using gradient descent. Formally, we wish to find the set of parameters that yeilds the least loss:

Here we can explain further the mechanism that drives adversarial training. We can use a variant of gradient descent, called projected gradient descent, to maximise loss in order to find worst-case perturbations. We ensure that the perturbation still lies within the -ball of the original data point by projecting those perturbations that escape the -ball back inside. Our new training objective becomes:

In other words, we want to find the perturbation that is within -distance of the data point that produces the largest loss (the worst-case perturbation). Then, we aim to find the optimsation parameters which minimises this loss value.

Logical Loss Functions

Traditional loss functions aim to minimise task loss. However, a neural network’s performance on a given task is not necessarily correlated with the likelihood that it satisfies logical properties such as robustness. Let us recall our initial question: how can we train a neural network to be more robust within a desirable ? Given what we now know about adversarial training and loss functions, we can reframe this question: how can we train a network to abide by any arbitrary logical property?

Gradient descent algorithms train networks to fit data. The big idea behind logical loss functions is to use that same algorithm to train the network to also obey the specification. Standard logic is insufficient for this task since we need a differentiable signal to find the gradient. Hence, we need a type of logic that we can differentiate.

Differentiable Logics

Traditional logics are difficult to translate to loss functions for neural networks because they consist only of boolean values and operations, which are undifferentiable. If we want to use gradient-based techniques for logical properties, we need a logical calculus which uses connectives that are both mathematically rigorous in terms of semantics and differentiable.

Differentiable logics (DLs) convert booleans and operations over booleans into equivalent numerical operations that are differentiable. We have numerous DLs at our disposal (including DL2 (Fischer et al., 2019) Fischer, M., Balunovic, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., & Vechev, M. T. (2019). DL2: Training and Querying Neural Networks with Logic. In K. Chaudhuri & R. Salakhutdinov (Eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA (Vol. 97, pp. 1931–1941). PMLR. http://proceedings.mlr.press/v97/fischer19a.html , DFLs (van Krieken et al., 2022) van Krieken, E., Acar, E., & van Harmelen, F. (2022). Analyzing Differentiable Fuzzy Logic Operators. Artif. Intell., 302, 103602. https://doi.org/10.1016/j.artint.2021.103602 , and more), and Vehicle implements a variety of these. One such logic that has shown particular promise is quantitative linear logic (QLL), or Capucci Logic (Capucci et al., 2026) Capucci, M., Atkey, R., Grellois, C., & Komendantskaya, E. (2026). Quantitative Linear Logic. https://arxiv.org/abs/2605.13348 . QLL defines the logical connectives with the following real-valued functions:

Negation:

Conjunction:

Disjunction:

Implication:

where , representing the hardness degree. As , the QLL connectives converge on their traditional definitions. This is one approach that conserves logical semantics whilst allowing us to use gradient-based methods for property-driven training.

Logical Loss Functions in Vehicle

Vehicle supports several different differentiable logics from the literature, though we will not explore them here. Instead, we will use a simple example to explain how logical loss functions can be generated using Vehicle with Pytorch. Here, we use the MNIST Fashion dataset to train a neural network. All files used in this example can be found in the supporting materials.

First, we will load our Vehicle specification and define our constraint loss function:

import vehicle_lang as vcl
from vehicle_lang.loss import pytorch as loss_pt

spec = loss_pt.load_specification(
    "mnist-robustness.vcl",
    logic=vcl.VehicleDifferentiableLogic(),
)

constraint_loss_fn = spec["robust"]

import vehicle_lang as vcl
from vehicle_lang.loss import tensorflow as loss_tf

spec = loss_tf.load_specification(
    "mnist-robustness.vcl",
    logic=vcl.VehicleDifferentiableLogic(),
)

constraint_loss_fn = spec["robust"]

The first parameter to the load_specification function is the path to the Vehicle specification. The second parameter defines which logic to use – this is optional, and defaults to DL2. We define which property from the specification to use as our constraint loss function by accessing it by name on the specification object.

Next, we will define a simple model and training procedure:

import torch
import torch.nn as nn
import torchvision
import torchvision.transforms as transforms
from torch.utils.data import DataLoader

model = nn.Sequential(
    nn.Flatten(),
    nn.Linear(784, 64),
    nn.ReLU(),
    nn.Linear(64, 32),
    nn.ReLU(),
    nn.Linear(32, 10)
)

def network(x: torch.Tensor) -> torch.Tensor:
    return model(x.reshape(1, 1, 28, 28)).reshape(10)

optimizer = torch.optim.Adam(model.parameters(), lr=1e-3)
cross_entropy = nn.functional.cross_entropy()

num_epochs = 5
alpha = 0.5

for epoch in range(num_epochs):
    for step, (images, labels) in enumerate(train_loader):
        optimizer.zero_grad()
        logits = model(images)
        loss = cross_entropy(logits, labels)

        constraint_loss = constraint_loss_fn(
            n=BATCH_SIZE,
            classifier=network,
            epsilon=torch.tensor(0.005),
            trainingImages=images.squeeze(1),
            trainingLabels=labels
        )

        constraint_loss = torch.stack(constraint_loss).mean()
        total_loss = alpha * loss + (1 - alpha) * constraint_loss

        total_loss.backward()
        optimizer.step()

import tensorflow as tf
from tensorflow.keras import layers, Sequential

model = Sequential([
    layers.InputLayer(shape=(1, 28, 28)),
    layers.Flatten(),
    layers.Dense(64, activation="relu"),
    layers.Dense(32, activation="relu"),
    layers.Dense(10)
])

def network(x: tf.Tensor) -> tf.Tensor:
    return tf.reshape(model(tf.reshape(x, (1, 1, 28, 28))), (10,))

optimizer = tf.keras.optimizers.Adam(learning_rate=1e-3)
cross_entropy = tf.keras.losses.SparseCategoricalCrossentropy(from_logits=True)

num_epochs = 5
alpha = 0.5

for epoch in range(num_epochs):
    for step, (images, labels) in enumerate(train_loader):
        with tf.GradientTape() as tape:
            logits = model(images)
            task_loss = cross_entropy(labels, logits)

            constraint_loss = constraint_loss_fn(
                n=BATCH_SIZE,
                classifier=network,
                epsilon=tf.constant(0.005),
                trainingImages=tf.squeeze(images, axis=-1),
                trainingLabels=labels
            )

            constraint_loss = tf.reduce_mean(tf.stack(constraint_loss))
            total_loss = alpha * task_loss + (1 - alpha) * constraint_loss

        grads = tape.gradient(total_loss, model.trainable_variables)
        optimizer.apply_gradients(zip(grads, model.trainable_variables))

Note that the network callable must match the type of the network declared in the Vehicle specification. The alpha parameter can be used to tweak the weighting of task loss vs. constraint loss, which are blended together in total_loss. We can now export this trained model to verify it using vehicle, with the hope that it is more robust as a result of training with constraint loss. Model exportation can be done like so:

import torch.onnx

model.eval()
input_tensor = torch.randn(1,1,28,28)

torch.onnx.export(
    model,
    input_tensor,
    "classifier.onnx", # file name
    external_data=False, # required for Marabou verification
)

model.export("classifier")

python -m tf2onnx.convert \
    --saved-model classifier \
    --output classifier.onnx

Exercises

Exercise #1 (⭑): Run the Chapter code

Download the required materials (or produce them yourself) and repeat the steps described in this chapter. All code used in this chapter is available from the tutorial repository.

Exercise #2 (⭑): Verifying and comparing networks

Use a vehicle specification (either the one provided, or your own) to verify a property (e.g., robustness) of a network trained with a logical loss function, and compare this to one trained without a logical loss function. Which is more robust, Which is has a better task accuracy, and why?

Exercise #3 (⭑⭑): Further experimentation

Try various combinations of task loss functions, constraint loss functions, and alpha values. How do these affect each other? Is there a combination that makes the network more robust? Is there a combination that makes the network more accurate? What happens when you use multiple constraint loss functions simultaneously?

Exercise #4 (⭑⭑⭑) Training a model from scratch

Finally, try creating your own model from scratch and repeat the experiments and comparisons described above. Explore the relationship between how complex a model is and to what degree it can satisfy robustness, and the effect robustness training can have on this.

Hint: a simple model is worse at spotting the difference between two different images. Does this make it more or less likely to be robust?