Инструментарий искусственного интеллекта определяет форму автоматических доказывателей теорем нового поколения, а вместе с этим – и взаимоотношения математики и машин

Говорят, что в 1970-е годы ныне почивший математик Пол Джозеф Коэн, единственный лауреат Филдсовской премии за работы по математической логике, сделал огульное предсказание, которое до сих пор продолжает как восторгать, так и раздражать математиков: «когда-нибудь в будущем математиков заменят компьютеры». Коэн, известный дерзостью методов в работе с теорией множеств, предсказал, что можно автоматизировать всю математику, включая и написание доказательств.

Доказательство – это пошаговая логическая аргументация, подтверждающая истинность гипотезы или математического предположения. После появления доказательства гипотеза становится теоремой. Оно как подтверждает правильность утверждения, так и объясняет, почему оно верно. Но доказательство – штука странная. Оно абстрактно, и не привязано к материальному опыту. «Они представляют собой результат безумного контакта между вымышленным, не физическим миром, и существами, появившимися в результате биологической эволюции», — сказал когнитивист Саймон Дедео из университета Карнеги-Меллона, изучающий математическую определённость через анализ структур доказательств. «К этому нас эволюция не готовила».

Компьютеры хорошо подходят для объёмных вычислений, но доказательствам требуется нечто другое. Гипотезы возникают на основе индуктивных рассуждений – особой интуиции, связанной с интересной задачей – а доказательств обычно следуют дедуктивной, пошаговой логике. Им часто требуется сложное творческое мышление, а также тяжёлая работа по заполнению пустот, и машины с такой комбинацией навыков не справляются.

Компьютеризованные доказыватели теорем можно разбить на две категории. Автоматические доказыватели теорем (automated theorem provers, ATP) обычно используют методы прямого перебора, перемалывая огромные кучи цифр. Интерактивные доказыватели теорем (interactive theorem provers, ITP) служат ассистентами для человека, и умеют проверять точность аргументов, а также искать ошибки в существующих доказательствах. Однако даже если объединить две эти стратегии (как делают более современные доказыватели), автоматической рассуждающей системы из них не выйдет.


Когнитивист Саймон Дедео из университета Карнеги-Меллона помог продемонстрировать, что люди и машины создают математические доказательства похожим образом

Кроме того, эти инструменты мало кто приветствует, и большинство математиков не используют их и не одобряют. «Для математиков это противоречивая тема, — сказал Дедео. – Большинству из них эта идея не нравится».

Одна из открытых трудных проблем в этой области — вопрос о том, какую часть процесса создания доказательства можно автоматизировать. Сможет ли система сгенерировать интересную гипотезу и доказать её так, чтобы это было понятно людям? Набор недавних прорывов, достигнутых лабораториями по всему миру, предлагает способы ответить на этот вопрос при помощи искусственного интеллекта (ИИ). Джозеф Урбан из Чешского института информатики, робототехники и кибернетики в Праге, изучает различные подходы, использующие машинное обучение для увеличения эффективности существующих доказывателей. В июле его группа показала набор оригинальных гипотез и доказательств, созданных и подтверждённых машинами. В июне группа из Google Research под руководством Кристиана Сзегеди опубликовала результаты попыток использовать сильные стороны систем обработки естественного языка, чтобы сделать компьютерные доказательства более похожими по структуре и объяснениям на человеческие.

Некоторые математики считают доказыватели теорем инструментами, способными кардинально изменить обучение студентов написанию доказательств. Другие говорят, что заставлять компьютеры писать доказательства для передовой математики не нужно, а вероятно, и невозможно. Однако система, способная предсказать полезную гипотезу и доказать новую теорему, сможет достичь чего-то нового – некоего машинного варианта понимания, сказал Сзегеди. А это говорит о возможности автоматических рассуждений.

Полезные машины

Математики, логики и философы давно уже спорят о том, какая часть создания доказательств является человеческой по своей природе, и дебаты о механизации математики продолжаются и сегодня – особенно в тех местах, где информатика объединяется с чистой математикой.

