# От конфет до авиабезопасности: как Стэндфорд учит формальной логике критических систем

Источник: https://www.youtube.com/watch?v=rBGh5uJhAmo
Канал: Stanford Online
Опубликовано: 07.04.2025

---

В рамках курса Стэнфордского университета AA228V, посвященного валидации критически важных с точки зрения безопасности систем, прошла лекция о спецификации свойств. В ходе занятия были рассмотрены методы выявления предпочтений экспертов, основы пропозициональной логики и применение временной логики сигналов (STL) для оценки надежности автономных агентов.

## 🍬 Выявление весов через предпочтения: метод «кэнди-логики»
[[JUMP:0:05]]

В проектировании систем часто возникают противоречивые метрики. Например, для системы предотвращения столкновений самолетов одинаково важны низкая частота столкновений и низкая частота ложных срабатываний [0:30]. Оптимальные решения лежат на фронте Парето, но для выбора конкретной конфигурации необходимо использовать композитные метрики, такие как взвешенная сумма [1:36].

Ключевая проблема заключается в определении весов (коэффициентов важности). Вместо того чтобы спрашивать эксперта напрямую: «Какой вес вы дадите алерту против столкновения?», эффективнее использовать парные сравнения [3:25].

В качестве эксперимента со студентами был использован набор сладостей (M&Ms, Sour Patch Kids и Skittles). Вместо задания весового вектора $W$ напрямую, участнику предлагалось выбирать между двумя пакетами с разным количеством конфет [6:15]. 

**Каждый выбор формирует математическое ограничение:**

*   Если выбран пакет A вместо B, значит взвешенная сумма весов для состава A больше, чем для B [7:15].
*   Это ограничение отсекает часть пространства возможных весов, формируя так называемое «полупространство» (half-space) [10:20].
*   После серии из 4–5 запросов область допустимых весов сужается до небольшого многогранника, центр которого и принимается за искомый вектор предпочтений эксперта [13:30].

**Важные нюансы метода:**

1.  **Активное обучение:** можно не просто давать случайные пакеты, а подбирать такие пары, которые максимально делят оставшееся пространство весов пополам [15:27].
2.  **Иррациональность:** если эксперт дает противоречивые ответы, область допустимых весов может стать пустой [16:07]. В реальных задачах (например, в обучении с подкреплением на основе человеческих предпочтений, RLHF) это решается переходом к вероятностным моделям и байесовскому оцениванию [16:34].

## 🧩 Основы формальной логики: от атомов до предикатов
[[JUMP:18:50]]

Логическая спецификация — это четкое определение требований к системе, которое всегда вычисляется в «истину» (true) или «ложь» (false) [18:58].

**Пропозициональная логика** оперирует атомарными суждениями, которые невозможно разложить далее [19:24]. Для их связи используются стандартные операторы:

*   **Отрицание (NOT):** меняет значение на противоположное [20:33].
*   **Конъюнкция (AND):** истинна, только если оба условия верны [20:59].
*   **Дизъюнкция (OR):** истинна, если верно хотя бы одно из условий [21:11].
*   **Импликация (IF-THEN):** условие $P \implies Q$ ложно только в одном случае — если $P$ истинно, а $Q$ ложно [21:40].

**Логика первого порядка** расширяет эти возможности, добавляя переменные, предикаты и кванторы [25:01].

*   **Квантор всеобщности ($\forall$):** свойство должно выполняться для всех элементов (например, «все состояния траектории должны быть безопасны») [26:35].
*   **Квантор существования ($\exists$):** должно существовать хотя бы одно состояние, удовлетворяющее условию (например, «агент должен хотя бы раз достичь целевой точки») [27:18].

## ⏳ Временная логика (LTL и STL)
[[JUMP:30:51]]

Для систем, действующих во времени, пропозициональной логики недостаточно. Линейная временная логика (LTL) вводит операторы для описания последовательностей [31:19]:

1.  **Always ($\square$):** свойство должно быть истинным во все моменты времени в будущем [31:44].
2.  **Eventually ($\diamondsuit$):** свойство станет истинным хотя бы один раз в будущем [34:10].
3.  **Until ($U$):** условие $P$ должно выполняться до тех пор, пока не станет истинным условие $Q$ [35:03].

**Временная логика сигналов (STL)** делает еще один шаг вперед, позволяя работать с сигналами, принимающими вещественные значения, и временными интервалами [39:51]. На лекции был приведен пример спецификации для авиации: относительная высота между самолетами должна быть более 50 метров именно в интервале от 40 до 41 секунды полета (момент потенциального сближения) [47:39].

## 📈 Робастность и «гладкая» логика
[[JUMP:49:39]]

Обычная логика бинарна: система либо нарушила правило, либо нет. Однако STL позволяет вычислить **робастность** — числовое значение, которое показывает «запас прочности» до нарушения спецификации [52:06].

*   Если робастность $> 0$, система в безопасности. Чем выше число, тем дальше мы от опасной границы [52:18].
*   Если робастность $< 0$, спецификация нарушена. Чем меньше число, тем «глубже» провал [52:44].

**Проблема градиентов:**
При оптимизации систем инженерам нужно знать, в какую сторону менять параметры, чтобы повысить безопасность. Однако использование функций $min$ и $max$ в формулах STL создает «ступенчатые» градиенты: производная равна либо 0, либо 1 только в одной точке, что бесполезно для алгоритмов оптимизации [1:01:58].

**Решение — Smooth Robustness (Гладкая робастность):**
Операторы $min$ и $max$ заменяются на **Soft-Min** и **Soft-Max** [1:03:40]. С помощью параметра $W$ можно регулировать «мягкость» функции:

*   При низких значениях $W$ результат приближается к среднему значению сигнала [1:04:06].
*   При стремлении $W$ к бесконечности функция превращается в жесткий $min/max$ [1:04:20].

Это позволяет рассчитывать честные градиенты для всей траектории, учитывая вклад каждого временного шага в общую оценку безопасности, что критически важно для автоматизированного поиска отказов и дообучения нейросетевых контроллеров [1:07:33].