OMLT Layers

Neural network layer classes.

We use the following notations to define a layer:

\[\begin{split}\begin{align*} F_{in} &:= \text{number of input features}\\ F_{out} &:= \text{number of output features}\\ x_i &:= \text{the $i$-th input, $0\le i<F_{in}$}\\ y_j &:= \text{the $j$-th output, $0\le j<F_{out}$}\\ w_{ij} &:= \text{weight from $x_i$ to $y_j$, $0\le i<F_{in}, 0\le j<F_{out}$}\\ b_j &:= \text{bias for $y_j$, $0\le j<F_{out}$}\\ \sigma &:= \text{activation function} \end{align*}\end{split}\]

class omlt.neuralnet.layer.ConvLayer2D(input_size, output_size, strides, kernel, *, activation=None, input_index_mapper=None)[source]

Bases: Layer2D

Two-dimensional convolutional layer.

Parameters:

input_size (tuple) – the size of the input.
output_size (tuple) – the size of the output..
strides (matrix-like) – stride of the cross-correlation kernel.
kernel (matrix-like) – the cross-correlation kernel.
activation (str or None) – activation function name
input_index_mapper (IndexMapper or None) – map indexes from this layer index to the input layer index size

property kernel: Return the cross-correlation kernel

property kernel_depth: Return the depth of the cross-correlation kernel

property kernel_shape: Return the shape of the cross-correlation kernel

kernel_with_input_indexes(out_d, out_r, out_c)[source]

Returns an iterator over the kernel value and input index for the output at index (out_d, out_r, out_c).

Parameters:

out_d (int) – the output depth.
out_r (int) – the output row.
out_c (int) – the output column.

class omlt.neuralnet.layer.DenseLayer(input_size, output_size, weights, biases, *, activation=None, input_index_mapper=None)[source]

Bases: Layer

The dense layer is defined by:

\[\begin{align*} y_j = \sigma\left(\sum\limits_{i=0}^{F_{in}-1}w_{ij}x_i+b_j\right), && \forall 0\le j<F_{out} \end{align*}\]

Parameters:

input_size (tuple) – the size of the input.
output_size (tuple) – the size of the output.
weight (matrix-like) – the weight matrix.
biases (array-like) – the biases.
activation (str or None) – activation function name
input_index_mapper (IndexMapper or None) – map indexes from this layer index to the input layer index size

property biases: Return the vector of node biases

property weights: Return the matrix of node weights

class omlt.neuralnet.layer.GNNLayer(input_size, output_size, weights, biases, N, *, activation=None, input_index_mapper=None)[source]

Bases: DenseLayer

We additionally introduce the following notations to describe the gnn layer:

\[\begin{split}\begin{align*} N &:= \text{the number of node in the graph}\\ u &:= \text{the node index of $x_i$, $u=\lfloor iN/F_{in}\rfloor$}\\ v &:= \text{the node index of $y_j$, $v=\lfloor jN/F_{out}\rfloor$}\\ A_{u,v} &:= \text{the edge between node $u$ and $v$}\\ \end{align*}\end{split}\]

The gnn layer is defined by:

\[\begin{align*} y_j = \sigma \left(\sum\limits_{i=0}^{F_{in}-1}A_{u,v}w_{ij}x_i+b_j\right), && \forall 0\le j<F_{out}, \end{align*}\]

For example, given a GraphSAGE layer with sum aggregation:

\[\begin{align*} \mathbf{y_v} =\sigma\left(\mathbf{w_1^T}\mathbf{x_v}+\mathbf{w_2}^T\sum\limits_{u\in\mathcal N(v)}\mathbf{x_u}+\mathbf{b}\right) \end{align*}\]

If the graph structure is fixed, assume that it is a line graph with $N=3$ nodes, i.e., the adjacency matrix $A=\begin{pmatrix}1 & 1 & 0\\1 & 1 & 1\\ 0 & 1 & 1\end{pmatrix}$. Then the corresponding GNN layer is defined with parameters:

\[\begin{split}\begin{align*} \mathbf{W}=\begin{pmatrix} \mathbf{w_1} & \mathbf{w_2} & \mathbf{0} \\ \mathbf{w_2} & \mathbf{w_1} & \mathbf{w_2} \\ \mathbf{0} & \mathbf{w_2} & \mathbf{w_1} \\ \end{pmatrix}, \mathbf{B}=\begin{pmatrix} \mathbf{b}\\\mathbf{b}\\\mathbf{b} \end{pmatrix} \end{align*}\end{split}\]

