Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verification

Xingqi Lin, Liangyu Chen, Min Wu, Min Zhang, Zhenbing Zeng

TL;DR

This work tackles robustness verification for RNNs by addressing the tightness of linear relaxations applied to the nonlinear Hadamard-product term in LSTM gates. It introduces a truncated rectangular prism relaxation formed by two planes and an objective that jointly minimizes prism volume and surface area, yielding a tighter abstract domain named DeepPrism. Through single- and multi-plane verifications, DeepPrism demonstrates superior robustness certification across image classification, speech recognition, and sentiment analysis tasks compared to state-of-the-art baselines, with controlled increases in computation. The approach provides theoretical guarantees, a flexible refinement strategy, and practical improvements for scalable RNN verification in real-world tasks.

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.

Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verification

TL;DR

This work tackles robustness verification for RNNs by addressing the tightness of linear relaxations applied to the nonlinear Hadamard-product term in LSTM gates. It introduces a truncated rectangular prism relaxation formed by two planes and an objective that jointly minimizes prism volume and surface area, yielding a tighter abstract domain named DeepPrism. Through single- and multi-plane verifications, DeepPrism demonstrates superior robustness certification across image classification, speech recognition, and sentiment analysis tasks compared to state-of-the-art baselines, with controlled increases in computation. The approach provides theoretical guarantees, a flexible refinement strategy, and practical improvements for scalable RNN verification in real-world tasks.

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.

Paper Structure

This paper contains 34 sections, 7 theorems, 62 equations, 21 figures, 15 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. LSTM
  5. DeepPoly
  6. Tighter Over-approximation
  7. Distance-based Method ryou2021scalable
  8. Volume-based Method
  9. Hybrid Volume-Area-based Method (DeepPrism)
  10. Verification Process
  11. Single-plane Approximation
  12. Multi-plane Approximation
  13. Experiments
  14. Experimental Setup
  15. Environment.
  16. ...and 19 more sections

Key Result

Theorem 1

The volume of the truncated poly-prism in Definition 1 is given by:

Figures (21)

  • Figure 1: An LSTM cell consists of a forget gate, an input gate, and an output gate. The regions highlighted by the red dashed line indicate the key challenge of over-approximation of $\sigma(x) \odot \tanh(y)$ and $\sigma(x) \odot y$.
  • Figure 1: A truncated poly-prism.
  • Figure 2: The upper and lower planes computed by linear programming based on the distance sum of sampling points.
  • Figure 2: A truncated triangular prism, where $P_1P_2P_3$ is a right triangle.
  • Figure 3: The truncated rectangular prism formed by four interval constraint planes and two relaxation planes.
  • ...and 16 more figures

Theorems & Definitions (8)

  • Definition 1
  • Theorem 1
  • Lemma 1
  • Lemma 2
  • Lemma 3
  • Theorem 2
  • Lemma 4
  • Lemma 5