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..25187aa 100644 --- a/src/chapters/3-proving-robustness.md +++ b/src/chapters/3-proving-robustness.md @@ -101,7 +101,7 @@ advises : Image -> Label -> Bool advises x i = forall j . j != i => classifier x ! i > classifier x ! j ``` -This completes the basic description if the data set and the model architecture in Vehicle. We are ready to define verification properties. +This completes the basic description of the data set and the model architecture in Vehicle. We are ready to define verification properties. ## Definition of Robustness Around a Point @@ -265,7 +265,7 @@ Make conclusion about feasibility and success rates of $\epsilon$-ball robustnes ## Exercise #4 (⭑): Strong Classification Robustness in Vehicle Using the same `.vcl` file as in all previous exercises, define and verify in Vehicle the property of _Strong Classification Robustness_, -that requires, for all $\mathbf{x}$ in the $\epsilon$-ball of $\hat{\mathbf{x}}$, that $f(\mathbf{x})_i \leq \eta$, for some small $\eta$. +that requires, for all $\mathbf{x}$ in the $\epsilon$-ball of $\hat{\mathbf{x}}$, that $f(\mathbf{x})_i \geq \eta$, for some small $\eta$. We now assemble the desired _strong classification robustness_ property definition: Given an $\hat{\mathbf{x}} \in \mathcal{X}$, @@ -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$ -->