Formal verification of neural networks via Lukasiewicz infinitely-valued logic

Abstract

A way to circumvent the black box method problem suffered by neural networks and allow its application in critical situations is by making the formal verification of desirable properties in these networks. The area of formal verification of neural networks is recent and there are challenges to be tackled; for that, the community proposed benchmarks and competitions for comparing the efficiency of the proposed methods. This research project aims to establish such methods by formalizing properties about neural networks in the language of Lukasiewicz infinitely-valued logic and reducing the problems of verification to decision problems related to this logical system. In order to achieve its objectives, this project is divided in three phases. First, it will be approached the neural networks that can be described as rational McNaughton functions which are particular cases of continuous piecewise linear functions with domain in R n and codomain in R, approached in the second phase. In the last phase, it will be approached nonlinear neural networks, whose activation functions are sigmoid and hyperbolic tangent. The developed methods will be implemented and tested in the benchmarks established in the 1st International Verification of Neural Networks Competition, which took place in 2020. (AU)