T ext V erifier: Robustness Verification for Textual Classifiers with Certifiable Guarantees (2023)

Abstract: When textual classifiers are deployed in safety-critical workflows, they must withstand the onslaught of AI-enabled model confusion caused by adversarial examples with minor alterations. In this paper, the main objective is to provide a formal verification framework, called TextVerifier, with certifiable guarantees on deep neural networks in natural language processing against word-level alteration attacks. We aim to provide an approximation of the maximal safe radius by deriving provable bounds both mathematically and automatically, where a minimum word-level L_0 distance is quantified as a guarantee for the classification invariance of victim models. Here, we illustrate three strengths of our strategy: i) certifiable guarantee: effective verification with convergence to ensure approximation of maximal safe radius with tight bounds ultimately; ii) high-efficiency: it yields an efficient speed edge by a novel parallelization strategy that can process a set of candidate texts simultaneously on GPUs; and iii) reliable anytime estimation: the verification can return intermediate bounds, and robustness estimates that are gradually, but strictly, improved as the computation proceeds. Furthermore, experiments are conducted on text classification on four datasets over three victim models to demonstrate the validity of tightening bounds. Our tool TextVerifier is available at https://github.com/TrustAI/TextVerifer .

## introduction deep neural networks (dnn) enable natural language processing (nlp) models to process human languages automatically and tackle various tasks, such as text classification @xcite , machine translation @xcite , information retrieval @xcite , dialogue understanding @xcite . meanwhile, the robustness of textual classifiers requires to be ⋆ corresponding author ensured to prevent malicious attempts from adversaries due to inherent vulnerability @xcite @xcite , which dates from computer vision @xcite and also emerges in nlp field @xcite . adversarial attacks @xcite @xcite are designed to generate semantically or superficially similar outputs to fool the victim models. with regard to adversarial defence, multiple strategies are devoted to resisting adversarial attacks. adversarial training @xcite is known as a mainstream mechanism to enhance the robustness of classifiers, which demands a substantial amount of adversarial examples for training. the shortcoming of this operation is the unavailability of all combinations with exponential growth among input sentences. additionally, another effective scheme is perturbationbased controlling @xcite , which aims to discern abnormal behaviors and rectify potential perturbations with safety risks. however, this scheme only specializes in dealing with visible perturbations, exclusive of unknown attacks. in that light, robustness verification is studied for solving the above problems. the main purpose is to provide a certificate for estimating robustness by identifying the local worst-case perturbations for a set of input sentences @xcite . in this paper, we mainly focus on performing local robustness verification by optimizing the problem of maximum safe radius (the minimum distance between an input and an adversarial example that changes the label prediction in hamming space) against word-level substitution attacks, which possess strengths in semantic imperceptibility and syntactic fluency @xcite . nevertheless, the computation process for such attacks has been shown to be an np-hard problem @xcite . as shown in figure 1 , given a clean input sentence, our objective is to calculate the upper and lower bounds to approximate the maximal safe radius with convergence guarantees and to process sets of potential adversarial sentences simultaneously via our efficient parallelization strategy. in our strategy, the lower bound ensures the nonexistence of adversarial examples within this safe region @xcite . while the upper bound is computed by any generated perturbations that result in incorrect predictions for nlp models, noted that the upper bound is utilized to approximate the safe radius from the upper side and localise the provably minimally-distorted adversarial example if it converges to the maximum safe radius @xcite . our approach verifies that the model is robust when the perturbations are below the lower bound (i.e., proving the robust region) and non-robust when the perturbations are above the upper bound (i.e., proving the non-robust region), leaving only the region between the lower and upper bounds unverifiable in terms of robustness. iteratively, our method increases the lower bound and decreases the upper bound to narrow the uncertainty region, eventually converging to the maximum safe radius with provable guarantees. our verification is an anytime algorithm. namely, even if our tool textverifier is interrupted before the verification process is complete, it can still provide valid lower and upper bounds of the maximal safe radius for certifying the robust and non-robust region. the main contributions are listed below. ## related work our work focuses primarily on robustness verification against word-level alteration-based attacks. so far, multiple representatives have been proposed based on synonym substitution, including @xcite @xcite . regarding realizing certified robustness by adversarial training, minimizing convex functions over convex sets is known as a convex optimization approach. in this line, worddp @xcite was proposed to realize certified robustness against word-level substitution adversaries using differential privacy in text classification. subsequently, a robust defence method called ranmask @xcite was proposed based on randomized smoothing. it randomly masks a portion of words to avoid the hypothesis of the access to synonym candidate sets. in the work @xcite , a curvature-based robustness certificate (crc) was proposed to compute a robustness certificate against l 2 -bounded attacks by utilizing convex optimization. nevertheless, it is inefficient to perform adversarial training via data augmentation for certified robustness. in terms of robustness verification against adversarial attacks, interval bound propagation (ibp) is known as an incomplete method and was first proposed in computer vision @xcite . following this, @xcite deployed ibp to the nlp settings, which considered the certified robustness of synonym substitution. meanwhile, @xcite introduced verifiable training to nlp models in the embedding space and computed tighter bounds. then (la malfa et al., 2020) measured robustness via maximal safe radius in the embedding space. however, the above strategies only focused on the embedding space has limited its application scenarios and ibp is difficult to extend to large network architectures such as bert with a loose outer bound. in summary, although robustness verification for nlp classifiers has been explored in previous research, existing approaches are either computationally expensive or cannot verify robustness in an anytime manner for hamming distance with strict convergence guarantees. ## preliminaries we start by providing supporting notations and problem formulations. the strategy for robustness verification will be detailed in the next section. given an input sentence @xmath0. then a pretrained m-way nlp classifier f performs a mapping from the input x to a prediction label y , i.e., f : @xmath1, where the label set is symbolized as @xmath2. assume that c refers to the classification probability (i.e., a confidence score). from this, it follows that the prediction label y for an input x is allocated via the highest confidence score, i.e., definition 1 (problem of maximal safe radius) for an input sequence x, a perturbation safe radius δ, a distance function ∥ • ∥ k with @xmath3, and a textual classifier f : @xmath4, a norm ball b(x, δ, k) denotes a subspace that holds: specifically, a norm ball b(x, δ, k) is regarded as safe as formalized below: hamming space our work sets @xmath5, which is known as the l 0 -norm or hamming distance. the hamming distance between a clean input and an adversarial counterpart quantifies nonidentical words. hamming distance @xcite can be an essential distance metric in the nlp field to measure the imperceptibility due to the discreteness of textual data. meanwhile, the property of semantic fluency and syntactic naturality is preserved as our strategy is against word-level alteration-based attacks @xcite @xcite . we further provide the definition of local robustness verification. definition 2 (verification for local robustness) given a clean text x, a model f with m labels, the confidence score c, the verification of local robustness verify(x) can be represented as: the problem of robustness verification is actually an np-hard problem due to the discreteness of the textual input and the non-convexity of the deep neural networks @xcite . this paper aims to tackle this challenging problem by providing upper and lower bounds on this maximum safe radius, with a provable guarantee that the upper and lower bounds will optimize as the computation proceeds and eventually converge to the maximum safe radius. the key novelty of our solution lies in the anytime manner, i.e., whenever interrupting the computation, our method can return certifiable upper and lower bounds for radius approximation, as illustrated in figure 1 . per bound computation) for robustness verification, as shown in figure 2 . the details of our anytime mechanism for approximation-based estimation of the maximal safe radius will be explained in the next section. ## anytime estimation and convergence guarantees we propose a safe-radius estimation method for obtaining an anytime robustness computation, ensuring the estimation results are controllable and flexible with convergence ultimately. ## experimental part as stated in section 2, previous research on robustness verification was mainly focused on l 2 and l ∞ space, which is different from our l 0 norm setting. moreover, since our method approximates the maximal safe radius from both lower and upper sides in a black-box manner, it effectively verifies the local robustness of large-scale, complex model structures such as large bert models under l 0 norm. in this sense, it is difficult to find a verification baseline that has the same capability. therefore, we evaluate the competitive tightness of upper bounds for approximating the maximal safe radius in subsection-6.2. moreover, we provide further experiments on both bounds in subsection-6.3 and appendix-b.4, demonstrating the convergence performance for robustness verification. ## conclusion the proposed strategy can verify the local robustness of nlp classifiers in hamming space against word-level attacks with provable guarantees. a reliable anytime estimation effectively incorporates the computation of the upper and lower bounds to enable a controllable approximation of the maximal safe radius. moreover, our framework is performed on a carefully-designed novel parallelization mechanism, ensuring its high efficiency. the extensive experiments demonstrate the competence of our method in obtaining very tight bounds for the maximal safe radius. our textverifier tool also shows superior performance in terms of computational runtime, and provable convergence guarantees.