Otherwise, if the input graph structure is not fixed, all weights and biases should be provided. In this case, the GNN layer is defined with parameters:

\[\begin{split}\begin{align*} \mathbf{W}=\begin{pmatrix} \mathbf{w_1} & \mathbf{w_2} & \mathbf{w_2} \\ \mathbf{w_2} & \mathbf{w_1} & \mathbf{w_2} \\ \mathbf{w_2} & \mathbf{w_2} & \mathbf{w_1} \\ \end{pmatrix}, \mathbf{B}=\begin{pmatrix} \mathbf{b}\\\mathbf{b}\\\mathbf{b} \end{pmatrix} \end{align*}\end{split}\]

In this case, all elements $A_{u,v},u\neq v$ are binary variables.

Parameters:

input_size (tuple) – the size of the input.
output_size (tuple) – the size of the output.
weight (matrix-like) – the weight matrix.
biases (array-like) – the biases.
N (int) – number of nodes in the graph
activation (str or None) – activation function name
input_index_mapper (IndexMapper or None) – map indexes from this layer index to the input layer index size

property N: Return the number of nodes in the graphs

property gnn_input_size: Return the size of the input tensor in original GNN

property gnn_output_size: Return the size of the output tensor in original GNN

class omlt.neuralnet.layer.IndexMapper(input_size, output_size)[source]

Bases: object

Map indexes from one layer to the other.

Parameters:

input_size (tuple) – the input size
output_size (tuple) – the mapped input layer’s output size

property input_size: Return the size of the input tensor

property output_size: Return the size of the output tensor

class omlt.neuralnet.layer.InputLayer(size)[source]

Bases: Layer

The first layer in any network.

Parameters:: size (tuple) – the size of the input.

class omlt.neuralnet.layer.Layer(input_size, output_size, *, activation=None, input_index_mapper=None)[source]

Bases: object

Base layer class.

Parameters:

input_size (list) – size of the layer input
output_size (list) – size of the layer output
activation (str or None) – activation function name
input_index_mapper (IndexMapper or None) – map indexes from this layer index to the input layer index size

property activation: Return the activation function

eval_single_layer(x)[source]

Evaluate the layer at x.

Parameters:: x (array-like) – the input tensor. Must have size self.input_size.

property input_index_mapper: Return the index mapper

property input_indexes: Return a list of the input indexes

property input_indexes_with_input_layer_indexes

Return an iterator generating a tuple of local and input indexes.

Local indexes are indexes over the elements of the current layer. Input indexes are indexes over the elements of the previous layer.

property input_size: Return the size of the input tensor

property output_indexes: Return a list of the output indexes

property output_size: Return the size of the output tensor

class omlt.neuralnet.layer.Layer2D(input_size, output_size, strides, *, activation=None, input_index_mapper=None)[source]

Bases: Layer

Abstract two-dimensional layer that downsamples values in a kernel to a single value.

Parameters:

input_size (tuple) – the size of the input.
output_size (tuple) – the size of the output.
strides (matrix-like) – stride of the kernel.
activation (str or None) – activation function name
input_index_mapper (IndexMapper or None) – map indexes from this layer index to the input layer index size

get_input_index(out_index, kernel_index)[source]: Returns the input index corresponding to the output at out_index and the kernel index kernel_index.

property kernel_depth: Return the depth of the kernel

kernel_index_with_input_indexes(out_d, out_r, out_c)[source]

Returns an iterator over the index within the kernel and input index for the output at index (out_d, out_r, out_c).

Parameters:

out_d (int) – the output depth.
out_r (int) – the output row.
out_c (int) – the output column.

property kernel_shape: Return the shape of the kernel

property strides: Return the stride of the layer

class omlt.neuralnet.layer.PoolingLayer2D(input_size, output_size, strides, pool_func_name, kernel_shape, kernel_depth, *, activation=None, input_index_mapper=None)[source]

Bases: Layer2D

Two-dimensional pooling layer.

Parameters:

input_size (tuple) – the size of the input.
output_size (tuple) – the size of the output.
strides (matrix-like) – stride of the kernel.
pool_func (str) – name of function used to pool values in a kernel to a single value.
transpose (bool) – True iff input matrix is accepted in transposed (i.e. column-major) form.
activation (str or None) – activation function name
input_index_mapper (IndexMapper or None) – map indexes from this layer index to the input layer index size

property kernel_depth: Return the depth of the kernel

property kernel_shape: Return the shape of the kernel