Dataset declarations allow specifications to reference external data at scale, without having to replicate it manually in the specification.
Datasets are declared as follows using the
@dataset myDataset : Tensor Rat [28, 28]
Datasets can be any type
t that can be constructed from the following
t ::= List t | Vector t n | Tensor t ns | s s ::= Index n | Nat | Int | Rat
n is a known constant and
ns is a list of known constants.
Once declared, datasets can be used as any other named
would be, e.g.
forall x in myDataset . robustAround x
The actual implementation of the dataset is provided when using the specification during training or verification.
At the moment only the
IDX format is supported. A full description of this
format can be found at the bottom of this page.
- There are numerous libraries for converting datasets into this format:
If you would be interested in other formats being supported, please get in touch.