From 8bf351817fa1e8257c926e6ee798e587ee3342b6 Mon Sep 17 00:00:00 2001 From: Gusts Gustavs Grinbergs Date: Wed, 17 Dec 2025 16:17:49 +0100 Subject: [PATCH 1/3] updated python stuff --- src/chapters/4-property-driven-training.md | 116 +++++++++++++++------ 1 file changed, 83 insertions(+), 33 deletions(-) diff --git a/src/chapters/4-property-driven-training.md b/src/chapters/4-property-driven-training.md index b9ee642..d77ac86 100644 --- a/src/chapters/4-property-driven-training.md +++ b/src/chapters/4-property-driven-training.md @@ -229,48 +229,98 @@ The definition of the optimisation problem above instantiates by taking: \mathcal{L}_{\mathcal{S}(\mathbf{x})} = \mathcal{I} ( || f(\mathbf{x}) - f(\hat{\mathbf{x}})|| \leq \delta) $$ -# Coding Example: generating a logical loss functions for mnist-robustness in Vehicle +# Coding Example: generating a logical loss function in Python -To generate a logical loss function usable in Python, we will use Vehicle's Python bindings that come pre-installed. +The Python bindings now ship backend-specific helpers in `vehicle_lang.loss.tensorflow` +and `vehicle_lang.loss.pytorch`. They both expose a single entry point +`load_specification(path, *, logic=..., samplers=..., declarations=..., declaration_context=...)` +which compiles your `.vcl` file to a dictionary of callable Python loss functions. -We open a new Python file and write: +- `logic` defaults to `DifferentiableLogic.DL2`, but you can also request `DifferentiableLogic.Vehicle`. +- `samplers` lets you override the search strategy for Vehicle `search` expressions. + If omitted, a default FGSM-based sampler is used (see `DefaultTensorFlowSampler` and + `DefaultPyTorchSampler`). +- The returned dictionary keys are the names of `@property` declarations in your spec. + +Below is a minimal PyTorch example that mirrors the tests in `vehicle-python/tests`: ```python -from vehicle_lang.compile import Target, to_python +import torch +from vehicle_lang.typing import DifferentiableLogic +from vehicle_lang.loss.pytorch import load_specification + +# Compile the Vehicle spec to PyTorch loss functions +spec = load_specification( + "test_trainable.vcl", # any Vehicle spec path + logic=DifferentiableLogic.Vehicle, +) -spec = to_python( - "mnist-robustness.vcl", - target=Target.LOSS_DL2, - samplers={"pertubation": sampler_for_pertubation}, +constraint_loss = spec["output_bounded"] # name of a @property in the spec +model = torch.nn.Sequential( + torch.nn.Linear(1, 8), torch.nn.ReLU(), torch.nn.Linear(8, 1) ) +optimizer = torch.optim.Adam(model.parameters(), lr=1e-2) -robust_loss_fn = spec["robust"] -``` +def network(x): + return model(x.reshape(1, 1)).reshape(1) + +for step in range(50): + optimizer.zero_grad() -which generates the loss function representing the logical loss function for the property `robust`. + # Task loss (e.g., MSE to a target function) + task_loss = torch.tensor(0.0) + for x_val, y_val in [(0.0, 0.0), (0.5, 1.0), (1.0, 2.0)]: + pred = network(torch.tensor(x_val, dtype=torch.float32))[0] + task_loss = task_loss + (pred - y_val) ** 2 + task_loss = task_loss / 3 -This can then be used in a standard training loop: + # Constraint loss produced by Vehicle; signature matches the Vehicle property + constraint_loss_value = constraint_loss(network) + + loss = 0.5 * task_loss + 0.5 * constraint_loss_value + loss.backward() + optimizer.step() +``` + +Switching to TensorFlow changes only the backend import and model definition; the +property call still follows the spec's argument list (typically a single +`network` callable for many specs): ```python -model = tf.Sequential([tf.Input(shape=(28,28)), tf.Dense(units=28), tf.Output(units=10)]) - -for epoch in range(num_epochs): - for x_batch_train, y_batch_train in train_dataset: - with tf.GradientTape() as tape: - # Calculate standard cross entropy loss - outputs = model(x_batch_train, training=True) - ce_loss_value = ce_batch_loss(y_batch_train, outputs) - - # Calculate the robustness loss - robust_loss_value = robust_loss_fn( - n=len(x_batch_train), - classifier=model, - epsilon=0.001, - trainingImages=x_batch_train, - trainingLabels=y_batch_train, - ) - weighted_loss = 0.5 * ce_loss_value + 0.5 * robust_loss_value - - grads = tape.gradient(weighted_loss, model.trainable_weights) - optimizer.apply_gradients(zip(grads, model.trainable_weights)) +import tensorflow as tf +from vehicle_lang.typing import DifferentiableLogic +from vehicle_lang.loss.tensorflow import load_specification + +spec = load_specification("test_trainable.vcl", logic=DifferentiableLogic.Vehicle) +constraint_loss = spec["output_bounded"] + +model = tf.keras.Sequential([ + tf.keras.layers.Input(shape=(1,)), + tf.keras.layers.Dense(8, activation="relu"), + tf.keras.layers.Dense(1), +]) + +def network(x): + return tf.reshape(model(tf.reshape(x, [1, 1])), [1]) + +optimizer = tf.keras.optimizers.Adam(learning_rate=1e-2) + +for step in range(50): + with tf.GradientTape() as tape: + task_loss = tf.constant(0.0) + for x_val, y_val in [(0.0, 0.0), (0.5, 1.0), (1.0, 2.0)]: + pred = network(tf.constant(x_val, dtype=tf.float32))[0] + task_loss = task_loss + (pred - y_val) ** 2 + task_loss = task_loss / 3 + + constraint_loss_value = constraint_loss(network) + loss = 0.5 * task_loss + 0.5 * constraint_loss_value + + grads = tape.gradient(loss, model.trainable_variables) + optimizer.apply_gradients(zip(grads, model.trainable_variables)) ``` + +To customise how Vehicle searches adversarial points, pass your own sampler to `samplers`. +Each sampler receives `(dims, lower_bound, upper_bound, search_lambda, minimise)` and must +return a stackable tensor of loss values; see `DefaultPyTorchSampler` / `DefaultTensorFlowSampler` +in the source tree for a reference implementation. From cd752b5ffd1b7a9a9618ca0e0efe3be3a46cc2eb Mon Sep 17 00:00:00 2001 From: Gusts Gustavs Grinbergs Date: Sun, 21 Dec 2025 19:39:31 +0100 Subject: [PATCH 2/3] implement suggestions --- src/chapters/1-introduction.md | 4 +- src/chapters/4-property-driven-training.md | 52 +++++++++------------- 2 files changed, 23 insertions(+), 33 deletions(-) diff --git a/src/chapters/1-introduction.md b/src/chapters/1-introduction.md index 306eddc..cc676ca 100644 --- a/src/chapters/1-introduction.md +++ b/src/chapters/1-introduction.md @@ -57,7 +57,7 @@ This tutorial will focus on problems 3 to 5, and will present Vehicle, a tool th Vehicle programs can be compiled to an unusually broad set of backends, including: -a) loss functions for Tensorflow which can be used to guide +a) loss functions for PyTorch and Tensorflow which can be used to guide both specification-directed training and gradient-based counter-example search. @@ -91,7 +91,7 @@ Quick installation instructions: 2. Install Marabou: just run `pip install maraboupy` -- Python (Tensorflow) and Agda installation will only be needed to follow Chapters 4 and 5. +- Python (PyTorch) and Agda installation will only be needed to follow Chapters 4 and 5. We suggest that you start this tutorial with just Vehicle and Marabou as tools. diff --git a/src/chapters/4-property-driven-training.md b/src/chapters/4-property-driven-training.md index d77ac86..f4ea757 100644 --- a/src/chapters/4-property-driven-training.md +++ b/src/chapters/4-property-driven-training.md @@ -231,16 +231,11 @@ The definition of the optimisation problem above instantiates by taking: # Coding Example: generating a logical loss function in Python -The Python bindings now ship backend-specific helpers in `vehicle_lang.loss.tensorflow` +The Python bindings ship backend-specific helpers in `vehicle_lang.loss.tensorflow` and `vehicle_lang.loss.pytorch`. They both expose a single entry point -`load_specification(path, *, logic=..., samplers=..., declarations=..., declaration_context=...)` -which compiles your `.vcl` file to a dictionary of callable Python loss functions. - -- `logic` defaults to `DifferentiableLogic.DL2`, but you can also request `DifferentiableLogic.Vehicle`. -- `samplers` lets you override the search strategy for Vehicle `search` expressions. - If omitted, a default FGSM-based sampler is used (see `DefaultTensorFlowSampler` and - `DefaultPyTorchSampler`). -- The returned dictionary keys are the names of `@property` declarations in your spec. +`load_specification(path, ...)` which compiles your `.vcl` file to a dictionary of +callable Python loss functions. The returned dictionary keys are the names of +`@property` declarations in your spec. Below is a minimal PyTorch example that mirrors the tests in `vehicle-python/tests`: @@ -256,26 +251,24 @@ spec = load_specification( ) constraint_loss = spec["output_bounded"] # name of a @property in the spec + +train_x = torch.tensor([0.0, 0.5, 1.0], dtype=torch.float32).unsqueeze(1) +train_y = torch.tensor([0.0, 1.0, 2.0], dtype=torch.float32) + model = torch.nn.Sequential( torch.nn.Linear(1, 8), torch.nn.ReLU(), torch.nn.Linear(8, 1) ) optimizer = torch.optim.Adam(model.parameters(), lr=1e-2) -def network(x): - return model(x.reshape(1, 1)).reshape(1) - for step in range(50): optimizer.zero_grad() # Task loss (e.g., MSE to a target function) - task_loss = torch.tensor(0.0) - for x_val, y_val in [(0.0, 0.0), (0.5, 1.0), (1.0, 2.0)]: - pred = network(torch.tensor(x_val, dtype=torch.float32))[0] - task_loss = task_loss + (pred - y_val) ** 2 - task_loss = task_loss / 3 + preds = model(train_x).squeeze(1) + task_loss = torch.mean((preds - train_y) ** 2) # Constraint loss produced by Vehicle; signature matches the Vehicle property - constraint_loss_value = constraint_loss(network) + constraint_loss_value = constraint_loss(model) loss = 0.5 * task_loss + 0.5 * constraint_loss_value loss.backward() @@ -294,33 +287,30 @@ from vehicle_lang.loss.tensorflow import load_specification spec = load_specification("test_trainable.vcl", logic=DifferentiableLogic.Vehicle) constraint_loss = spec["output_bounded"] +train_x = tf.constant([[0.0], [0.5], [1.0]], dtype=tf.float32) +train_y = tf.constant([0.0, 1.0, 2.0], dtype=tf.float32) + model = tf.keras.Sequential([ tf.keras.layers.Input(shape=(1,)), tf.keras.layers.Dense(8, activation="relu"), tf.keras.layers.Dense(1), ]) -def network(x): - return tf.reshape(model(tf.reshape(x, [1, 1])), [1]) - optimizer = tf.keras.optimizers.Adam(learning_rate=1e-2) for step in range(50): with tf.GradientTape() as tape: - task_loss = tf.constant(0.0) - for x_val, y_val in [(0.0, 0.0), (0.5, 1.0), (1.0, 2.0)]: - pred = network(tf.constant(x_val, dtype=tf.float32))[0] - task_loss = task_loss + (pred - y_val) ** 2 - task_loss = task_loss / 3 + preds = tf.squeeze(model(train_x), axis=1) + task_loss = tf.reduce_mean(tf.square(preds - train_y)) - constraint_loss_value = constraint_loss(network) + constraint_loss_value = constraint_loss(model) loss = 0.5 * task_loss + 0.5 * constraint_loss_value grads = tape.gradient(loss, model.trainable_variables) optimizer.apply_gradients(zip(grads, model.trainable_variables)) ``` -To customise how Vehicle searches adversarial points, pass your own sampler to `samplers`. -Each sampler receives `(dims, lower_bound, upper_bound, search_lambda, minimise)` and must -return a stackable tensor of loss values; see `DefaultPyTorchSampler` / `DefaultTensorFlowSampler` -in the source tree for a reference implementation. +Optional parameters such as `logic`, `samplers`, `declarations`, and `declaration_context` are +available on `load_specification`; see the [Python API docs](https://vehicle-lang.readthedocs.io/en/stable/training.html) for defaults and examples. To customise +how Vehicle searches adversarial points, you can supply your own sampler (cf. the default FGSM-based +samplers in the source tree) when you have domain-specific needs. From 6f23128da8cb034b0262724e6c8ee093eb4b49b5 Mon Sep 17 00:00:00 2001 From: Gusts Gustavs Grinbergs Date: Sun, 21 Dec 2025 19:44:10 +0100 Subject: [PATCH 3/3] implement suggestions --- src/chapters/4-property-driven-training.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/chapters/4-property-driven-training.md b/src/chapters/4-property-driven-training.md index f4ea757..845b0d6 100644 --- a/src/chapters/4-property-driven-training.md +++ b/src/chapters/4-property-driven-training.md @@ -310,7 +310,7 @@ for step in range(50): optimizer.apply_gradients(zip(grads, model.trainable_variables)) ``` -Optional parameters such as `logic`, `samplers`, `declarations`, and `declaration_context` are +Optional parameters such as `logic`and `samplers` are available on `load_specification`; see the [Python API docs](https://vehicle-lang.readthedocs.io/en/stable/training.html) for defaults and examples. To customise how Vehicle searches adversarial points, you can supply your own sampler (cf. the default FGSM-based samplers in the source tree) when you have domain-specific needs.