Core Operations

Core Operations

Our ability to cast the input-output constraints of a neural net to an efficient set of linear and integer constraints boils down to the following basic operations, over which the layers provide a convenient layer of abstraction.

Index

Internal

MIPVerify.abs_ge — Method.
abs_ge(x)

Expresses a one-sided absolute-value constraint: output is constrained to be at least as large as |x|.

Only use when you are minimizing over the output in the objective.

MIPVerify.is_constant — Method.
is_constant(x)

Checks whether a JuMPLinearType is constant (and thus has no model associated) with it. This can only be true if it is an affine expression with no stored variables.

MIPVerify.lazy_tight_lowerbound — Method.

Calculates the lower_bound only if u is positive; otherwise, returns u (since we expect) the ReLU to be fixed to zero anyway.

MIPVerify.masked_relu — Method.
masked_relu(x, m; nta)

Expresses a masked rectified-linearity constraint, with three possibilities depending on the value of the mask. Output is constrained to be:

1) max(x, 0) if m=0,
2) 0 if m<0
3) x if m>0
MIPVerify.maximum — Method.

Expresses a maximization constraint: output is constrained to be equal to max(xs).

MIPVerify.maximum_ge — Method.
maximum_ge(xs)

Expresses a one-sided maximization constraint: output is constrained to be at least max(xs).

Only use when you are minimizing over the output in the objective.

NB: If all of xs are constant, we simply return the largest of them.

MIPVerify.relax_integrality_context — Method.
relax_integrality_context(f, model, should_relax_integrality)

Context manager for running f on model. If should_relax_integrality is true, the integrality constraints are relaxed before f is run and re-imposed after.

MIPVerify.relu — Method.

Expresses a rectified-linearity constraint: output is constrained to be equal to max(x, 0).

MIPVerify.set_max_indexes — Method.
set_max_indexes(model, xs, target_indexes; margin)

Imposes constraints ensuring that one of the elements at the targetindexes is the largest element of the array x. More specifically, we require x[j] - x[i] ≥ margin for some `j ∈ targetindexesand for alli ∉ target_indexes`.

MIPVerify.tight_bound — Method.

Calculates a tight bound of type bound_type on the variable x using the specified tightening algorithm nta.

If an upper bound is proven to be below cutoff, or a lower bound is proven to above cutoff, the algorithm returns early with whatever value was found.

MIPVerify.tight_bound_helper — Method.
tight_bound_helper(m, bound_type, objective, b_0)

Optimizes the value of objective based on bound_type, with b_0, computed via interval arithmetic, as a backup.

  • If an optimal solution is reached, we return the objective value. We also verify that the objective found is better than the bound b_0 provided; if this is not the case, we throw an error.
  • If we reach the user-defined time limit, we compute the best objective bound found. We compare this to b_0 and return the better result.
  • For all other solve statuses, we warn the user and report b_0.