Tutorial

Requirements

Clone

git clone https://github.com/Verified-Intelligence/GEAR.git
cd GEAR

The repository holds solver/ (the code), benchmarks/ (the 505 models as one archive), logs/ and baselines/ (the results behind the paper) and site/ (this page). All commands below run from the repository root unless a cd is shown.

Environment

IPOPT comes with cyipopt from conda-forge; PyTorch comes from the CUDA 12.8 wheel index; the remaining packages are pinned in solver/requirements.txt.

conda create -y -p ./env -c conda-forge python=3.11 cyipopt
./env/bin/python -m pip install torch==2.8.0 torchvision==0.23.0 --index-url https://download.pytorch.org/whl/cu128
./env/bin/python -m pip install -r solver/requirements.txt

The solver is used in place; point Python at it:

export PYTHONPATH=$PWD/solver:$PWD/solver/complete_verifier PYTHONNOUSERSITE=1

Check that the imports come from the checkout, that PyTorch is 2.8.0 and that it sees the GPU:

./env/bin/python -c "
import auto_LiRPA, gear, nlp_solver, torch, cyipopt
for m in (auto_LiRPA, gear, nlp_solver): print(m.__name__, m.__file__)
print('torch', torch.__version__, torch.__file__, 'cuda available:', torch.cuda.is_available())
assert torch.__version__.startswith('2.8.0')
print('cyipopt', cyipopt.__version__, cyipopt.__file__)
"

The module paths must lie under solver/.

Get the benchmarks

benchmarks/gear-benchmarks.tar.xz (9.3 MB) holds the 505 converted models: 265 from GAMS World and 240 from MINLPLib. Each instance is a PyTorch module, its parameters and a specification of the variable bounds and the objective and constraint outputs. benchmarks/README.md lists the sources and their licenses; benchmarks/instances.tsv lists the instances.

(cd benchmarks && sha256sum -c SHA256SUMS && tar -xJf gear-benchmarks.tar.xz)

This creates benchmarks/gams_world/ and benchmarks/minlplib_linear/ (987 MiB). The conversion tools from the AMPL and GAMS sources are not part of the repository, and no AMPL or GAMS license is needed to run GEAR on the models.

Solve one instance from the command line

cd solver/complete_verifier
../../env/bin/python nlp_example.py --problem_name hs030 --benchmark gams_world --benchmark_root ../../benchmarks \
    --config exp_configs/NLP_solver/f3.yaml --device cuda --use_beta False --override_timeout 180 --batch_size 1 \
    --result_json ../../hs030.json
cd ../..

The configuration f3.yaml is the default configuration of the release: the version frozen for the NeurIPS 2026 submission. --override_timeout is the time limit in seconds; the paper's runs use 180. The first run of an instance parses its specification and writes <instance>.vnnlib.compiled next to benchmarks/<family>/vnnlib_*/<instance>.vnnlib; later runs read it. Delete these files to regenerate them; the archive does not contain them.

Reading the output

[Op] nlp t=6.088 s=2.2587 work=1 dD=0 dP=0
[Op] search_state t=6.089 s=0.0001 work=1 dD=0 dP=0
[Op] incumbent t=6.089 s=0.0001 work=1 dD=0 dP=inf
[UnifiedRoot] closed after incumbent at 2.35s: P=1 D=1
Primal Solution tensor([1.]), Dual Solution 1.0
Solution gap: 0.0
Found optimal object: tensor([1.])
[best-primal] objective=1.0 x=[1.0, 0.0, 0.0]
problem_name=hs030 status=verified success=True

The strict re-check evaluates the returned point on the original model in float64 and requires every constraint and bound to hold to absolute tolerance 10⁻⁶. Its result is in the JSON file:

{
 "status": "OPTIMAL",
 "termination": "GAP_CLOSED",
 "primal_bound": 1.0,
 "dual_bound": 1.0,
 "gap_rel": 0.0,
 "x": {
  "X_0": 1.0,
  "X_1": 0.0,
  "X_2": 0.0
 },
 "replay": {
  "feas_tol": 1e-06,
  "max_bound_violation": 0.0,
  "max_row_violation": -1e-12,
  "ok": true,
  "worst_row": "row 0"
 }
}

