# Валидация систем безопасности: модели Тейлора и вероятностная достижимость в курсе AA228V Источник: https://www.youtube.com/watch?v=GysI7p6y1Hs Канал: Stanford Online Опубликовано: 07.04.2025 --- В рамках курса по валидации систем критической безопасности (AA228V) в Стэнфорде прошла лекция, посвященная методам дискретной достижимости (Reachability). После разбора нелинейных систем на предыдущих занятиях профессора перешли к одной из самых надежных стратегий анализа безопасности — преобразованию непрерывных динамических систем в дискретные графы. В ходе лекции были представлены методы борьбы с эффектом «раздувания» множеств и способы получения вероятностных гарантий безопасности даже в условиях неопределенности. ## 🛠 От интервалов к Тейлоровским моделям [[JUMP:0:05]] Лекция началась с ретроспективы проблем, возникших при анализе нелинейных систем, таких как перевернутый маятник. Основная сложность заключалась в том, что использование интервальной арифметики и естественных функций включения приводило к слишком грубой переаппроксимации (over-approximation) [0:58]. Множество достижимости «раздувалось» настолько быстро, что сделать вывод о безопасности системы становилось невозможно. Даже функции включения на основе теоремы о среднем значении лишь ненадолго откладывали этот процесс [1:10]. Ключевым решением стали **модели Тейлора (Taylor models)**. В отличие от стандартных функций включения, которые всегда выдают на выходе гиперпрямоугольники, модели Тейлора позволяют работать с гораздо более выразительными формами [2:41]. Особенности моделей Тейлора: * **Состав:** Полином Тейлора степени $n-1$ плюс интервальный остаток ($\alpha$) [4:02]. * **Смысл:** Полином аппроксимирует функцию, а интервал $\alpha$ (остаток Лагранжа) ограничивает ошибку этой аппроксимации [5:31]. * **Гибкость:** При использовании моделей второго порядка мы получаем политопы, а третьего — невыпуклые гладкие формы [8:41]. Однако лектор подчеркнула, что работа с невыпуклыми множествами третьего и выше порядков крайне затруднительна — операции пересечения таких множеств с «опасными зонами» (avoid sets) вычислительно сложны [9:32]. ## 📉 Консервативная линеаризация [[JUMP:11:57]] Частным случаем моделей Тейлора второго порядка является **консервативная линеаризация** [11:57]. Этот метод позволяет свести сложную нелинейную задачу к линейной достижимости, с которой инженеры уже умеют работать. Процесс выглядит следующим образом: 1. Функция линеаризуется в центре текущего множества с использованием Якобиана ($J$) [13:17]. 2. К линейному преобразованию добавляется интервальный остаток, учитывающий ошибку линеаризации. 3. Для вычислений используются суммы Минковского и матричное умножение [14:01]. На примере маятника было показано, что консервативная линеаризация дает гораздо более плотные границы множеств, чем простые интервалы, хотя в долгосрочной перспективе даже она может привести к расхождению границ [17:46]. ## 🧬 Символьная vs Конкретная достижимость [[JUMP:18:13]] Собеседники обсудили два концептуальных подхода к вычислению множеств во времени: * **Символьная достижимость:** Рассматривает функцию «развертки» (roll-out) на несколько шагов вперед как единый объект. Она не страдает от «эффекта обертывания», но вычислительно дорога из-за накопления нелинейностей [20:25]. * **Конкретная достижимость (Concretization):** Аппроксимирует и фиксирует (конкретизирует) множество на каждом временном шаге [19:06]. Главный риск конкретной достижимости — **эффект обертывания (wrapping effect)**. Это накопление ошибки из-за того, что на каждом шаге мы вынуждены описывать реальное множество сложной формы более простой фигурой (например, прямоугольником), включая в расчет лишние, недостижимые состояния [22:09]. Тем не менее, комбинация конкретизации и консервативной линеаризации позволила успешно верифицировать безопасность маятника на 14 шагов вперед, что ранее было недоступно [25:05]. ## 📊 Дискретная абстракция и графы [[JUMP:34:00]] Центральной темой второй половины лекции стал переход к **дискретной достижимости**. Любую систему с дискретными состояниями можно представить в виде направленного графа, где узлы — это состояния, а ребра — переходы с определенными весами (вероятностями) [34:26]. Алгоритмы на графах позволяют выполнять: 1. **Прямую достижимость (Forward reachability):** Поиск всех состояний, достижимых из начального с помощью поиска в ширину (BFS) [39:02]. 2. **Обратную достижимость (Backward reachability):** Определение состояний, из которых можно попасть в «плохую» зону [38:37]. 3. **Поиск инвариантных множеств:** Легко проверяется через подмножества узлов графа [41:12]. По мнению лектора, даже если система непрерывна, ее выгодно «дискретизировать» через разбиение (partitioning) пространства состояний на ячейки. Каждая ячейка становится узлом графа. Чтобы сохранить гарантии безопасности, ребра в таком графе должны строиться из условия перекрытия: если из ячейки А можно попасть в область, задевающую ячейку Б, в графе рисуется ребро А $\rightarrow$ Б [1:03:13]. Чем мельче разбиение, тем точнее аппроксимация [1:06:33]. ## 🎲 Вероятностная достижимость [[JUMP:47:27]] В отличие от детерминированного подхода («достижимо или нет»), вероятностная достижимость отвечает на вопрос: «С какой вероятностью мы окажемся в опасности?» [50:33]. Для объяснения лектор привела личный пример спора с мужем: что произойдет быстрее — она отобьет битой мяч на скорости 90 миль в час или он выполнит «тройной прыжок» через скакалку? [48:05]. Обычный анализ достижимости скажет, что оба события возможны. Вероятностный же анализ покажет, что шанс случайно отбить мяч значительно выше [49:39]. В лекции были выведены две ключевые метрики: 1. **Probability of Occupancy:** Вероятность нахождения в конкретном состоянии $s$ в момент времени $t$ [50:46]. 2. **Probability of Reachability:** Общая вероятность того, что система попадет в целевое множество за отведенный горизонт времени [55:24]. В финале лекции эксперты сошлись во мнении, что методы достижимости находят реальное применение в навигации роботов и, что особенно актуально, в анализе выходных множеств нейронных сетей умеренного размера [1:07:35].