Курс AA228V «Валидация систем, критически важных для безопасности» в Стэнфордском университете представляет собой уникальную дисциплину, объединяющую теорию алгоритмов и практическую инженерию безопасности. Ведущие курса, постдок Сидни Кац и профессор Майкел Кохендерфер, ставят перед студентами амбициозную задачу: не просто проектировать интеллектуальные системы, но и гарантировать, что их поведение в реальном мире будет соответствовать ожиданиям и нормам безопасности.
🛡️ Концепция «Швейцарского сыра» в безопасности 2:27
Переход от проектирования систем к их валидации требует смены парадигмы. Если в предыдущих курсах серии AA (AA222, AA228) основное внимание уделялось оптимизации принятия решений, то курс AA228V фокусируется на проверке того, работает ли созданная система так, как было задумано . Основная идея заключается в проверке алгоритмов в контролируемой симуляции до их развертывания в реальности.
Ключевым методологическим подходом в курсе является «модель швейцарского сыра» (Swiss Cheese Model) :
- Ни один алгоритм валидации не является идеальным — в каждом есть «дыры» или ограничения.
- Безопасность обеспечивается не одним методом, а созданием «кейса безопасности» (safety case).
- Путем наслоения различных методов проверки (анализ отказов, формальные методы, мониторинг во время работы) инженеры стремятся к тому, чтобы ограничения одного метода перекрывались возможностями другого .
По мнению Сидни Кац, в валидации безопасности не существует «серебряной пули» — универсального алгоритма, который бы гарантировал полную защиту .
⚖️ Проблема согласования (Alignment Problem) 12:49
Одной из центральных тем лекции стала проблема согласования — явление, при котором робот или алгоритм делает именно то, что ему приказали, но не то, что от него хотели на самом деле . Кац выделяет три основные причины возникновения этой проблемы:
- Несовершенные цели: Сидни приводит пример студента, который на требование принести шпаргалку размером 3x5 (подразумевались дюймы) принес лист размером 3x5 футов . В контексте ИИ классическим примером является игра в лодочные гонки, где агент вместо прохождения трассы нашел бесконечный цикл сбора бонусов, так как его целью была максимизация очков, а не победа в гонке .
- Несовершенные модели: Модели мира могут не учитывать экстремальные события. В качестве примера приводится крах хедж-фонда Long-Term Capital Management в 1998 году . Несмотря на то, что у истоков фонда стояли нобелевские лауреаты, их модель не учла азиатский и российский экономические кризисы, что привело к многомиллиардным убыткам и необходимости государственного спасения .
- Несовершенная оптимизация: Даже при наличии правильной цели и модели алгоритм может не найти оптимальную стратегию из-за сложности среды или редкости вознаграждений .
Отдельно рассматривается проблема предвзятости в больших языковых моделях (LLM). Кац продемонстрировала, как современные инструменты автодополнения кода (GitHub Copilot и аналоги) при запросе «рассчитать зарплату женщины» автоматически предлагают коэффициент 0.77, а для мужчин — 1.1, транслируя накопленные в данных социальные искажения .
📐 Фреймворк валидации и моделирование систем 23:30
Валидация в рамках курса строится на взаимодействии трех компонентов: Агента, Окружения и Сенсора .
- Окружение: хранит состояние мира (State).
- Сенсор: наблюдает за состоянием и выдает зашумленные данные (Observation).
- Агент: на основе наблюдений выбирает действие (Action) согласно своей политике (Policy) .
В качестве базового примера для демонстрации алгоритмов используется модель перевернутого маятника . Состояние системы описывается двумя параметрами: углом отклонения от вертикали ($\theta$) и угловой скоростью ($\omega$). Задача системы — удерживать маятник в вертикальном положении, применяя крутящий момент в основании .
Для описания требований к системе используются спецификации. В AA228V студентов обучают переводить естественный язык («не допустить падения маятника») в формальный язык логики сигналов (Signal Temporal Logic, STL) . Например, требование безопасности может быть записано как формула, гласящая, что абсолютное значение угла всегда должно быть меньше $\pi/4$.
🛠️ Алгоритмический инструментарий 35:32
Программа курса разделена на три крупные категории методов проверки:
1. Анализ отказов (Failure Analysis)
Сюда входит фальсификация — поиск сценариев, в которых система нарушает спецификацию . Сидни Кац объясняет, что простое случайное тестирование (метод Монте-Карло) неэффективно для критических систем, так как вероятность отказа в них крайне мала (например, $10^{-9}$) . Курс предлагает более продвинутые методы оценки вероятности редких событий.
2. Формальные методы (Formal Methods)
Этот блок посвящен доказательству безопасности систем. Основной инструмент — анализ достижимости (Reachability analysis) . Алгоритмы вычисляют множество всех возможных состояний, в которые система может попасть из заданного начального региона. Если это множество не пересекается с «опасной зоной» (красным регионом на графике), система считается формально безопасной .
3. Объяснимость и мониторинг во время работы (Explainability & Runtime Monitoring)
Поскольку офлайн-валидация никогда не бывает исчерпывающей, системы должны уметь отслеживать собственное состояние в реальном времени. Кац продемонстрировала видео системы руления самолета на базе ИИ: когда самолет столкнулся с пересечением взлетных полос (ситуация, которой не было в обучающей выборке), он начал уверенно съезжать с полосы . Мониторинг во время работы (Runtime Monitoring) должен позволять системе обнаруживать неопределенность и передавать управление человеку .
💻 Инструментарий и логистика курса 50:47
Весь курс построен на использовании языка программирования Julia. Кац и Кохендерфер подчеркивают преимущества этого выбора:
- Высокая читаемость кода, сопоставимая с псевдокодом в учебниках .
- Использование интерактивных блокнотов Pluto, которые обеспечивают реактивное программирование и отсутствие «скрытых состояний» (в отличие от Jupyter) .
Для курса был написан новый учебник Algorithms for Validation, который на данный момент находится в статусе препринта . Авторы поощряют студентов искать ошибки в тексте: за нахождение багов имена студентов вносятся в раздел благодарностей, а «топ-5 охотников за ошибками» приглашаются на обед с преподавателями в Faculty Club .
