Tips and tricks
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  -> 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.
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
network classify : Tensor Rat [24, 24] -> Tensor Rat 
and wanted to encode that it did not answer confidently
for some out-of-distribution input
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  -> 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
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
We will now describe some functions that are useful building blocks when writing specifications.
isArgmin : Index n -> Tensor Rat [n] -> Bool isArgmin i x = forall j . i != j => x ! i < x ! j
isArgmax : Index n -> Tensor Rat [n] -> Bool isArgmax i x = forall j . i != j => x ! i > x ! j
For a classification task where the network produces a score
for each class and the class with the lowest score is chosen,
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  advises : Index 10 -> Tensor Rat [24, 24] -> Bool advises i x = forall j . i != j => classify x ! i < classify x ! j