Чтобы перестроить работу над ИИ в соответствии с новыми принципами, нужно заложить надежный фундамент. Когда на кону стоит будущее человечества, надежд и благих намерений — как и образовательных инициатив, отраслевых кодексов поведения, правового регулирования и экономических стимулов действовать правильно — недостаточно. Все эти меры могут подвести и часто подводят. В подобной ситуации мы хотим строгих определений и педантичных пошаговых математических доказательств, чтобы получить бесспорные гарантии.
Это хорошее начало, но нам нужно больше. Нужна уверенность, насколько она вообще возможна, что предмет гарантии отражает наши истинные желания и что допущения, использованные в доказательстве, верны. Сами доказательства появляются в журнальных статьях, написанных для специалистов, но я считаю полезным разобраться, в чем они заключаются, что могут и чего не могут обеспечить в плане реальной безопасности. «Доказуемо полезный» в названии главы — скорее цель, а не обещание, но это правильная цель.
Мы захотим в конце концов доказать теоремы о том, что конкретный способ создания ИИ-систем гарантирует их полезность для людей. Теорема — всего лишь красивое название утверждения, сформулированного достаточно точно, чтобы можно было проверить его истинность в любой конкретной ситуации. Пожалуй, самой известной является Последняя теорема Ферма, сформулированная французским математиком Пьером де Ферма в 1637 г. и наконец доказанная Эндрю Уайлсом в 1994 г. после 357 лет попыток (разумеется, не только Уайлса)[251]. Теорему можно записать одной строкой, но доказательство превышает сотню страниц сложной математики.
Доказательства начинаются с аксиом — утверждений, истинность которых попросту принимается. Часто аксиомы являются всего лишь определениями, как, например, определения целого числа, сложения и возведения в степень, требующиеся для теоремы Ферма. Доказательство движется от аксиом логически неопровержимыми шагами, добавляя новые утверждения, пока сама теорема не будет представлена как следствие одного из шагов.
Вот довольно очевидная теорема, вытекающая из определения целого числа и сложения: 1 + 2 = 2 + 1. Назовем ее теоремой Рассела. Никакого откровения в ней не содержится. Напротив, Последняя теорема Ферма воспринимается как нечто совершенно новое — открытие прежде неизвестного. Разница, однако, лишь в степени. Истинность обеих теорем, Рассела и Ферма, уже содержится в аксиомах. Доказательства лишь делают явным то, что прежде было неявным. Они могут быть длинными или короткими, но ничего нового не добавляют. Теорема хороша лишь постольку, поскольку хороши входящие в нее допущения.