From 691171a5da28850fa9dc785827039ab3d4193f3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Iv=C3=A1n=20Renison?= <85908989+IvanRenison@users.noreply.github.com> Date: Mon, 21 Sep 2026 12:01:01 -0300 Subject: [PATCH 1/2] Fix vehicle flag, it's `--solver` instead of `--verifier` --- src/chapters/5-exporting-to-ITPs.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/chapters/5-exporting-to-ITPs.md b/src/chapters/5-exporting-to-ITPs.md index 9a8a377..c8617e9 100644 --- a/src/chapters/5-exporting-to-ITPs.md +++ b/src/chapters/5-exporting-to-ITPs.md @@ -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 ``` @@ -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): From 7536dd6705e3cc869e048d114167ea2cb525b69a Mon Sep 17 00:00:00 2001 From: "pre-commit-ci[bot]" <66853113+pre-commit-ci[bot]@users.noreply.github.com> Date: Mon, 21 Sep 2026 15:02:43 +0000 Subject: [PATCH 2/2] [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --- src/assets/bibliography.bib | 2 +- src/chapters/1-introduction.md | 3 +-- src/chapters/3-proving-robustness.md | 2 +- src/chapters/4-property-driven-training.md | 8 ++++---- 4 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/assets/bibliography.bib b/src/assets/bibliography.bib index 6fedc60..1a0fe91 100644 --- a/src/assets/bibliography.bib +++ b/src/assets/bibliography.bib @@ -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}, } diff --git a/src/chapters/1-introduction.md b/src/chapters/1-introduction.md index 2cacaf9..6457db7 100644 --- a/src/chapters/1-introduction.md +++ b/src/chapters/1-introduction.md @@ -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.: @@ -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). - diff --git a/src/chapters/3-proving-robustness.md b/src/chapters/3-proving-robustness.md index 404c4a9..39ebb29 100644 --- a/src/chapters/3-proving-robustness.md +++ b/src/chapters/3-proving-robustness.md @@ -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. \ No newline at end of file +Wish to contribute a new solution? Let us know and we will add it. diff --git a/src/chapters/4-property-driven-training.md b/src/chapters/4-property-driven-training.md index 907e526..bee9aff 100644 --- a/src/chapters/4-property-driven-training.md +++ b/src/chapters/4-property-driven-training.md @@ -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 @@ -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 @@ -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 @@ -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$ -->