Machine learning models are becoming widespread and are being implemented in many processes that have critical properties, which failure leads to serious problems. Traditional model validation on limited datasets estimates the percentage of correct results but cannot guarantee that a given property is fulfilled. The task of verification is to provide a strict proof that the required properties are fulfilled. Traditional verification approaches are computationally expensive, so nowadays the development of promising methods for verifying neural network models is a big challenge. Within the framework of this work, approaches for analyzing the reliability of neural network models that consider the architecture of the models are investigated. As demonstration, the verification of noise reduction models [1] was chosen, which makes it possible to effectively process non-stationary signals. As part of the work, some properties for neural network models of signal processing have been verified. In addition, an approach has been proposed and compared with an existing one.

formal methods, constraint programming, logic programming, neural networks, neural network verification

Polevoi Anton Vyacheslavovich,  polevoianton@bk.ru,  orcid.org/0009-0000-2216-0468,  Lomonosov Moscow State University

Korukhova Yulia Stanislavovna,  yulia@cs.msu.ru,  orcid.org/0000-0001-5221-5730,  Lomonosov Moscow State University