Сотрудники факультета ВМК МГУ имени М.В. Ломоносова создали и проверили методику формальной верификации нейронных сетей, которая дает возможность оценивать их надежность и стабильность в процессе решения задач, требующих безошибочной работы. Результаты исследования были доложены на конференции « Научный сервис в сети Интернет» и опубликована в трудах ИПМ им. М.В. Келдыша.
В настоящее время методы машинного обучения находят применение в областях, где даже незначительная ошибка может иметь серьезные последствия: в медицине, авиации, беспилотном транспорте и системах промышленного управления. Обычное тестирование с использованием наборов данных позволяет лишь оценить точность работы модели, однако не обеспечивает уверенности в ее постоянном соответствии требуемым характеристикам. В связи с этим, формальная верификация – строгая математическая проверка соответствия заданным требованиям – становится приоритетным направлением научных изысканий.
Авторы в своей работе рассматривают существующие подходы к верификации и объясняют, почему многие из них являются вычислительно затратными или не подходят для нейронных сетей со сложной структурой. Подробно изучаются методы, учитывающие структуру нейронной сети, такие как веса, функции активации и особенности распространения сигнала между слоями.
Чтобы продемонстрировать потенциал разработанного подхода, исследователи изучили характеристики нейросетевой модели, используемой для активного шумоподавления. Данная модель прогнозирует параметры адаптивного фильтра, предназначенного для компенсации нестационарного шума, такого как шум от транспорта или авиации. Авторы определили свойства, которым должна соответствовать такая сеть, включая, например, исключение нулевых значений весов при интенсивном шуме или различия в коэффициентах для разных типов акустических сигналов, и подтвердили, что модель правильно удовлетворяет этим условиям.
Для решения поставленной задачи была создана комбинация инструментов, включающая преобразование весов модели из формата ONNX в систему ограничений и последующую проверку их соответствия с использованием Prolog-верификатора. Результаты, полученные таким образом, были сопоставлены с системой Marabou, являющейся одним из общепризнанных лидеров в области проверки нейронных сетей. Проведенные эксперименты демонстрируют, что разработанный метод характеризуется высокой скоростью проверки и сниженным потреблением памяти при анализе крупных моделей и свойств.
В представленной работе также содержится подробный анализ применяемых на данный момент способов проверки, среди которых:
- методы, основанные на решении систем ограничений и модифицированных симплекс-процедурах (полная верификация);
- методы, использующие абстрактную интерпретацию и интервализацию (частичная верификация);
- анализ актуальных систем, участвующих в соревновании по верификации VNN-COMP (Marabou, α,β-CROWN, PyRAT, NNV и др.).
В своих работах авторы отмечают, что создание действенных способов формальной верификации представляет собой одну из важнейших задач современной науки, ведь именно они способны гарантировать безопасность использования искусственного интеллекта в системах, функционирование которых имеет решающее значение.
Полученные данные служат фундаментом для развития инструментов проверки, включая более совершенные алгоритмы активного шумоподавления и решения других задач, связанных с обработкой сигналов.