Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verification

TL;DR

This paper introduces a novel tight approximation method for RNN robustness verification that improves accuracy by reducing over-estimation in nonlinear activation bounds, demonstrated through DeepPrism.

Contribution

It proposes a truncated rectangular prism approximation for nonlinear surfaces, enhancing the tightness of over-approximation in RNN verification.

Findings

DeepPrism outperforms state-of-the-art methods in accuracy.

The approach improves verification in image, speech, and sentiment tasks.

Tighter bounds lead to more reliable robustness guarantees.

Abstract

Robustness verification is a promising technique for rigorously proving Recurrent Neural Networks (RNNs) robustly. A key challenge is to over-approximate the nonlinear activation functions with linear constraints, which can transform the verification problem into an efficiently solvable linear programming problem. Existing methods over-approximate the nonlinear parts with linear bounding planes individually, which may cause significant over-estimation and lead to lower verification accuracy. In this paper, in order to tightly enclose the three-dimensional nonlinear surface generated by the Hadamard product, we propose a novel truncated rectangular prism formed by two linear relaxation planes and a refinement-driven method to minimize both its volume and surface area for tighter over-approximation. Based on this approximation, we implement a prototype DeepPrism for RNN robustness verification. The experimental results demonstrate that \emph{DeepPrism} has significant improvement compared with the state-of-the-art approaches in various tasks of image classification, speech recognition and sentiment analysis.