Чтобы машины могли создавать математические доказательства, превратите их в головоломку

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

Введение

Математические головоломки, которые Марийн Хойл помог решить за последнее десятилетие, звучат как кодовые имена, взятые из научно-фантастического шпионского романа: пустой шестиугольник. Число Шура 5. Гипотеза Келлера, измерение семь. На самом деле, они являются (или, точнее, являлись) одними из самых трудноразрешимых проблем геометрии и комбинаторики, не поддающихся решению уже 90 лет или более. Хойл использовал вычислительный швейцарский армейский нож под названием выполнимость, или SAT, чтобы свести их к минимуму. Теперь, будучи членом Института компьютерного мышления в математике Университета Карнеги-Меллона, он считает, что SAT можно объединить с большими языковыми моделями (LLM) для создания инструментов, достаточно мощных, чтобы справиться даже со сложными задачами чистой математики.

«Магистры права (LLM) завоевали медали на Международной математической олимпиаде, но все эти задачи могут решить и люди», — сказал Хойл. «Я очень хочу увидеть, как ИИ решит первую задачу, которую не могут решить люди. А самое замечательное в SAT то, что уже было показано, что он способен решить несколько задач, для которых нет доказательств, подтверждающих это с помощью человека».

SAT на самом деле является одной из основ самого искусственного интеллекта, хотя и не того типа ИИ, который попадает в заголовки газет, имитируя беглую беседу или пугая исследователей якобы «злыми» мыслями. Вместо этого SAT принадлежит к традиции символического искусственного интеллекта (также известного как GOFAI, или «старый добрый ИИ»), который использует жестко запрограммированные правила, а не непостижимые взаимодействия внутри глубокой нейронной сети, для получения результатов. Фактически, SAT примерно настолько прост, насколько это возможно для ИИ, если говорить концептуально: он опирается на утверждения, которые могут иметь только два возможных значения, «истина» или «ложь», связанных вместе в железные логические цепочки. Если проблемы можно разбить на эти логические «атомы», компьютерные программы, называемые решателями SAT, часто могут строить неопровержимые доказательства для них — процесс, который называется, уместно, «автоматизированным рассуждением». Эти доказательства могут быть длинными, иногда слишком длинными для того, чтобы люди когда-либо могли их разобрать. Но они надежны.

Хьюл признает, что его экспертиза заключается не обязательно в фактической математике, лежащей в основе таких доказательств, а скорее в мышлении, подобном головоломкам, необходимом для перевода задач в формат, который могут решать решатели SAT. И его талант проявился рано. «По словам моих родителей, я смог собрать свою первую головоломку из 100 частей, когда мне был 1 год — то есть, до того, как я научился ходить», — сказал Хьюл. Хьюл посетил свой первый курс по выполнимости, будучи студентом Делфтского технического университета, вскоре после этого построил свой первый решатель SAT и получил докторскую степень по информатике под руководством Ханса ван Маарена, «одного из отцов-основателей области» исследования выполнимости, сказал Хьюл. Двое мужчин впоследствии стали соавторами окончательного учебника по SAT объемом 1500 страниц.

Хьюл говорит, что его давно интересует, способны ли компьютеры решать задачи, выходящие за рамки человеческого мышления. «Этот вопрос я всё ещё задаю себе: как автоматизировать рассуждения? Можно ли это сделать так же, как это делают люди, или нужно что-то совершенно иное? Пока что я склоняюсь ко второму выводу. Все мои успехи основаны на этом понимании».

Quanta поговорила с Heule о разнице между машинным и человеческим мышлением, о том, почему простота SAT — его секретное оружие, и почему понимание переоценено в математике. Интервью было сокращено и отредактировано для ясности.

Начнем с самого главного: что такое SAT?

В нём используется так называемая пропозициональная формула, которую можно представить как очень большую доску судоку. В каждой клетке у вас есть только два варианта: один или ноль, что соответствует истине или ложи. Также существуют правила, или ограничения, на количество нулей и единиц, которые могут быть в каждой строке или столбце. Сможете ли вы вписать все нули и единицы так, чтобы все эти ограничения были соблюдены?

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

Это просто похоже на двоичные вычисления. Чем решение SAT отличается от всего остального, что делает цифровой компьютер?

То, что делают инструменты SAT, принципиально отличается от обычных вычислений. Стандартная программа принимает входные данные и выполняет последовательность операций для получения выходных данных. Инструмент SAT не вычисляет с помощью нулей и единиц. Вместо этого он ищет их комбинацию, удовлетворяющую всем ограничениям.

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

Каким образом генеративный ИИ может расширить возможности решателей SAT?

