Шрирам Кришнамуртхи, профессор компьютерных наук в Университете Брауна, уверен: создатели инструментов формальной верификации совершают фундаментальную ошибку, игнорируя человеческий фактор. В рамках семинара в Стэнфордском университете он представил результаты многолетних исследований, доказывающих, что математически безупречные алгоритмы могут быть бесполезны и даже вредны, если они не учитывают особенности человеческого восприятия и когнитивные искажения.
🧩 От математической логики к «человеческим SAT-солверам» 0:09
Кришнамуртхи начинает выступление с интерактивного упражнения, предлагая аудитории решить задачи на выполнимость логических формул (SAT). Этот простой тест служит метафорой: любые технические вопросы безопасности или сетевой инженерии в конечном итоге сводятся к вопросам выполнимости. Инструменты вроде Alloy (разработанный в MIT) позволяют преобразовывать сложные спецификации систем в логические формулы, которые затем обрабатываются солверами.
Процесс работы с такими инструментами обычно выглядит так:
- Инженер пишет спецификацию (например, для бинарного дерева).
- Формулирует свойства, которые должны быть истинны.
- Нажимает кнопку «выполнить».
- Если свойство ложно, система выдает контрпример — визуальную схему, показывающую, где именно произошел сбой.
Однако, как отмечает Кришнамуртхи, здесь кроется «фатальный изъятие»: если пользователь не может четко артикулировать свойства системы, инструмент не сделает ровным счетом ничего. Именно в этот момент формальные методы сталкиваются с психологией: как человек понимает, что именно он хочет проверить?
📉 Провал «минимализма»: когда математика мешает пониманию 6:31
Одной из классических идей в верификации является поиск «минимальных» контрпримеров. Логика проста: чем меньше объектов на экране, тем легче найти ошибку. Команда Кришнамуртхи даже разработала системы Aluminum (для поиска минимальных моделей) и Amalgam (для отслеживания происхождения данных), за которые получила академические награды.
Однако последующее исследование на реальных пользователях (студентах и работниках Mechanical Turk) показало катастрофические результаты:
- Пользователи отвергли «улучшенные» инструменты: Большинство участников исследования предпочли вернуться к стандартному Alloy, который выдавал «грязные» и сложные примеры.
- Минимализм вводит в заблуждение: Студенты, использовавшие минимальные модели, чаще совершали ошибки в коде. Кришнамуртхи утверждает, что слишком лаконичные примеры не давали достаточного контекста для понимания сути проблемы.
По мнению спикера, это стало болезненным уроком: то, что заставляет «математиков пускать слюни» (элегантная минимизация), на практике оказывается абсолютно непригодным для обучения и работы людей.
👁️ Принцип контрастных случаев и обучение через негатив 14:09
Чтобы исправить ситуацию, Кришнамуртхи предлагает обратиться к когнитивной психологии, в частности к работам Дэна Шварца из Стэнфорда. Основная идея — «принцип контрастных случаев», согласно которому люди учатся лучше, когда видят несколько систематически связанных примеров одновременно.
В ходе экспериментов с абстрактными моделями («общество блобов») были сделаны важные выводы:
- Негативные примеры критически важны: Показ того, чем система не является, помогает пользователю очертить границы допустимого пространства гораздо эффективнее, чем только позитивные примеры.
- Эффект переключения (Toggle): Самым успешным методом обучения оказалась возможность мгновенно переключаться между позитивным примером и ближайшим к нему негативным. Пользователи нажимали кнопку переключения до семи раз, используя свою зрительную кору для поиска тонких различий.
🧠 Эффект Струпа в визуализации данных 22:24
Кришнамуртхи жестко критикует стандартные «универсальные» визуализаторы. Он демонстрирует классическую проблему: когда графические инструменты расставляют объекты случайно или просто фиксируют их положение, они игнорируют пространственно-временные смыслы домена.
В качестве примера приводится «Эффект Струпа» — задержка реакции, когда цвет слова не совпадает с его значением (например, слово «красный», написанное синим цветом). Аналогично, если в визуализации криптографического протокола сообщения между Алисой и Бобом перемешаны или лишены временной последовательности («дорожек» или swim lanes), мозг пользователя тратит лишние ресурсы на расшифровку картинки вместо анализа сути.
Новый инструмент автора, Forge, стремится решить это через:
- Доменно-специфичные визуализации: Отрисовка протоколов в привычном для криптографов виде.
- Учет пространственных свойств: Фиксация левой и правой сторон там, где это семантически важно (например, в задаче об обедающих философах или переправе через реку).
🚦 Ловушка «естественного» языка в логике (LTL) 31:12
Особое внимание Кришнамуртхи уделяет линейной темпоральной логике (LTL). Исследование показало, что даже профессиональные исследователи постоянно ошибаются в интерпретации оператора Until (до тех пор, пока).
Проблема заключается в «вернакулярном заблуждении» (vernacular misconception): мы берем слово из обычного языка и наделяем его строгим техническим смыслом.
- Пример: Фраза «двигатель включен, пока робот не достигнет цели». В жизни мы ожидаем, что у цели двигатель выключится. Но в математической логике LTL это не обязательно так.
Спикер полагает, что использование интуитивно понятных слов в названиях логических операторов может быть вредным, так как пользователи привносят в них багаж бытовых ассоциаций. Он предлагает проектировать языки логики «снизу вверх», основываясь на том, как люди реально воспринимают эти конструкции, а не на эстетике математиков.
🎓 Радикальный тезис: любой разработчик — это учитель 40:45
В финале выступления Кришнамуртхи выдвигает провокационную идею: любой человек, создающий инструменты (от компиляторов до мобильных приложений), занимается образованием.
«Когда компилятор выдает сообщение об ошибке, он не просто констатирует факт. Он пытается научить вас правилам формальной системы и особенностям вашего собственного артефакта одновременно».
Автор признает, что даже его собственные проекты с благими намерениями, такие как DrRacket (бывший DrScheme), после 15 лет разработки провалили формальные тесты на удобство для студентов. Это подчеркивает главную мысль лекции: добрых намерений недостаточно — инструменты формальных методов должны проходить жесткую валидацию с точки зрения когнитивных наук и теорий обучения.
