В рамках курса Стэнфордского университета AA228V, посвященного валидации критически важных с точки зрения безопасности систем, прошла лекция о спецификации свойств. В ходе занятия были рассмотрены методы выявления предпочтений экспертов, основы пропозициональной логики и применение временной логики сигналов (STL) для оценки надежности автономных агентов.
🍬 Выявление весов через предпочтения: метод «кэнди-логики» 0:05
В проектировании систем часто возникают противоречивые метрики. Например, для системы предотвращения столкновений самолетов одинаково важны низкая частота столкновений и низкая частота ложных срабатываний . Оптимальные решения лежат на фронте Парето, но для выбора конкретной конфигурации необходимо использовать композитные метрики, такие как взвешенная сумма .
Ключевая проблема заключается в определении весов (коэффициентов важности). Вместо того чтобы спрашивать эксперта напрямую: «Какой вес вы дадите алерту против столкновения?», эффективнее использовать парные сравнения .
В качестве эксперимента со студентами был использован набор сладостей (M&Ms, Sour Patch Kids и Skittles). Вместо задания весового вектора $W$ напрямую, участнику предлагалось выбирать между двумя пакетами с разным количеством конфет .
Каждый выбор формирует математическое ограничение:
- Если выбран пакет A вместо B, значит взвешенная сумма весов для состава A больше, чем для B .
- Это ограничение отсекает часть пространства возможных весов, формируя так называемое «полупространство» (half-space) .
- После серии из 4–5 запросов область допустимых весов сужается до небольшого многогранника, центр которого и принимается за искомый вектор предпочтений эксперта .
Важные нюансы метода:
- Активное обучение: можно не просто давать случайные пакеты, а подбирать такие пары, которые максимально делят оставшееся пространство весов пополам .
- Иррациональность: если эксперт дает противоречивые ответы, область допустимых весов может стать пустой . В реальных задачах (например, в обучении с подкреплением на основе человеческих предпочтений, RLHF) это решается переходом к вероятностным моделям и байесовскому оцениванию .
🧩 Основы формальной логики: от атомов до предикатов 18:50
Логическая спецификация — это четкое определение требований к системе, которое всегда вычисляется в «истину» (true) или «ложь» (false) .
Пропозициональная логика оперирует атомарными суждениями, которые невозможно разложить далее . Для их связи используются стандартные операторы:
- Отрицание (NOT): меняет значение на противоположное .
- Конъюнкция (AND): истинна, только если оба условия верны .
- Дизъюнкция (OR): истинна, если верно хотя бы одно из условий .
- Импликация (IF-THEN): условие $P \implies Q$ ложно только в одном случае — если $P$ истинно, а $Q$ ложно .
Логика первого порядка расширяет эти возможности, добавляя переменные, предикаты и кванторы .
- Квантор всеобщности ($\forall$): свойство должно выполняться для всех элементов (например, «все состояния траектории должны быть безопасны») .
- Квантор существования ($\exists$): должно существовать хотя бы одно состояние, удовлетворяющее условию (например, «агент должен хотя бы раз достичь целевой точки») .
⏳ Временная логика (LTL и STL) 30:51
Для систем, действующих во времени, пропозициональной логики недостаточно. Линейная временная логика (LTL) вводит операторы для описания последовательностей :
- Always ($\square$): свойство должно быть истинным во все моменты времени в будущем .
- Eventually ($\diamondsuit$): свойство станет истинным хотя бы один раз в будущем .
- Until ($U$): условие $P$ должно выполняться до тех пор, пока не станет истинным условие $Q$ .
Временная логика сигналов (STL) делает еще один шаг вперед, позволяя работать с сигналами, принимающими вещественные значения, и временными интервалами . На лекции был приведен пример спецификации для авиации: относительная высота между самолетами должна быть более 50 метров именно в интервале от 40 до 41 секунды полета (момент потенциального сближения) .
📈 Робастность и «гладкая» логика 49:39
Обычная логика бинарна: система либо нарушила правило, либо нет. Однако STL позволяет вычислить робастность — числовое значение, которое показывает «запас прочности» до нарушения спецификации .
- Если робастность $> 0$, система в безопасности. Чем выше число, тем дальше мы от опасной границы .
- Если робастность $< 0$, спецификация нарушена. Чем меньше число, тем «глубже» провал .
Проблема градиентов: При оптимизации систем инженерам нужно знать, в какую сторону менять параметры, чтобы повысить безопасность. Однако использование функций $min$ и $max$ в формулах STL создает «ступенчатые» градиенты: производная равна либо 0, либо 1 только в одной точке, что бесполезно для алгоритмов оптимизации .
Решение — Smooth Robustness (Гладкая робастность): Операторы $min$ и $max$ заменяются на Soft-Min и Soft-Max . С помощью параметра $W$ можно регулировать «мягкость» функции:
- При низких значениях $W$ результат приближается к среднему значению сигнала .
- При стремлении $W$ к бесконечности функция превращается в жесткий $min/max$ .
Это позволяет рассчитывать честные градиенты для всей траектории, учитывая вклад каждого временного шага в общую оценку безопасности, что критически важно для автоматизированного поиска отказов и дообучения нейросетевых контроллеров .
