# Профессор Кришнамуртхи о формальных методах: почему математически идеальные модели вредят пользователям? Источник: https://www.youtube.com/watch?v=wBRtEQ02-HI Канал: Stanford Online Опубликовано: 07.05.2024 --- Шрирам Кришнамуртхи, профессор компьютерных наук в Университете Брауна, уверен: создатели инструментов формальной верификации совершают фундаментальную ошибку, игнорируя человеческий фактор. В рамках семинара в Стэнфордском университете он представил результаты многолетних исследований, доказывающих, что математически безупречные алгоритмы могут быть бесполезны и даже вредны, если они не учитывают особенности человеческого восприятия и когнитивные искажения. ## 🧩 От математической логики к «человеческим SAT-солверам» [[JUMP:00:09]] Кришнамуртхи начинает выступление с интерактивного упражнения, предлагая аудитории решить задачи на выполнимость логических формул (SAT). Этот простой тест служит метафорой: любые технические вопросы безопасности или сетевой инженерии в конечном итоге сводятся к вопросам выполнимости. Инструменты вроде **Alloy** (разработанный в MIT) позволяют преобразовывать сложные спецификации систем в логические формулы, которые затем обрабатываются солверами. Процесс работы с такими инструментами обычно выглядит так: * Инженер пишет спецификацию (например, для бинарного дерева). * Формулирует свойства, которые должны быть истинны. * Нажимает кнопку «выполнить». * Если свойство ложно, система выдает контрпример — визуальную схему, показывающую, где именно произошел сбой. Однако, как отмечает Кришнамуртхи, здесь кроется «фатальный изъятие»: если пользователь не может четко артикулировать свойства системы, инструмент не сделает ровным счетом ничего. Именно в этот момент формальные методы сталкиваются с психологией: как человек понимает, что именно он хочет проверить? ## 📉 Провал «минимализма»: когда математика мешает пониманию [[JUMP:06:31]] Одной из классических идей в верификации является поиск «минимальных» контрпримеров. Логика проста: чем меньше объектов на экране, тем легче найти ошибку. Команда Кришнамуртхи даже разработала системы **Aluminum** (для поиска минимальных моделей) и **Amalgam** (для отслеживания происхождения данных), за которые получила академические награды. Однако последующее исследование на реальных пользователях (студентах и работниках Mechanical Turk) показало катастрофические результаты: 1. **Пользователи отвергли «улучшенные» инструменты:** Большинство участников исследования предпочли вернуться к стандартному Alloy, который выдавал «грязные» и сложные примеры. 2. **Минимализм вводит в заблуждение:** Студенты, использовавшие минимальные модели, чаще совершали ошибки в коде. Кришнамуртхи утверждает, что слишком лаконичные примеры не давали достаточного контекста для понимания сути проблемы. По мнению спикера, это стало болезненным уроком: то, что заставляет «математиков пускать слюни» (элегантная минимизация), на практике оказывается абсолютно непригодным для обучения и работы людей. ## 👁️ Принцип контрастных случаев и обучение через негатив [[JUMP:14:09]] Чтобы исправить ситуацию, Кришнамуртхи предлагает обратиться к когнитивной психологии, в частности к работам Дэна Шварца из Стэнфорда. Основная идея — «принцип контрастных случаев», согласно которому люди учатся лучше, когда видят несколько систематически связанных примеров одновременно. В ходе экспериментов с абстрактными моделями («общество блобов») были сделаны важные выводы: * **Негативные примеры критически важны:** Показ того, чем система *не является*, помогает пользователю очертить границы допустимого пространства гораздо эффективнее, чем только позитивные примеры. * **Эффект переключения (Toggle):** Самым успешным методом обучения оказалась возможность мгновенно переключаться между позитивным примером и ближайшим к нему негативным. Пользователи нажимали кнопку переключения до семи раз, используя свою зрительную кору для поиска тонких различий. ## 🧠 Эффект Струпа в визуализации данных [[JUMP:22:24]] Кришнамуртхи жестко критикует стандартные «универсальные» визуализаторы. Он демонстрирует классическую проблему: когда графические инструменты расставляют объекты случайно или просто фиксируют их положение, они игнорируют пространственно-временные смыслы домена. В качестве примера приводится «Эффект Струпа» — задержка реакции, когда цвет слова не совпадает с его значением (например, слово «красный», написанное синим цветом). Аналогично, если в визуализации криптографического протокола сообщения между Алисой и Бобом перемешаны или лишены временной последовательности («дорожек» или swim lanes), мозг пользователя тратит лишние ресурсы на расшифровку картинки вместо анализа сути. Новый инструмент автора, **Forge**, стремится решить это через: * **Доменно-специфичные визуализации:** Отрисовка протоколов в привычном для криптографов виде. * **Учет пространственных свойств:** Фиксация левой и правой сторон там, где это семантически важно (например, в задаче об обедающих философах или переправе через реку). ## 🚦 Ловушка «естественного» языка в логике (LTL) [[JUMP:31:12]] Особое внимание Кришнамуртхи уделяет линейной темпоральной логике (**LTL**). Исследование показало, что даже профессиональные исследователи постоянно ошибаются в интерпретации оператора **Until** (до тех пор, пока). Проблема заключается в «вернакулярном заблуждении» (vernacular misconception): мы берем слово из обычного языка и наделяем его строгим техническим смыслом. * **Пример:** Фраза «двигатель включен, пока робот не достигнет цели». В жизни мы ожидаем, что у цели двигатель выключится. Но в математической логике LTL это не обязательно так. Спикер полагает, что использование интуитивно понятных слов в названиях логических операторов может быть вредным, так как пользователи привносят в них багаж бытовых ассоциаций. Он предлагает проектировать языки логики «снизу вверх», основываясь на том, как люди реально воспринимают эти конструкции, а не на эстетике математиков. ## 🎓 Радикальный тезис: любой разработчик — это учитель [[JUMP:40:45]] В финале выступления Кришнамуртхи выдвигает провокационную идею: любой человек, создающий инструменты (от компиляторов до мобильных приложений), занимается образованием. > «Когда компилятор выдает сообщение об ошибке, он не просто констатирует факт. Он пытается научить вас правилам формальной системы и особенностям вашего собственного артефакта одновременно». Автор признает, что даже его собственные проекты с благими намерениями, такие как **DrRacket** (бывший DrScheme), после 15 лет разработки провалили формальные тесты на удобство для студентов. Это подчеркивает главную мысль лекции: добрых намерений недостаточно — инструменты формальных методов должны проходить жесткую валидацию с точки зрения когнитивных наук и теорий обучения.