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
MIPVerify.MaxPoolMIPVerify.conv2dMIPVerify.getoutputsizeMIPVerify.getpoolviewMIPVerify.getsliceindexMIPVerify.matmulMIPVerify.matmulMIPVerify.permute_and_flattenMIPVerify.poolMIPVerify.poolmapMIPVerify.Conv2dMIPVerify.Conv2dMIPVerify.FlattenMIPVerify.LinearMIPVerify.MaskedReLUMIPVerify.NormalizeMIPVerify.PoolMIPVerify.ReLUMIPVerify.SkipBlockMIPVerify.Zero
Public Interface
MIPVerify.Conv2d — Type
struct Conv2d{T<:Union{Real, JuMP.VariableRef, JuMP.AffExpr}, U<:Union{Real, JuMP.VariableRef, JuMP.AffExpr}, V<:Integer} <: LayerRepresents 2-D convolution operation.
p(x) is shorthand for conv2d(x, p) when p is an instance of Conv2d.
Dimension conventions (TensorFlow-style NHWC/HWIO):
This follows the conventions of tf.nn.conv2d:
- Input:
(batch, height, width, in_channels)— NHWC format, matching TensorFlow's defaultdata_format="NHWC" - Filter:
(filter_height, filter_width, in_channels, out_channels)— HWIO format, matching TensorFlow's filter shape fortf.nn.conv2d - Output:
(batch, out_height, out_width, out_channels)— NHWC format
To convert from PyTorch (OIHW filters, NCHW inputs), use convert_conv_filter_from_pytorch and convert_images_from_pytorch.
To convert from Flux.jl (WHIO filters, WHCN inputs), use convert_conv_filter_from_flux and convert_images_from_flux.
Fields:
filterbiasstridepadding
MIPVerify.Conv2d — Method
Conv2d(filter)
Convenience function to create a Conv2d struct with the specified filter and zero bias.
MIPVerify.Flatten — Type
struct Flatten{T<:Integer} <: LayerRepresents a flattening operation.
p(x) is shorthand for permute_and_flatten(x, p.perm) when p is an instance of Flatten.
Fields:
n_dimperm
MIPVerify.Linear — Type
struct Linear{T<:Real, U<:Real} <: LayerRepresents matrix multiplication.
p(x) is shorthand for matmul(x, p) when p is an instance of Linear.
Dimension convention:
- Weight matrix:
(in_features, out_features)— note: transposed during forward pass - Bias:
(out_features,) - Computation:
transpose(matrix) * x + bias
This matches the TensorFlow/Keras Dense layer convention. To convert from PyTorch's nn.Linear (which stores weights as (out_features, in_features)), use convert_linear_weights_from_pytorch.
Fields:
matrixbias
MIPVerify.MaskedReLU — Type
struct MaskedReLU{T<:Real} <: LayerRepresents 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:
masktightening_algorithm
MIPVerify.Normalize — Type
struct Normalize <: LayerRepresents a Normalization operation.
MIPVerify.MaxPool — Method
MaxPool(strides)
Convenience function to create a Pool struct for max-pooling.
MIPVerify.Pool — Type
struct Pool{N} <: LayerRepresents a pooling operation.
p(x) is shorthand for pool(x, p) when p is an instance of Pool.
Stride convention:
Strides are specified as an N-tuple matching the input dimensions. For 4D input in NHWC format: (1, stride_height, stride_width, 1) (batch and channel strides are typically 1).
Fields:
stridespooling_function
MIPVerify.ReLU — Type
struct ReLU <: LayerRepresents a ReLU operation.
p(x) is shorthand for relu(x) when p is an instance of ReLU.
MIPVerify.SkipBlock — Type
struct SkipBlock <: LayerA layer that implements a skip connection pattern, commonly used in residual networks (ResNets).
A SkipBlock takes multiple input tensors and applies a corresponding transformation layer to each input. The outputs of these transformations are then combined through element-wise addition.
When used within a SkipSequential, a SkipBlock processes inputs from the most recent layers in the network. If the block has n layers, it will take the outputs from the last n layers as input, in order. For example, with a 2-layer SkipBlock:
- The second layer processes the output from the immediately preceding layer
- The first layer processes the output from two layers back
Typically used in conjunction with SkipSequential to create networks with skip connections, where the outputs from earlier layers can bypass intermediate layers and be combined with later layer outputs.
Example:
skip_block = SkipBlock([
Linear(input_size_1, output_size), # Transform from one path
Linear(input_size_2, output_size) # Transform from another path
])Fields:
layers
MIPVerify.Zero — Type
struct Zero <: LayerAlways outputs exactly zero.
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 TensorFlow, with strides = [1, params.stride, params.stride, 1].
Dimension conventions:
- Input:
(batch, height, width, in_channels)— NHWC format - Filter:
(filter_height, filter_width, in_channels, out_channels)— HWIO format - Output:
(batch, out_height, out_width, out_channels)— NHWC format
Padding:
SamePadding(): TensorFlow-styleSAMEpadding is used, so output spatial size is(ceil(input_height / stride), ceil(input_width / stride)).ValidPadding(): No padding is added.- Fixed padding, specified as:
- A single integer, interpreted as padding for both axes
- A tuple of two integers, interpreted as
(y_padding, x_padding) - A tuple of four integers, interpreted as
(top, bottom, left, right)
Throws
- AssertionError if
inputandfilterare not compatible.
MIPVerify.permute_and_flatten — Method
Permute dimensions of array in specified order, then flattens the array.
MIPVerify.matmul — Method
matmul(x, params)
Computes the result of pre-multiplying x by the transpose of params.matrix and adding params.bias.
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.
MIPVerify.getoutputsize — Method
getoutputsize(input_array, strides)
For pooling operations on an array, returns the expected size of the output array.
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.
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.
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.
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.