Formalization of deep learning techniques with the Why3 proof platform

Abstract

Machine Learning como um campo, parte integrante da área de Inteligência Artificial, tem crescido exponencialmente, principalmente nesta última década, onde passou de quase desconhecido pelo público em geral para a existência de carros autónomos e até robôs humanóides como o robô Sophia da Arábia Saudita. A maioria de nós agora lida com Inteligência Artificial todos os dias, em anúncios direcionados por exemplo, o que é agora a norma. Deep Learning, um ramo específico de Machine Learning de onde originaram as Redes Neuronais, é vastamente utilizado no desenvolvimento de sistemas autónomos de alta complexidade. Alguns destes sistemas em particular podem ser classificados como sistemas críticos, o que traz a necessidade de fornecer alguma forma de garantia de que estes sistemas vão sempre funcionar como é suposto, uma vez que qualquer falha em sistemas desta categoria pode ter consequências graves. Isto naturalmente levanta preocupações relativas à segurança, levando a comunidade a procurar uma forma de obter tais garantias, eventualmente levando-os aos métodos de Verificação Formal para atingir os níveis de confiabilidade necessários para a adoção pública de tais sistemas. Tem havido um interesse crescente quanto a este assunto, uma vez que as aplicações de Redes Neuronais estão em constante expansão, e muitas ferramentas de software já resultaram deste trabalho, sendo algumas dessas ferramentas analisadas nesta dissertação. Este estudo vem contribuir para esse esforço, e tem como objetivo principal a avaliação do Why3, a fim de compreender se esta ferramenta possui as características necessárias que lhe permitam juntar-se a estas ferramentas já existentes como um novo meio de verificação da correção de Redes Neuronais. Para atingir este objetivo, primeiramente criamos um proof-of-concept a fim de analisar se o Why3 fornece o suporte necessário para esta tarefa. Em seguida, damos um passo em frente e formalizamos uma Rede Neuronal à escala de uma aplicação real no Why3, de onde tiraremos as nossas conclusões. Durante o trabalho sobre a formalização de Redes Neuronais, pretendemos também compilar um guia abrangente sobre Why3, desde as funcionalidades que oferece, até exemplos de como pode ser aplicado explicados passo a passo, com o objetivo de oferecer uma base de conhecimento compreensiva para qualquer pessoa interessada em explorar o Why3, contribuindo ao mesmo tempo para a escassa documentação existente sobre o Why3.

Machine Learning as a field, from the realms of Artificial Intelligence, has been growing exponentially, especially in this last decade, where it went from the general public barely even hearing about it to the existence of self-driving cars and even humanoid robots like the Saudi Arabian Sophia. Most of us now deal with AI everyday, in targeted ads for example, and it has become the norm. Deep Learning, a particular branch of Machine Learning from where Neural Networks stem, is widely used in the development of high-complexity autonomous systems. Some of these systems in particular can be classified as critical systems, which brings the necessity of providing some form of guarantee that these will always work as intended, since any failure from this category of systems can have serious consequences. This naturally raises security concerns, hence leading the community to search for a way of attaining such guarantees, eventually leading them to Formal Verification methods to achieve the necessary reliability levels for the public adoption of said systems. There has been a growing interest regarding this matter, since the applications of Neural Networks are continuously expanding, and many software tools have already resulted from this work, some of which will be analysed in this dissertation. This study comes to contribute to this effort, and has as its main objective the evaluation of Why3, in order to understand if this tool possesses the necessary characteristics that may allow it to join these already existing tools as a new mean of verifying the correctness of Neural Networks. To achieve this objective, firstly we create a proof-of-concept in order to analyse if Why3 provides the necessary support for this task. Then we go a step further and formalize a real life application scale Neural Network in Why3, from where we will draw our conclusions. While working on the formalization of Neural Networks, we also aim to compile a comprehensive guide on Why3, where we go from the functionalities that it provides, to examples of how it can be applied explained step by step, with the goal of offering an understandable knowledge base for anyone that may be interested in exploring Why3, while also contributing to the scarce existing documentation of Why3.