Source-linked AI summary
Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation
Po-Sen Huang, Robert Stanforth, Johannes Welbl, Chris Dyer, Dani Yogatama, Sven Gowal, Krishnamurthy Dvijotham, Pushmeet Kohli
TL;DR
Neural NLP models remain vulnerable to discrete adversarial text perturbations that heuristic defenses may not exhaustively cover. The paper models synonym and character substitutions as a simplex, applies IBP, and trains models using efficiently computable bounds. Verifiably trained models achieve the highest exhaustive verification accuracy on SST and AG News while retaining comparable nominal performance, within a scope limited to shallow CNN and fully connected models.
Problem
Neural NLP defenses based on adversarial training and augmentation may miss worst-case attacks in the complex space of discrete text perturbations.
Method
The paper represents synonym and character perturbations as a simplex, uses Interval Bound Propagation for verification, and derives a training objective from efficiently computed bounds.
Results
Verifiably trained models achieve the highest exhaustive verification accuracy on SST and AG News, with comparable nominal test accuracy and exponentially more efficient IBP verification than exhaustive search.
Takeaways & Limitations
Simplex bounds with IBP provide an efficiently computable formal guarantee against the specified synonym and character perturbations.
Takeaways & Limitations
The study investigates only few-layer models with CNN and fully connected architectures, and IBP bounds may loosen as model depth increases.
Abstract
from arXiv · showhide
Neural networks are part of many contemporary NLP systems, yet their empirical successes come at the price of vulnerability to adversarial attacks. Previous work has used adversarial training and data augmentation to partially mitigate such brittleness, but these are unlikely to find worst-case adversaries due to the complexity of the search space arising from discrete text perturbations. In this work, we approach the problem from the opposite direction: to formally verify a system's robustness against a predefined class of adversarial attacks. We study text classification under synonym replacements or character flip perturbations. We propose modeling these input perturbations as a simplex and then using Interval Bound Propagation -- a formal model verification method. We modify the conventional log-likelihood training objective to train models that can be efficiently verified, which would otherwise come with exponential search complexity. The resulting models show only little difference in terms of nominal accuracy, but have much improved verified accuracy under perturbations and come with an efficiently computable formal guarantee on worst case adversaries.
1 Introduction
Neural NLP models are vulnerable to semantically invariant adversarial text changes, while adversarial training and augmentation do not guarantee protection against stronger attacks. This paper instead formally verifies robustness to specified synonym and character substitutions using simplex modeling and IBP.
- Small, semantically invariant text alterations can cause drastic prediction changes in neural NLP models.
- Adversarial training and data augmentation improve adversarial-example accuracy but do not guarantee robustness against stronger attacks.
- Formal verification provides provable guarantees that a model satisfies a specified robustness condition for all allowed perturbations.
- The paper models synonym and character substitutions as a simplex and applies Interval Bound Propagation to compute worst-case specification bounds.
- An auxiliary training objective produces efficiently verifiable classifiers with improved adversarial robustness and comparable nominal test accuracy.
- The work introduces verification and verifiable training for neural networks in natural language processing.
2 Related Work
Prior NLP defenses target adversarial examples, while formal verification methods trade exactness for scalability. This paper extends incomplete verification to text classification by representing substitution perturbations on a simplex and optimizing worst-case bounds.
- The paper studies word- and character-level HotFlip attacks based on synonym and character replacements.
- It compares the verifiable approach with adversarial training and data augmentation defenses.
- Complete verification methods provide exact robustness bounds through exhaustive search but are expensive and difficult to scale.
- Incomplete methods use convex relaxations to obtain looser but more scalable bounds that can support robust model training.
- This work extends incomplete verification to text classification by modeling input perturbations on a simplex and minimizing worst-case attack bounds.
- Word lattices and hypergraphs compactly represent exponentially many sentence alternatives without exhaustive enumeration.
3 Methodology
The method formally verifies prediction consistency over bounded synonym or character substitutions by over-approximating the perturbation space with a simplex and propagating interval bounds through the network. It also trains models against worst-case logit bounds so verification remains computationally tractable.
- 3.1 Verification: Verification requires every perturbed input in Xin(x0) to satisfy an output constraint, with the true-class logit at least as large as every competing logit.This ensures predictions remain constant across the specified synonym or character substitutions.
- 3.3 Modeling Input Perturbations using Simplices: The attack space contains sentences formed by up to δ synonym or character substitutions, but an axis-aligned embedding box can over-approximate it by allowing all symbols to change simultaneously.This loose relaxation makes interval bounds less informative for sparse symbol substitutions.
- 3.3 Modeling Input Perturbations using Simplices: The proposed simplex is a tighter over-approximation built from the unperturbed sentence and elementary one-substitution perturbations, then dilated to cover up to δ substitutions.For δ > 1, the dilated simplex retains M + 1 vertices while containing the exponentially growing perturbation set.
- 3.4 Interval Bound Propagation: The simplex is propagated through each network layer by computing lower and upper activation bounds with interval arithmetic rather than explicitly constructing the convex hull.For the first layer, bounds can be computed by passing each perturbation vertex through the layer; subsequent layers propagate interval bounds recursively.
- 3.4 Interval Bound Propagation: The output-logit bounds provide an efficiently computable upper bound on the worst-case verification objective, using the true class lower bound and competing-class upper bounds.The resulting bound requires only two forward passes for upper and lower bounds through the network and is used to define a verifiable-training loss.
4 Experiments
The experiments compare normal, adversarial, data-augmentation, and IBP-verifiable training for character- and word-level text classification under discrete perturbations. IBP training improves verified robustness while retaining comparable nominal performance and avoids exhaustive search over exponentially growing perturbation spaces.
- 4.3 Setup: The study evaluates SST and AG News models against character typos or synonym substitutions, using nominal, adversarial, and exhaustively verified accuracy.The SST experiments include both word- and character-level settings, while AG News uses character-level experiments.
- 4.3 Setup: The baselines are normal training, adversarial training, and data augmentation, alongside verifiable training based on simplex bounds with IBP.Adversarial training searches for HotFlip examples, data augmentation samples valid perturbations, and verifiable training optimizes IBP-derived bounds.
- 4.5 Results: 74.9 / 76.8 / 85.5% adversarial accuracy for adversarially trained models falls to 25.8 / 74.6 / 81.6% under exhaustive oracle evaluation across SST-character, SST-word, and AG-character settings.The gap shows that defending against HotFlip does not ensure robustness against the strongest perturbations in the defined space.
- 4.5 Results: IBP-trained models achieve the highest exhaustively verified accuracy with only moderate nominal-accuracy deterioration.IBP training covers the full perturbation simplex rather than sampling individual points.
- 4.5 Results: 73.1% versus 25.8% and 76.5% versus 74.6% are the oracle-robustness comparisons between IBP and adversarial training in the larger SST-character and SST-word perturbation spaces.The larger perturbation space produces a larger gap between adversarial accuracy and true robustness, and magnifies the advantage of IBP over adversarial training.
- 4.6 Computational Cost: IBP verification requires two forward passes per sample, whereas exhaustive verification needs several orders of magnitude more and becomes prohibitively expensive as perturbation budgets grow.The perturbation space grows exponentially with the budget, while IBP provides constant-time verification for arbitrary δ.
5 Discussion
The experiments show that adversarial attacks may miss worst-case inputs, while exhaustive verification is expensive. Simplex bounds with IBP offer a scalable verification approach, but the study is limited to shallow CNN and fully connected models.
- Adversarial attacks are not always the worst adversarial inputs, which verification can reveal.
- Exhaustive verification is computationally very expensive because perturbation spaces grow exponentially with the perturbation radius.
- Simplex bounds with IBP can verify a sizable number of test samples and provide a potent NLP verification method.
- The work studies only few-layer models with CNN and fully connected architectures, and IBP bounds may loosen as depth increases.
- The study investigates HotFlip symbol substitutions, while noting that the framework could extend to lexical entailment perturbations and prefix or suffix additions.
6 Conclusion
The paper introduces formal verification for text classification models under synonym and character-flip perturbations. Its experiments find that IBP-based simplex bounds improve verification efficiency and accuracy relative to exhaustive-search alternatives.
- The paper introduces formal verification of text classification models against synonym and character-flip perturbations.
- Verifiably trained models achieve the highest exhaustive verification accuracy on SST and AG News.
- IBP verifies models in constant time, exponentially outperforming naive verification through exhaustive search.
- Experiments demonstrate the effectiveness of simplex bounds with IBP during both training and testing, while exposing weaknesses of adversarial training under exhaustive verification.
A.1 Dataset Statistics
The experiments use SST and AG News, with model architectures selected to trade off nominal and robust accuracy. SST models use fixed pre-trained embeddings, and training uses Adam with validation-based early stopping and hyperparameter tuning.
- SST contains 67,349 training, 872 validation, and 1,821 test samples with binary sentiment labels, while AG News contains 120,000 training and 7,600 test samples across four classes.
- SST word-level experiments use a one-layer convolutional network with 100 width-5 kernels, ReLU, average pooling, and a linear layer.
- The SST word-level models use fixed pre-trained 300-dimensional GloVe embeddings, with counter-fitted embeddings used in a separate experiment.
- Models are selected using the validation set to trade off nominal and robust accuracy.
- Training uses Adam, early stopping, and validation-set tuning of the learning rate and loss ratio κ.
B.1 Ease of Verification (Computation of True Robustness)
Exhaustive verification computes true robustness but is extremely expensive, whereas IBP supplies a cheaper bound. IBP-verifiable training tightens these bounds and improves verification rates with little or no nominal-accuracy deterioration.
- Exhaustive verification computes true robustness but is extremely computationally expensive, especially for character-level perturbations.
- IBP provides a lower bound on worst-case results, though the bound is generally loose for arbitrary networks.
- IBP-verifiable training tightens verification bounds and substantially improves test-time IBP verification rates compared with other training methods.
- Models trained with the IBP objective achieve better adversarial and exhaustively verified accuracy with small or no nominal-accuracy deterioration compared with normal training.
B.3 AG News
On AG News character-level models, verifiable training delivers the strongest adversarial and oracle accuracy while producing tight bounds to oracle results. IBP verification is also far cheaper than exhaustive evaluation.
- Figure 7 compares normal, adversarial, augmented, and verifiable training across nominal, adversarial, oracle, and IBP verified accuracy under varying perturbation budgets.
- Verifiable training achieves the strongest adversarial and oracle accuracy among the evaluated AG News character-level models.
- IBP verification requires 2 forward passes, whereas exhaustive oracle evaluation uses up to 260,282 forward passes for one example at δ = 2.