Для специалистов по информатике доказыватели теорем не являются чем-то противоречивым. Они дают чёткий способ подтвердить работоспособность программы, а аргументы об интуиции и творческом начале менее важны, чем поиск эффективных способов решения задач. К примеру, Адам Члипала, специалист по информатике из Массачусетского технологического института, разработал инструменты для доказывания теорем, генерирующие криптографические алгоритмы, оберегающие транзакции в интернете – при том, что обычно такие алгоритмы придумывают люди. Код его группы уже используется в большей части коммуникаций браузера Google Chrome.


Эмили Риел из Университета Джонса Хопкинса использует доказыватели теорем для обучения студентов и компьютерных ассистентов.

«Можно взять любое математическое утверждение и закодировать его при помощи одного инструмента, а потом объединить все аргументы, и получить доказательство безопасности», — сказал Члипала.

В математике доказыватели теорем помогли выдать сложные и перегруженные вычислениями доказательства, на которые иначе ушли бы тысячи математических человеко-лет. Ярким примером служит гипотеза Кеплера о плотнейшей упаковке шаров в трёхмерном пространстве (исторически это были апельсины или пушечные ядра). В 1998 году Томас Хейлс со своим студентом Сэмом Фергюсоном завершили это доказательство при помощи различных компьютеризованных математических технологий. Результат получился таким громоздким – доказательство заняло 3 ГБ – что 12 математиков несколько лет анализировали его, прежде чем объявить, что на 99% уверены в его истинности.

Гипотеза Кеплера – не единственная знаменитая задача, решённая машинами. С теоремой о четырёх красках, утверждающая, что для закраски любой двумерной карты, при которой не будет никаких двух соприкасающихся участков одинакового цвета, всегда хватит четырёх красок, разобрались в 1977 году при помощи компьютерной программы, обработавшей пятицветные карты, и показавшей, что всех их можно превратить в четырёхцветные. В 2016 году трое математиков использовали компьютерную программу, чтобы доказать долго существовавшую булеву проблема пифагоровых троек, однако первая версия доказательства получилась размером в 200 ТБ. Если у вас достаточно быстрый канал в интернет, вы сможете скачать его недели за три.

Смешанные чувства

Такие примеры часто преподносятся как успехи, но они тоже добавляют свою толику в споры. Компьютерный код, более 40 лет назад доказавший теорему о четырёх красках, невозможно было проверить человеку. «Математики с тех пор спорят, считать ли это доказательством, или нет», — сказал математик Майкл Харрис из Колумбийского университета.


Многие математики вместе с Майклом Харрисом из Колумбийского университета сомневаются в необходимости создавать компьютеризированных доказывателей теорем – и в том, что последние сделают математиков ненужными

Ещё одно недовольство математиков связано с тем, что если те хотят использовать доказыватели теорем, сначала им нужно научиться программировать, а потом придумать, как выразить свою задачу на понятном компьютеру языке – а всё это отвлекает от занятий математикой. «К тому времени, как я переформулирую вопрос в виде, подходящем для этой технологии, я эту задачу решу и сам», — сказал Харрис.

Многие просто не видят необходимости в использовании решателей теорем. «У них своя система, карандаш и бумага, и она работает», — сказал Кевин Баззард, математик из Имперского колледжа в Лондоне, три года назад поменявший направление исследований от чистой математики к доказывателям теорем и формальным доказательствам. «Компьютеры проводят для нас потрясающие вычисления, однако они никогда не решали сложную задачу самостоятельно, — сказал он. – И пока такого не случится, математики на всё это не купятся».

Но Баззард и другие считают, что, возможно, им всё-таки стоит присмотреться к технологиям. К примеру, «компьютерные доказательства могут оказаться не такими чуждыми, как нам кажется», — сказал Дедео. Недавно совместно со Скоттом Витери, специалистом по информатике из Стэнфорда, он провёл реверс-инжиниринг нескольких известных канонических доказательств (включая и некоторые из "Начал" Евклида) и десятков доказательств, сгенерированных компьютерной программой для доказательства теорем Coq в поисках схожих моментов. Они обнаружили, что ветвящаяся структура машинных доказательств была примечательно похожа на структуру доказательств, сделанных людьми. Это общее свойство, по его словам, может помочь исследователям найти способ заставить вспомогательные программы объясниться.

