GEAR：借力神经网络验证的 GPU 加速非线性规划全局求解器
GEAR: A GPU-Accelerated Global Solver for Bounded Continuous Nonlinear Programs via Linear Bound Propagation
把神经网络验证里的边界传播搬到通用优化求解上，一个 GPU 版全局求解器，505 道题解出 421 道，比 Gurobi 和 BARON 还多解出 16 道它们认证不了的题。做运筹优化或依赖求解器的团队可以看看这条新路线。
一篇 arXiv 论文提出 GEAR，一个受神经网络验证中线性边界传播框架启发的 GPU 加速全局求解器，用于求解有界连续非线性规划问题。在 180 秒时限内，GEAR 在 GAMS 与 MINLPLib 基准的 505 道题中解出 421 道，超过对比的六个全局求解器，包括商业求解器 Gurobi、BARON 和开源的 SCIP。
技术核心是把边界传播产生的线性界视为非线性约束的松弛，用于提供下界、检测不可行性并引导搜索原始解。作者还针对双线性、商函数等 NLP 常见非线性函数提出更紧的线性松弛，并设计投影增广拉格朗日方法与对偶求解过程紧耦合来产出原始解。
其中 16 道题是六个对比求解器都无法认证的，这些题均含指数、对数或三角函数项，正是传统方法的难点。对优化与运筹领域开发者而言，这项工作展示了 NN 验证技术向更广泛数值优化迁移的可行路径。
GEAR: A GPU-Accelerated Global Solver for Bounded Continuous Nonlinear Programs via Linear Bound Propagation
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.
This report is categorized under AITOP's "Papers" desk, focusing on US frontier AI labs and Silicon Valley technology leaders. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows. Key entities and technical topics under continuous tracking include GEAR, Gurobi, BARON, SCIP.
Source attribution: curated from arXiv cs.LG (@Duo Zhou, Hesun Chen, Xiangru Zhong, Grani A. Hanasusanto, Huan Zhang).
