# NLP Verification: Towards a General Methodology for Certifying Robustness

arXiv: https://arxiv.org/abs/2403.10144 · HTML: https://mlsanity.com/paper/2403.10144/

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- Builds on 44 of its 74 references that are in the map.
- First posted on arXiv 15 Mar 2024.

## Builds on (most cited first, 30 of 44)

- [Faster R-CNN: Towards Real-Time Object Detection with Region Proposal Networks](https://mlsanity.com/paper/1506.01497/) (2015)
- [TruthfulQA: Measuring How Models Mimic Human Falsehoods](https://mlsanity.com/paper/2109.07958/) (2021)
- [Character-level Convolutional Networks for Text Classification](https://mlsanity.com/paper/1509.01626/) (2015)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Is BERT Really Robust? A Strong Baseline for Natural Language Attack on Text Classification and Entailment](https://mlsanity.com/paper/1907.11932/) (2019)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [A Survey of Data Augmentation Approaches for NLP](https://mlsanity.com/paper/2105.03075/) (2021)
- [TextBugger: Generating Adversarial Text Against Real-world Applications](https://mlsanity.com/paper/1812.05271/) (2018)
- [Black-box Generation of Adversarial Text Sequences to Evade Deep Learning Classifiers](https://mlsanity.com/paper/1801.04354/) (2018)
- [Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers](https://mlsanity.com/paper/1906.04584/) (2019)
- [Style Transfer from Non-Parallel Text by Cross-Alignment](https://mlsanity.com/paper/1705.09655/) (2017)
- [MiniLMv2: Multi-Head Self-Attention Relation Distillation for Compressing Pretrained Transformers](https://mlsanity.com/paper/2012.15828/) (2020)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Polyjuice: Generating Counterfactuals for Explaining, Evaluating, and Improving Models](https://mlsanity.com/paper/2101.00288/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Data Augmentation Can Improve Robustness](https://mlsanity.com/paper/2111.05328/) (2021)
- [Certified Adversarial Robustness with Additive Noise](https://mlsanity.com/paper/1809.03113/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Measure and Improve Robustness in NLP Models: A Survey](https://mlsanity.com/paper/2112.08313/) (2021)
- [SoK: Certified Robustness for Deep Neural Networks](https://mlsanity.com/paper/2009.04131/) (2020)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Evaluating the Robustness of Neural Language Models to Input Perturbations](https://mlsanity.com/paper/2108.12237/) (2021)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [SAFER: A Structure-free Approach for Certified Robustness to Adversarial Word Substitutions](https://mlsanity.com/paper/2005.14424/) (2020)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Certified Robustness to Text Adversarial Attacks by Randomized [MASK]](https://mlsanity.com/paper/2105.03743/) (2021)
- [Searching for an Effective Defender: Benchmarking Defense against Adversarial Word Substitution](https://mlsanity.com/paper/2108.12777/) (2021)
- [Black-Box Certification with Randomized Smoothing: A Functional Optimization Based Framework](https://mlsanity.com/paper/2002.09169/) (2020)

## Built on by (most cited first, 16 of 16)

- [Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations](https://mlsanity.com/paper/2506.08505/) (2025)
- [A Neurosymbolic Approach to Natural Language Formalization and Verification](https://mlsanity.com/paper/2511.09008/) (2025)
- [Shh, don't say that! Domain Certification in LLMs](https://mlsanity.com/paper/2502.19320/) (2025)
- [Towards Formal Verification of Deep Neural Networks for Object Detection](https://mlsanity.com/paper/2407.01295/) (2024)
- [Beyond Benchmarks: On The False Promise of AI Regulation](https://mlsanity.com/paper/2501.15693/) (2025)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [How Catastrophic is Your LLM? Certifying Risk in Conversation](https://mlsanity.com/paper/2510.03969/) (2025)
- [Floating-Point Neural Network Verification at the Software Level](https://mlsanity.com/paper/2510.23389/) (2025)
- [BEAVER: An Efficient Deterministic LLM Verifier](https://mlsanity.com/paper/2512.05439/) (2025)
- [Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture](https://mlsanity.com/paper/2605.16407/) (2026)
- [A General Framework for Property-Driven Machine Learning](https://mlsanity.com/paper/2505.00466/) (2025)
- [Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline](https://mlsanity.com/paper/2604.18882/) (2026)
- [Extensional Properties of Recurrent Neural Networks](https://mlsanity.com/paper/2410.22730/) (2024)
- [Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement](https://mlsanity.com/paper/2605.14294/) (2026)
- [Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees](https://mlsanity.com/paper/2608.17070/) (2026)

## Abstract (arXiv)

Machine Learning (ML) has exhibited substantial success in the field of Natural Language Processing (NLP). For example large language models have empirically proven to be capable of producing text of high complexity and cohesion. However, they are prone to inaccuracies and hallucinations. As these systems are increasingly integrated into real-world applications, ensuring their safety and reliability becomes a primary concern. There are safety critical contexts where such models must be robust to variability or attack, and give guarantees over their output. Computer Vision had pioneered the use of formal verification of neural networks for such scenarios and developed common verification standards and pipelines, leveraging precise formal reasoning about geometric properties of data manifolds. In contrast, NLP verification methods have only recently appeared in the literature. While presenting sophisticated algorithms, these papers have not yet crystallised into a common methodology. They are often light on the pragmatical issues of NLP verification and the area remains fragmented. In this paper, we attempt to distil and evaluate general components of an NLP verification pipeline, that emerges from the progress in the field to date. Our contributions are two-fold. Firstly, we propose a general methodology to analyse the effect of the embedding gap, a problem that refers to the discrepancy between verification of geometric subspaces and the semantic meaning of sentences, which the geometric subspaces are supposed to represent. We propose a number of practical NLP methods that can help to quantify the effects of the embedding gap. Secondly, we give a general method for training and verification of neural networks that leverages a more precise geometric estimation of semantic similarity of sentences in the embedding space and helps to overcome the effects of the embedding gap in practice.