GEAR

How GEAR works

The linear bounds are already an LP

On one box, each constraint has a linear lower bound, so every feasible point satisfies Ax + c ≤ 0. With the objective’s linear bound, that is an LP relaxation of the box, on every box, from one propagation over all outputs.

Its dual is closed form, so a valid bound needs no LP solve

The smallest example: minimize x on [0, 1] subject to x ≥ 1/2. Without the constraint the bound stays 0 however far the box is split. Move the slider to add the constraint with a multiplier: the line flattens and its minimum over the box rises to the optimum.

λ = 0

Every λ ≥ 0 gives a valid bound in closed form, at O(mn) per evaluation, with a(λ) = a₀ + A^Tλ, and the best λ reaches the LP. LP solvers only propose multipliers. These multipliers act on the linear bounds and are distinct from the ALM multipliers of the primal search.

One tensor, five uses

All boxes form one tensor: K boxes × (m+1) functions × n variables. Each use is a sum or a min along its axes, which is why it batches. Pick a use to see the part of the tensor it reads and what it does on one box.

Primal and dual share the bounds

The minimizer of the bound and its multipliers start a projected augmented Lagrangian, which needs only graph evaluations, autodiff and projection, so it batches like the bounds. Its incumbent removes every box whose bound reaches it. On Modlangerman (10 variables), P stays at −0.517 for nine iterations while D rises from −2.46 to −0.972; then the search inside the tree finds −0.965 and the gap closes. P improves in the tree on 21 of 420 certified runs: most optimal points are found at the root, and the tree supplies the proof.

A real run, box by box

HS059 has two variables on [0, 75] × [0, 65], three nonlinear constraints and a nonconvex feasible set (shaded). Rectangles: the boxes still open in GEAR’s run. Move the slider to follow the run.

The price, and what the GPU gives

One linear bound per output is looser than an LP with all McCormick planes. Tighter operator relaxations narrow that: for a product, the best plane on the box moves the bound from −10 to 2; for a quotient, planes built for x/y directly move it from 0.32 to 0.50.

xy, fixed plane: −10xy, best plane: 2x/y, via reciprocal: 0.32x/y, direct: 0.50

On the GPU, throughput grows with the batch: up to 1,048,576 boxes in one step, and on 6 to 20 variables from 17 boxes per second in small steps to 284,000 in the largest.

What each part of the solver adds

Components are added one group per row, up to the full solver (Table 2 of the paper). Feasible: the returned point satisfies every constraint to 10⁻⁶. Optimal: that point is also within the relative gap of the best known value, with or without a dual certificate. Solved: a certified lower bound closes the gap.

421 of 505 certified in 180 seconds

505 bounded continuous nonlinear programs (265 from gams_world, 240 from MINLPLib) against six global and six local solvers through AMPL, all on one workstation (AMD Ryzen 9700X, 16 threads, one RTX 5090), 180 s per instance, one configuration per solver tuned on a 40-instance subset.

Where GEAR leads, and where it does not

Broken down by size, constraint count and kind of nonlinearity, the benchmark shows one regime where GEAR leads and one where it does not (Appendix D.1 of the paper).

The 16 instances only GEAR certifies

Grouped by cause, read from the Gurobi and SCIP logs (Appendix D.2 of the paper). Twelve close at the root; on three, a baseline’s point fails the 10⁻⁶ re-check. All contain transcendental terms. Each opens in the gap atlas with its formulation, every solver’s gap over time, the commands and the logs.

Relative gap between the best known optimum and each solver’s certified lower bound, over time. GEAR closes it within seconds; the six global solvers end their 180 s with the gap still open.

Reproduce every number

The repository holds the 505 models, the baseline harness with every configuration it tried, the log of every run behind the tables and the scored per-instance results. The GEAR source will be released there; until then its configuration and the exact command of every run are published with its logs.

1. The scoring rule

   A run is solved when its returned point satisfies every constraint and bound of the original model, with equalities kept exact, to absolute tolerance 10⁻⁶, and its primal value P and certified lower bound D satisfy

   (P − D) / max(1, |P|, |D|) ≤ 10⁻⁴.

   Baseline points are re-evaluated in AMPL; GEAR replays its point on the original model before returning it. Local solvers have no D and are credited when their feasible P matches the tightest bound a global solver certified. A certificate contradicted by a better feasible point from any run is withdrawn, and an infeasibility verdict counts once two global solvers confirm it.

2. Get the logs and verify them

   One archive per solver, one log per instance, local paths replaced; the checksums cover every archive, the GEAR configuration, its per-instance results and the manifest.

   git clone https://github.com/Verified-Intelligence/GEAR.git
   cd GEAR
   (cd logs && sha256sum -c SHA256SUMS)
   tar -xJf logs/gear.tar.xz       # gear/<family>/<instance>.log

   Copy

3. Recount Table 1 from the scored results

   One row per solver and instance, with the certificate, P, D, the maximum violation and the time.

   # global solvers: column 6 (criterion b); local solvers: column 10 (match with a certified bound)
   awk -F'\t' 'NR>1 && (($2=="global") ? $6 : $10)==1 {n[$1]++} END {for (s in n) print s, n[s]}' \
       baselines/results/per_instance_long.tsv
   # GEAR: one row per instance, column 4 = certified
   awk -F'\t' 'NR>1 && $4==1 {n++} END {print "gear", n}' logs/gear_results.tsv

   Copy

4. Rerun the baselines

   The harness runs each solver through its AMPL driver with its chosen configuration; baselines/commands.md lists every option string and thread layout.

   pip install amplpy
   python -m amplpy.modules install base coin baron knitro lgo lindoglobal minos scip snopt gurobi xpress conopt
   python -m amplpy.modules activate <your-license-uuid>
   cd baselines
   python harness/bl.py drive --config configs/chosen/gurobi_cfg.json --run final_gurobi --time-limit 180
   bash harness/run_campaign.sh     # all solvers: tuning, then the final runs

   Copy

5. The GEAR runs

   One instance at a time on one RTX 5090 with 16 CPU threads, the same configuration for all 505 instances (int3p_crownmerge.yaml). Every GEAR log starts with the command that produced it:

   python nlp_example.py --problem_name hs101 --benchmark gams_world --benchmark_root benchmarks \
       --device cuda --override_timeout 180.0 --config configs/int3p_crownmerge.yaml

   Copy

   The Configurations: block at the top of a GEAR log lists argument defaults, not the settings in effect.

6. Inspect any instance

   The gap atlas shows, for any subset of GEAR and the 12 AMPL solvers, which of them certify each instance, how each bound closes over time, the formulation, the command and the full logs.

   baselines/benchmark/	the 505 AMPL models and manifest.tsv (family, instance, sense, size, sha256)
   baselines/configs/	every configuration tried in tuning, the chosen one per solver, the 40-instance subset
   baselines/results/	scored per-instance tables, the final table and the tuning log
   logs/	logs of the 13 final runs, gear_results.tsv, the GEAR configuration, manifest and checksums
   site/	this page and the gap atlas

BibTeX

@inproceedings{zhou2026gear,
  title     = {{GEAR}: A {GPU}-Accelerated Global Solver for Bounded Continuous Nonlinear Programs via Linear Bound Propagation},
  author    = {Zhou, Duo and Chen, Hesun and Zhong, Xiangru and Hanasusanto, Grani A. and Zhang, Huan},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year      = {2026}
}