Исследователи нашли пределы ускорения верификации нейросетей и создали FastCert

Проверка надежности нейросетей становится всё более важной задачей по мере их внедрения в критически важные сферы. Системы на основе искусственного интеллекта используются в медицине, транспорте и промышленности, где ошибки могут иметь серьезные последствия. Для подтверждения корректности работы моделей применяются методы формальной верификации, которые проверяют, соответствуют ли поведение сети заданным требованиям.

Однако полная верификация сложных нейросетей часто требует больших вычислительных ресурсов. Для ускорения процесса исследователи используют различные эвристики, в том числе переиспользование промежуточных абстрактных состояний или шаблонов между разными запросами. Такой подход, называемый proof sharing, позволяет сократить время проверки, используя уже найденные доказательства для похожих случаев.

В новой работе, опубликованной на arXiv, авторы систематически изучили эффективность шаблонного ускорения. Они выяснили, что уровень переиспользования шаблонов сильно варьируется в зависимости от архитектуры сети, свойств, наборов данных и методов обучения. В некоторых сценариях такой подход практически не дает выигрыша, что ставит вопрос о его универсальности.

Чтобы объяснить наблюдаемые различия, исследователи предложили новую метрику — совместно стабильные нейроны. Она показывает, какие нейроны остаются стабильными при разных запросах, и позволяет предсказать, когда шаблонные методы с высокой вероятностью не дадут ускорения. Это помогает заранее определить, стоит ли применять данную технику в конкретной задаче.

На основе этих наблюдений авторы разработали метод FastCert. Он автоматически распределяет шаблоны по слоям нейросети, чтобы повысить эффективность переиспользования, и полностью отказывается от шаблонов, если они вряд ли приведут к ускорению. Такой адаптивный подход позволяет избежать лишних вычислений и сосредоточить ресурсы на действительно полезных операциях.

Эксперименты проводились на большом наборе задач L0-верификации, основанных на комбинаторных схемах покрытия. Результаты показали, что FastCert в среднем ускоряет работу в 1,13 раза по сравнению с существующим методом переиспользования шаблонов. Прирост может показаться скромным, но для ресурсоемких процессов верификации он значим.

Авторы отмечают, что их работа помогает лучше понять границы применимости шаблонного ускорения и предлагает инструмент для автоматического выбора стратегии. Дальнейшие исследования могут быть направлены на расширение методов и их адаптацию к другим типам верификации, что повысит доверие к нейросетевым системам.