Я отчасти мог понять, почему это достижение так радует Виньялса. Его проект похож на обучение алгоритма джазовой импровизации, только выбирается не оптимальная следующая нота, а оптимальный следующий логический шаг. Алгоритм существенно расширил возможности компьютера. Он освоил новую территорию. Компьютер создал новые теоремы – как если бы он сочинил новую музыку.
Однако, должен признать, я уходил из 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 % проголосовавших. Из них половина была уверена в своем решении, а другая половина сомневалась. Существенную долю составили респонденты, с уверенностью утверждавшие, что доказательство, на самом деле написанное человеком, было составлено компьютером. Как правило, за произведение компьютера ошибочно принимали работу студента.
Как же лауреат Филдсовской премии относится к тому, что в его область вторгаются компьютеры? В своем блоге Гауэрс пишет:
Я не вижу никаких принципиальных препятствий тому, чтобы компьютеры в конце концов заняли наше место. Это было бы печально, но путь к этому состоянию может быть чрезвычайно захватывающим: вмешательства человека будет требоваться все меньше и меньше, а к «скучным» частям доказательств, которые можно будет поручить компьютерам, будут относиться все более сложные вещи, и это позволит нам думать о по-настоящему интересных частях.
Но меня беспокоила не только лингвистическая проблема проекта «Мицар». Было ли среди этих дополнительных 3 % теорем, которые удалось создать группе DeepMind и Google, что-нибудь такое, что поразило бы меня, заставило бы ахнуть от удивления? Мне начало казаться, что весь этот проект упускает из виду самую суть занятий математикой. Но в чем она, эта суть?
«Вавилонская библиотека» математики
Найти ответ на этот вопрос мне поможет один из моих любимых рассказов. В «Вавилонской библиотеке» Хорхе Луиса Борхеса рассказывается о библиотекаре, который путешествует, пытаясь обойти всю свою библиотеку. Он начинает с описания своего рабочего места: «Вселенная – некоторые называют ее Библиотекой – состоит из огромного, возможно, бесконечного числа шестигранных галерей… Из каждого шестигранника видно два верхних и два нижних этажа – до бесконечности»
[92]. Не существует ничего, кроме Библиотеки. Разумеется, Вавилонская библиотека – это метафора нашей собственной библиотеки (мы называем ее Вселенной). Как и подобает библиотеке, этот громадный улей залов полон книг. Все книги имеют одни и те же размеры. В каждой по 410 страниц, на каждой странице по 40 строк, и каждая строка состоит из 80 орфографических символов, число которых равно двадцати пяти.
