ИСТИНА

Нейронные сети используются для решения все более важных задач, и в некоторых случаях неправильные выходные данные могут привести к дорогостоящим последствиям. Традиционно проверка нейронных сетей сосредоточена на тестировании — оценке сети на большом наборе точек во входном пространстве и определении того, соответствуют ли выходы желаемым. Однако, поскольку входное пространство фактически бесконечно по мощности, невозможно проверить все возможные входные данные. Формальная провер- ка обеспечивает ортогональную альтернативу тестированию, которая предоставляет формальные (математические) гарантии в отношении производительности искусственной нейронной сети на всей области входных данных. Постановка задачи. Рассмотреть проблему формальной верификации искусственных нейронных сетей (ИНС); исследовать существующие методы формальной верификации ИНС; изучить алгоритмы на основе исследуемых методов; провести сравнительный анализ изученных алгоритмов. Методы. Использование формальной верификации для аппаратного и программного обеспечения существует давно. Тем не менее, исследования по верификации нейронных сетей, активно велись всего лишь последние 10 лет. Существует 4 основных способа верификации: решение SAT/SMT, линейное программирование, доказательство теорем и неполная проверка. На основе выбранных методов были разработаны алгоритмы верификации. В данной работе исследуются и сравниваются следующие алгоритмы: ReluPlex, ReluVal, AI2, Neurify, NSVerify, Convdual.