Tips and tricks

Naming indices

When individual indices of the input and output vectors have meaningful semantics, the readability of the spec can be significantly enhanced by assigning names to the indices.

For example consider a network responsible for controlling an agent navigating in a grid based world. The agent can either move in one of the 4 directions or stay still and, given some information about the current state of the world, the network calculates a score for each possible action.

@network
action : Tensor Rat [12] -> Tensor 5 [Rat]

Suppose the first and second outputs are the scores for staying still and moving up respectively, and that we would like to encode the constraint that in the state x the network assigns a higher score to staying still than moving up. This can be written as:

action x ! 0 > action x ! 1

However, a reader of the spec will not know what indices 0 and 1 correspond to. Instead, by assigning names for these indices:

stayStill = 0
moveUp    = 1
moveRight = 2
moveDown  = 3
moveLeft  = 4

this can be rewritten as:

action x ! stayStill > action x ! moveUp

which is significantly more understandable.

Use relations, not computation

A general trick is to try and define your specification in terms of relations rather than computation, especially computation that involves conditional statements.

For example, suppose you had an image classifier that assigns 10 classes a score between 0 and 1

network classify : Tensor Rat [24, 24] -> Tensor Rat [10]

and wanted to encode that it did not answer confidently for some out-of-distribution input x. A “computational” approach to encoding this constraint would be to calculate the maximum score and then require it to be less than 0.2:

max : Rat -> Rat -> Rat
max x y = if x <= y then x else y

largestScore : Tensor Rat [10] -> Rat
largestScore xs = fold max 0 xs

isUncertainAbout : Tensor Rat [24, 24] -> Bool
isUncertainAbout x = largestScore (classify x) <= 0.2

However, this definition would experience an exponential blow-up when compiled down to low-level verification queries, as each branch of the 10 if statements would need to be explored. In total 1024 queries would be generated.

This blow-up can be avoided by instead using a “relational” approach to encoding the constraint, instead stating that all classes scores must be less than 0.2:

isUncertainAbout : Tensor Rat [24, 24] -> Bool
isUncertainAbout x = forall i . x ! i <= 0.2

In summary, prefer to use relations to express your constraints and only perform computation and use if statements when you absolutely have to.

Useful functions

We will now describe some functions that are useful building blocks when writing specifications.

argmin

isArgmin : Index n -> Tensor Rat [n] -> Bool
isArgmin i x = forall j . i != j => x ! i < x ! j

argmin

isArgmax : Index n -> Tensor Rat [n] -> Bool
isArgmax i x = forall j . i != j => x ! i > x ! j

advises

For a classification task where the network produces a score for each class and the class with the lowest score is chosen, the definition isArgmin can be extended as follows to form a predicate that says the network advises the i`th class when applied to input `x:

@network
classify : Tensor Rat [24, 24] -> Tensor Rat [10]

advises : Index 10 -> Tensor Rat [24, 24] -> Bool
advises i x = forall j . i != j => classify x ! i < classify x ! j