Benchmarks

Scripts for benchmarking MIPVerify on the MNIST WK17a network.

benchmark_wk17a_first100.jl

Runs adversarial example search on MNIST test samples using the MNIST.WK17a_linf0.1_authors network. It records formulation structure, progressive bound tightening, ReLU stability, and HiGHS work in addition to solve outcomes.

Usage

julia --project=benchmarks benchmarks/benchmark_wk17a_first100.jl \
  --out /tmp/bench-output \
  --samples 1:100 \
  --tightening interval_arithmetic \
  --main-time-limit 120 \
  --objective feasibility \
  --norm-order Inf \
  --log-level warn

Arguments

Argument	Default	Description
--out	(required)	Output directory for CSV results
--samples	1:100	Sample indices (start:stop, start:step:stop, or comma-separated)
--tightening	mip	Tightening algorithm: interval_arithmetic, lp, or mip
--main-time-limit	120	Time limit in seconds for the main solve
--objective	feasibility	Adversarial-example objective: feasibility or closest
--norm-order	Inf	Norm order for the perturbation (Inf or a number)
--log-level	warn	MIPVerify log level

The benchmark defaults to feasibility because its primary series tracks fixed-budget robustness. MIPVerify's public API still defaults to the exact minimum-distance closest objective. Pass --objective closest to benchmark that objective.

The benchmark environment constrains HiGHS.jl to 1.23.x and HiGHS_jll to 1.14.x. Keep these constraints aligned with the test environment so local, nightly, and paired measurements use the same solver generation.

Output

• benchmark_per_sample.csv — per-sample solve outcome, objective, target and perturbation witness checks, timing, formulation structure, aggregate bound-tightening work, ReLU stability, and main-solver work; witness_output and perturbed_input_value are semicolon-separated numeric arrays
• benchmark_relu_layers.csv — one row per sample and ReLU layer, with layer shape, applied tightening algorithm (interval_arithmetic when the layer has no nonconstant inputs, since constants need no bound solves), bounds and constraint-imposition timing (bounds_time_seconds, constraint_time_seconds), and stable or unstable counts
• benchmark_tightening.csv — one row per sample, ReLU layer, applied tightening algorithm, and bound direction; layer index 0 identifies bounds computed outside a ReLU layer
• benchmark_metrics.csv — aggregate wall-clock time, summed solve times, status and witness counts, and run metadata, including objective, Julia version, and dependency snapshot hash
• dependency_versions.csv — normalized resolved-package snapshot with package versions, tree hashes, source kind, and direct-dependency markers
• dependency_manifest.toml — copy of the active benchmark Manifest.toml for manual debugging (not consumed by any scripts)

Inputs that the network already misclassifies have status SKIPPED_PREDICTED_IN_TARGETED. They do not require a model or solve, but they count as zero-distance adversarial examples in the semantic totals and have objective value and bound 0.

Only INFEASIBLE counts as a robustness certificate. INFEASIBLE_OR_UNBOUNDED does not identify which condition the solver established, so the benchmark leaves it unresolved. It does not promote the benchmark formulation's expected boundedness into a solver proof.

Per-sample instrumentation

formulation_time_seconds covers model construction, progressive tightening, target constraints, the objective, and main-optimizer setup. bound_tightening_time_seconds is the sum of each ReLU layer's complete bounds phase plus solver wall time for bounds computed outside a ReLU layer. formulation_residual_time_seconds is formulation time minus that bound-tightening time. The residual includes target and objective construction, optimizer setup, and any unscoped bound-loop work that is not measured by a solver timer. formulation_excluding_bound_solver_time_seconds subtracts only optimization-based bound-solver wall time, leaving interval propagation and bound-loop overhead in the formulation time.

The two solver timing fields have different sources:

• main_solve_wall_time_seconds measures the wall time around the final optimize! call.
• solve_time_seconds is the final solve time reported by HiGHS.

