Он проверяет надежность и устойчивость ИИ-моделей при выполнении критически важных задач. Исследователи отмечают, что традиционное тестирование на наборах данных позволяет оценивать только точность, но не дает гарантий, что всегда будут соблюдаться заданные свойства.

Подход испытали на модели, применяемой в задаче активного шумоподавления. Для этого ученые разработали набор инструментов: преобразование весов из формата ONNX в систему ограничений и проверка их выполнимости с помощью Prolog-верификатора.

Метод сравнили с системой Marabou — одним из наиболее известных инструментов для проверки нейросетей. Новый подход обеспечил высокую скорость и требовал меньше памяти при анализе больших моделей и свойств.