Batch Processing

batch_find_untargeted_attack(
    nn,
    dataset,
    target_indices,
    optimizer,
    main_solve_options;
    save_path,
    solve_rerun_option,
    pp,
    norm_order,
    tightening_algorithm,
    tightening_options,
    solve_if_predicted_in_targeted,
    adversarial_example_objective
)

Runs find_adversarial_example for the specified neural network nn and dataset for samples identified by the target_indices, with the target labels for each sample set to the complement of the true label.

It creates a named directory in save_path, with the name summarizing

1. the name of the network in nn,
2. the perturbation family pp,
3. the norm_order.

Within this directory, a summary of all the results is stored in summary.csv, and results from individual runs are stored in the subfolder run_results.

This function is designed so that it can be interrupted and restarted cleanly; it relies on the summary.csv file to determine what the results of previous runs are (so modifying this file manually can lead to unexpected behavior.)

If the summary file already contains a result for a given target index, the solve_rerun_option determines whether we rerun find_adversarial_example for this particular index.

optimizer specifies the optimizer used to solve the MIP problem once it has been built and main_solve_options specifies the options that will be passed to the optimizer for the main solve.

Named Arguments:

• save_path: Directory where results will be saved. Defaults to current directory.
• pp, norm_order, tightening_algorithm, tightening_options, adversarial_example_objective, solve_if_predicted_in_targeted are passed through to find_adversarial_example and have the same default values; see documentation for that function for more details.
• solve_rerun_option::MIPVerify.SolveRerunOption: Options are never, always, resolve_ambiguous_cases, and refine_insecure_cases. See run_on_sample_for_untargeted_attack for more details. refine_insecure_cases rejects the feasibility objective because refinement computes an exact objective.

batch_find_targeted_attack(
    nn,
    dataset,
    target_indices,
    optimizer,
    main_solve_options;
    save_path,
    solve_rerun_option,
    target_labels,
    pp,
    norm_order,
    tightening_algorithm,
    tightening_options,
    solve_if_predicted_in_targeted,
    adversarial_example_objective
)

Runs find_adversarial_example for the specified neural network nn and dataset for samples identified by the target_indices, with each of the target labels in target_labels individually targeted.

Otherwise same parameters as batch_find_untargeted_attack.

extract_results_for_save(result)

Build the serializable subset of a solver-backed result without mutating result. Numeric witness values are retained whenever a candidate is available, including when independent verification fails. Unavailable objective values and bounds are stored as NaN.

has_available_unverified_witness(row)

Return whether row records an available candidate that does not pass every independent witness check. Missing or inconsistent verification fields fail closed through has_verified_witness.

has_legacy_objective_value(row)

Return whether an older row has numeric objective evidence but predates independent perturbation verification. This evidence is not a verified witness, but it keeps a legacy row's historical scheduling: it may select the row for an exact rerun and counts as a completed attack for resolve_ambiguous_cases.

has_verified_witness(row)

Return true only when all four witness flags exist, are non-missing, and are true. Incomplete or internally inconsistent legacy rows fail closed.

is_infeasible(status)

Return whether a solve status is exactly INFEASIBLE, given either a MathOptInterface.TerminationStatusCode or its string form. Combined or ambiguous statuses, including INFEASIBLE_OR_UNBOUNDED, do not certify infeasibility. This is the single source of truth for that rule; BenchmarkHelpers.is_infeasible_status delegates to it.

persist_summary_migration!(summary_file_path, dt, needs_migration)

Rewrite summary_file_path from the in-memory migrated dt and clear needs_migration. Callers invoke this immediately before appending the first new summary row, so the appended row aligns with the migrated header and an append-free batch never modifies the archived file.

read_summary_file(summary_file_path)

Read a batch summary and upgrade its schema in memory when necessary, returning the migrated DataFrame and whether it differs from the file on disk. The file itself is never modified here; persist_summary_migration! writes the migration immediately before the first new row is appended, so a batch that appends nothing leaves the archive untouched. The migration treats only plain INFEASIBLE as proven infeasible and leaves unavailable legacy objective and witness fields as missing. Non-missing objective names must match a current AdversarialExampleObjective. Summaries from the unreleased boolean-objective schema are rejected instead of migrated. Unrelated extra columns are retained.

run_on_sample_for_targeted_attack(
    sample_number,
    target_label,
    summary_dt,
    solve_rerun_option
)

Determines whether to run a solve on a sample depending on the solve_rerun_option by looking up information on the most recent completed solve recorded in summary_dt matching sample_number.

summary_dt is expected to be a DataFrame with columns :SampleNumber, :TargetIndexes, :SolveStatus, :ObjectiveValue, :WitnessAvailable, :WitnessTargetVerified, :WitnessPerturbationVerified, and :WitnessVerified. A witness from an older summary that lacks either independent check is unresolved as a verdict, but its numeric objective evidence keeps the row's historical scheduling: it counts as a completed attack for resolve_ambiguous_cases and can still select a non-optimal result for exact refinement.

run_on_sample_for_untargeted_attack(
    sample_number,
    summary_dt,
    solve_rerun_option
)

Determines whether to run a solve on a sample depending on the solve_rerun_option by looking up information on the most recent completed solve recorded in summary_dt matching sample_number.

summary_dt is expected to be a DataFrame with columns :SampleNumber, :SolveStatus, :ObjectiveValue, :WitnessAvailable, :WitnessTargetVerified, :WitnessPerturbationVerified, and :WitnessVerified. A witness from an older summary that lacks either independent check is unresolved as a verdict, but its numeric objective evidence keeps the row's historical scheduling.

Behavior for different choices of solve_rerun_option:

• never: true if and only if there is no previous completed solve.
• always: true always.
• resolve_ambiguous_cases: true if there is no previous completed solve, or if the most recent completed solve has neither a verified counterexample nor a proof of infeasibility, or if an available witness failed verification despite a contradictory infeasible status. Legacy rows without witness columns keep their historical meaning for scheduling: a recorded numeric objective counts as a completed attack and is not rerun.
• refine_insecure_cases: true if there is no previous completed solve, or if the most recent complete solve a) did find a verified counterexample, or recorded legacy objective evidence, but b) did not reach a provably optimal exact objective. A feasibility result still needs refinement even when it terminated with OPTIMAL.

save_to_disk(sample_number, main_path, results_dir, summary_file_path, result)

Persist one batch result and append its summary row. Solver-backed results write a MAT file and store its relative path; an original-input fast path appends only the CSV row.

should_refine_insecure(row)

Return whether attack evidence needs an exact-objective rerun. A feasibility solve still needs refinement when it terminated OPTIMAL, because that status proves only that a candidate exists.

should_resolve_ambiguous(row)

Return whether a batch row lacks either a strict infeasibility proof or a verified witness. An available but rejected witness remains ambiguous even alongside a contradictory infeasible status. Rerun options schedule work; they do not issue verdicts. Legacy rows that predate witness verification therefore keep their historical scheduling: numeric objective evidence counts as a completed attack even though it is not a verified witness. Rerun with always to replace legacy evidence with verified witnesses.

summary_witness_margin(result)

Return the recorded numeric witness margin when a candidate is available, otherwise NaN for the CSV summary.

uses_feasibility_objective(row)

Return whether a row records the feasibility objective. Missing objective metadata is treated as an exact historical result rather than a feasibility result.

validate_batch_refinement_objective(solve_rerun_option, objective)

Reject a feasibility objective for refine_insecure_cases, which must compute an exact objective.