The bound columns report logical requests, actual solver calls and statuses, progressive skips, solver time, and work counters. Tightening rows name the algorithm used at that stage, so a layer requested with MIP tightening can produce separate LP and MIP rows. ReLU columns use the formulation's four phase classes: zero_output, linear_in_input, constant_output, and split. Stable count is the sum of the first three; unstable count is split.

num_structural_constraints excludes variable bounds and integrality declarations. num_total_constraints includes them. Main node, simplex-iteration, barrier-iteration, and relative gap fields are missing when the solver does not expose a nonnegative value.

In benchmark_tightening.csv, status_counts and skip_counts contain sorted semicolon-separated name=count pairs. Dedicated columns cover optimal and time-limit statuses and each progressive skip reason.

benchmark_schema_version identifies the timing and output schema. Schema 6 records the adversarial-example objective by name. Schema 5 splits witness verification into target and perturbation checks. Schema 4 added verified-witness fields and solution- and objective-limit status counts. Schema 3 recorded LP and MIP stages separately when progressive MIP tightening is requested. semantic_outcome_schema_version identifies the outcome-counting rules. Semantic schema 4 requires both the numeric target check and perturbation-family membership check before counting an adversarial example. Semantic schema 3 first required a verified target witness and recorded failed verification separately. Semantic schema 2 added already-misclassified skipped inputs to the adversarial count. Comparison tooling rejects runs with different schema versions or objectives. Metrics without objective metadata predate feasibility benchmarking and use closest.

Nightly Benchmark Workflow

A GitHub Actions workflow (.github/workflows/nightly-benchmark.yml) runs the feasibility WK17a benchmark nightly on 500 samples with lp tightening.

Schedule

Runs daily at 6 AM UTC. Manual runs default to feasibility; select the closest-objective variant with gh workflow run nightly-benchmark.yml -f objective=closest.

Results storage

Results are committed to the benchmark-results branch:

• tracking.csv — one row per nightly run with aggregate metrics (append-only)
• runs/YYYY-MM-DD/<run_id>/ — immutable per-run artifacts for each nightly or rerun (benchmark_metrics.csv, benchmark_per_sample.csv, benchmark_relu_layers.csv, benchmark_tightening.csv, dependency_versions.csv, dependency_manifest.toml)

tracking.csv columns

Column	Description
date	Run date (YYYY-MM-DD)
run_id	Immutable per-run identifier (UTC timestamp + SHA)
commit_sha	Git commit SHA benchmarked
benchmark_schema_version	Version of the benchmark timing and output schema
semantic_outcome_schema_version	Version of the semantic outcome-counting rules
adversarial_example_objective	feasibility or closest; missing historical values mean closest
julia_version	Julia version used for the benchmark
dependency_snapshot_sha256	SHA-256 hash of the normalized dependency snapshot
dependency_change_summary	Text diff against the previous appended run's snapshot; [no dependency changes] when identical, missing when unavailable
wall_clock_seconds	Total wall-clock time for the benchmark run
sum_total_time_seconds	Sum of per-sample total times
sum_solve_time_seconds	Sum of per-sample solve times
median_solve_time_seconds	Median per-sample solve time
p90_solve_time_seconds	90th percentile per-sample solve time
num_samples	Number of samples evaluated
num_skipped_predicted_in_targeted	Already-misclassified inputs skipped before model construction; subset of adversarial outcomes
num_certified_no_adversarial_example	Samples proven robust (infeasible)
num_adversarial_example_found_or_best_known	Samples with adversarial examples found
num_time_limit_unresolved	Samples that hit the time limit
num_no_primal_solution_other	Samples with other non-primal outcomes
num_witness_verification_failed	Samples with an available witness that failed either independent check
num_witness_target_verification_failed	Available witnesses that failed the numeric network target or margin check; can overlap the perturbation failure count
num_witness_perturbation_verification_failed	Available witnesses that failed perturbation-family membership; can overlap the target failure count

append_to_tracking.jl

