GPU-Accelerated Global Solver GEAR: Tackling Nonlinear Programming with Linear Bound Propagation

From Neural Network Verification to Nonlinear Programming: GEAR's Cross-Domain Inspiration

Global nonlinear programming (NLP) is one of the hard problems in optimization. Traditional solvers such as Gurobi, BARON, and SCIP often take enormous time when handling non-convex constraints. A recent paper proposes a GPU-accelerated global solver called GEAR, whose core idea originates from the linear bound propagation framework used in neural network verification. In neural network verification, this framework has been shown to deliver order-of-magnitude speedups; GEAR migrates this paradigm to the more complex NLP problems, attempting to address challenges that traditional methods struggle to overcome.

According to the paper, neural network verification usually deals only with well-structured input box constraints and does not directly optimize an objective function; in contrast, global NLP solvers must effectively exploit all possibly unstructured nonlinear constraints to improve the objective. GEAR bridges this gap by fully exploiting the linear bounds produced by bound propagation—these linear bounds can be regarded as relaxations of nonlinear constraints, used to provide lower bounds, detect infeasibility, and guide the search for primal solutions.

Linear Bound Propagation is a core technique in formal verification of neural networks, used to compute safe bounds on neural network outputs with respect to input perturbations. Its basic idea is: given an interval constraint on the input layer (e.g., (x \in [l, u]), propagate linear upper and lower bounds layer by layer, ultimately obtaining interval bounds on the output layer. Specifically, for each layer, it uses linear relaxations of activation functions (e.g., the triangle relaxation of ReLU) and interval arithmetic on weight matrices to propagate the bounds from the previous layer to the next layer. Since the entire process involves only matrix multiplications and element-wise operations, its computational complexity is comparable to a forward pass of the network and is highly parallelizable, thus enabling order-of-magnitude speedups on large-scale networks. This framework has been widely adopted in verification tools such as ERAN and CROWN.

How Linear Bound Propagation Is Used for Global Optimization

GEAR's key innovation lies in deeply coupling the entire process of linear bound propagation with the global solving workflow. Specifically, linear bounds are used as relaxations of nonlinear constraints, thereby providing lower bounds for branch-and-bound; when bound propagation detects that a subregion is infeasible, it can be safely pruned; at the same time, these bounds can also guide primal heuristic search, helping to quickly find feasible solutions.

To handle complex nonlinear terms commonly encountered in NLP, such as bilinear terms and quotient functions, the authors propose tighter linear relaxation methods. These improvements enable linear bound propagation to apply to a broader range of function types, rather than being limited to the simple activation functions common in neural network verification.

In addition, GEAR designs a projected augmented Lagrangian method tightly coupled with the dual solving process, used to generate primal solutions. This coupling ensures efficient interaction between primal and dual information and avoids the extra overhead caused by the separation of primal-dual iterations in traditional methods.

Branch-and-Bound is the most classic exact algorithm framework in global optimization. Its core workflow is: relax the original problem into an easier-to-solve subproblem (usually a linear program or convex relaxation), and solve the relaxation to obtain a lower bound; if the lower bound is greater than the objective value of the currently known feasible solution (upper bound), then the subregion cannot contain a better solution and can be safely pruned; otherwise, branch the region into smaller subregions and process them recursively. The efficiency of branch-and-bound depends heavily on the tightness of the relaxation—the tighter the relaxation, the closer the lower bound is to the true optimum, and the more effective the pruning. GEAR uses linear bound propagation as the relaxation method, precisely exploiting its ability to produce relatively tight linear bounds, thereby providing high-quality lower bounds for branch-and-bound.

Projected Augmented Lagrangian Method is a class of algorithms for solving constrained optimization problems, particularly suitable for nonlinear programming. The augmented Lagrangian method adds a penalty term (usually quadratic) to the Lagrangian function to handle constraints and improve convergence. Its basic iterations include: fixing the Lagrange multipliers, solving an unconstrained (or simply constrained) subproblem to update the primal variables; then updating the multipliers. The projection operation is used to handle simple box constraints on variables, that is, projecting the variables back into the feasible region after each iteration. GEAR tightly couples this method with the dual solving process, so that primal solution generation and dual bound computation proceed synchronously, avoiding the extra overhead caused by the separation of primal-dual iterations in traditional methods.

Benchmark Results: Outperforming Commercial and Open-Source Solvers

On the GAMS and MINLPLib benchmark sets, GEAR solved 421 of 505 bounded continuous NLP problems within a 180-second limit. The paper claims that this result surpasses the six global solvers it compares against, including the commercial solvers Gurobi and BARON, as well as the open-source solver SCIP.

One noteworthy detail is that 16 problems could not be proven globally optimal by any of the compared solvers, while GEAR successfully solved them. These problems all contain exponential, logarithmic, or trigonometric terms, precisely the areas where traditional methods often encounter difficulties. This suggests that GEAR's linear relaxation technique has better adaptability to these transcendental functions.

However, the paper does not provide detailed data comparing each solver individually, nor does it give specific numbers for average solving time or relative speedup. Therefore, GEAR's performance advantages in practical applications still require more independent reproduction and testing to verify.

Technical Details and Potential Impact

Another highlight of GEAR is its use of GPU acceleration. Linear bound propagation is inherently a highly parallel operation, suitable for batch processing on GPUs. Although the paper abstract does not disclose specific implementation details, it can be inferred that GEAR significantly improves the efficiency of bound propagation through large-scale parallel computation, thereby exploring more branches within the same amount of time.

From a broader perspective, GEAR demonstrates the value of cross-domain method transfer: efficient techniques from neural network verification, after adaptation, can be used to solve classic operations research problems. This approach may inspire more research to bring tools from the machine learning community into the traditional optimization field.

Of course, GEAR currently targets only bounded continuous NLP problems, and the test set is limited in scale. Its performance on mixed-integer nonlinear programming, large-scale sparse problems, or complex constraints in real industrial scenarios remains to be tested. But in any case, GEAR provides a promising direction for GPU-accelerated global optimization.

The project webpage has been made public, containing more implementation details and experimental results; interested readers can consult it further.

One-line Summary

GEAR transfers linear bound propagation from neural network verification to global nonlinear programming, outperforming six solvers with GPU acceleration.

Paragraph Summary

GEAR is a GPU-accelerated global nonlinear programming solver whose core innovation is transferring the linear bound propagation framework from neural network verification to NLP problems. GEAR uses linear bounds as relaxations of nonlinear constraints to provide lower bounds for branch-and-bound, detect infeasibility, and guide primal heuristic search. For complex nonlinear terms such as bilinear terms and quotient functions, the authors propose tighter linear relaxation methods and design a projected augmented Lagrangian method coupled with dual solving to generate primal solutions. On the GAMS and MINLPLib benchmark sets, GEAR solved 421 of 505 bounded continuous NLP problems within 180 seconds, surpassing six solvers including Gurobi, BARON, and SCIP; 16 problems (all containing exponential, logarithmic, or trigonometric terms) could not be proven globally optimal by any other compared solver. However, the paper does not provide detailed per-solver comparison data, and the actual performance advantages still require independent verification.