Чтобы узнать, насколько они продвинулись в попытках создать настоящее математическое доказательство, Хассабис посоветовал мне поговорить с Ориолом Виньялсом. Виньялс родом из Испании; сначала он учился на математическом факультете, но потом понял, что его истинная страсть – искусственный интеллект. Поэтому он поехал учиться в аспирантуре в Калифорнию, где его и взяли на работу сначала в Google Brain, а затем – в DeepMind.
Должен признаться, что, когда передо мной открылась дверь лифта, за которой меня встречал Виньялс, мне было одновременно тревожно и интересно. Но я очень скоро успокоился. Как и многие из тех, кто бродит по кампусу Google, Виньялс очень легко вписался бы в атмосферу моего оксфордского факультета. Это не корпоративная среда, а место, где вполне уместны футболки и джинсы (если только на футболке имеется какая-нибудь достаточно заумная надпись).
Мы зашли в один из конференц-залов: все они названы в честь первопроходцев науки. Та комната, в которой оказались мы, вполне закономерно называлась именем Ады Лавлейс. Виньялс объяснил, что в проекте участвуют не только исследователи из DeepMind, но и исследователи Google, разбросанные по всему миру. Какого же рода математику исследуют эти сотрудники Google? Пытаются ли они разобраться с какой-нибудь теоремой из моей области, посвященной симметрии? Или доказать что-нибудь, имеющее отношение к сетям и комбинаторике? Или же установить, есть ли решения у разных вариантов уравнений Ферма? Виньялс вскоре объяснил, что они подходят к вопросу совершенно с другой стороны, нежели я ожидал, – со стороны, показавшейся мне чрезвычайно чуждой сути математики, как ее понимаю я.
Исследователи из DeepMind и Google решили сосредоточиться на проекте под названием «Мицар», начатом в 1970-х годах в Польше. Целью этого проекта было создание библиотеки доказательств, записанных формальным языком, благодаря чему компьютер мог бы понимать и проверять их.
Замысел проекта «Мицар» принадлежал польскому математику Анджею Трыбулецу, но название придумала его жена.
Она как раз листала астрономический атлас, когда муж попросил ее придумать хорошее название для проекта, и она предложила слово «Мицар» – название звезды в созвездии Большой Медведицы.
Вносить доказательства, записанные на этом формальном языке, мог любой желающий, и к моменту смерти Трыбулеца в 2013 году математическая библиотека «Мицар» насчитывала самое большое в мире количество компьютеризованных доказательств. Некоторые из этих доказательств были составлены людьми, но записаны на компьютерном языке, а другие были созданы компьютером. Сейчас этот проект поддерживают и развивают исследовательские группы в Белостокском университете в Польше, в Университете провинции Альберта в Канаде и в Университете Синсю в Японии. В последние годы интерес к проекту ослаб, и библиотека пополнялась медленно. Никто и не подозревал, что DeepMind и Google решили взяться за существенное расширение этой библиотеки.
Пока что ученые, работавшие над проектом «Мицар» в течение нескольких десятилетий, сумели создать базу данных, содержащую более 50 000 теорем. Поскольку доказательства, входящие в эту базу данных, написаны на языке, понятном компьютеру, а не человеку, участники проекта «Мицар» старались выбирать теоремы, особенно дорогие сердцу математиков-людей. Например, там есть формализованное компьютерное доказательство Основной теоремы алгебры, которая гласит, что любой полином n-й степени имеет n корней в комплексных числах.
Присутствие этой теоремы в библиотеке интересно. С начала XVII века человечество прошло через огромное множество ошибочных доказательств, причем среди них были и ложные доказательства многих выдающихся математиков – например Эйлера, Гаусса и Лапласа. Первое доказательство, признанное полным, наконец получил в 1806 году Жан-Робер Арган. Изъяны предыдущих доказательств часто бывали очень неочевидными. Выявление таких ошибок занимало долгое время. Но, когда было найдено доказательство, которое может проверить компьютер, уверенность в его справедливости чрезвычайно возросла.
То, как компьютер генерирует доказательство, которое можно включить в библиотеку «Мицар», чем-то похоже на игру по определенным правилам. Вначале есть список основополагающих аксиом о числах и геометрических фигурах. Есть некоторые правила вывода следствий. Исходя из этого, компьютер прокладывает пути к новым утверждениям, связанным между собою этими правилами вывода. В некотором смысле это похоже на игру в го. В начале партии доска пуста. Правила логического вывода состоят в том, что игрок может поставить камень (поочередно черный или белый) в любое положение на доске, еще не занятое другим камнем. Теоремы аналогичны завершениям игры – финалам, к которым стремятся прийти игроки.
Именно это поняли сотрудники DeepMind. Доказывание теорем и игра в го концептуально связаны: оба этих занятия сводятся к поиску определенных точек на дереве возможных исходов. Из каждой точки могут отходить в разных направлениях многочисленные ветви, и путь к финалу по каждой такой ветви может быть чрезвычайно долгим. Требуется оценить, в каком направлении следует сделать следующий ход, чтобы добраться до желательного финала: выиграть партию или доказать теорему.
Эта модель позволяет предположить, что можно просто запустить компьютер и начать производить теоремы. Но это не так интересно. Поскольку к одному и тому же финалу можно прийти несколькими разными путями, получится множество повторений. По-настоящему же интересно вот что: можно ли, исходя из некоего утверждения или потенциального финала, найти путь к этому утверждению, то есть его доказательство? А если это невозможно, можно ли найти путь к доказательству обратного утверждения?
Когда сотрудники 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 году, когда он получил Филдсовскую премию, и в том же году стал профессором кафедры имени Роуза Болла.
Ганесалингам сначала шел по похожему пути: он изучал математику в кембриджском Тринити-колледже. Однако, после того как он был выбран лучшим на своем курсе («старшим ранглером») и получил одну из высших студенческих наград, он решил сменить род занятий и, к удивлению всего своего факультета, получил магистерскую степень по англосаксонскому английскому. Получив награду за лучшие результаты на кембриджском факультете английской филологии, он поступил в аспирантуру по информатике, в которой занимался анализом математического языка с точки зрения формальной лингвистики. Вскоре этому сочетанию математики и лингвистики нашлось практическое применение. Гауэрс и Ганесалингам познакомились в Тринити-колледже и вскоре поняли, что их обоих интересует вопрос о непроницаемости компьютерного языка. Они решили объединить свои усилия, чтобы создать инструмент для разработки компьютерных доказательств, которые смогут читать люди.