«Машинные доказательства могут оказаться не такими загадочными, как кажется», — сказал Дедео.

Другие говорят, что доказыватели теорем могут стать полезными инструментами для обучения как информатике, так и математике. В университете Джонса Хопкинса математик Эмили Риел разработала курсы, на которых студенты пишут доказательства при помощи доказывателей теорем. «Это заставляет их быть очень организованными и ясно мыслить, — сказала она. – Студенты, пишущие доказательство впервые, могут не сразу понять, что от них требуется или осознать логическую структуру».

Риел также говорит, что в последнее время всё чаще использует доказыватели теорем в своей работе. «Их не обязательно использовать постоянно, и они никогда не заменят каракули на кусочке бумажки, — сказала она, — но использование компьютерных ассистентов для доказательств изменило моё представление о том, как нужно записывать доказательства».

Доказыватели теорем также предлагают способ сохранения честности в математике. В 1999 году советский, российский и американский математик Владимир Александрович Воеводский, обнаружил ошибку в одном из своих доказательств. С тех пор вплоть до своей смерти в 2017 году он активно пропагандировал использование компьютеров для проверки доказательств. Хейлс сказал, что они с Фергюсоном нашли сотни ошибок в своих оригинальных доказательствах, проверив их при помощи компьютеров. Даже самые первые теоремы в «Началах» Евклида не идеальны. Если машина может помочь математикам избежать таких ошибок, почему бы этим не воспользоваться? Харрис предложил практическое возражение этому предложению, правда, неизвестно, насколько обоснованное: если математикам придётся тратить время на формализацию математики, чтобы её понял компьютер, это время они не смогут потратить на новую математику.

Однако Тимати Гауэрс, математик, лауреат Филдсовской премии из Кембриджа, хочет пойти ещё дальше: он представляет, как в будущем доказыватели теорем заменят людей-рецензентов в крупных журналах. «Я вижу, как это может стать стандартной практикой – если вы хотите, чтобы вашу работу приняли, вам нужно прогнать её через автоматизированного проверяющего».

Разговор с компьютерами

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

Сегодняшние доказыватели теорем разрабатывались без оглядки на дружественность к математикам. Первый их тип, ATP, обычно использовался для проверки истинности утверждения, часто через проверку всех возможных вариантов. Спросите ATP, можно ли проехать из Майами до Сиэтла, и он, вероятно, переберёт все города, к которым ведут дороги из Майами, и в итоге найдёт город, дорога из которого ведёт в Сиэтл.


Тимати Гауэрс из Кембриджского университета считает, что доказыватели теорем когда-нибудь заменят людей-рецензентов

Используя ATP, программист может закодировать все правила, или аксиомы, а потом задать вопрос, следует ли определённая гипотеза этим правилам. А потом всю работу делает компьютер. «Вы просто вводите гипотезу, которую хотите доказать, и надеетесь получить ответ», — сказал Дэниел Хуан, специалист по информатике, недавно ушедший из Калифорнийского университета в Беркли ради стартапа.

Но есть проблема: ATP не объясняет свою работу. Все вычисления идут внутри машины, а для человека они выглядят как длинная последовательность нулей и единиц. Хуан сказал, что просмотреть доказательство и проверить рассуждения невозможно, поскольку всё это выглядит как кучка случайных данных. «Ни один человек не сможет посмотреть на такое доказательство и сказать: Всё понятно», — сказал он.

У второй категории, ITP, есть огромные наборы данных, содержащие до десятков тысяч теорем и доказательств, при помощи которых они могут проверять точность доказательства. В отличие от ATP, работающих внутри чёрного ящика, который просто выдаёт ответы, ITP требуют взаимодействия и иногда указаний от человека, поэтому они не такие неприступные. «Человек может сесть и разобраться в том, какие техники используются для доказательства», — сказал Хуан. Такие доказательства и изучали Дедео и Витери.

В последние годы ITP становятся всё популярнее. В 2017 году троица, доказавшая булеву проблему пифагоровых троек использовала ITP под названием Coq, чтобы создать и проверить формальную версию своего доказательства. В 2005 году Жорж Гонтье из Microsoft Research Cambridge использовал Coq для формализации теоремы о четырёх красках. Хейлс тоже использовал ITP под названием HOL Light и Isabelle для формального доказательства гипотезы Кеплера (HOL – это higher-order logic, «логика высшего порядка»).

