Certified Robustness to Programmable Transformations in LSTM s (2021)

Abstract: Deep neural networks for natural language processing are fragile in the face of adversarial examples—small input perturbations, like synonym substitution or word duplication, which cause a neural network to change its prediction. We present an approach to certifying the robustness of LSTMs (and extensions of LSTMs) and training models that can be efficiently certified. Our approach can certify robustness to intractably large perturbation spaces defined programmatically in a language of string transformations. Our evaluation shows that (1) our approach can train models that are more robust to combinations of string transformations than those produced using existing techniques; (2) our approach can show high certification accuracy of the resulting models.

## introduction adversarial examples are small perturbations of an input that fool a neural network into changing its prediction @xcite . in nlp, adversarial examples involve modifying an input string by, for example, replacing words with synonyms, deleting stop words, inserting words, etc. @xcite @xcite . ideally, a defense against adversarial examples in nlp tasks should fulfill the following desiderata: (1) handle recursive models, like lstms and extensions thereof, which are prevalent in nlp. (2) construct certificates (proofs) of robustness. (3) defend against arbitrary string transformations, like combinations of word deletion, insertion, etc. it is quite challenging to fulfill all three desiderata; indeed, existing techniques are forced to make tradeoffs. for instance, the theoretical insights underlying a number of certification approaches are intimately tied to symbol substitution @xcite @xcite @xcite , and some techniques cannot handle recursive models @xcite . on the other hand, techniques that strive to be robust to arbitrary string transformations achieve this at the expense of certification @xcite . in this paper, we ask: can we develop a certified defense to arbitrary string transformations that applies to recursive neural networks? our approach. certifying robustness involves proving that a network's prediction is the same no matter how a given input string is perturbed. we assume that the perturbation space is defined as a program describing a set of possible string transformations @xcite )-e.g., if you see the word "movie", replace it with "film" or "movies". such transformations can succinctly define a perturbation space that is exponentially large in the length of the input; so, certification by enumerating the perturbation space is generally impractical. we present arc (abstract recursive certification), an approach for certifying robustness to programmatically defined perturbation spaces. arc can be used within an adversarial training loop to train robust models. we illustrate the key ideas behind arc through a simple example. consider the (partial) input sentence to the movie..., and say we are using an lstm for prediction. say we have two string transformations: (t1) if you see the word movie, you can replace it with film or movies. (t2) if you see the word the or to, you can delete it. arc avoids enumerating the large perturbation space (fig. 1(a )) using two key insights. memoization: arc exploits the recursive structure of lstm networks, and their extensions (bil-stms, treelstms), to avoid recomputing intermediate hidden states. arc memoizes hidden states of prefixes shared across multiple sequences in the perturbation space. for example, the two sentences to the movie... and to the film.... share the prefix to the, and therefore we memoize the hidden state after the word the, as illustrated in fig. 1(b) with dashed blue lines. the critical challenge is characterizing which strings share prefixes without having to explicitly explore the perturbation space. abstraction: arc uses abstract interpretation @xcite to symbolically represent sets of perturbed strings, avoiding a combinatorial explosion. specifically, arc represents a set of strings as a hyperrectangle in a r n and propagates the hyperrectangle through the network using interval arithmetic @xcite .this idea is illustrated in fig. 1(b) , where the words film and movies are represented as a hyperrectangle. by joining hidden states of different sentences (a common idea in program analysis), arc can perform certification efficiently. memoization and abstraction enable arc to efficiently certify robustness to very large perturbation spaces. note that arc subsumes @xcite because arc can certify arbitrary string transformations, while @xcite only works on word substitutions. contributions. we make the following contributions: (1) we present arc, an approach for training certifiably robust recursive neural networks. we demonstrate our approach on lstms, bilstms, and treelstms. (2) we present a novel application of abstract interpretation to symbolically capture a large space of strings, defined programmatically, and propagate it through a recursive network (section 4). (3) our evaluation shows that arc can train models that are more robust to arbitrary perturbation spaces than those produced by existing techniques; arc can show high certification accuracy of the resulting models; and arc can certify robustness to attacks (transformations) that are out-of-scope for existing techniques (section 5). ## related work certification of robustness in nlp. see @xcite for a survey of robust training. some works focus on certifying the l p norm ball of each word embedding for lstms @xcite and transformers @xcite . others focus on certifying word substitutions for cnns @xcite and lstms @xcite , and word deletions for the decomposable attention model @xcite . existing techniques rely on abstract interpretation, such as ibp @xcite and crown @xcite . we focus on certifying the robustness of lstm models (including treelstms) to a programmable perturbation space, which is out-of-scope for existing techniques. note that @xcite also uses memoization and abstraction to certify, but arc subsumes @xcite because arc can certify arbitrary string transformations. we use ibp, but our approach can use other abstract domains, such as zonotopes @xcite . safer @xcite ) is a model-agnostic approach that uses randomized smoothing @xcite to give probabilistic certificates of robustness to word substitution. our approach gives a non-probabilistic certificate and can handle arbitrary perturbation spaces beyond substitution. robustness techniques in nlp. adversarial train-ing is an empirical defense method that can improve the robustness of models by solving a robust-optimization problem @xcite , which minimizes worst-case (adversarial) loss. some techniques in nlp use adversarial attacks to compute a lower bound on the worst-case loss @xcite . ascc @xcite overapproximates the word substitution attack space by a convex hull where a lower bound on the worst-case loss is computed using gradients. other techniques compute upper bounds on adversarial loss using abstract interpretation @xcite . @xcite al. (2019) and jia et al. (2019); xu et al. (2020) used abstract interpretation to train cnn and lstm models against word substitutions. a3t @xcite trains robust cnn models against a programmable perturbation space by combining adversarial training and abstraction. our approach uses abstract interpretation to train robust lstms against programmable perturbation spaces as defined in @xcite . ## robustness problem and preliminaries we consider a classification setting with a neural network f θ with parameters θ, trained on samples from domain x and labels from y. the domain x is a set of strings over a finite set of symbols σ (e.g., english words or characters), i.e., @xmath0. we use @xmath1; x @xmath2; x i:j to denote the substring x i , . . . , x j ; to denote the empty string; and len x to denote the length of the string. robustness to string transformations. a perturbation space s is a function in σ * → 2 σ * , i.e., s takes a string x and returns a set of possible perturbed strings obtained by modifying x. intuitively, s(x) denotes a set of strings that are semantically similar to x and therefore should receive the same prediction. we assume @xmath3. given string x with label y and a perturbation space s, we say that a neural network f θ is srobust on (x, y) iff ∀@xmath4. f θ (z) = y (1) our primary goal in this paper is to certify, or prove, s-robustness (eq 1) of the neural network for a pair (x, y). given a certification approach, we can then use it within an adversarial training loop to yield certifiably robust networks. robustness certification. we will certify srobustness by solving an adversarial loss objective: certified training. if we have a procedure to compute adversarial loss, we can use it for adversarial training by solving the following robust optimization objective @xcite , where d is the data distribution: ## arc: abstract recursive certification in this section, we present our technique for proving s-robustness of an lstm on (x, y). formally, we do this by computing the adversarial loss, max @xmath5, y). recall that if the solution @xmath6, then we have proven s-robustness. to solve adversarial loss optimally, we effectively need to evaluate the lstm on all of s(x) and collect all final states: computing f precisely is challenging, as s(x) may be prohibitively large. therefore, we propose to compute a superset of f , which we will call f . this superset will therefore yield an upper bound on the adversarial loss. we prove s-robustness if the upper bound @xmath7. to compute f , we present two key ideas that go hand-in-hand: in section 4.1, we observe that strings in the perturbation space share common prefixes, and therefore we can memoize hidden states to reduce the number of evaluations of lstm cells-a form of dynamic programming. we carefully derive the set of final states f as a system of memoizing equations. the challenge of this derivation is characterizing which strings share common prefixes without explicitly exploring the perturbation space. in section 4.2, we apply abstract interpretation to efficiently and soundly solve the system of memoizing equations, thus computing an overapproximation f ⊇ f . ## evaluation we implemented arc in pytorch. the source code is available online foot_0 and provided in the supplementary materials. ## conclusion we present arc, which uses memoization and abstract interpretation to certify robustness to programmable perturbations for lstms. arc can be used to train models that are more robust than those trained using existing techniques and handle more complex perturbation spaces. last, the models trained with arc have high certification accuracy, which can be certified using arc itself.