6. The CAISAR modelling language¶
6.1. Origin: WhyML¶
CAISAR heavily relies on Why3 and uses the WhyML language as a basis for its own interpretation language. A reference of WhyML is available on the original Why3 manual.
However, since Why3 aims to verify a whole range of programs, it cannot specialize on a particular program structure. For further background, the paper [F2013] from one of Why3’s original author details the rationale and tradeoff involved in the WhyML design and implementation. To quote the author, “[the Why3 team] has come up with logic of compromise”.
As CAISAR focuses on artificial intelligence systems, it can make some additional assumptions on the nature of the inputs, program and users:
users will have a basic background on linear algebra, and expect CAISAR to reflect this
inputs will mostly be multidimensional vectors (machine learning community coined the term “tensor” as well) of floating point values, strings, ints or chars
the program control flow will mostly be composed of a lot of real or floating-point arithmetic operations: there is no loop with runtime invariant, nor conditional
With those constraints in mind, CAISAR provides several extensions to WhyML, that we detail here. They can be used directly in any WhyML file provided to CAISAR.
Some of those extensions will be “interpreted”. During the translation from “pure” WhyML terms to actual inputs to provers, symbols will be replaced with other symbols, or directly computed by CAISAR.
6.2. Built-ins¶
The built-ins are available under stdlib/caisar/. To access the symbols they
define, the corresponding theory needs to be imported in the scope of the
current one. For instance, to import the symbols defined by the theory
Vector, prepend use caisar.types.Vector at the top of the file.
6.2.1. Vector¶
6.2.1.1. Types¶
type vector 'a
type index = int
6.2.1.2. Functions¶
val function ([]) (v: vector 'a) (i: index) : 'a
val function length (v: vector 'a) : int
val function clip (v: vector 'a) (lower: 'b) (upper: 'b) : vector 'a
val function softmax (v: vector 'a) : vector 'a
val function argmax (v: vector 'a) : 'a
(** Returns a vector with the i-th element as v1[i] - v2[i]. **)
val function (-) (v1: vector 'a) (v2: vector 'a) : vector 'a
(** Returns a vector with the i-th element as v1[i] + v2[i]. **)
val function (+) (v1: vector 'a) (v2: vector 'a) : vector 'a
val function mapi (v: vector 'a) (f: index -> 'a -> 'b) : vector 'b
val function map (v: vector 'a) (f: 'a -> 'b) : vector 'b
val function map2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c
let function foreach (v: vector 'a) (f: 'a -> 'b) : vector 'b =
map v f
let function foreach2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c =
map2 v1 v2 f
6.2.1.3. Predicates¶
predicate has_length (v: vector 'a) (i: int)
predicate valid_index (v: vector 'a) (i: index) = 0 <= i < length v
predicate forall_ (v: vector 'a) (f: 'a -> bool) =
forall i: index. valid_index v i -> f v[i]
predicate forall2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> bool) =
length(v1) = length(v2) -> forall i: index. valid_index v1 i -> f v1[i] v2[i]
This vector type is abstract and can be extended. For instance, the vector theory for integer is defined likeso:
theory VectorInt
use IntWithBounds
use Vector
type t = vector IntWithBounds.t
predicate valid (b: IntWithBounds.bounds) (v: t) =
Vector.forall_ v (IntWithBounds.valid b)
end
6.2.2. Model¶
6.2.2.1. Types¶
type model 'a
type kind
6.2.2.2. Functions¶
val function read_model (m: string) : model 'a
(** Returns an output vector resulting from the application of a model
on an input vector. **)
val function (@@) (m: model 'a) (v: vector 'a) : vector 'a
6.2.3. Dataset¶
6.2.3.1. Types¶
use caisar.types.Vector
type a
type b
(** Dataset type. Type [dataset] is a [vector (a, b)] representing a dataset entry.
Data is of type [a], and the ground truth is of type [b]. **)
type dataset = vector (a, b)
6.2.3.2. Functions¶
(** Returns a symbol for the dataset given its filename. **)
function read_dataset (f: string) : dataset
6.2.3.3. Predicates¶
predicate forall_ (d: dataset) (f: a -> b -> bool) =
Vector.forall_ d (fun e -> let a, b = e in f a b)
6.2.4. The Neural Intermediate Representation (NIR)¶
NIR is CAISAR’s internal representation of machine learning models.
It is a Directed Acyclic Graph (DAG) where nodes are describing operations on
multidimensional arrays (also called tensors), and edges describe the dataflow
from inputs to outputs.
The NIR is heavily influenced by the ONNX
representation of neural networks. Unless stated otherwise in the code
documentation, the semantics of NIR nodes follows the ONNX semantics.
Here is the list of supported operators:
type descr = t param_descr [@@deriving show]
Jean-Christophe Filiâtre, One Logic to Use Them All, CADE 24 - the 24th International Conference on Automated Deduction