A evolução da capacidade computacional e abundância de dados vêm fazendo com que o uso de inteligência artificial (IA) para contribuições em diversas áreas seja intensificado, tais como aplicações críticas em relação à segurança (safety). Entre as questões relevantes para pesquisa nesse tema estão métodos para avaliar se sistemas com IA são suficientemente seguros para serem usados nessas aplicações.
Esta pesquisa busca aprofundar uma avaliação de segurança crítica em um sistema baseado em redes neurais profundas que foi desenvolvido para auxiliar na detecção de arritmias cardíacas em eletrocardiogramas. Para isso, a pesquisa tem como objetivo sobreaproximar o conjunto imagem da inteligência artificial por meio de regras lógico-aritméticas que descrevem a aplicação em análise e avaliar os resultados para averiguar a garantia de segurança crítica.
Abaixo temos a figura das arquiteturas das redes neurais, em cima o modelo utilizado como base da análise, embaixo o modelo utilizado traduzido para a especificação ONNX, utilizada como padrão de facto para verificação em redes neurais. Devido a diferencia entre as duas linguagens de especificação, as operações são diferentes, mas equivalentes. Além da arquitetura, a inferência da rede no conjunto de dados e os valores atribuídos aos neurônios foram utilizados como parâmetros para validação.
A estratégia utilizada para verificação formal neste trabalho foi o uso de ataques adversários com algoritmos de Projected Gradient Descent (PGD), essa estratégia consiste em estimular a rede com entradas peturbadas até encontrar a perturbação em que ocorre uma mudança na classificação de saída da rede, indicando um possível erro de classificação.
Neste trabalho foram apresentados: (i.) a arquitetura de uma solução para verificação formal em sistema de redes neurais que classifica arritmias cardíacas; (ii.) a implementação da tradução dos sistemas de redes, com a verificação de equivalência do sistema original; (iii.) uma primeira estratégia de verificação, baseada em ataques adversários; (iv.) as limitações dessa estratégia e (v.) a motivação para a necessidade de uma verificação formal de segurança mais ampla. Na etapa correspondente à presente entrega, foram realizadas as atividades (iii.) até (v.).
Para trabalhos futuros, consideram-se necessários ajustes na ferramenta de verificação formal alpha-beta-crown para permitir a análise formal completa da rede neural, uma vez que foram identificadas limitações impeditivas para essa avaliação durante o presente trabalho. Além disso, a estratégia de ataques adversários adotada até o momento também possui limitações que restringem a abrangência da análise formal de segurança – sobretudo devido à geração de cenários de entradas impróprias que não caracterizam situações plausíveis para batimentos cardíacos de seres humanos vivos.
Agradecimentos:
Trabalho por: Gabriel Stephano Santos
Orientadores: Prof. Dr. Paulo Sérgio Cugnasca
Co-orientador: Prof. Dr. Antonio Vieira da Silva Neto
Colaboradora: Ana Vitória Abreu Murad