Layers

Layers

Each layer in the neural net corresponds to a struct that simultaneously specifies: 1) the operation being carried out in the layer (recorded in the type of the struct) and 2) the parameters for the operation (recorded in the values of the fields of the struct).

When we pass an input array of real numbers to a layer struct, we get an output array of real numbers that is the result of the layer operating on the input.

Conversely, when we pass an input array of JuMP variables, we get an output array of JuMP variables, with the appropriate mixed-integer constraints (as determined by the layer) imposed between the input and output.

Index

Public Interface

MIPVerify.Conv2d — Type.
struct Conv2d{T<:Union{JuMP.GenericAffExpr{Float64,JuMP.Variable}, JuMP.Variable, Real}, U<:Union{JuMP.GenericAffExpr{Float64,JuMP.Variable}, JuMP.Variable, Real}, V<:Int64} <: MIPVerify.Layer

Represents 2-D convolution operation.

p(x) is shorthand for conv2d(x, p) when p is an instance of Conv2d.

Fields:

  • filter

  • bias

  • stride

source
MIPVerify.Conv2d — Method.
Conv2d(filter)

Convenience function to create a Conv2d struct with the specified filter and zero bias.

source
MIPVerify.Flatten — Type.
struct Flatten{T<:Integer} <: MIPVerify.Layer

Represents a flattening operation.

p(x) is shorthand for flatten(x, p.perm) when p is an instance of Flatten.

Fields:

  • n_dim

  • perm

source
MIPVerify.Linear — Type.
struct Linear{T<:Real, U<:Real} <: MIPVerify.Layer

Represents matrix multiplication.

p(x) is shorthand for matmul(x, p) when p is an instance of Linear.

Fields:

  • matrix

  • bias

source
MIPVerify.MaskedReLU — Type.
struct MaskedReLU{T<:Real} <: MIPVerify.Layer

Represents a masked ReLU activation, with mask controlling how the ReLU is applied to each output.

p(x) is shorthand for masked_relu(x, p.mask) when p is an instance of MaskedReLU.

Fields:

  • mask

  • tightening_algorithm

source
MIPVerify.MaxPool — Method.
MaxPool(strides)

Convenience function to create a Pool struct for max-pooling.

source
MIPVerify.Pool — Type.
struct Pool{N} <: MIPVerify.Layer

Represents a pooling operation.

p(x) is shorthand for pool(x, p) when p is an instance of Pool.

Fields:

  • strides

  • pooling_function

source
MIPVerify.ReLU — Type.
primitive type ReLU <: MIPVerify.Layer 64

Represents a ReLU operation.

p(x) is shorthand for relu(x) when p is an instance of ReLU.

source

Internal

MIPVerify.conv2d — Method.
conv2d(input, params)

Computes the result of convolving input with the filter and bias stored in params.

Mirrors tf.nn.conv2d from the tensorflow package, with strides = [1, 1, 1, 1], padding = 'SAME'.

Throws

  • AssertionError if input and filter are not compatible.

source
MIPVerify.flatten — Method.

Permute dimensions of array in specified order, then flattens the array.

source
MIPVerify.matmul — Method.
matmul(x, params)

Computes the result of pre-multiplying x by the transpose of params.matrix and adding params.bias.

source
MIPVerify.matmul — Method.
matmul(x, params)

Computes the result of pre-multiplying x by the transpose of params.matrix and adding params.bias. We write the computation out by hand when working with JuMPLinearType so that we are able to simplify the output as the computation is carried out.

source
MIPVerify.getoutputsize — Method.
getoutputsize(input_array, strides)

For pooling operations on an array, returns the expected size of the output array.

source
MIPVerify.getpoolview — Method.
getpoolview(input_array, strides, output_index)

For pooling operations on an array, returns a view of the parent array corresponding to the output_index in the output array.

source
MIPVerify.getsliceindex — Method.
getsliceindex(input_array_size, stride, output_index)

For pooling operations on an array where a given element in the output array corresponds to equal-sized blocks in the input array, returns (for a given dimension) the index range in the input array corresponding to a particular index output_index in the output array.

Returns an empty array if the output_index does not correspond to any input indices.

Arguments

  • stride::Integer: the size of the operating blocks along the active dimension.

source
MIPVerify.pool — Method.
pool(input, params)

Computes the result of applying the pooling function params.pooling_function to non-overlapping cells of input with sizes specified in params.strides.

source
MIPVerify.poolmap — Method.
poolmap(f, input_array, strides)

Returns output from applying f to subarrays of input_array, with the windows determined by the strides.

source