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