Это хорошее начало, но нам нужно больше. Нужна уверенность, насколько она вообще возможна, что предмет гарантии отражает наши истинные желания и что допущения, использованные в доказательстве, верны. Сами доказательства появляются в журнальных статьях, написанных для специалистов, но я считаю полезным разобраться, в чем они заключаются, что могут и чего не могут обеспечить в плане реальной безопасности. «Доказуемо полезный» в названии главы — скорее цель, а не обещание, но это правильная цель.

Мы захотим в конце концов доказать теоремы о том, что конкретный способ создания ИИ-систем гарантирует их полезность для людей. Теорема — всего лишь красивое название утверждения, сформулированного достаточно точно, чтобы можно было проверить его истинность в любой конкретной ситуации. Пожалуй, самой известной является Последняя теорема Ферма, сформулированная французским математиком Пьером де Ферма в 1637 г. и наконец доказанная Эндрю Уайлсом в 1994 г. после 357 лет попыток (разумеется, не только Уайлса)[251]. Теорему можно записать одной строкой, но доказательство превышает сотню страниц сложной математики.

Доказательства начинаются с аксиом — утверждений, истинность которых попросту принимается. Часто аксиомы являются всего лишь определениями, как, например, определения целого числа, сложения и возведения в степень, требующиеся для теоремы Ферма. Доказательство движется от аксиом логически неопровержимыми шагами, добавляя новые утверждения, пока сама теорема не будет представлена как следствие одного из шагов.

Вот довольно очевидная теорема, вытекающая из определения целого числа и сложения: 1 + 2 = 2 + 1. Назовем ее теоремой Рассела. Никакого откровения в ней не содержится. Напротив, Последняя теорема Ферма воспринимается как нечто совершенно новое — открытие прежде неизвестного. Разница, однако, лишь в степени. Истинность обеих теорем, Рассела и Ферма, уже содержится в аксиомах. Доказательства лишь делают явным то, что прежде было неявным. Они могут быть длинными или короткими, но ничего нового не добавляют. Теорема хороша лишь постольку, поскольку хороши входящие в нее допущения.

Когда речь идет о математике, все прекрасно, поскольку математика работает с абстрактными объектами, которым мы даем определения, — числами, множествами и т. д. Аксиомы верны, потому что мы так сказали. Если же вы хотите доказать что-то связанное с реальным миром — например, что ИИ-системы, разработанные таким-то образом, не убьют вас преднамеренно, — ваши аксиомы должны выполняться в реальном мире. Если они не выполняются, значит, вы доказали нечто о воображаемом мире.

Наука и инженерное дело имеют долгую и славную историю доказательства результатов, связанных с воображаемыми мирами. К примеру, в строительном проектировании можно увидеть математический анализ, начинающийся: «Допустим, АВ — это жесткая балка…» Слово «жесткая» здесь не означает «сделанная из чего-то прочного, скажем, стали»; оно значит «бесконечно твердая», то есть совершенно не гнущаяся. Жестких балок не существует, так что это воображаемый мир. Хитрость заключается в том, чтобы знать, насколько можно удалиться от реального мира, сохраняя полезность результатов. Скажем, если допущение о жесткой балке позволяет инженеру рассчитать силы, действующие в конструкции, которая включает эту балку, причем эти силы так слабы, что изгибают реальную балку ничтожно мало, то инженер имеет обоснованную уверенность, что анализ можно перенести из воображаемого мира в реальный.

У хорошего инженера вырабатывается чутье на моменты, когда этот перенос может провалиться: например, если балка является сжатой и огромные силы давят на нее с обоих концов, то даже крохотный изгиб может привести к возникновению больших поперечных сил, увеличивающих изгиб, и так далее, что приведет к катастрофическому разрушению конструкции. В таком случае анализ переделывается с другими условиями: «Допустим, АВ — упругая балка с жесткостью К». Это, разумеется, по-прежнему воображаемый мир, поскольку реальные балки не бывают однородными в смысле жесткости. В них обязательно присутствуют микроскопические неоднородности, которые могут привести к растрескиванию, если подвергать балку многократному изгибанию. Процесс устранения нереалистических допущений продолжается, пока инженер не будет в достаточной мере уверен, что оставшиеся допущения истинны в реальном мире. В конце концов, инженерные системы можно испытать в реальности, но результаты теста нельзя понимать расширительно. Они не доказывают, что та же система будет работать в других условиях или что другие варианты системы будут вести себя так же, как исходная.

Один из классических примеров ложного допущения в программировании происходит из сферы компьютерной безопасности. В этой области требуются огромные объемы математического анализа, чтобы продемонстрировать, что определенные цифровые протоколы являются доказуемо надежными — скажем, когда вы вводите пароль в интернет-приложении, то хотите быть уверены, что он будет зашифрован до отправки, чтобы кто-нибудь, подсматривающий в сети, не смог прочитать ваш пароль. Такие цифровые системы часто являются доказуемо надежными, но в реальности остаются уязвимыми для атак. Ложное допущение здесь состоит в том, что это цифровой процесс. Это не так. Он функционирует в реальном, физическом мире. Слушая звуки вашей клавиатуры или измеряя напряжение в электрической цепи, питающей ваш персональный компьютер, взломщик может «услышать» пароль или увидеть вычисления в процессе кодирования/декодирования. Специалисты по компьютерной безопасности сегодня противодействуют этим так называемым атакам по сторонним каналам — например, пишут такую программу кодировки, которая создает одни и те же изменения напряжения, независимо от того, какое сообщение кодируется.

Давайте рассмотрим своеобразную теорему, которую в дальнейшем захотим доказать, — о машинах, полезных для людей. Вот один из возможных вариантов: