Verificação formal de redes neurais via lógica infinitamente-valorada de Lukasiewicz

Resumo

Uma forma de contornar o problema do método da caixa preta sofrido por redes neurais e viabilizar sua aplicação em situações críticas é fazendo a verificação formal de propriedades desejáveis nestas redes. A área da verificação formal de redes neurais é recente e há desafios serem enfrentados; para isso, a comunidade propôs benchmarks e competições para comparar a eficiência dos métodos propostos. Este projeto de pesquisa visa estabelecer tais métodos formalizando propriedades sobre redes neurais na linguagem da lógica infinitamente-valorada de Lukasiewicz e reduzindo os problemas de verificação para problemas de decisão associados a este sistema lógico. Para atingir seus objetivos, este projeto é dividido em três fases. Primeiro, serão abordadas as redes neurais que podem ser descritas como funções racionais de McNaughton, que são casos particulares de funções contínuas lineares por partes com domínio em Rn e contradomínio em R, abordadas na segunda fase. Na última fase, serão abordadas redes neurais não-lineares, cujas funções de ativação são sigmoide e tangente hiperbólica. Os métodos desenvolvidos serão implementados e testados em benchmarks estabelecidos na primeira competição internacional de verificação de redes neurais - 1st International Verification of Neural Networks Competition -, ocorrida no ano de 2020. (AU)