Active learning of regular languages as an approach to neural language models verification.

Abstract

This work tackles the general problem of verifying the behavior of sequence processing neural networks, specifically neural acceptors and neural language models. The contribution is a framework for extracting formal abstractions of the networks under analysis and verifying whether they satisfy given requirements. This process steps on two core ideas: 1) treating the neural network as a black box, and 2) using a probabilistic framework to analyze how much the extracted model approximates the original one. For this matter, a series of active learning algorithms and techniques are proposed, developed and analyzed. For the case of neural acceptors a procedure for checking properties of neural networks is presented. This approach is able to check properties without explicitly building representations of the network. We show that this approach offers better guarantees and is more efficient than post-learning verification where the property is checked on a learned model of the network. Besides, it does not require resorting to an external decision procedure for verification nor fixing a specific requirement specification formalism. For the case of neural language models, a learning algorithm based on a congruence over strings which is parameterized by an equivalence relation over probability distributions is presented. The learning algorithm is implemented using a tree data structure and shown to be empirically more efficient than reference techniques.

El presente trabajo aborda el problema general de la verificación del comportamiento de redes neuronales que procesan secuencias, en concreto los aceptores neuronales y los modelos neuronales de lenguaje. La tesis desarrolla un marco teórico-práctico para la extracción de abstracciones formales y la verificación de las redes neuronales bajo análisis. Este proceso se basa en dos ideas centrales: 1) tratar la red neuronal como una caja negra, y 2) utilizar un marco probabilístico para analizar en que medida el modelo extraído se aproxima al original. Para ello, se proponen, desarrollan y analizan una serie de algoritmos y técnicas de aprendizaje activo. Para el caso de los aceptores neuronales se presenta un procedimiento de verificación de propiedades de redes neuronales. Este enfoque es capaz de verificar propiedades sin construir explícitamente representaciones de la red. Se demuestra que este enfoque ofrece mejores garantías y es mas eficiente que la verificación posterior al aprendizaje, en la que la propiedad se verifica únicamente sobre el modelo aprendido de la red. Además, no requiere recurrir a un procedimiento de decisión externo para la verificación ni fijar un formalismo específico de especificación de requisitos. Para el caso de los modelos neuronales de lenguaje se presenta un algoritmo de aprendizaje basado en una congruencia sobre secuencias que se parametriza mediante una relación de equivalencia sobre distribuciones de probabilidad. El algoritmo de aprendizaje se implementa utilizando una estructura de datos en árbol y se muestra que es empíricamente mas eficiente que las técnicas de referencia.