Deep neural networks have exhibited substantial success in the field of Natural Language Processing (NLP) and ensuring their safety and reliability is crucial: there are safety critical contexts where such models must be robust to variability or attack, and give guarantees over their output. Unlike Computer Vision, NLP lacks a unified verification methodology and, despite recent advancements in literature, they are often light on the pragmatical issues of NLP verification. In this paper, we make an 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 give a general characterisation of verifiable subspaces that result from embedding sentences into continuous spaces. We identify, and give an effective method to deal with, the technical challenge of semantic generalisability of verified subspaces; and propose it as a standard metric in the NLP verification pipelines (alongside with the standard metrics of model accuracy and model verifiability). Secondly, we propose a general methodology to analyse the effect of the embedding gap, a problem that refers to the discrepancy between verification of geometric subpspaces on the one hand, and semantic meaning of sentences which the geometric subspaces are supposed to represent, on the other hand. In extreme cases, poor choices in embedding of sentences may invalidate verification results. We propose a number of practical NLP methods that can help to identify the effects of the embedding gap; and in particular we propose the metric of falsifiability of semantic subpspaces as another fundamental metric to be reported as part of the NLP verification pipeline. We believe that together these general principles pave the way towards a more consolidated and effective development of this new domain.

翻译：深度神经网络在自然语言处理（NLP）领域取得了显著成功，确保其安全性与可靠性至关重要：在安全关键场景下，这类模型必须对数据变异或攻击具有鲁棒性，并为其输出提供保障。与计算机视觉不同，NLP缺乏统一的验证方法论，尽管近年来文献中取得了进展，但这些研究往往对NLP验证的实践性问题涉及不足。本文尝试提炼并评估NLP验证流水线中的通用组件，这些组件源自该领域迄今取得的进展。我们的贡献包含两个方面。首先，我们对将句子嵌入连续空间所得到的可验证子空间进行了通用刻画；识别并提出了处理已验证子空间语义泛化性技术挑战的有效方法，并将其作为NLP验证流水线的标准度量指标（与模型准确率和模型可验证性等标准度量指标并列）。其次，我们提出了一种通用方法论来分析嵌入间隙的影响——该问题涉及几何子空间验证与几何子空间本应表示的句子语义之间存在的差异。在极端情况下，句子嵌入的不良选择可能导致验证结果失效。我们提出了一系列实用NLP方法，有助于识别嵌入间隙的影响，特别地，我们提出将语义子空间的可证伪性度量作为NLP验证流水线中需报告的另一基础度量。我们相信，这些通用原则共同为该新兴领域的整合化与高效化发展铺平了道路。