Since neural network verification problems can be formulated as optimization problems, linear programming (LP) solvers have been deployed as off-the-shelf tools in such processes. However, existing LP solvers running on CPU scale poorly on large networks. To expedite the process, we propose an LP-solving theorem tailored to neural network verification. In practice, we transform the constrained solving problem into an unconstrained problem that can be executed on GPUs, significantly speeding up the solving process. We explicitly include constraints on layers that take more than one predecessor instead of handling multiple predecessors by inefficient concatenation. Our theorem applies to widely used networks, such as fully connected, convolutional, and residual networks. From our evaluation, our GPU-aided solver achieves comparable precision to the state-of-the-art (SOTA) solver GUROBI with significant speed improvements and helps acquire competitive verification precision compared to advanced verification methods.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

GRENA: GPU-Aided Abstract Refinement for Neural Network Verification

  • Yuyi Zhong,
  • Shaun Zong Zhi Tan,
  • Hanping Xu,
  • Siau-Cheng Khoo

摘要

Since neural network verification problems can be formulated as optimization problems, linear programming (LP) solvers have been deployed as off-the-shelf tools in such processes. However, existing LP solvers running on CPU scale poorly on large networks. To expedite the process, we propose an LP-solving theorem tailored to neural network verification. In practice, we transform the constrained solving problem into an unconstrained problem that can be executed on GPUs, significantly speeding up the solving process. We explicitly include constraints on layers that take more than one predecessor instead of handling multiple predecessors by inefficient concatenation. Our theorem applies to widely used networks, such as fully connected, convolutional, and residual networks. From our evaluation, our GPU-aided solver achieves comparable precision to the state-of-the-art (SOTA) solver GUROBI with significant speed improvements and helps acquire competitive verification precision compared to advanced verification methods.