Verification of machine learning models used in Natural Language Processing (NLP) is known to be a hard problem. In particular, many known neural network verification methods that work for computer vision and other numeric datasets do not work for NLP. Here, we study technical reasons that underlie this problem. Based on this analysis, we propose practical methods and heuristics for preparing NLP datasets and models in a way that renders them amenable to known verification methods based on abstract interpretation. We implement these methods as a Python library called ANTONIO that links to the neural network verifiers ERAN and Marabou. We perform evaluation of the tool using an NLP dataset R-U-A-Robot suggested as a benchmark for verifying legally critical NLP applications. We hope that, thanks to its general applicability, this work will open novel possibilities for including NLP verification problems into neural network verification competitions, and will popularise NLP problems within this community.

翻译：自然语言处理中机器学习模型的验证被公认为一个难题。具体而言，许多适用于计算机视觉及其他数值数据集的神经网络验证方法无法直接应用于NLP领域。本文首先探究了导致该问题的技术根源，并基于分析结果提出了一系列实用方法与启发式策略，通过特定的数据集与模型构建方式使其能够适配基于抽象解释的现有验证方法。我们以Python库形式实现这些方法，并将其命名为ANTONIO，该工具可与ERAN和Marabou等神经网络验证器协同工作。利用面向法律关键型NLP应用验证的基准数据集R-U-A-Robot，我们对工具进行了评估。我们期望凭借其通用性，本研究能为将NLP验证问题纳入神经网络验证竞赛开辟新途径，并推动该领域对NLP问题的关注普及。