status is OPTIMAL (gap closed), INFEASIBLE (proved), FEASIBLE (a point, no closed gap) or NO_SOLUTION; termination gives the reason (GAP_CLOSED, TIME_LIMIT, ...). replay.ok is the strict re-check, with the largest row violation and bound violation it found.

The same kind of solve through the gear command:

cd solver/complete_verifier
../../env/bin/python -m gear.cli solve --legacy hs071 --family gams_world --root ../../benchmarks \
    --device cuda --time_limit 180 --result_json ../../hs071.json
cd ../..

Solve from Python

A benchmark instance

from pathlib import Path
import gear as gr
c = gr.compile(gr.read_legacy("hs071", root=Path("benchmarks").resolve(), family="gams_world"))
r = gr.solve(c, gr.Options(preset="gear-f0", device="cuda", time_limit=180))
print(r.status, r.primal_bound, r.dual_bound, r.replay.ok)

Run it from the repository root with the PYTHONPATH set above (./env/bin/python script.py). Pass the benchmark root as an absolute path: a relative root is resolved against solver/complete_verifier, not the working directory. The preset gear-f0 is the f3 configuration. The result carries status, primal_bound (P), dual_bound (D), gap_rel, the point x, replay (the strict re-check) and stats.

Status.OPTIMAL 17.01401660197175 17.01236204099385 True

Your own problem in PyTorch

A problem is a torch.nn.Module that maps a batch of points x (shape [1, n]) to a row of outputs, a box, the index of the objective output, and the indices of the outputs that must be ≤ 0 (le) or = 0 (eq). The box is a pair of float64 arrays. Use operations of a single dense forward pass (torch.cat, arithmetic, sin, exp, tanh, matrix products, ...); an unsupported operation raises UnsupportedModelError at gr.compile, before any solve. Example: minimize (x₀ − 1)² + sin(x₁) subject to x₀x₁ − 1 ≤ 0 on [−2, 2] × [−3, 3]:

import numpy as np, torch
import gear as gr

class Problem(torch.nn.Module):
    # outputs: [objective, g]
    def forward(self, x):
        x0, x1 = x[:, 0:1], x[:, 1:2]
        return torch.cat([(x0 - 1.0) ** 2 + torch.sin(x1), x0 * x1 - 1.0], dim=1)

box = (np.array([-2.0, -3.0]), np.array([2.0, 3.0]))
c = gr.compile(Problem(), box=box, objective=0, le=[1])
r = gr.solve(c, gr.Options(preset="gear-f0", device="cuda", time_limit=60))
print(r.status, r.primal_bound, r.dual_bound, r.x, r.replay.ok)

Status.OPTIMAL -1.0 -1.0 {'X_0': 0.9999999974696404, 'X_1': -1.570796318436919} True

The point is x = (1, −π/2) with value −1; P and D agree to the gap tolerance.

Reproduce the 505 runs

One instance at a time, the same configuration for all instances, 180 s each. benchmarks/instances.tsv lists the family and name of the 505 instances; N limits the number of instances (set N=2 for a trial).

N=${N:-505}
tail -n +2 benchmarks/instances.tsv | head -n $N | while IFS=$'\t' read -r family name; do
  mkdir -p runs/gear/$family
  (cd solver/complete_verifier && ../../env/bin/python nlp_example.py --problem_name $name --benchmark $family \
      --benchmark_root ../../benchmarks --config exp_configs/NLP_solver/f3.yaml --device cuda --use_beta False \
      --override_timeout 180 --batch_size 1 --result_json ../../runs/gear/$family/$name.json) \
      > runs/gear/$family/$name.log 2>&1
done
grep -h '^problem_name=' runs/gear/*/*.log | grep -c 'status=verified'

The last command counts the instances that ended verified. The paper's table scores each run again: the returned point must satisfy every constraint and bound to 10⁻⁶ on the original model, and (P − D) / max(1, |P|, |D|) ≤ 10⁻⁴; the per-instance results of the paper's runs are in logs/gear_results.tsv. Counts depend on the GPU, the number of CPU threads and the load of the machine, because several stages run under wall-clock budgets.

Where logs and results go