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

Мы зашли в один из конференц-залов: все они названы в честь первопроходцев науки. Та комната, в которой оказались мы, вполне закономерно называлась именем Ады Лавлейс. Виньялс объяснил, что в проекте участвуют не только исследователи из DeepMind, но и исследователи Google, разбросанные по всему миру. Какого же рода математику исследуют эти сотрудники Google? Пытаются ли они разобраться с какой-нибудь теоремой из моей области, посвященной симметрии? Или доказать что-нибудь, имеющее отношение к сетям и комбинаторике? Или же установить, есть ли решения у разных вариантов уравнений Ферма? Виньялс вскоре объяснил, что они подходят к вопросу совершенно с другой стороны, нежели я ожидал, – со стороны, показавшейся мне чрезвычайно чуждой сути математики, как ее понимаю я.

Математика «Мицара»

Исследователи из DeepMind и Google решили сосредоточиться на проекте под названием «Мицар», начатом в 1970-х годах в Польше. Целью этого проекта было создание библиотеки доказательств, записанных формальным языком, благодаря чему компьютер мог бы понимать и проверять их.

Замысел проекта «Мицар» принадлежал польскому математику Анджею Трыбулецу, но название придумала его жена.

Она как раз листала астрономический атлас, когда муж попросил ее придумать хорошее название для проекта, и она предложила слово «Мицар» – название звезды в созвездии Большой Медведицы.

Вносить доказательства, записанные на этом формальном языке, мог любой желающий, и к моменту смерти Трыбулеца в 2013 году математическая библиотека «Мицар» насчитывала самое большое в мире количество компьютеризованных доказательств. Некоторые из этих доказательств были составлены людьми, но записаны на компьютерном языке, а другие были созданы компьютером. Сейчас этот проект поддерживают и развивают исследовательские группы в Белостокском университете в Польше, в Университете провинции Альберта в Канаде и в Университете Синсю в Японии. В последние годы интерес к проекту ослаб, и библиотека пополнялась медленно. Никто и не подозревал, что DeepMind и Google решили взяться за существенное расширение этой библиотеки.

Пока что ученые, работавшие над проектом «Мицар» в течение нескольких десятилетий, сумели создать базу данных, содержащую более 50 000 теорем. Поскольку доказательства, входящие в эту базу данных, написаны на языке, понятном компьютеру, а не человеку, участники проекта «Мицар» старались выбирать теоремы, особенно дорогие сердцу математиков-людей. Например, там есть формализованное компьютерное доказательство Основной теоремы алгебры, которая гласит, что любой полином n-й степени имеет

n корней в комплексных числах.

Присутствие этой теоремы в библиотеке интересно. С начала XVII века человечество прошло через огромное множество ошибочных доказательств, причем среди них были и ложные доказательства многих выдающихся математиков – например Эйлера, Гаусса и Лапласа. Первое доказательство, признанное полным, наконец получил в 1806 году Жан-Робер Арган. Изъяны предыдущих доказательств часто бывали очень неочевидными. Выявление таких ошибок занимало долгое время. Но, когда было найдено доказательство, которое может проверить компьютер, уверенность в его справедливости чрезвычайно возросла.

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

Именно это поняли сотрудники DeepMind. Доказывание теорем и игра в го концептуально связаны: оба этих занятия сводятся к поиску определенных точек на дереве возможных исходов. Из каждой точки могут отходить в разных направлениях многочисленные ветви, и путь к финалу по каждой такой ветви может быть чрезвычайно долгим. Требуется оценить, в каком направлении следует сделать следующий ход, чтобы добраться до желательного финала: выиграть партию или доказать теорему.

Эта модель позволяет предположить, что можно просто запустить компьютер и начать производить теоремы. Но это не так интересно. Поскольку к одному и тому же финалу можно прийти несколькими разными путями, получится множество повторений. По-настоящему же интересно вот что: можно ли, исходя из некоего утверждения или потенциального финала, найти путь к этому утверждению, то есть его доказательство? А если это невозможно, можно ли найти путь к доказательству обратного утверждения?