Reads benchmark_metrics.csv and dependency_versions.csv, derives the dependency summary against the previous run when available, and appends a summary row to tracking.csv. Used by the nightly workflow.

Usage

julia --project=benchmarks benchmarks/append_to_tracking.jl \
  --metrics-csv /tmp/bench/benchmark_metrics.csv \
  --dependency-versions-csv /tmp/bench/dependency_versions.csv \
  --tracking-csv /path/to/tracking.csv \
  --date 2024-01-15 \
  --commit-sha abc1234 \
  --run-id 2024-01-15T06-00-00Z-abc1234

compare_wk17a_benchmark.jl

Compares two benchmark runs and gates on a maximum allowed regression in wall-clock and total solve time.

Usage

julia --project=benchmarks benchmarks/compare_wk17a_benchmark.jl \
  --baseline /tmp/bench-before \
  --candidate /tmp/bench-after \
  --max-regression 0.05

Arguments

Argument	Default	Description
--baseline	(required)	Directory containing baseline benchmark_metrics.csv
--candidate	(required)	Directory containing candidate benchmark_metrics.csv
--max-regression	0.05	Maximum allowed regression ratio (0.05 = 5%)

Output

Prints a CSV-formatted comparison of wall-clock and total time plus outcome counts. The gate requires matching schemas, matching semantic partition counts, complete schema-2 partitions, and timing regressions within the configured limit. It exits with code 0 on PASS and 1 on FAIL.

Paired before/after mini-reports

For a performance-affecting change, produce a paired before/after report that shows the distribution of per-sample improvements (not just aggregate totals) and attach it to the PR. The workflow is three steps: run, analyze, publish.

1. Run both commits — run_pair.sh

Runs the WK17a benchmark on two commits, each in its own throwaway git worktree (so each uses that commit's own src + benchmarks), then analyzes the pair. The current branch and working tree are untouched. The runner develops each worktree's MIPVerify checkout into its benchmark environment and applies the same HiGHS.jl 1.23.x / HiGHS_jll 1.14.x constraints to both sides, including older commits whose benchmark project did not yet contain the pin.

benchmarks/run_pair.sh \
  --base <base-commit> --candidate <candidate-commit> \
  --out /tmp/pair-<slug> --samples 1:500 --tightening lp --main-time-limit 120 \
  --base-objective closest --candidate-objective feasibility

The side-specific objective flags are optional; without them, each commit uses its own benchmark default.

Produces /tmp/pair-<slug>/{base,candidate} (benchmark outputs) and /tmp/pair-<slug>/analysis (plots + tables). Write the filled report template to analysis/report.md before publishing.

2. Analyze — analysis/

run_pair.sh calls it for you; run it directly to re-analyze existing run dirs. It reports the per-sample ratio distribution, aggregate saving and concentration, solve-status counts, and grouped status and semantic-outcome changes, plus ECDF and scatter plots. See analysis/README.md.

3. Publish — publish_report.sh

Publishes an analysis dir to the benchmark-reports branch under a unique pairs/<slug>/. It stages the analyzer's flat PNG files under plots/, keeps report.md and the statistics at the archive root, and copies the sibling base/ and candidate/ runs as baseline/ and candidate/. The publisher is append-only and never forces: it aborts rather than overwrite an existing slug, and retries a rejected push with fetch+rebase, so nothing already on the branch can be clobbered.

benchmarks/publish_report.sh /tmp/pair-<slug>/analysis <YYYY-MM-DD-slug>

After a successful push, the publisher prints the pinned raw URL base used by the report template's {{pinned-raw-base}} plot links.

Then post a PR comment following REPORT_TEMPLATE.md: preamble (what the PR changes, benchmark setup, link to the published pairs/<slug>/ folder), ## Summary, then ## Detailed statistics with ### Plots as its first subsection — plots come before every table so readers get the shape of the distribution before the numbers.

benchmark-reports is a manual, human-published branch, separate from the CI-managed benchmark-results branch — the two never share a path.