В нынешнем кампусе компания DeepMind занимает два этажа. Один отведен под коммерческие приложения ее работы, но меня отвезли на шестой этаж, на котором ведутся исследования. Программисты на этом этаже разрабатывают сразу несколько интересных проектов. Они пытаются применять машинное обучение для ориентирования в ускользающем, полном случайностей мире квантовой физики; активно развиваются и проекты, нацеленные на проникновение в биологию и химию. Но меня интересовала их работа в математике.
Чтобы узнать, насколько они продвинулись в попытках создать настоящее математическое доказательство, Хассабис посоветовал мне поговорить с Ориолом Виньялсом. Виньялс родом из Испании; сначала он учился на математическом факультете, но потом понял, что его истинная страсть – искусственный интеллект. Поэтому он поехал учиться в аспирантуре в Калифорнию, где его и взяли на работу сначала в 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 %. Хотя это достижение может показаться не особенно выдающимся, следует признать, что это нетривиальное качественное изменение, полученное благодаря применению новых технологий. Речь идет не просто о еще одной теореме или еще одной выигранной партии. Речь идет о трехпроцентном увеличении доли доказательств, доступных для компьютера.
