updated python stuff

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.
 

src/chapters/4-property-driven-training.md

@@ -229,48 +229,88 @@ 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 ship backend-specific helpers in `vehicle_lang.loss.tensorflow`
+and `vehicle_lang.loss.pytorch`. They both expose a single entry point
+`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.
 
-We open a new Python file and write:
+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,
+)
+
+constraint_loss = spec["output_bounded"]  # name of a @property in the spec
 
-spec = to_python(
-    "mnist-robustness.vcl",
-    target=Target.LOSS_DL2,
-    samplers={"pertubation": sampler_for_pertubation},
+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)
 
-robust_loss_fn = spec["robust"]
-```
+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)
+    preds = model(train_x).squeeze(1)
+    task_loss = torch.mean((preds - train_y) ** 2)
 
-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(model)
+
+    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"]
+
+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),
+])
+
+optimizer = tf.keras.optimizers.Adam(learning_rate=1e-2)
+
+for step in range(50):
+    with tf.GradientTape() as tape:
+        preds = tf.squeeze(model(train_x), axis=1)
+        task_loss = tf.reduce_mean(tf.square(preds - train_y))
+
+        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))
 ```
+
+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.