Проверка моделей как средство верификации нейронных сетей

Проверка моделей — активно использующийся в индустрии подход, основанный на LTL (линейная темпоральная логика) и предназначенный для проверки некоторой системы с конечным числом состояний (программы, микросхемы, ансамбля роботов/механизмов/устройств) на соответствие спецификации, как правило включающей свойства безопасности (недостижимость “опасных” состояний) и витальности (достижимость “хороших” состояний).
С появлением и развитием нейронных сетей, включающих миллионы и миллиарды параметров, неизбежно встаёт вопрос верификации их свойств. В данном докладе мы постараемся произвести обзор современных применений техник проверки моделей к верификации нейронных сетей.