Proving properties of binary classification neural networks via Lukasiewicz logic

Author(s)

Preto, Sandro ; Finger, Marcelo

• Document type: Journal article
• Source: LOGIC JOURNAL OF THE IGPL; v. N/A, p. 17-pg., 2022-06-10.

Abstract

Neural networks are widely used in systems of artificial intelligence, but due to their black box nature, they have so far evaded formal analysis to certify that they satisfy desirable properties, mainly when they perform critical tasks. In this work, we introduce methods for the formal analysis of reachability and robustness of neural networks that are modeled as rational McNaughton functions by, first, stating such properties in the language of Lukasiewicz infinitely-valued logic and, then, using the reasoning techniques of such logical system. We also present a case study where we employ the proposed techniques in an actual neural network that we trained to predict whether it will rain tomorrow in Australia. (AU)

• FAPESP's process: 14/12236-1 - AnImaLS: Annotation of Images in Large Scale: what can machines and specialists learn from interaction?
• Grantee: Alexandre Xavier Falcão
• Support Opportunities: Research Projects - Thematic Grants
• FAPESP's process: 19/07665-4 - Center for Artificial Intelligence
• Grantee: Fabio Gagliardi Cozman
• Support Opportunities: Research Grants - Research Program in eScience and Data Science - Research Centers in Engineering Program
• FAPESP's process: 15/21880-4 - PROVERBS -- PRobabilistic OVERconstrained Boolean Systems: reasoning tools and applications
• Grantee: Marcelo Finger
• Support Opportunities: Regular Research Grants
• FAPESP's process: 21/03117-2 - Formal verification of neural networks via Lukasiewicz infinitely-valued logic
• Grantee: Sandro Márcio da Silva Preto
• Support Opportunities: Scholarships in Brazil - Post-Doctoral