Код креативности. Как искусственный интеллект учится писать, рисовать и думать

Когда сотрудники DeepMind и Google начали рассматривать теоремы, учтенные в «Мицаре», они выяснили, что в 56 % случаев доказательства были сформулированы без участия человека. Их целью было увеличить эту долю. Нужно было создать новый алгоритм машинного обучения, доказывающий теоремы, который учился бы на этих доказательствах, успешно сгенерированных компьютером. Они надеялись, что алгоритм сможет извлечь из данных, уже имеющихся в математической библиотеке «Мицар», действенные стратегии продвижения по дереву доказательств. В статье, которую с гордостью вручил мне Виньялс, группа DeepMind и Google сумела, используя свой алгоритм для создания доказательств, увеличить содержание компьютерных доказательств в библиотеке с 56 до 59 %. Хотя это достижение может показаться не особенно выдающимся, следует признать, что это нетривиальное качественное изменение, полученное благодаря применению новых технологий. Речь идет не просто о еще одной теореме или еще одной выигранной партии. Речь идет о трехпроцентном увеличении доли доказательств, доступных для компьютера.

Я отчасти мог понять, почему это достижение так радует Виньялса. Его проект похож на обучение алгоритма джазовой импровизации, только выбирается не оптимальная следующая нота, а оптимальный следующий логический шаг. Алгоритм существенно расширил возможности компьютера. Он освоил новую территорию. Компьютер создал новые теоремы – как если бы он сочинил новую музыку.

Однако, должен признать, я уходил из DeepMind несколько разочарованным. Казалось бы, такое ускорение прогресса математики должно было привести меня в полный восторг, но я увидел лишь бездумную машинную штамповку математической жвачки, а не услышал волнующую меня музыку сфер. Никто не пытался оценить значение вновь открытых утверждений, никого не интересовало, содержатся ли в них какие-либо откровения. Они были новыми, и только. Казалось, что в них недостает двух третей того, что составляет акт творчества.

Математический тест Тьюринга

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

reserve n, p for Nat;

theorem Euclid: ex p st p is prime & p > n proof

set k = n! + 1;

n! > 0 by NEWTON:23;

then n! >= 0 + 1 by NAT1:38; then k >= 1 + 1 by

REAL1:55;

then consider p such that

A1: p is prime & p divides k by INT2:48; A2: p <> 0 & p > 1

by A1, INT2: def 5; take p;

thus p is prime by A1;

assume p <= n;

then p divides n! by A2, NATLAT:16;

then p divides 1 by A1, NAT1:57;

hence contradiction by A2, NAT1:54;

end;

theorem p: p is prime is infinite

from Unbounded(Euclid).

Совершенно невразумительно даже для меня, профессионального математика! Это ни в коей мере не соответствует тому, как рассказывал бы эту историю любой человек. В некотором смысле тут возникает проблема языкового барьера.

Если можно создать алгоритмы, переводящие с испанского на английский, нельзя ли найти способ перевода с компьютерного языка на тот язык, которым излагают доказательства люди? Исследовать этот вопрос взялись два кембриджских математика, Тимоти Гауэрс и Мохан Ганесалингам. Гауэрс впервые приобрел широкую известность в 1998 году, когда он получил Филдсовскую премию, и в том же году стал профессором кафедры имени Роуза Болла.

Ганесалингам сначала шел по похожему пути: он изучал математику в кембриджском Тринити-колледже. Однако, после того как он был выбран лучшим на своем курсе («старшим ранглером») и получил одну из высших студенческих наград, он решил сменить род занятий и, к удивлению всего своего факультета, получил магистерскую степень по англосаксонскому английскому. Получив награду за лучшие результаты на кембриджском факультете английской филологии, он поступил в аспирантуру по информатике, в которой занимался анализом математического языка с точки зрения формальной лингвистики. Вскоре этому сочетанию математики и лингвистики нашлось практическое применение. Гауэрс и Ганесалингам познакомились в Тринити-колледже и вскоре поняли, что их обоих интересует вопрос о непроницаемости компьютерного языка. Они решили объединить свои усилия, чтобы создать инструмент для разработки компьютерных доказательств, которые смогут читать люди.