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

• Processo: 21/03117-2
• Modalidade de apoio: Bolsas no Brasil - Pós-Doutorado
• Data de Início da vigência: 01 de agosto de 2021
• Data de Término da vigência: 30 de abril de 2024
• Área de conhecimento: Ciências Exatas e da Terra - Ciência da Computação - Metodologia e Técnicas da Computação
• Pesquisador responsável: Marcelo Finger
• Beneficiário: Sandro Márcio da Silva Preto
• Instituição Sede: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brasil
• Empresa: Universidade de São Paulo (USP). Centro de Inovação da USP (INOVA)
• Vinculado ao auxílio: 19/07665-4 - Centro de Inteligência Artificial, AP.eScience.CPE
• Bolsa(s) vinculada(s): 21/10134-0 - Computando consequência lógica na lógica infinitamente-valorada de Lukasiewicz, BE.EP.PD
• Assunto(s): Inteligência artificial Lógicas não clássicas Redes neurais (computação)
• Palavra(s)-Chave do Pesquisador: Lógica Infinitamente-valorada de Lukasiewicz | Lógicas não clássicas | Métodos Formais | Redes neurais | Verificação Formal | Métodos Formais e Inteligência Artificial

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)

Publicações científicas

(4)

(Referências obtidas automaticamente do Web of Science e do SciELO, por meio da informação sobre o financiamento pela FAPESP e o número do processo correspondente, incluída na publicação pelos autores)

FINGER, MARCELO; PRETO, SANDRO. Polyhedral semantics and the tractable approximation of Lukasiewicz infinitely-valued logic. JOURNAL OF LOGIC AND COMPUTATION, v. N/A, p. 15-pg., 2023-10-13. (19/07665-4, 14/12236-1, 15/21880-4, 21/03117-2)

PRETO, SANDRO; FINGER, MARCELO. Proving properties of binary classification neural networks via Lukasiewicz logic. LOGIC JOURNAL OF THE IGPL, v. N/A, p. 17-pg., 2022-06-10. (14/12236-1, 19/07665-4, 15/21880-4, 21/03117-2)

PRETO, SANDRO; FINGER, MARCELO. Efficient representation of piecewise linear functions into Lukasiewicz logic modulo satisfiability. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, v. N/A, p. 26-pg., 2022-05-17. (21/03117-2, 14/12236-1, 19/07665-4, 15/21880-4)

PRETO, SANDRO; FINGER, MARCELO. Regional, Lattice and Logical Representations of Neural Networks. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, v. N/A, n. 421, p. 153-pg., 2025-01-01. (19/07665-4, 21/03117-2, 14/12236-1, 15/21880-4)