On a formal verification of machine learning systems

Dmitry Namiot, Eugene Ilyushin, Ivan Chizhov


The paper deals with the issues of formal verification of machine learning systems. With the growth of the introduction of systems based on machine learning in the so-called critical systems (systems with a very high cost of erroneous decisions and actions), the demand for  confirmation of the stability of such systems is growing. How will the built machine learning system perform on data that is different from the set on which it was trained? Is it possible to somehow verify or even prove that the behavior of the system, which was demonstrated on the initial dataset, will always remain so? There are different ways to try to do this. The article provides an overview of existing approaches to formal verification. All the considered approaches already have practical applications, but the main question that remains open is scaling. How applicable are these approaches to modern networks with millions and even billions of parameters?

Full Text:



DCCN 2021 https://2021.dccn.ru/ Retrieved: Mar, 2022

Ilyushin, E., Namiot, D., & Chizhov, I. (2022). Attacks on machine learning systems-common problems and methods. International Journal of Open Information Technologies, 10(3), 17-22.

Namiot, D., Ilyushin, E., & Chizhov, I. (2021). The rationale for working on robust machine learning. International Journal of Open Information Technologies, 9(11), 68-74.

Namiot, D., Ilyushin, E., & Chizhov, I. (2021). Military applications of machine learning. International Journal of Open Information Technologies, 10(1), 69-76.

Artificial Intelligence in Cybersecurity. http://master.cmc.msu.ru/?q=ru/node/3496 (in Russian) Retrieved: Apr, 2022

Roscher, Ribana, et al.”Explainable machine learning for scientific insights and discoveries.” IEEE Access 8 (2020): 42200-42216.

Došilović, Filip Karlo, Mario Brčić, and Nikica Hlupić. "Explainable artificial intelligence: A survey." 2018 41st International convention on information and communication technology, electronics and microelectronics (MIPRO). IEEE, 2018.

Leofante, Francesco, et al. ”Automated verification of neural networks: Advances, challenges and perspectives.” arXiv preprint arXiv:1805.09938 (2018).

Bride, Hadrien, et al. ”Towards dependable and explainable machine learning using automated reasoning.” International Conference on Formal Engineering Methods. Springer, Cham, 2018.

”A Model-Based Approach for Robustness Testing” (PDF). Dl.ifip.org. Retrieved 01-02-2022.

1990. IEEE Standard Glossary of Software Engineering Terminology, IEEE Std 610.12-1990

Chen, Chen, et al.”A systematic review of fuzzing techniques.” Computers & Security 75 (2018): 118-137.

Huang, Ling, et al.”Adversarial machine learning.” Proceedings of the 4th ACM workshop on Security and artificial intelligence. 2011.

Rouani, Bita Darvish, et al.”Safe machine learning and defeating adversarial attacks.” IEEE Security & Privacy 17.2 (2019): 31-38.

Plösch, Reinhold. "Evaluation of assertion support for the java programming language." Journal of Object Technology 1.3 (2002): 5-17.

Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia, and U.C. Berkeley. “Verifying robustness of human-aware autonomous cars”. In: IFAC-PapersOnLine 51.34 (2019), pp. 131–138.

Shafique, Muhammad, et al.”Robust machine learning systems: Challenges, current trends, perspectives, and the road ahead.” IEEE Design & Test 37.2 (2020): 30-57.

Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel Kochenderfer. “Reluplex: An efficient SMT solver for verifying deep neural networks”. In: International Conference on Computer Aided Verification . Springer. 2017, pp. 97–117.

Lin, Xuankang, et al.”ART: abstraction refinement-guided training for provably correct neural networks.” 2020 Formal Methods in Computer Aided Design (FMCAD). IEEE, 2020.

Marabou https://github.com/NeuralNetworkVerification/Marabou

Wang, Kunxia, et al.”Wavelet packet analysis for speaker-independent emotion recognition.” Neurocomputing 398 (2020): 257-264.


  • There are currently no refbacks.

Abava  Absolutech Convergent 2020

ISSN: 2307-8162