Как только вы определитесь с правильным представлением проблемы, называемым кодировкой, инструменты SAT становятся невероятно мощными. Один из моих навыков заключается в том, что я действительно хорошо умею находить правильное представление. Я досконально изучил, как работают эти инструменты; я знаю, что требуется, чтобы вы могли извлечь из них максимум пользы. Но в идеале эти знания вам не понадобятся. Я бы очень хотел выйти из этого уравнения — тогда технология сможет раскрыться по-настоящему.

Итак, как же сделать эти эффективные переводы ещё и автоматическими? Если предоставить LLM множество хороших примеров того, как это делать, он предложит что-то гораздо лучшее, чем среднестатистический пользователь. Конечно, сложность здесь заключается в том, как гарантировать правильность перевода.

Математики, такие как Теренс Тао, считают , что генеративный ИИ может помочь самому процессу исследований. Какое место в этой картине занимает SAT?

Магистратура LLM может генерировать множество правдоподобно звучащих лемм [утверждений, используемых для доказательства более сложных теорем], а автоматизированные рассуждения могут проверить их правильность. Но как только что-то оказывается неверным, решатель SAT может выдать контрпримеры — в идеале, самые минимальные. Потому что решатель отлично разбирается: «Хорошо, та ошибка, которую я только что допустил, от чего она зависит?»

Это важно, поскольку в математике контрпримеры невероятно ценны для развития интуиции. Если вы спросите программу для решения SAT: «Существует ли контрпример?», вы же не хотите, чтобы она вернула огромный, непонятный объект. Небольшой контрпример часто сразу же показывает, почему утверждение неверно. Передача таких контрпримеров обратно LLM может направлять его так же, как это сделал бы человек: помогая ему уточнить свои предложения и предложить более удачные леммы.

Что-то вроде «компьютера наведения» для ИИ?

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

Чтобы сделать всю историю достоверной, нужна система вроде Lean [формальная система проверки доказательств], которая проверяет все доказательства и все соединения: корректность лемм и их соответствие общему утверждению. Таким образом, LLM выполняет высокоуровневую высечку, автоматизированное рассуждение сертифицирует каждую часть, а Lean гарантирует целостность всей конструкции. Когда всё это складывается в единое целое, части действительно складываются.

Эти автоматизированные доказательства могут оказаться невероятно длинными — настолько длинными, что человеку даже сложно их прочитать, не говоря уже о том, чтобы понять. Не станет ли это ещё большей проблемой, если к делу присоединятся магистры права, которых и так сложно понять ?

Первоначальная критика моей работы была в основном связана с этим непониманием. Тимоти Гауэрс [математик, лауреат Филдсовской премии] назвал мою работу над задачей о пифагорейских тройках «самым отвратительным доказательством из всех когда-либо существовавших». Но я считаю, что понимание в математике сильно переоценено.

Дело в том, что нет ни одного математика, который понимал бы всю математику. Скорее, есть авторитетные математики, которые могут сказать о каждом маленьком фрагменте головоломки: «Хорошо, я проверил. Это верно». И теперь другие могут строить на этом. Они переоценивают понимание и недооценивают доверие. Я думаю, нам действительно следует принять доверие как ключевой фактор для развития математики, и именно это может дать вам автоматизация. Магистры права могут заниматься любой ерундой, но как только автоматизированное мышление способно сказать: «Хорошо, но эта часть действительно верна, и вот доказательство», оно становится более достоверным, чем большинство существующих доказательств, написанных от руки и на бумаге. Если есть хорошая история доверия, то вы можете строить на этом и действительно помогать математике. Таким образом, вы можете рассматривать его как «соавтора», потому что он следует за вами и пытается обнаружить пробелы в ваших рассуждениях.

Предположим, что продуктивное взаимодействие между LLM и SAT, описанное вами, действительно было бы реализовано. Что бы оставалось делать математикам-людям?

Когда я решал открытые задачи с помощью SAT, я всегда делал это вместе с математиками. Они уже много лет усердно размышляли над этими вопросами. Я взял их идеи и закодировал их, чтобы решатель мог завершить работу. Если бы я попытался сделать это в одиночку, начиная с нуля, я бы ничего не добился.

Я ожидаю, что будущее будет выглядеть похожим. Моя роль заключалась в переводе математических знаний в формат SAT, но степень магистра права могла бы помочь многим математикам научиться делать это самостоятельно, так что им не понадобится моё посредничество. Это невероятно интересно. Благодаря сотрудничеству математиков, генеративного искусственного интеллекта и автоматизированного мышления у нас есть реальный шанс решить давно существующие проблемы. Но полностью исключать людей из этого процесса было бы ошибкой. Творческая интуиция, концептуальное переосмысление — всё это по-прежнему уникально и развито у людей. Волшебство рождается в сотрудничестве.

Источник: www.quantamagazine.org