Single Image

find_adversarial_example(
    nn,
    input,
    target_selection,
    optimizer,
    main_solve_options;
    invert_target_selection,
    pp,
    norm_order,
    adversarial_example_objective,
    tightening_algorithm,
    tightening_options,
    solve_if_predicted_in_targeted,
    margin,
    collect_stats
)

Perturbs input such that the network nn classifies the perturbed image in one of the categories identified by the indexes in target_selection.

IMPORTANT:

1. target_selection can include the correct label for input.
2. It is possible (particularly with the closest objective) to see 'ties' – that is, the perturbed input produces an output with two logits (one corresponding to a target category, and one corresponding to a non-target category) taking on the same maximal value. See the formal definition below for more; in particular, note that '≥' sign.

optimizer is used to build and solve the MIP problem.

The output dictionary records whether a numeric incumbent was available in :WitnessAvailable. :WitnessTargetVerified records whether an independent network forward pass satisfied the target condition. :WitnessPerturbationVerified records whether the numeric input satisfied the selected perturbation family's input constraints. :WitnessVerified is true only when both checks pass for a numeric candidate. Available witnesses also have numeric :PerturbedInputValue, :WitnessOutput, :WitnessMargin, and :WitnessDistance entries. Numeric comparisons allow an absolute or relative tolerance of 1e-8. An L-infinity budget uses only the relative tolerance so a small budget is not expanded by a larger fixed tolerance; a blur-kernel sum uses only the absolute tolerance so it does not grow with the channel count. These verification tolerances are deliberately stricter than typical solver primal feasibility tolerances (HiGHS defaults to 1e-7 and Gurobi to 1e-6), so a solver can return an incumbent that sits on a constraint boundary yet fails verification. Such a result is unresolved, not a solver wrong answer; tighten the solver's feasibility tolerance if boundary-tight witnesses must verify. Solver-backed results also have keys :Model, :PerturbationFamily, :TargetIndexes, :SolveStatus, :PrimalStatus, :Perturbation, :PerturbedInput, :Output. :AdversarialExampleObjective records the selected search objective. See the tutorial on what individual dictionary entries correspond to.

Formal Definition: If there are a total of n categories, the numeric output vector y=d[:WitnessOutput]=d[:PerturbedInputValue] |> nn has length n. If :WitnessVerified is true, then d[:PerturbedInputValue] belongs to pp around input, and y[j] - y[i] ≥ margin within the documented comparison tolerance for some j ∈ target_selection and for all i ∉ target_selection. These claims are checked numerically; a solver termination status alone does not establish them. Custom perturbation families fail this check unless they implement verify_perturbation_witness.

Keyword Arguments:

