Статья подготовлена на основе лекции курса AA228V Стэнфордского университета, посвященной валидации систем, критически важных для безопасности. Ведущий лекции подробно разбирает математические аспекты распределения отказов и методы семплирования из сложных распределений.
📈 Математика распределения отказов 1:36
В задачах верификации безопасности систем важно не просто найти единичный сценарий отказа (фальсификация), а понять структуру всех возможных сбоев. Для этого вводится понятие распределения отказов (failure distribution).
По словам лектора, распределение отказов — это условная вероятность, которая определяет, насколько вероятна траектория $\tau$ при условии, что она является отказом . Математически это выражается через номинальное распределение траекторий $P(\tau)$ и индикаторную функцию:
- Индикаторная функция возвращает 1, если траектория является отказом, и 0 в противном случае .
- Числитель уравнения дает форму распределения: он совпадает с номинальным распределением в зонах отказа и равен нулю везде, где система работает корректно .
- Знаменатель (нормализующая константа) необходим для того, чтобы интеграл распределения был равен единице .
Основная техническая сложность заключается в том, что знаменатель крайне трудно (а иногда невозможно) вычислить аналитически, так как он требует интегрирования по всем возможным траекториям . Однако для многих алгоритмов достаточно знать только числитель — так называемую ненормированную плотность вероятности .
🎯 Метод Rejection Sampling: аналогия с дартсом 12:00
Для визуализации процесса семплирования из ненормированных распределений лектор использует аналогию с прямоугольной доской для дартса .
Алгоритм Rejection Sampling (выборочное отклонение) включает следующие шаги:
- На доске рисуется форма целевой плотности (которую мы хотим получить) .
- Дротики бросаются в доску равномерно .
- Все дротики, приземлившиеся выше линии целевой плотности, отбрасываются (reject) .
- Оставшиеся дротики проецируются на нижнюю ось, образуя искомое распределение .
Математически этот процесс описывается через proposal distribution ($Q(\tau)$) — это вспомогательное распределение, из которого мы умеем легко извлекать выборку . Важнейшее условие метода: вспомогательное распределение, умноженное на константу $C$, должно всегда «накрывать» целевое распределение $P(\tau) \le C \cdot Q(\tau)$ .
Если в качестве вспомогательного распределения использовать номинальное распределение системы, алгоритм сводится к простому правилу: «запустите симуляцию, если произошел отказ — оставьте образец, если нет — удалите» . Главный недостаток этого подхода — экстремально низкая эффективность при оценке редких событий: если отказ случается раз на миллион запусков, почти все вычисления будут потрачены впустую .
⛓️ Цепи Маркова и метод Монте-Карло (MCMC) 50:47
Более мощным инструментом является алгоритм Metropolis-Hastings (разновидность MCMC). В отличие от независимых бросков в Rejection Sampling, здесь создается цепочка, где каждый новый образец зависит от предыдущего .
Процесс работы MCMC:
- Выбирается начальное состояние $\tau_0$ .
- На каждом шаге предлагается новое состояние $\tau'$ с помощью функции перехода (ядра), обычно это гауссовское распределение вокруг текущей точки .
- Новое состояние принимается с определенной вероятностью. Если новое состояние более вероятно (имеет более высокую плотность $P(\tau)$), оно принимается всегда .
- Если новое состояние менее вероятно, оно принимается лишь с некоторой вероятностью, пропорциональной отношению плотностей .
Лектор подчеркивает, что этот метод гарантированно сходится к истинному распределению при бесконечном количестве итераций . Однако на практике возникают проблемы «прогрева» (Burn-in period): первые образцы могут быть далеки от реальности, поэтому их часто отбрасывают .
🌊 Сглаживание и проблема нескольких режимов отказа 1:09:51
Одной из самых сложных проблем для MCMC является наличие изолированных «островов» отказов — нескольких различных режимов сбоя, разделенных областью нормальной работы . Алгоритм может «застрять» в одной зоне и никогда не найти другую, так как вероятность случайного прыжка через область нулевой плотности крайне мала .
Для решения этой проблемы лектор предлагает метод сглаживания (smoothing):
- Вводится функция расстояния до отказа ($\Delta\tau$) .
- Вместо жесткой индикаторной функции (0 или 1) используется гладкая функция, например, спадающая экспонента или гауссиана .
- Это позволяет алгоритму «видеть» очертания зон отказа, даже находясь в безопасной зоне, и перемещаться между ними .
Параметр $\epsilon$ позволяет контролировать степень сглаживания: при $\epsilon \to 0$ мы возвращаемся к исходному распределению, а при больших значениях — получаем широкое распределение, удобное для поиска новых зон отказа .
