Quantifiers

Quantifying over infinite sets

(⤴)

One of the main advantages of Vehicle compared to a testing framework is that it can be used to state and prove specifications that describe the network’s behaviour over an infinite set of values.

Suppose you have the following network which produces two outputs:

@network
f : Tensor Real [10, 10] -> Tensor Real [2]

and would like to specify that for any input the network’s first output is always positive. This can be achieved by using the forall quantifier as follows:

forall x . f x ! 0 > 0

which brings a new variable x of type Tensor Real [10, 10] into scope. The variable x has no assigned value and therefore represents an arbitrary input.

Similarly, if trying to specify that there exists at least one input for which the network’s first output is positive, the exists quantifier can be used as follows:

exists x . f x ! 0 > 0

As with lambda functions, the quantified variables can be annotated with their types:

exists (x : Tensor Real [10, 10]) . f x ! 0 > 0

and multiple variables can be quantified over at once:

exists x i . f x ! i > 0

In many cases you don’t want the property to hold over all the values in the set, but only a (still infinite) subset of them. For example, network inputs are frequently normalised to lie within the range [0, 1]. If the quantified variable’s domain is not also restricted to this range, then Vehicle will produce spurious counter-examples to the specification.

In general such restrictions can be achieved by combining a quantifier with an implication as follows:

forall x. (forall i j . 0 <= x ! i ! j <= 1) => f x ! 0 > 0

Quantifying over finite sets

While most specifications will quantify over at least one variable with an infinite domain, sometimes one might also want to quantify over a finite set of values. There are multiple ways of doing this:

Quantifying over an Index

The first approach is to quantify over a variable with the Index type. For example:

pointwiseLess : Vector Real 3 -> Vector Real 3 -> Bool
pointwiseLess x y = forall (i : Index 3) . x ! i < y ! i

is semantically equivalent to:

pointwiseLess : Vector Real 3 -> Vector Real 3 -> Bool
pointwiseLess x y = x ! 0 < y ! 0 and x ! 1 < y ! 1 and x ! 2 < y ! 2

The type annotation Index 3 on the quantified variable i is included for clarity but are not need in practice as it can be inferred by the compiler.

Quantifying over a collection

Alternatively quantifiers can be modified with the in keyword to quantify over all the values contained within a List, Vector or Tensor:

myList : List Real
myList = [0.4, 1.1, 0.2]

myListInRange : Bool
myListInRange = forall x in myList . 0 <= f x <= 1

During compilation Vehicle will automatically expand this out to a sequence of conjunctions as follows:

myListInRange : Bool
myListInRange = 0 <= f 0.4 <= 1 and 0 <= f 1.1 <= 1 and 0 <= f 0.2 <= 1