В рамках авиационного и системного проектирования верификация систем, критичных для безопасности, представляет собой сложнейшую математическую задачу. В лекции из серии Stanford Online рассматриваются передовые методы анализа достижимости (reachability analysis) для линейных и нелинейных систем с использованием языка программирования Julia. Преподаватель демонстрирует, как преодолеть проблему «проклятия размерности» при расчете безопасных траекторий и почему классические подходы уступают современным методам интервального анализа и моделям Тейлора.
📉 Преодоление вычислительного взрыва в линейных системах 0:05
Анализ достижимости для линейных систем при распространении многогранников (polytopes) через уравнения динамики неизбежно сталкивается с проблемой геометрического усложнения. На каждом временном шаге количество вершин расчетных фигур увеличивается, что приводит к экспоненциальному росту вычислительной сложности. На определенной глубине симуляции задача становится вычислительно неразрешимой.
Для решения этой проблемы лектор предлагает несколько альтернативных подходов:
- Использование зонотопов (zonotopes): в этом случае количество генераторов растет линейно с увеличением глубины анализа. Однако этот метод имеет фундаментальное ограничение — далеко не каждый многогранник можно представить в виде зонотопа.
- Избыточная аппроксимация (over-approximation): построение внешнего описывающего множества (обозначается чертой сверху $\bar{X}$), которое гарантированно содержит в себе истинное расчетное множество достижимости. Такой подход позволяет существенно сократить число отслеживаемых вершин.
Использование избыточной аппроксимации сохраняет строгие гарантии безопасности системы. Если аппроксимированное множество достижимости не пересекается с опасным множеством (avoid set), то истинное множество также гарантированно безопасно. Если же пересечение происходит, анализ считается нерезультативным: система не обязательно небезопасна, просто точность модели не позволяет сделать однозначный вывод.
На практике инженеры проводят аппроксимацию с заданной периодичностью (например, каждые несколько итераций в зависимости от специфики задачи). Автоматизировать этот процесс помогает специализированная библиотека LazySets для языка Julia, которая предоставляет готовую функцию overapproximate с возможностью настройки допустимой погрешности.
🎯 Концепция опорных векторов и аппроксимация множеств 5:01
В основе алгоритмов избыточной аппроксимации лежит математический концепт опорного вектора (support vector). Опорный вектор представляет собой функцию $\sigma(d)$, которая принимает вектор заданного направления $d$ и возвращает точку множества, максимизирующую скалярное произведение со значением этого направления.
Геометрический смысл этой концепции чрезвычайно интуитивен:
- В пространстве выбирается определенное направление $d$.
- Перпендикулярно этому направлению проводится гиперплоскость (линия в двухмерном пространстве).
- Плоскость «сдвигается» в заданном направлении до тех пор, пока она едва касается границы исследуемого множества.
Точка касания и является опорным вектором, а сама плоскость определяет полупространство (halfspace), жестко ограничивающее фигуру. Повторяя эту процедуру для различных направлений, можно сформировать описывающий многогранник (bounding polytope). Чем больше направлений используется для расчета, тем точнее аппроксимация соответствует реальному множеству, но тем больше вершин приходится учитывать алгоритму.
Программный пакет LazySets использует интеллектуальный алгоритм выбора направлений для достижения максимальной вычислительной эффективности. Лектор дает шуточную подсказку студентам для выполнения учебного проекта №3: для оптимизации результатов в таблице лидеров (leaderboard score) необходимо проявить изобретательность при выборе направлений, в то время как для простого получения зачета достаточно ограничиться стандартным выравниванием по осям (bounding box). При этом, по мнению преподавателя, для компенсации неопределенностей системы правильнее использовать моделирование внешних возмущений, а не искусственное раздувание размеров множества достижимости. Стоит отметить, что аппарат опорных функций способен ограничивать даже невыпуклые (non-convex) множества, преобразуя их в выпуклые оболочки, хотя в таком случае аппроксимация теряет свою былую плотность.
⚙️ Оптимизационный подход без распространения множеств 12:39
Вместо классического пошагового распространения геометрических фигур инженеры могут вычислять опорные векторы напрямую, сводя задачу к математической оптимизации. В такой постановке общая функция заменяется состояниями системы в целевой момент времени. Целью становится максимизация скалярного произведения вектора направления и вектора состояния на шаге $D$.
Задача формулируется с учетом строгих ограничений:
- Начальное состояние должно принадлежать заданному множеству начальных состояний.
- Внешние возмущения на каждом шаге не должны выходить за рамки допустимых интервалов возмущений.
- Каждый последующий шаг траектории должен быть физически реализуем и строго соответствовать уравнениям динамики системы.
Если ограничивающие множества представлены в виде многогранников, данная структура превращается в классическую задачу линейного программирования (Linear Program), методы решения которой подробно изучаются в специализированном курсе AA222.
Главным преимуществом оптимизационного фреймворка является отсутствие необходимости отслеживать геометрические вершины и проводить явное пошаговое распространение множеств. Вычислительная эффективность метода во многом зависит от структуры конкретной системы и используемого LP-солвера.
Более того, если инженеру требуется лишь проверить гипотезу о безопасности (property checking) без построения детальной формы множества достижимости, оптимизационная задача может быть решена абсолютно точно. Для этого целевая функция переписывается на минимизацию расстояния между расчетным множеством достижимости и опасной зоной. Если минимум равен нулю, это сигнализирует о потенциальном нарушении безопасности. Переменными оптимизации в этом случае выступают последовательности состояний и возмущений для выбранного направления. В программном коде на Julia для этого применяется библиотека JuMP.jl (или convex.jl), при этом в качестве инструмента решения может использоваться универсальный SCS-солвер, возможности которого лектор считает избыточными для чисто линейных задач.
📊 Анализ главных компонент (PCA) для выбора направлений 19:39
Качество избыточной аппроксимации критически зависит от стратегии выбора векторов направлений. Лектор демонстрирует это на примере четырех различных подходов:
- Выравнивание по осям (bounding box): расчет ведется по четырем стандартным ортогональным направлениям. Метод дает колоссальную погрешность, оставляя много пустого неиспользуемого пространства.
- 10 случайных направлений: аппроксимация многогранниками дает неоднозначный результат; из-за неудачного распределения векторов расчетное множество может ошибочно пересечь опасную зону.
- 50 случайных направлений: ситуация заметно улучшается, точность аппроксимации возрастает.
- Анализ главных компонент (PCA): наиболее эффективная стратегия, требующая всего четырех опорных векторов. На основе предварительных симуляций траекторий (rollouts) определяются ключевые направления вытягивания данных, что позволяет построить исключительно плотную и точную оболочку множества достижимости.
Предварительные симуляции также служат отличным инструментом для проверки корректности вычислений (sanity check): если хотя бы одна смоделированная траектория выходит за границы рассчитанного множества достижимости, это однозначно указывает на ошибку в коде.
🔄 Переход к нелинейным системам и интервальная арифметика 25:09
Применение линейных операторов к многогранникам математически тривиально и сводится к умножению матриц и сложению векторов. Однако реальный мир нелинеен. Попытка пропустить многогранник через нелинейный оператор (например, функцию синуса) превращает исходный отрезок в сложную кривую, которая теряет свойства выпуклости. Работа с невыпуклыми множествами резко увеличивает сложность вычислений, поэтому стандартной практикой становится их аппроксимация выпуклыми фигурами.
Одним из базовых инструментов борьбы с нелинейностью является интервальная арифметика. Вместо точечных значений переменные представляются в виде интервалов $[x]$ с жестко заданными нижней $\underline{x}$ и верхней $\overline{x}$ границами. В многомерном пространстве декартово произведение таких интервалов образует «интервальный бокс» (interval box), физически представляющий собой ориентированный по осям гиперпрямоугольник.
Математические операции в интервальной арифметике переопределяются для работы с множествами. Например, сложение двух интервалов напоминает сумму Минковского, где результатом становится новый интервал, нижняя граница которого равна сумме нижних границ, а верхняя — сумме верхних. Так, сумма интервалов $[-1, 1]$ и $[2, 4]$ дает интервал $[1, 5]$.
Аналогичным образом в замкнутой форме определяются и другие операции:
- Вычитание: из нижней границы первого интервала вычитается верхняя граница второго, а из верхней — нижняя.
- Умножение и деление: требуют тестирования комбинаций конечных точек для поиска глобальных минимумов и максимумов. При этом деление на интервал, содержащий ноль, является математически неопределенным.
Для монотонно возрастающих элементарных функций (экспонента, логарифм, квадратный корень) расчет интервального аналога тривиален — достаточно вычислить значения функции на границах интервала. Для немонотонных функций (например, $x^2$ или $\sin(x)$) алгоритм усложняется и требует разбора частных случаев. В частности, для функции $x^2$, если интервал содержит ноль, нижняя граница результата принудительно устанавливается в ноль. Вся эта логика инкапсулирована в готовой Julia-библиотеке IntervalArithmetic.jl, избавляющей инженеров от ручного написания правил ветвления.
🔍 Функции включения и проблема зависимости 39:18
В реальных инженерных задачах, таких как верификация перевернутого маятника, уравнения динамики содержат сложные комбинации тригонометрических функций и перемножаемых состояний. Точный расчет выходного интервала для таких комплексных выражений часто невозможен, поэтому математики используют так называемые функции включения (inclusion functions). Функция включения, обозначаемая как $f$, возвращает интервал, который гарантированно содержит в себе истинное множество значений функции, выступая в роли его избыточной аппроксимации.
Для расчета многомерного множества достижимости общая нелинейная функция разбивается на систему координатных функций $R_1 \dots R_n$, каждая из которых генерирует одномерный интервал для конкретной переменной состояния (например, отдельно для угла $\theta$ и угловой скорости $\omega$ маятника). Их последующее декартово произведение дает итоговый гиперпрямоугольник достижимости.
Фундаментальным недостатком такого подхода является жесткое ограничение формы расчетного множества исключительно рамками гиперпрямоугольника. Если реальное облако состояний наклонено или вытянуто по диагонали, интервальный бокс порождает огромную избыточную погрешность.
Самым простым способом построения функции включения является естественная функция включения (natural inclusion function), получаемая путем тривиальной замены всех элементарных операций в исходном выражении их интервальными аналогами. Однако этот метод страдает от колоссального консерватизма из-за «эффекта зависимости» (dependency effect). Эффект возникает, когда одна и та же переменная встречается в уравнении несколько раз (например, в выражении $x - \sin(x)$). Интервальная арифметика некорректно трактует эти вхождения как независимые переменные, предполагая, что из любого значения интервала можно вычесть любое другое значение того же интервала, что приводит к искусственному раздуванию границ. На примере перевернутого маятника естественная функция включения приводит к лавинообразному росту погрешности, делая анализ полностью нерезультативным уже на втором временном шаге симуляции.
📐 Теорема о среднем значении и функции включения Тейлора 51:38
Для преодоления эффекта зависимости лектор предлагает обратиться к классической математической теореме о среднем значении (Mean Value Theorem). Преподаватель иронично замечает, что в школе эта теорема казалась многим абсолютно бесполезной, но именно она легла в основу современных систем детской безопасности в ракетостроении и авиации. Существует даже шуточный студенческий мем: если пририсовать к графику теоремы глаза и перевернуть его, она превращается в «теорему о приятном значении» (Nice Value Theorem).
Опираясь на эту теорему, математическую функцию можно выразить через ее значение в центре интервала $c$ и значение производной в некоторой промежуточной точке:
$$f(x) = f(c) + f'(x')(x - c)$$
Поскольку точка $x'$ гарантированно лежит внутри исходного интервала $[x]$, мы можем заменить ее на сам интервал, получив формулу функции включения по среднему значению:
$$[f]_{MV}([x]) = f(c) + f'([x] - c)$$
Где $[f']$ — естественная функция включения для производной. Этот аппарат легко обобщается на многомерный случай путем замены производной на градиент.
Лектор приводит наглядный аналитический пример для функции $f(x) = x - \sin(x)$ на интервале $[-1, 1]$ с центром $c = 0$:
- Естественная функция включения: дает результат $[-1.84, 1.84]$.
- Функция включения по среднему значению: через производную $f'(x) = 1 - \cos(x)$ и интервал градиента дает диапазон всего $[-0.44, 0.44]$.
Такое впечатляющее сжатие границ объясняется тем, что линеаризация выражения частично нивелирует пагубный эффект зависимости. Данный подход можно масштабировать до полиномов Тейлора более высоких порядков (Taylor inclusion functions). При этом нулевой порядок Тейлора эквивалентен естественной функции включения, а первый порядок — функции по среднему значению. Эксперименты показывают, что переход к полиномам третьего порядка позволяет получить беспрецедентно плотные и точные границы множеств.
💣 Накопление нелинейностей и взгляд в будущее 1:09:56
Несмотря на очевидный прогресс при использовании функций Тейлора первого и второго порядков, нелинейные системы сохраняют свою коварную природу. При моделировании на длительную временную перспективу операции начинают циклически накладываться друг на друга, вызывая эффект компаундинга (накопления) нелинейностей. Множество возмущений расширяется, а тригонометрические функции возводятся в степени, из-за чего даже вторая степень приближения Тейлора со временем демонстрирует взрывной рост погрешности. К сильному разочарованию инженеров, интервальные боксы неизбежно остаются привязанными к прямоугольной сеткой координат.
В финале лекции преподаватель делится интригующим анонсом: на следующем занятии будет представлен принципиально новый математический класс — модели Тейлора (Taylor models). Этот инструмент позволяет уйти от навязанной прямоугольной формы геометрических границ и описывать сложные, изогнутые и невероятно экспрессивные множества состояний. Демонстрационный слайд будущей лекции с идеально гладкой и плотной нелинейной оболочкой вызывает у аудитории искренний восторг.
