В дискуссиях вокруг безопасности искусственного интеллекта доминируют два полюса: апокалиптические сценарии скорого вымирания человечества и пренебрежительное отрицание любых угроз. На площадке YC Paper Club содиректоры Stanford Center for AI Safety Кларк Барретт и Майкел Кохендерфер вместе с ведущим Франсуа разобрали реальные инженерные методы верификации сложных систем, перенесённые из авиации и математической логики в современный стек машинного обучения.
🛰️ Истерия против науки: уроки технологических кризисов 0:07
Обсуждение безопасности искусственного интеллекта регулярно скатывается в эмоциональные крайности, уходя от проверяемых гипотез и математической строгости . По оценке ведущего Франсуа, паника возникает там, где общество не способно измерить масштаб явления, но не прекращает о нём говорить .
Исторические параллели показывают, что подобная тревожность сопровождала практически каждую крупную техническую революцию:
- В ходе Манхэттенского проекта учёные всерьёз обсуждали гипотезу о том, что ядерный взрыв подожжёт земную атмосферу .
- В 1950-х годах Алан Тьюринг высказывал опасения, что машины быстро превзойдут человеческие способности во всех сферах, однако его временные рамки оказались оторванными от реальности .
- На заре промышленной автоматизации Карл Маркс и Джон Мейнард Кейнс прогнозировали необратимую тотальную технологическую безработицу .
- Изобретатель Ethernet Роберт Меткалф публично предрекал скорый катастрофический коллапс интернета из-за лавинообразного роста трафика и DDoS-атак — позже ему пришлось в буквальном смысле перемолоть свою статью в блендере и выпить её .
- Массовое появление поисковых систем и смартфонов критики трактовали как необратимый упадок человеческого интеллекта .
Ян Лекун и Дженсен Хуанг настаивают на том, что безопасность критических технологий — это сугубо инженерная задача, требующая строгих методов проектирования, а не абстрактных рассуждений . В авиации надёжность сложнейших систем вроде MCAS на Boeing 737 или комплексов предупреждения столкновений ACAS X достигается десятилетиями направленных проверок .
На противоположном полюсе находятся заявления исследователей вроде Джейкоба Стенхардта, оценивающих риск потери контроля над интеллектуальными системами с последующим вымиранием человечества более чем в 10% в ближайшие 10 лет .
🕵️ Инцидент с Hugging Face: фактчекинг заголовков 6:04
Показательным примером искажения реальности в медиа ведущий называет резонансное освещение инцидента с OpenAI и платформой Hugging Face . В заголовках утверждалось, что автономный агент вышел из-под контроля разработчиков, сбежал на внешние серверы и начал взламывать правительственные ресурсы .
Реальная картина инцидента, изложенная в 60-страничном техническом отчёте исследовательской группы ExploitDev, носит совершенно иной характер :
- Атака была полностью управляемым процессом в рамках тестирования, в котором задействовали сеть из более чем 1200 взаимодействующих агентов с длинными цепочками рассуждений (chain of thought) .
- Утечка и несанкционированные действия стали следствием банального сбоя конфигурации тестовой среды: модуль мониторинга CO2 был непреднамеренно отключён .
- Защитные барьеры продакшн-окружения не сработали исключительно потому, что агент запускался в изолированном экспериментальном контуре, где эти механизмы были деактивированы инженерами .
По словам Франсуа, миф о вероятности глобальной катастрофы «10% за 10 лет» во многом базируется на неверно интерпретированном опросе 2023 года среди 1200 авторов научных публикаций по ИИ . Респондентам задавали вопрос о гипотетическом риске исчезновения человечества на горизонте 100 лет, а не текущего десятилетия . При этом ведущий подчеркнул: попытки предсказывать столь отдалённое будущее экспертами малопродуктивны, так как в 2012 году ни один профессор Стэнфорда не смог бы точно спрогнозировать прогресс в решении математических задач тысячелетия с помощью нейросетей .
🔓 Реальная угроза: открытые веса и асимметрия кибероружия 11:21
По мнению Франсуа, экзистенциальный риск зарождения у языковых моделей собственной воли или стремления поработить людей в горизонте 10–20 лет пренебрежимо мал . Главная практическая опасность кроется в доступности мощных моделей с открытыми весами для преступных группировок и враждебных государств .
В качестве примера ведущий приводит реальный инцидент в польской районной больнице, компьютерные системы которой были парализованы на три недели в результате атаки вымогателей . Мощные открытые модели существенно снижают порог входа для разработки подобных кибератак и создания биологических угроз .
Популярные инициативы регуляторов по предотвращению этих рисков спикер считает неэффективными:
- Запрет открытых моделей с весами: невыполним технически, так как веса китайских моделей (вроде Kimi k1.5 или GLM) уже скачаны тысячами инженеров по всему миру .
- Регистрация и лицензирование GPU: невозможно проконтролировать чипы в частных гаражах или запретить аренду вычислительных мощностей в зарубежных юрисдикциях .
- Мониторинг потребления электросети: хотя энергокомпании способны выявлять паттерны мощных потребителей, этот барьер легко обходится распределёнными инфраструктурами .
Единственным устойчивым решением остаётся масштабная инвестиция в средства киберзащиты . Инфраструктура многих корпораций и финансовых институтов опирается на устаревшие системы, где базовой уязвимостью до сих пор остаются стандартные пароли admin . Опережающее развитие передовых оборонительных ИИ-моделей позволяет парировать атаки, использующие менее совершенные открытые алгоритмы .
📐 Автоматизированные рассуждения: математическая броня для софта 17:25
Кларк Барретт, содиректор Stanford Center for AI Safety, раскрыл концепцию конвергенции генеративного искусственного интеллекта и автоматизированных рассуждений (automated reasoning, AR) . Если нейросети отлично обобщают сложные неструктурированные данные, но не гарантируют безошибочность, то формальные математические методы обеспечивают стопроцентную строгость доказательств, но исторически плохо масштабируются .
Классическая формальная верификация требовала сотен часов работы редких специалистов . Однако Барретт настаивает: математически верифицированный код невозможно взломать в рамках заявленных спецификаций .
Для масштабирования этого подхода стэнфордская лаборатория вместе с создателем системы Lean Леонардо де Моурой запустила открытый проект CSLib . По аналогии с математической библиотекой Mathlib, CSLib формирует базу формализованных теорий компьютерных наук и инфраструктуру для верификации кода :
- Исходный код на произвольном языке программирования транслируется в единый промежуточный язык логических утверждений .
- Генератор условий корректности формирует набор лемм в среде Lean .
- Для закрытия целей доказательства применяются как легковесные SMT-солверы (инструмент Lean SMT), решающие большинство задач за доли секунды на CPU, так и специализированные нейросетевые агенты .
┌────────────────────────────────────────────────────────┐
│ Исходный код (Rust / C) │
└──────────────────────────┬─────────────────────────────┘
│
▼
┌────────────────────────────────────────────────────────┐
│ Логическое представление (предусловия, инварианты) │
└──────────────────────────┬─────────────────────────────┘
│
▼
┌────────────────────────────────────────────────────────┐
│ Генератор условий верификации (CSLib / Lean) │
└──────────────────────────┬─────────────────────────────┘
│
┌────────────┴────────────┐
▼ ▼
┌───────────────────────────┐ ┌──────────────────────────┐
│ Lean SMT (мгновенно, CPU)│ │ LLM-агенты доказательств │
└───────────────────────────┘ └──────────────────────────┘
В качестве практического подтверждения Барретт продемонстрировал верификацию криптографической библиотеки Dick Light на Rust . Из 35 сгенерированных формальных теорий модуль Lean SMT мгновенно доказал 32, а оставшиеся три были закрыты после однократного раскрытия определений .
Более сложный эксперимент лаборатории показал: криптографическая библиотека на Rust объёмом 30 000 строк кода, ручная верификация которой ранее заняла у пяти экспертов три месяца, была полностью автоматически доказана за 11 часов с помощью разработанного верификационного агента .
Для решения проблемы написания спецификаций команда Барретта создала утилиту Varys Forge . Разработчик формулирует требования на обычном английском языке, инструмент генерирует структурированные спецификации, пишет код на Rust и немедленно доказывает его корректность во встроенном верификаторе, исключая расхождения . Барретт также объявил о создании стартапа Untruth, цель которого — построение промышленного движка сквозного доказательства программного обеспечения .
✈️ Адаптивное стресс-тестирование: от автопилотов к LLM 27:55
Майкел Кохендерфер представил методики обеспечения надёжности, разработанные в Стэнфордской лаборатории интеллектуальных систем (SISL) . В коммерческой авиации золотым стандартом безопасности является непревышение порога в $10^{-9}$ катастрофических отказов на один лётный час .
Прямое статистическое моделирование для подтверждения такой надёжности требует нереалистичных вычислительных затрат: чтобы зафиксировать хотя бы 10 инцидентов, необходимо смоделировать порядка $10^{10}$ часов полёта . Решением стала методология адаптивного стресс-тестирования (Adaptive Stress Testing, AST), изначально созданная аспирантом Ричи Ли в сотрудничестве с NASA для валидации авиационной системы ACAS X .
Метод AST заменяет случайный перебор целенаправленным поиском отказов с помощью алгоритмов обучения с подкреплением и выборки по значимости (importance sampling) :
- Вместо реального распределения сценариев $P$ генерируется смещённое распределение предложений $Q$, концентрирующееся на критических режимах .
- Итоговая вероятность сбоя корректируется обратным весовым коэффициентом $P / Q$ .
- Для охвата мультимодальных отказов (например, отклонение перевёрнутого маятника или спуск лунного модуля) применяются диффузионные модели и нормализующие потоки, предотвращающие застревание алгоритма в одном сценарии .
Сегодня лаборатория Кохендерфера переносит принципы AST на большие языковые модели для поиска токсичности и деструктивных выводов . Если в авиации катастрофа формализована как физическое сближение воздушных судов ближе 500 футов по горизонтали и 100 футов по вертикали, то в LLM целевой функцией ошибки выступает высокая токсичность (оцениваемая моделью Llama Guard) при минимальной перплексии (естественности текста) .
Кроме того, исследователи разработали фреймворки Reluplex и Marabou для формальной верификации глубоких нейросетей с кусочно-линейными функциями активации , а также открытую библиотеку POMDPs.jl на языке Julia для планирования решений в условиях неполной наблюдаемости . Совместно с Airbus стэнфордские учёные развивают мониторинг во время исполнения (runtime monitoring) для бортовых систем компьютерного зрения .
Для стандартизации тестов запущена открытая платформа BetterBench, выявляющая моменты насыщения бенчмарков и анализирующая систематические ошибки в суждениях оценщиков .
🏛️ Архитектура доверия: NTSB для искусственного интеллекта 43:53
Обсуждая институциональные механизмы регулирования, Майкел Кохендерфер предложил масштабировать на сферу искусственного интеллекта опыт Национального совета по безопасности на транспорте США (NTSB) . Благодаря деятельности независимого NTSB и внедрению в 1967 году системы добровольных анонимных отчётов об инцидентах ASRS коммерческая авиация стала в 80 раз безопаснее по сравнению с 1970-ми годами [45:44, 46:34].
Ключевые принципы авиационного подхода к расследованию инцидентов:
- Независимость от регулирующих и коммерческих органов: следователи не преследуют цели наказать виновных, их единственная задача — выявить первопричину сбоя .
- Иммунитет от преследования: инженеры и пилоты открыто передают данные об ошибках без страха санкций .
- Глобальная юрисдикция по компонентам: присутствие американских компонентов в конструкции даёт право участвовать в расследовании катастроф по всему миру .
Франсуа предостерёг от опасности регуляторного захвата (regulatory capture), когда монополисты используют правила для удушения конкурентов . В качестве примера ведущий привёл статус сервисов Uber, Lyft, DoorDash и Instacart, исключённых в ряде штатов из стандартных требований трудового законодательства по форме 1099, что блокирует запуск новых стартапов . Аналогично, если бы регулирование интернета строилось под диктовку технологических гигантов, выдача SSL-сертификатов или регистрация доменов могли бы стать их исключительной прерогативой .
Барретт поддержал идею независимого аудита, отметив, что frontier-лаборатории сами заинтересованы в беспристрастной внешней оценке . Однако роль аудитора должна заключаться не в выдаче субъективных вердиктов («верьте нам»), а в предоставлении машиночитаемых криптографических сертификатов, которые любой пользователь может проверить самостоятельно .
🛡️ Безопасность на практике: модель швейцарского сыра 52:18
Кларк Барретт высказал оптимистичный прогноз: в течение трёх–пяти лет проблема кибербезопасности программного кода может быть принципиально решена за счёт математической верификации . По его мнению, современная программная инженерия слишком долго полагалась на слепое тестирование вместо строгих научных принципов . При наличии формального доказательства отпадает необходимость даже в 100-процентном покрытии юнит-тестами — они полезны для быстрой отладки, но математический вывод перекрывает их по надёжности .
На гипотетический вопрос о том, как бы Барретт распорядился бюджетом в $10 млрд на посту директора по информационной безопасности Bank of America, профессор ответил:
- Нанять пул ведущих специалистов по формальным методам и развернуть вычислительную инфраструктуру на GPU с агентами доказательств .
- Транслировать легаси-код банка в безопасные языки (Rust, Lean) .
- Математически доказать базовые глобальные инварианты — прежде всего, абсолютную безопасность работы с памятью (memory safety), что навсегда исключит уязвимости переполнения буфера, до сих пор удерживающие первое место по числу атак [1:02:12, 1:07:07].
- Формализовать фундаментальные бизнес-правила (например, закон сохранения баланса при выполнении финансовых транзакций) .
При этом исследователи подчеркнули разницу между верификацией софта и физического мира. Как отметил Кохендерфер, любая математическая модель базируется на исходных предположениях . Формальные методы задают границы неопределённости множествами, но если в реальном мире другой пилот решит намеренно протаранить самолёт, формальное доказательство безопасности окажется невалидным .
В связи с этим спикеры призвали опираться на проверенную в авиации концепцию «швейцарского сыра» Джеймса Ризона . Безопасность сложной системы обеспечивается серией эшелонированных фильтров:
[Данные обучения / Деконтаминация] ──► (Слой 1)
│
▼
[Предобучение и фильтрация весов] ──► (Слой 2)
│
▼
[Постобучение: RLHF / DPO / RSI] ──► (Слой 3)
│
▼
[Стресс-тестирование (AST/Llama Guard)] ──► (Слой 4)
│
▼
[Мониторинг исполнения (Runtime) + Архитектура Zero Trust] ──► ВЫХОД
Отверстия в ломтиках сыра — это неизбежные локальные уязвимости отдельных методов. Главная цель инженерии — спроектировать систему так, чтобы отверстия в разных слоях никогда не выстраивались на одной линии . Недавний инцидент с Hugging Face как раз продемонстрировал пробитие нескольких слоёв: отказ монитора цепочки рассуждений совпал с отключением защитных барьеров окружения .
💡 Будущее индустрии и ответы на вопросы 1:05:43
В рамках сессии ответов на вопросы профессора Стэнфорда затронули ключевые вызовы практического внедрения систем безопасности:
- Генерация спецификаций: в корпоративном коде спецификации отсутствуют почти всегда. По мнению Барретта, современные ИИ-ассистенты уже способны вести диалог с разработчиком, предлагая учесть крайние случаи и автоматически формулируя инварианты . Даже частичная формализация требований существенно превосходит качество обычного кода .
- Специфика регулирования: профессор Крис Гердес (экс-директор по инновациям Министерства транспорта США, ныне работающий в Waymo) показал регуляторам в Вашингтоне, что директивно предписывать конкретные алгоритмы преждевременно . Стандарты должны задавать высокоуровневые метрики безопасности, не ограничивая инженерный поиск . При этом компании сегмента автономного вождения не конкурируют на безопасности: авария автомобиля Zoox наносит прямой репутационный ущерб Waymo, и наоборот .
- Принцип бритвы Оккама в ML: Кохендерфер подчеркнул, что в корпоративных внедрениях руководители часто поддаются соблазну неоправданно использовать трансформеры . Если прикладную задачу можно решить линейной регрессией или деревьями решений, следует выбирать именно их, так как интерпретируемость напрямую обеспечивает надёжность .
- Экспоненциальный рост нагрузки на человеческий аудит: в эпоху интернета масштаб казался управляемым, однако автоматические агенты создают угрозу функционального DDoS для общественных институтов . Франсуа отметил, что на конференции ICLR число заявок достигло 60 000 в год , а массовое использование ИИ-агентов для подачи исков в суды мелких тяжб способно полностью парализовать правовую систему .
В завершение дискуссии Франсуа указал на необходимость создания независимого модерируемого репозитория бенчмарков наподобие App Store от Apple . Сегодня бенчмарки на Hugging Face напоминают «Дикий Запад», где на один тест GSM8K существуют сотни несовместимых версий с повреждёнными данными, что мешает объективному научному прогрессу .