• invert_target_selection: Defaults to false. If true, sets target_selection to be its complement.
• pp: Defaults to UnrestrictedPerturbationFamily(). Determines the search space for adversarial examples.
• norm_order: Defaults to 1. Determines the distance norm used to determine the distance from the perturbed image to the original. Allowed options are 1 and Inf, and 2 if the optimizer can solve MIQPs.
• adversarial_example_objective: Defaults to closest. Allowed options are closest, worst, or feasibility.
  • closest finds the closest adversarial example, as measured by the norm_order norm.
  • worst finds the adversarial example with the largest gap between max(y[j) for j ∈ target_selection and max(y[i]) for all i ∉ target_selection.
  • feasibility asks whether any adversarial example satisfies the constraints. A returned WitnessDistance describes that candidate but is not necessarily minimal.
• tightening_algorithm: Defaults to mip. Determines how we determine the upper and lower bounds on input to each nonlinear unit. Allowed options are interval_arithmetic, lp, mip.
  • interval_arithmetic looks at the bounds on the output to the previous layer.
  • lp solves an lp corresponding to the mip formulation, but with any integer constraints relaxed.
  • mip solves the full mip formulation.
• tightening_options: Solver-specific options passed to optimizer when used to determine upper and lower bounds for input to nonlinear units. Note that these are only used if the tightening_algorithm is lp or mip (no solver is used when interval_arithmetic is used to compute the bounds). Defaults for Gurobi and HiGHS to a time limit of 20s per solve, with output suppressed.
• solve_if_predicted_in_targeted: Defaults to true. The prediction that nn makes for the unperturbed input can be determined efficiently. If the predicted index is one of the indexes in target_selection, we can skip the relatively costly process of building the model for the MIP problem since we already have an "adversarial example" –- namely, the input itself. We skip only when that input also passes the perturbation-family check. We continue building the model and solve the (trivial) MIP problem if solve_if_predicted_in_targeted is true, the requested margin is not met, or perturbation-family membership cannot be verified.
• margin: Defaults to 0.0. If specified, the target category must have logits strictly larger (by at least margin) than any non-target category.
• collect_stats: Defaults to false. If true, records formulation structure, progressive bound tightening work, ReLU stability, and main-solver work in the returned dictionary. The statistics keys are absent when no model is built (that is, when the predicted index is in target_selection and solve_if_predicted_in_targeted is false).

frac_correct(nn, dataset, num_samples)

Returns the fraction of items the neural network correctly classifies of the first num_samples of the provided dataset. If there are fewer than num_samples items, we use all of the available samples.

Named Arguments:

• nn::NeuralNet: The parameters of the neural network.
• dataset::LabelledDataset:
• num_samples::Integer: Number of samples to use.

Objective used when searching for an adversarial example.

closest minimizes perturbation distance, worst maximizes the target margin, and feasibility asks only whether any input satisfies the target and perturbation constraints.

Supertype for types encoding the family of perturbations allowed.

get_target_margin(output, target_indexes)

Return the largest target logit minus the largest non-target logit. If every index is targeted, return Inf because the target condition is vacuous. Throw ArgumentError when target_indexes is empty or contains an index outside output.

witness_satisfies_target(output, target_indexes, required_margin)

Return the observed target margin and whether it meets required_margin. The check fails for any non-finite output. Values within the witness verification tolerances of required_margin pass.

clear_witness_values!(result)

Remove every witness value recorded by an earlier evaluation. The witness flags always stay present; witness values exist only while a candidate is available.

record_no_witness!(result)

Mutate result to record that no numeric witness is available. Remove any stale witness values and set all witness verification flags to false.

record_witness!(result, nn, input, perturbed_input, pp, required_margin)

Independently evaluate and record a numeric witness candidate. The candidate is marked available even when its target or perturbation check fails; :WitnessVerified is true only when both pass. This function records the candidate, network output, observed margin, verification flags, and any perturbation-specific values. Stale values from an earlier evaluation are removed first, so verification never reads a previously recorded witness. The caller records :WitnessDistance when applicable.

witness_value_in_closed_interval(value, lower, upper; atol, rtol)

Return whether finite value lies in the closed interval [lower, upper], allowing the supplied absolute and relative tolerances at either boundary. Non-finite values always fail.

witness_inputs_satisfy_common_constraints(input, perturbed_input)

Return whether the original and perturbed inputs have the same shape, both contain only finite values, and every perturbed value lies in [0, 1]. Boundary comparisons use WITNESS_VERIFICATION_ATOL and WITNESS_VERIFICATION_RTOL.

witness_arrays_are_approximately_equal(lhs, rhs)

Return whether lhs and rhs have the same shape and each pair of values is approximately equal under the witness-verification tolerances.

blur_kernel_size_is_valid(pp)

Return whether both dimensions of pp.blur_kernel_size are positive integers.

verify_perturbation_witness(pp, input, perturbed_input, result)

Independently check that perturbed_input belongs to pp around input. Return (verified, auxiliary_values), where auxiliary_values contains numeric diagnostics that the caller merges into the result even when verified is false. Implementations should treat result as read-only and must check the numeric perturbation constraints instead of trusting solver status.

The generic fallback returns (false, Dict{Symbol,Any}()), so custom PerturbationFamily implementations fail closed until they define this method. Built-in methods require matching input shapes, finite values, and a perturbed input in [0, 1]. The L-infinity method also checks the perturbation radius with zero absolute tolerance and WITNESS_VERIFICATION_RTOL. The blur method checks the numeric kernel's shape, coefficient bounds, channel sum, and reconstructed input; the channel sum uses WITNESS_VERIFICATION_ATOL with zero relative tolerance, while other boundary and reconstruction checks use both witness-verification tolerances.

identity_blur_kernel(pp, input)

Return a Float64 identity blur kernel with shape (filter_height, filter_width, input_channels, input_channels), aligned with Conv2d's SAME padding for odd or even filter dimensions. Return nothing when input is not four dimensional, the filter dimensions are invalid, or the input has no channels.

numeric_blur_kernel(pp, input, result)

Return the numeric blur kernel available in result. Prefer a persisted :WitnessBlurKernel, then try to extract values from the JuMP variables in :BlurKernel. If neither key exists, construct an identity kernel for the original-input fast path. Failed JuMP value extraction returns nothing instead of substituting the identity kernel. This function does not mutate result or validate the kernel; verify_perturbation_witness performs those checks.