7. Transformations in CAISAR

7.1. What are transformations

ONNX is the de-facto standard to represent neural networks. No solver supports all ONNX operators; neither does CAISAR for that matter. Adding support for one ONNX operator to a solver is not a trivial task: it requires resource and it is error-prone; it is also a liability as it makes code more difficult to maintain.

Fortunately, some ONNX operators can be described as a combination of other, generally simpler, operators. They are syntactic sugar. Transformations in CAISAR are automatic operations that modify an existing ONNX to replace certain operators (that were in the original model being tested or that have been added by CAISAR itself) with equivalent sub-networks that include simpler operators. In this way, it is possible to call an existing solver on a problem that contains an ONNX operator that the solver does not support, as long as it supports those operators that the transformation introduced.

Some transformations might appear surprising or unnecessary. For instance, it is possible to transform the Add operator with Constant and Sub by using the equality \(x+y = x - (0-y)\). Most solvers will not use this transformation as they will probably support Add; however, if one wants to remove support to the Add operator for any reason (provability of correctness, maintainability, efficiency, etc.), this option is available.

Transformations can be chained, which gives a sort of hierarchy of operators. However, this hierarchy is not strict, and CAISAR offers a wide array of transformations.

7.2. Using transformations during verification

The list of transformations to apply is specified in the driver of the solver. For instance, application of the transform_arg_max transformation, which replaces the ArgMax operator with a combination of basic operators such as MatMul, Add, Sign, and ReLu, can be indicated by the following instruction:

transformation "transform_arg_max"

Transformations are called in order. One transformation may introduce an operator that is not supported. Consider for instance a scenario where both ArgMin and ArgMax operators need to be removed from the network. The transformation for operator ArgMin introduces a copy of ArgMax; thus, it is important to apply the transformer that removes ArgMax after applying the one that removes ArgMin.

7.3. Transforming existing ONNX

CAISAR is also able to apply the transformations to an ONNX and output the resulting ONNX. This feature is used through the following command:

caisar simplify -i input_file.onnx -o output_file.onnx -s list_of_transforms.txt

where

  • input_file.onnx is the path to the ONNX file on which the transformations are to be applied;

  • output_file.onnx is the path to the ONNX file generated by CAISAR; and

  • list_of_transforms.txt is a text file that contains the names of the transformations to apply (one per line).

7.4. Existing transformations and hierarchy

The list of transformations can be accessed with the following ocaml command:

Nir.Transform.registrables |> Base.List.map ~f:(fun (_,n,_) -> n);;

7.4.1. Base operators

The base ONNX operators are those that we might expect pretty much all solvers to support. Nonetheless, there are some operations within this set.

We consider that the base operators are:

  • Constant,

  • Add,

  • Sub,

  • Mul,

  • MatMul,

  • ReLu,

  • Transpose,

  • and Sign.

The last two operators are less often supported. As proof-of-concept, CAISAR includes a transformation that rewrites the operator Add with Constant and Sub so that A + B is rewritten A - (0 - B). This transformation is called transform_add.

7.4.2. ReduceSum

Operator ReduceSum can be rewritten only when its second input (the list of axes upon which the operation is to be made) is a Constant tensor. ReduceSum is then composed of a sequence of triplets (each associated with one of the axes) in which a Transpose is first performed to move the dimension at the end, a MatMul is used to sum up the elements, and a Transpose is performed to restore the position of the axis. (The Tranpose is not performed when the axis is already the last one.) Finally, a Reshape may be applied if the keepdims flag is negative.

7.4.3. ArgMax and ArgMin

images/argmax.png

Fig. 7.1 Transforming ArgMax and ArgMin operators into basic operators.

ArgMax and ArgMin can be transformed using the transform_arg_max and transform_arg_min transformations, respectively. ArgMax is transformed into base operators, including Sign and Relu; ArgMin is transformed into ArgMax. The two transformations are shown on Fig. 7.1.

The semantics of ArgMax transformation as well as its proof is available in a separate document.