Сегодня на переднем крае этой области пытаются объединить обучение с рассуждением. ATP часто комбинируют с ITP, интегрируя в них машинное обучение, чтобы улучшать эффективность обеих техник. Специалисты считают, что программы ATP/ITP могут использовать дедуктивные рассуждения и даже обмениваться математическими идеями так же, как это делают люди, или хотя бы похожим образом.

Пределы рассуждений

Джозеф Урбан считает, что такой комбинированный подход сможет поженить дедуктивное и индуктивное рассуждение, что необходимо для получения доказательств. Его группа создавала доказыватели теорем, работающие под управлением машинного обучения, позволяющего компьютерам самостоятельно обучаться на опыте. За последние несколько лет они изучали возможности нейросетей – слоёв вычислительных единиц, помогающих машинам обрабатывать информацию способом, примерно похожим на работу нейронов нашего мозга. В июле их группа сообщила о новых гипотезах, сгенерированных нейросетью, обученной на доказательствах теорем.

Частью Урбан вдохновлялся работами Андрея Карпаты, который несколько лет назад обучил нейросеть на выдачу бессмыслицы математического вида, которая выглядела убедительно для непрофессионалов. Но Урбану не нужна была бессмыслица – они с группой разработали собственный инструмент, который ищет доказательства, натренировавшись на миллионах теорем. Они использовали сеть для генерации новых гипотез и проверки их истинности при помощи ATP-программы под названием «Е».

Сеть выдала более 50 000 новых формул, хотя десятки тысяч из них повторялись. «Кажется, мы пока ещё не можем доказывать более интересные гипотезы», — сказал Урбан.

Сзегеди из Google Research считает проблему автоматических рассуждений в компьютерных доказательствах частью гораздо более обширной области: обработки естественного языка, в которую входит распознавание закономерностей использования слов и предложений. Распознавание закономерностей также является основной идеей компьютерного зрения, которым Сзегеди ранее занимался в Google. Как и другие группы, его команда хочет создать доказыватели теорем, способные искать полезные доказательства и объяснять их.

Вдохновившись быстрым развитием ИИ-инструментов типа AlphaZero – программы компании DeepMind, способной обыграть людей в шахматы, го и сёги – группа Сзегеди хочет воспользоваться последними достижениями в области распознавания языка, чтобы записывать доказательства. Он сказал, что языковые модели могут демонстрировать неожиданно точные математические рассуждения.

Его группа в Google Research недавно описала способ использовать языковые модели – которые часто используют нейросети – для генерации новых доказательств. Обучив модель распознавать древовидную структуру доказанных теорем, они запустили свободный эксперимент, просто предлагая нейросети генерировать и доказывать теоремы без надзора. Из тысяч сгенерированных гипотез 13% оказались доказываемыми и новыми (не повторяющими другие теоремы в базе). Он сказал, что такой эксперимент говорит, что нейросети могут научиться в каком-то смысле понимать, как выглядит доказательство.

«Нейросети способны выработать искусственное подобие интуиции», — сказал Сзегеди.

Конечно, до сих пор не ясно, исполнят ли эти попытки пророчество Коэна сорокалетней давности. Гауэрс сказал, что он считает, что компьютеры смогут опередить математиков в рассуждениях к 2099 году. Он говорит, что сначала математики будут наслаждаться золотым веком, «когда они будут заниматься интересными вещами, а компьютеры – скучными. Но я думаю, что это продлится очень недолго».

Ведь если машины будут всё сильнее развиваться, и иметь доступ к огромному количеству данных, они должны научиться очень хорошо делать и интересные вещи. «Они научатся делать собственные запросы», — сказал Гауэрс.

Харрис не соглашается. Он не считает компьютерные доказыватели необходимыми, или что они в итоге «сделают людей-математиков ненужными», Если специалисты по информатике, говорит он, когда-нибудь и смогут запрограммировать синтетическую интуицию, она всё равно не будет соперничать с человеческой. «Даже если компьютеры будут понимать, они не будут понимать в человеческом смысле».