TitleData Hallucination, Falsification and Validation using Generative Models and Formal Methods
Publication TypeThesis
Year of Publication2018
AuthorsValle, R
Academic DepartmentComputational and Data Science and Engineering
DegreeDoctor of Philosophy
Number of Pages84
Date Published2/22/2018
Thesis TypeDissertation
Keywordsfalsification, formal, generative, hallucination, machine learning, validation

The increasing pervasiveness and fast-paced development of deep learning (DL) systems with human-like perception, agency and creativity has brought concern related to information reliability: the generative models that have surprised and confused humans with their high quality media hallucinations can be used to fool other computer systems and humans to believe that the generated media is real. In addition to developing strategies to increase the quality of the data produced with generative models, specially generative adversarial networks (GANs), our research community has been exploring mechanisms to better understand and control the data they generate.

In the context of data falsification, formal methods (FM) and formal specifications (FS) can be used to prevent adversarial attacks by verifying that some potentially adversarial data follows the specifications of the real data. Formal methods and formal specifications can also be used to guide the output of a generator such that, as much as possible, the generated data fulfills the specifications of the real data. Although formal methods have been largely and sucessfuly used in the field of software and hardware engineering, their interaction with Artificial Neural Networks (ANNs) poses many challenges that are yet to be solved.

In this thesis, we address challenges related to hallucination, falsification and validation of data using generative models and formal methods. We start by focusing on artistic applications related to music by developing an automata-based system for machine improvisation with formal specifications. We briefly describe the Control Improvisation framework and describe its application to machine improvisation with formal specifications. We propose data abstractions derived from symbolic music data and describe strategies for mining specifications from them. We then use the mined specification to summarize a musical style and guide the improvisation of a generative model.

Next, we focus on security applications in speech synthesis and investigate the efficiency of generative models such as WaveNet, SampleRNN and our own GAN 2 model in performing spoofing attacks to fool a text-independent speaker recognition system. Inspired by universal background models (UBMs) in speech, we propose a modification to the Wasserstein GAN objective function such that data from multiple speakers can be used to generate data from a single speakers, increasing the efficiency of our spoofing attacks.

Last, in the hope of preventing adversarial attacks produced with data synthesized by generative models, specially GANs, we look at the properties of synthesized samples hoping to find traces of the data generation process that can be used to identify the data as adversarial. We empirically show that the data produced with these generative models do not follow the specifications of the real data and that they have universal properties, byproducts from the models and the algorithms used to train them, that can be used to identify the source of the data.