Код креативности. Как искусственный интеллект учится писать, рисовать и думать - Маркус Дю Сотой Страница 67

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

Однако, должен признать, я уходил из 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 году, когда он получил Филдсовскую премию, и в том же году стал профессором кафедры имени Роуза Болла.

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

Чтобы проверить качество своего алгоритма, они поставили опыт в блоге Гауэрса. Гауэрс опубликовал пять теорем о метрических пространствах, о которых студентам рассказывают на первом курсе, вместе с тремя доказательствами каждой теоремы. Одно из них было написано аспирантом, другое – студентом, а третье – алгоритмом. Чтобы не вносить искажений в результаты опыта, о происхождении этих доказательств читателям блога не сообщалось. Гауэрс просто попросил их высказать свое мнение о качестве доказательств. Им было предложено выставить каждому доказательству оценки. Гауэрс хотел проверить, заподозрит ли кто-нибудь, что не все они были написаны людьми. Ни один из ответивших ничем не показал, что у него возникло такое подозрение. Во втором сообщении в блоге Гауэрс рассказал, что одно из доказательств было написано компьютером. Теперь он предложил участникам опроса попытаться определить, какое именно доказательство было компьютерным.

В среднем доказательство, написанное компьютером, правильно указали около 50 % проголосовавших. Из них половина была уверена в своем решении, а другая половина сомневалась. Существенную долю составили респонденты, с уверенностью утверждавшие, что доказательство, на самом деле написанное человеком, было составлено компьютером. Как правило, за произведение компьютера ошибочно принимали работу студента.

Как же лауреат Филдсовской премии относится к тому, что в его область вторгаются компьютеры? В своем блоге Гауэрс пишет: