What they found
The authors built GEAR, a solver that finds provably best answers to nonlinear optimization problems with bounded, continuous variables. It reuses linear bound propagation, a fast method from neural network verification that runs on GPUs. The linear bounds act as simple stand-ins for hard nonlinear constraints. The solver uses them to get lower bounds, spot infeasible regions, and guide the search for good solutions. The authors also propose tighter linear relaxations for bilinear and quotient functions and other common nonlinear functions. They add a projected augmented Lagrangian method to produce solutions. On 505 problems from the GAMS and MINLPLib benchmarks, GEAR solved 421 under a 180-second limit. That is more than each of the six global solvers compared, including Gurobi, BARON and SCIP. Sixteen of these problems were certified by none of the six other solvers. All sixteen contain exponential, logarithmic, or trigonometric terms.
Why it matters
Global nonlinear optimization appears in engineering, energy, chemical design and many other fields. Traditional solvers can be slow on hard cases. The abstract points to the ability to move a method from SI model verification to a different, older field. It also shows GPUs can speed up work that has mostly run on CPUs. The abstract gives results only on the named benchmarks, so wider performance is not stated.
How it changes the race
This is mainly a tool for optimization, not a step in SI capability. If the result holds, it shows that GPU hardware and SI verification techniques can compete with long-established commercial solvers. That could widen access to strong global solvers.
Safety and control
The method comes from neural network verification, which is a safety-related field. The abstract does not test any safety use of GEAR itself.
The abstract, by the authors
We present a novel GPU-accelerated global solver for constrained nonlinear programming (NLP) inspired by the efficient linear bound propagation framework in neural network (NN) verification. Existing work on NN verification, a problem that can be cast as feasibility detection for a nonlinear objective, demonstrated orders-of-magnitude speedups with the linear bound propagation-based framework when compared to traditional solvers. Extending this paradigm to global nonlinear programming requires addressing many challenges: a global constrained NLP solver must effectively exploit all, possibly unstructured, nonlinear constraints to improve the objective, whereas NN verification typically handles simple input box constraints over a well-structured NN and does not directly optimize an objective function. We address these challenges by fully exploiting the linear bounds produced by bound propagation: these linear bounds can be viewed as relaxations of nonlinear constraints and used to provide lower bounds, check infeasibility, and guide the search for a primal solution. In addition, we propose tighter linear relaxations for bilinear, quotient, and other commonly used nonlinear functions in NLP problems, and a projected augmented Lagrangian method tightly coupled to our dual solving procedure to produce primal solutions. Our method solves 421 of 505 bounded and continuous NLP problems in the GAMS and MINLPLib benchmarks under a 180-second limit, more than each of the six global solvers we compare with, including Gurobi and BARON (commercial), and SCIP (open-source). Sixteen of these problems are certified by none of the six global solvers; all of them contain exponential, logarithmic, or trigonometric terms, which are often challenging for traditional approaches. Project webpage is at https://verified-intelligence.github.io/GEAR.
Quoted from arXiv:2611.10487. The research and its words belong to its authors.
