Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/assets/bibliography.bib
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ @misc{affeldt2026
}

@misc{capucci2026,
title={Quantitative Linear Logic},
title={Quantitative Linear Logic},
author={Matteo Capucci and Robert Atkey and Charles Grellois and Ekaterina Komendantskaya},
year={2026},
}
Expand Down
3 changes: 1 addition & 2 deletions src/chapters/1-introduction.md
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ If you are interested to know more about the theoretical underpinnings of Vehicl

- Daggitt, M., Kokke, W., Atkey, R., Komendantskaya, E., Slusarz, N., and Arnaboldi, L. *Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs.* Invited paper at 10th International Conference on Formal Structures for Computation and Deduction (FSCD'25).

- Daggitt, M., Komendantskaya, E.,
- Daggitt, M., Komendantskaya, E.,
Sirman, A., Bruni, A., Teuber, S., Smart, J., Passmore, G.: *Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice.* International Conference on Functional Programming (ICFP'26).

- Casadio, M., Komendantskaya, E., Daggitt, M.L., Kokke, W., Katz, G., Amir, G., Refaeli, I.:
Expand All @@ -127,4 +127,3 @@ ACM (2023).


- Sirman, A., Conway, F., Ciupa, J., Grinbergs, G., Komendantskaya, E., Hoang, S., Rawson, M., Bruni, A., Belle, V., Williams, M. *Vancomycert: A Certified Neuro-Symbolic Drug Delivery System (Case Study).* Symposium on AI Verification (SAIV'26).

2 changes: 1 addition & 1 deletion src/chapters/3-proving-robustness.md
Original file line number Diff line number Diff line change
Expand Up @@ -309,4 +309,4 @@ Once this is done, define the spec and verify its robustness. Experiment with di

Some sample solutions are available in [this folder](https://github.com/vehicle-lang/tutorial/tree/exercises/chapter-3/solutions). But we recommend that you try solving all exercises first.

Wish to contribute a new solution? Let us know and we will add it.
Wish to contribute a new solution? Let us know and we will add it.
8 changes: 4 additions & 4 deletions src/chapters/4-property-driven-training.md
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ Models learn by iteratively tweaking their optimisation parameters with the goal

$$\min_\theta\mathcal{L}(\hat x,y)$$

We are now ready to code all of this.
We are now ready to code all of this.

## Getting Started with the Code

Expand Down Expand Up @@ -155,7 +155,7 @@ Keeping the data in the range the specification talks about costs us nothing her
network below trains perfectly well on raw pixels --- and it keeps a single meaning for
$\epsilon$ across training and verification. Part II returns to this: it is a small
instance of the general difficulty of interfacing a logical specification with an
optimisation objective. One of the exercises in this chapter will give you a chance to reconstruct the whole training-verification pipeline *with* normalisation baked into the training.
optimisation objective. One of the exercises in this chapter will give you a chance to reconstruct the whole training-verification pipeline *with* normalisation baked into the training.

Finally, note that the two frameworks store images differently: PyTorch's `ToTensor`
produces channel-first batches of shape `(N, 1, 28, 28)`, whereas here we append the
Expand Down Expand Up @@ -309,7 +309,7 @@ training objective helps, we need a radius at which the network is genuinely vul
At $\epsilon = 0.005$ there is one image to win back; at $\epsilon = 0.02$ there are
sixteen.

We will first consider traditional machine learning methods that were introduced to address the problem of adversarial robustness.
We will first consider traditional machine learning methods that were introduced to address the problem of adversarial robustness.


## Data augmentation
Expand Down Expand Up @@ -476,7 +476,7 @@ X = \left\{ x \in \mathbb{R}^5 :\;\;
&960 \le x_5 \le x_5^{\max}
\end{aligned}
\right\}
$$
$$

Where $x_n^{max}$ is the maximum input value for attribute $x_n$ -->

Expand Down
4 changes: 2 additions & 2 deletions src/chapters/5-exporting-to-ITPs.md
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ A neural network controller `controller.onnx` can be verified against the specif
vehicle verify \
--specification windController.vcl \
--network controller:controller.onnx \
--verifier Marabou \
--solver Marabou \
--cache controller-result
```

Expand Down Expand Up @@ -717,7 +717,7 @@ Navigate to the `chapter-5/chapter-code` directory of the [tutorial repository](
vehicle verify \
--specification windController.vcl \
--network controller:controller.onnx \
--verifier Marabou \
--solver Marabou \
--cache controller-result
```
2. Export the verified specification to your ITP of choice (e.g. Rocq):
Expand Down
Loading