Математикам больше всего нравятся доказательства с ясным началом, серединой и концовкой, захватывающей историей от формулировки гипотезы до выведения теоремы. Повествование здесь важнее, чем придирчивая логика. Цели должны быть ясными, четкими и, самое главное, убедительными. При этом следует помнить, что математиков всегда было очень трудно убедить.
Специалисты по информатике, изучающие машинную проверку доказательств, предложили совершенно иной подход: интерактивные доказательства. Вместо того чтобы представлять доказательство как повествование, написанное одним математиком и читаемое другим, этот подход превращает доказательство в диспут. Один математик, традиционно его называют Пат, хочет убедить Ванну в том, что его доказательство корректно. Ванна, напротив, хочет убедить его, что он ошибается. Они задают друг другу вопросы и дают на них ответы, пока один из них не уступит. (Пат Саджак и Ванна Уайт были ведущими популярного американского телешоу «Колесо фортуны».) Все это напоминает партию в шахматы, где Пат обещает «мат в четыре хода». Ванна не соглашается, так что Пат делает ход. Ванна ходит в ответ: «А что, если я пойду так?» И Пат делает следующий ход. Этот обмен репликами продолжается до тех пор, пока Ванна не проиграет. После этого она начинает отыгрывать назад. «А если бы мой последний ход был таким на самом деле?» Пат ходит по-другому, шах и мат! И так продолжается до тех пор, пока Ванна не исчерпает возможные ответы, а Пат не выиграет, или до тех пор, пока он не признает, что мат в четыре хода невозможен. Согласно моему опыту, именно так ведут себя настоящие математики, когда работают вместе над решением исследовательской задачи, и споры разгораются нешуточные. А нарратив нужен, чтобы представить окончательный результат на семинаре.
Ласло Бабаи и другие ученые ввели методы «диалогового» доказательства такого типа в концепцию прозрачного доказательства, использовав при этом такие математические инструменты, как многочлены над конечными полями и корректирующие коды{31}. После отладки этих методов выяснилось, что компьютеры способны использовать одно свойство, которое несовместимо с ясностью и лаконичностью, а именно избыточность. Оказывается, любое логическое доказательство можно переписать таким образом, что оно станет намного длиннее, но при этом и ошибка, если она в нем присутствует, проявится едва ли не всюду. Каждый логический шаг размазывается по всему доказательству в виде многочисленных взаимосвязанных почти идентичных копий. Это немного напоминает принцип голограммы, где изображение преобразуется так, что его можно восстановить по любой небольшой части данных. После этого доказательство можно проверить, взяв из него небольшой случайный образец. Ошибка почти наверняка окажется в нем. Сделайте это, и вы получите прозрачное доказательство. Интересующая нас теорема о невозможности существования приближенных решений класса P – следствие этой процедуры.
Вернемся к голубиной статье Гибсона, Уилкинсона и Келли в журнале Animal Cognition. Авторы начинают с замечания о том, что в последнее время задача коммивояжера используется для исследования некоторых аспектов когнитивных процессов у людей и животных, в первую очередь способности планировать действия до их осуществления. Однако долгое время было неясно, ограничивается ли эта способность приматами. Могут ли другие животные тоже планировать действия заранее, или они просто следуют жестким правилам, выработанным в процессе эволюции? Исследователи решили использовать голубей в лабораторных испытаниях с двумя или тремя точками-кормушками. Голуби стартуют из одного места, посещают все кормушки в каком-то порядке и улетают к финишу. Исследователи пришли к выводу, что «голуби отдавали предпочтение ближайшей локации, но, судя по всему, планировали на несколько шагов вперед, когда издержки неэффективного поведения очевидно возрастали. Результаты ясно свидетельствуют, что не только приматы способны планировать сложные маршруты передвижения».
В одном из интервью исследователи объяснили связь с голубем, мечтавшим водить автобус. По их мнению, водителя автобуса может беспокоить, что голубь не способен безопасно вести автобус. Еще больше его может беспокоить то, что голубь не сумеет выбрать маршрут, позволяющий подобрать всех пассажиров на остановках города. Судя по заголовку статьи, ученые сделали вывод, что вторая причина для беспокойства не имеет под собой оснований.
Пусть голубь ведет автобус.
Если правительствам стран мира и автопроизводителям удастся добиться своего, то очень скоро для управления автобусом не нужен будет ни водитель, ни голубь. Автобус будет ездить сам по себе. Мы на всех парах идем в дивную новую эпоху беспилотных транспортных средств.
А может быть, и нет.
Самым сложным аспектом для беспилотного транспорта является корректная интерпретация окружающей местности и обстановки. Снабдить авто собственными «глазами» несложно, поскольку маленькие камеры высокого разрешения сегодня производятся массово. Но зрению, помимо глаз, необходим мозг, так что автомобили, грузовики и автобусы должны получить также программы компьютерного зрения. Имея то и другое, они будут знать, что видят, и смогут реагировать соответственно.
Если верить производителям, одним из потенциальных преимуществ беспилотных машин является безопасность. Водители совершают ошибки и потому попадают в дорожные происшествия. Компьютер не отвлекается и после достаточной отработки, по идее, должен обеспечивать более высокую безопасность. Еще одно преимущество в том, что беспилотному автобусу не нужно платить. Большой недостаток, если не считать потерю работы водителями, – то, что эта технология пока находится в начальной стадии развития, и нынешние системы не оправдывают ожиданий. Случайные прохожие и ряд водителей-испытателей уже стали жертвами аварий, однако беспилотные автомобили продолжают тестироваться на улицах больших городов в разных странах. Оправдывается это тем, что их необходимо испытывать в реальном мире и что в конечном итоге они спасут больше жизней, чем отнимают сейчас. Готовность, с которой регулирующие органы соглашаются с подобными аргументами, удивительна. Если бы кто-то предложил испытывать новое лекарство на случайных людях, ничего им не сообщая и не спрашивая согласия, под тем предлогом, что в результате это спасет больше людей, чем сейчас убьет, это вызвало бы волну возмущения. Мало того, это было бы незаконно почти во всех странах и определенно неэтично.
Два изображения, различающиеся всего несколькими пикселями. Нейронная сеть Inception V3, которой они были продемонстрированы, идентифицировала левое изображение как кошку, а правое как мексиканское блюдо гуакамоле
Технология, лежащая в основе компьютерного зрения, представляет собой еще более модную область машинного обучения. Нейросети глубокого обучения, которые настраивают веса своих связей так, чтобы корректно распознавать изображения, тренируют на громадном массиве изображений до тех пор, пока не будет достигнут приемлемый уровень точности. Эта процедура чрезвычайно успешно используется в широком спектре приложений. Однако в 2013 году стало очевидно, что до сих пор слишком много внимания уделялось успехам машинного обучения и слишком мало – его потенциальным неудачам. Серьезной темой стали «состязательные примеры» – намеренно модифицированные изображения, которые человек воспринимает правильно, а компьютер нет.
На приведенном рисунке слева и справа показаны кошки. Все очевидно. Изображения различаются всего несколькими пикселями и для нас выглядят совершенно идентичными. Стандартная нейросеть, натренированная на громадном количестве изображений кошек и некошек, верно распознает на левой картинке кошку. Однако она считает, что на картинке справа изображено гуакамоле – мексиканское блюдо из авокадо. Мало того, уверенность компьютера в том, что это гуакамоле, составляет 99 %, тогда как для кошки уверенность не превышает 88 %. Как говорится, компьютер – это устройство, способное очень быстро делать миллионы ошибок.
Изображения такого рода называют «состязательными», поскольку они появляются, когда кто-то пытается намеренно обмануть систему. На практике компьютер воспримет большинство подобных изображений как кошку. Кристиан Сегеди с коллегами обратил внимание на существование таких изображений в 2013 году{32}. В 2018 году Ади Шамир с коллегами{33} объяснил, почему в системах глубокого обучения могут возникать состязательные примеры, почему они неизбежны и почему достаточно изменить всего несколько пикселей, чтобы ввести нейросеть в заблуждение.
Корень такой восприимчивости к серьезным ошибкам кроется в размерности. Обычный способ измерения различия между двумя битовыми строками состоит в том, чтобы найти расстояние Хэмминга между ними: определить, сколько бит следует заменить, чтобы из одной строки получить другую. Так, расстояние Хэмминга между 10001101001 и 10101001111 равно четырем, и различают их выделенные жирным цифры: 10101001111. В компьютере любое изображение представлено в виде очень длинной битовой строки. Если изображение занимает 1 Мб (мегабайт), то длина этой строки составляет 223, или около 8 млн бит. Так что пространство изображений имеет размерность 8 млн над конечным полем, состоящим из 0 и 1. Оно содержит 28 388 608 точек.
Алгоритм распознавания образов, воплощенный в обученной нейросети, должен поместить каждое изображение в этом пространстве в одну из гораздо меньшего числа категорий. В простейшем случае это сводится к рассечению пространства образа на отдельные области при помощи гиперплоскостей – эта процедура для двумерного пространства показана на рисунке ниже. Она делит пространство на множество сегментов, по одному на каждую категорию. Если мы меняем изображение на другое, отстоящее от него, скажем, на 40 единиц по Хэммингу, то на картинке изменяются всего 40 бит. Глаз воспринимает одновременно 8 млн бит, так что эти 40 бит составят всего лишь 0,0005 % от общего их числа – намного меньше порогового значения, при котором человек способен заметить какую-либо разницу. Однако число изображений на таком хэмминговском расстоянии от первого составляет 2