[Перевод] Стала ли AlphaGeometry прорывом в ИИ?
Примерно полгода назад математическое сообщество услышало новость о том, что исследователи DeepMind создали ИИ-систему, решающую геометрические задачи с Международной математической олимпиады на уровне, близком к золотым медалистам ММО. (Эту новость обсуждали в сабреддите \math, см., например, здесь и здесь.) За этими новостями, как часто бывает с новостями о прогрессе ИИ, последовала волна страха и ужаса, усиленная множеством громких газетных статей с картинками (разумеется, сгенерированными ИИ), на которых искусственные мозги решают ужасно сложные уравнения. По коллективной спине математического сообщества побежали мурашки, снова всплыли на поверхность обычные экзистенциальные вопросы о будущем человеческого интеллекта, а Интернет заполнили мемы о грядущем восстании машин.
Я бы хотел взглянуть на эту тему под новым углом. (Предупреждение: возможно, для вас он не будет новым. Если вы имели дело с евклидовой геометрией, понимаете основы линейной алгебры и внимательно читаете журнал Nature, то могли прийти ко всем этим выводам самостоятельно. Но поскольку некоторые критичные аспекты изложены мелким шрифтом (вероятно, намеренно), я всё равно считаю, что их нужно сделать более очевидными.)
Я узнал об этих исследованиях, когда кто-то выложил ссылку на пресс-релиз DeepMind в групповом чате моих друзей, любящих математику. Один мой друг с небольшими нотками паники рассказывал, что некий ИИ смог решить какую-то сложную задачу с ММО при помощи рассуждений, состоящих примерно из двухсот логических шагов. Вскоре все в чате начали грустно шутить о своём неизбежном увольнении и безработице.
Когда я сам открыл и вкратце просмотрел его, то на меня накатили примерно такие волны удивления и потрясения. Я не мог поверить глазам. Меня практически никак не затронуло появление ChatGPT и ей подобных моделей, хоть и нельзя сказать, что это бесполезные инструменты, напротив — я постоянно использую ChatGPT при отладке своего кода на LaTeX, но связанный с ними ажиотаж казался мне чрезмерным. И вот передо мной появилось доказательство того, что ажиотаж вполне оправдан. В списке из тридцати геометрических задач из последних редакций ММО искусственный интеллект смог решить 25 (решения можно увидеть в файле, который я в дальнейшем буду называть просто Файл). Казалось, что ИИ всё-таки добрался до высшей лиги, что и предрекали постоянно пророки ИИ, и я уже ждал, что в течение месяца мы получим сгенерированное ИИ доказательство гипотезы Римана. (Ну, не совсем, но вы поняли смысл.)
А потом я внимательнее изучил статью в Nature, и моя точка зрения полностью поменялась.
Наверно, самая простая линия атаки на задачи евклидовой геометрии — это стратегия, называемая на олимпиадном жаргоне «загон в угол» (angle-chasing). По сути, вы выводите из условий задачи соотношения углов, выражаете нужный вывод в форме каких-то других соотношений углов, а затем пытаетесь вывести вторые из первых. Вот глупый (но распространённый) пример: если в задаче требуется доказать, что MK=ML, то можно попробовать доказать, что равны углы MKL и KLM. Чтобы сделать это, на самом простом уровне мы многократно пользуемся тем, что в случае трёх линий r, s, t угол, образованный r и t, будет суммой углов, образованных r и s и s и t, то есть тем, что сумма внутренних углов треугольника равна 180º. Я буду называть это «тривиальным загоном в угол».
Маловероятно, что этого будет достаточно для решения задачи уровня ММО. Иногда угол, который вы хотите получить, как будто недостижим. Однако в некоторых ситуациях для решения этой проблемы можно использовать два фундаментальных инструмента. Наверно, это самые простые «нетривиальные» результаты в инструментарии решателя олимпиадных геометрических задач:
Циклические четырёхугольники: допустим, A, B, C, D — это четыре точки на плоскости, и вы при помощи простого загона в угол выяснили, что угол между AB и BD равен углу между AC и CD. Из этого следует, что A, B, C, D находятся на окружности. А из этого, в свою очередь, следует, что угол между BC и CA равен углу между BD и DA, то есть возникает новое соотношение углов, которое не удалось бы получить простым загоном в угол.
Подобные треугольники: допустим, A, B, C, D, E, F — это шесть точек на плоскости и мы знаем, что углы CAB и FDE равны. Также мы выяснили, что AB/AC=DE/DF. Тогда можно сделать вывод, что треугольники ABC и DEF подобны, а значит, и углы ABC и DEF равны.
Команда разработчиков AlphaGeometry создала инструмент, названный ею DD+AR (если мне не изменяет память, это расшифровывается как Deductive Database + Algebraic Relations), который, по сути, вычисляет все равенства углов и соотношений, которые можно вывести из условий многократным применением описанных выше инструментов. DD+AR получает из переданных ему условий равенства углов и соотношений, вычисляет при помощи тривиального загона в угол все возможные следующие из них равенства углов, проверяет по приведённым выше критериям, какие из них подразумевают наличие циклических четырёхугольников или подобных треугольников, вычисляет из этого новые равенства углов, и повторяет процесс до того момента, пока невозможно будет найти новые соотношения углов.
Лежащий в основе этого принцип на самом деле достаточно прост. Я объясню его на примере равенства соотношений, потому что мне кажется, так будет понятнее, но для углов принцип фактически будет изоморфным. Допустим, у нас есть список равенств соотношений, относящийся к длинам отрезков в следующей конфигурации: в качестве примитивного примера, который позволит нам понять принцип, скажем, что мы знаем равенства a/b=c/d и a/e=c/f для неких длин a, b, c, d, e, f, и нам нужно найти все равенства соотношений, следующие из этих двух, в виде m/n=p/q, где m, n, p, q принадлежат {a, b, c, d, e, f}. Все эти равенства соотношений будут следовать из перемножения соответствующих степеней двух исходных равенств: что-то наподобие 
. Это упрощается до
Разумеется, при типичных значениях x и y это нельзя преобразовать в равенство вида m/n=p/q для неких m, n, p, q in {a, b, c, d, e, f}. Это преобразуется в подобное равенство ровно в том случае, когда из шести степеней из выражения (x-y, -x, -y, y-x, x, y) два равны 1, два равны -1, а ставшиеся равны нулю 0. Но при любой комбинации двух степеней, равных 1, и двух степеней, равных -1, можно проверить, существуют ли значения x и y, дающие эти степени, решив систему линейных уравнений! Например, в данном случае мы видим, что если взять x=1 и y=-1, то мы получим кортеж степеней (0,-1,1,0,1,-1), что, как мы говорили ранее, находится в соответствии с равенством соотношений, и в данном случае даёт нам «новое» равенство соотношений e/b=f/d, следующее из исходных.
Именно такую операцию и многократно выполняет DD+AR! В общем случае, можно убедиться, что это сводится к следующему: скажем, что вектор R^n допустим, если у него есть две координаты 1, две координаты -1, а оставшиеся равны 0. Тогда набор равенств соотношений (например, равенств углов) соответствует множеству S допустимых векторов, и поиск того, какие равенства соотношений (соответственно, равенства углов) следуют из этого, соответствует поиску всех допустимых векторов в S. Это простое, хоть и скучное упражнение; выполняющие его эффективно алгоритмы придуманы ещё Гауссом, а то и раньше, и компьютеры использовались для решения систем линейных уравнений ещё до моего рождения (и, вероятно, до рождения всех читателей этой статьи).
То есть самая главная хитрость заключается в том, что в DD+AR вообще не используется НИКАКОГО ИИ! (Разумеется, тут можно погрузиться в философские рассуждения о том, что же такое ИИ. Я имею в виду, что DD+AR — это просто традиционный детерминированный алгоритм, который можно было реализовать ещё тогда, когда только появились компьютеры.)
Возникает вопрос: что происходит, если DD+AR не может решить задачу? До этого мы доберёмся, но сначала нужно подчеркнуть, что это само по себе очень важное «если». Потому что, как оказалось, из этих 25 задач с ММО, которые удалось решить AlphaGeometry, 14 были решены одним только DD+AR. Иными словами, в 14 из 25 решений вообще не применялся ИИ. Но и это ещё не всё.
Лежащая в основе AlphaGeometry философия заключается в том, что когда DD+AR не справляется с какой-то задачей, то есть задача не сводится к выявлению достаточного количества циклических четырёхугольников и подобных треугольников, то возможно, он сможет её решить, если добавить в формулировку задачи ещё одну точку. Например, допустим, задача начинается с треугольника ABC: возможно, DD+AR не может решить задачу, но если учесть среднюю точку стороны BC или проекцию A на BC, то появится циклический четырёхугольник с этой дополнительной точкой, который позволит нам двигаться дальше. То есть если DD+AR потерпел неудачу, мы можем попробовать добавить в формулировку задачи новую точку (это часто применяется и в решениях живых математиков). И тут на помощь приходит ИИ: он решает, какие точки нужно добавить. Использованная в AlphaGeometry модель LLM обучена приблизительно начинать со случайных геометрических условий, выводить все возможные последствия при помощи DD+AR, смотреть, какие точки можно удалить, потому что они не встречаются в условиях или выводе (только на промежуточных этапах), получая таким образом «понимание» того, какие виды точек чаще всего полезны при добавлении на чертёж.
Создав систему, способную строить новые точки, её естественным образом можно скомбинировать с DD+AR. Сначала мы выполняем DD+AR. Если он пришёл к решению, проверяем его. Если нет, строим новую точку, попросив об этом LLM, а затем снова выполняем DD+AR. Если он пришёл к решению, проверяем его. Если нет, добавляем новую точку. Намылить, смыть и повторить. Вот и всё, что делает AlphaGeometry.
И это чётко видно в Файле. Например рассмотрим решение задачи 4 с ММО 2014 года на странице 47 Файла. Доказательство начинается с «Построим точку L как отзеркаленную точку C относительно O», после чего идёт последовательность из 22 этапов, пронумерованных как «Этап 1, …, Этап 22». Задача «ИИ» здесь заключается ТОЛЬКО В ПЕРВОЙ СТРОКЕ! Все 22 этапа — это просто работа чисто детерминированного DD+AR! И фундаментально важный факт, который, как мне кажется, не был чётко донесён в статьях по этой теме, заключается в том, что логические рассуждения из двухсот с лишним этапов, удивившие моего друга тем, что «их может выполнять ИИ» при решении задачи P6 с ММО 2019 года (начинается на странице 66 Файла), на самом деле не выполнялись ИИ. Вклад ИИ заключался «лишь» в первых двух строках, где были построены две дополнительные точки (а в большинстве задач он не делает и этого); остальные 212 строк — это работа абсолютно традиционного DD+AR.
Однако можно попробовать сделать это и без ИИ, создав чёткое множество детерминированных правил построения новых точек в случае неудачи DD+AR. Допустим, мы можем запрограммировать систему так, чтобы в случае неудачи DD+AR при наличии трёх точек A, B и C таких, что AB=AC, мы бы добавляли среднюю точку M отрезка BC. Исследователи пробовали такое делать, они передавали подобный список, который назвали «спроектированные человеком эвристики». И он оказал существенное влияние: благодаря нему AlphaGeometry смогла решить 18 из 30 задач. То есть этот чисто традиционный подход, никак не использующий ИИ, уже мог решать 18 из 25 задач, которые смогла решить AlphaGeometry. Такая «AlphaGeometry без ИИ» сама по себе близка к типичному уровню медалиста ММО по геометрии, пусть и не золотого.
Можно ещё больше углубить эти рассуждения; должен при этом сказать, что этот и следующий абзацы будут исключительно гипотетическими. Я заметил, что в существенном количестве решений, в которых используется не только DD+AR (то есть в тех, где добавляются новые точки), все эти точки оказываются средними точками отрезков из исходного чертежа. Предположительно, можно добавить в программу инструкцию о том, что если DD+AR терпит неудачу в первом раунде, нужно добавить все средние точки всех отрезков, заданных двумя точками исходного чертежа, а затем заново запустить DD+AR. (Я сказал, что это гипотетические рассуждения, потому что при этом добавляется гораздо больше точек, чем было изначально, поэтому время исполнения DD+AR может существенно увеличиться; я не обдумывал это особо подробно). Судя по решениям, представленным в Файле, можно заметить, что AlphaGeometry, вооружённая только DD+AR, готовыми эвристиками и этой моей новой инструкцией, может решить 21 из 30 задач. В том числе и две из трёх самых сложных задач, которые удалось решить AlphaGeometry, а именно P6 с ММО 2000 года и P3 с ММО 2015 года.
Подведём итог: из 25 решённых AlphaGeometry задач ММО она может решить 21, в том числе P3 и P6, вообще без использования «ИИ»! Тут мы уже приближаемся к результативности серебряного медалиста ММО.
Но что же это значит в конечном итоге? Что меня теперь не удивляет то, на что способна AlphaGeometry? Напротив, по-прежнему удивляет, но когда я понял, как работает AlphaGeometry, причина моего удивления поменялась. Меня, как бывшего олимпиадника, больше всего удивляет, что DD+AR, то есть многократное использование циклических четырёхугольников и подобных треугольников, гораздо эффективнее, чем я думал. Дело в том. что мы, живые «решающие устройства», не решаем большинство задач при помощи «DD+AR». В определённой степени мы пробуем, но в случае, если долго не находим ни одного циклического четырёхугольника или пары подобных треугольников, сдаёмся и переходим к более сложным техникам: используем понятие степени точки относительно окружности, проективную геометрию, инверсию и так далее. AlphaGeometry научила меня тому, что на удивление часто существует решение DD+AR, скрывающееся под тонким слоем всего двух-трёх дополнительных точек, а чаще всего не нужно и этого! (Если вы знакомы с теми, как устроены олимпиады, то для вас станет хорошим примером P4 с ММО 2013 года. Я был на ММО, где была представлена эта задача, и с тех пор многократно использовал её как пример задачи на уроках. Во всех известных мне стандартных решениях на чертёж добавлялась одна конкретная точка. Когда я увидел в Файле, что AlphaGeometry решила задачу вообще без добавления новой точки, то есть DD+AR добился успеха в первом раунде, меня это очень удивило. Оказалось, что на чертеже есть подобие треугольников, решающее задачу, и за все эти годы я его не заметил!) Иными словами, если бы я знал, что такие задачи вообще имеют подобные решения, то меня бы не удивило, что компьютер можно запрограммировать на их поиск.
И ещё пара примечаний под конец. Во-первых, всё вышесказанное не следует рассматривать как принижение труда, затраченного на создание AlphaGeometry. Напротив, несмотря на то, что роль ИИ в ней меньше, чем нас убеждали, и всю основную нагрузку выполняет традиционный алгоритм, это не значит, что в результате получился неинтересный проект. Я считаю, что он найдёт применение в олимпиадном сообществе. Есть у меня и опасения: например, о снижении доверия к онлайн-олимпиадам. (Думаю, мы можем поучиться у сообщества шахматистов, которому уже десятки лет приходится решать эту проблему!) Но вижу я в этой модели и полезный инструмент для генерации задач; например, лишь благодаря использованию DD+AR мы можем перед публикацией задачи убедиться, что у неё нет очевидного решения с загоном в угол.
И, наконец, разобравшись с тем, как работает AlphaGeometry, и насколько большую её часть составляет детерминированный алгоритм DD+AR, я считаю, можно с уверенностью сказать, что нет никаких доказательств того, что AlphaGeometry стала первым шагом по замене людей в математике искусственным интеллектом. В конечном итоге оказалось, что на удивление большое количество геометрических задач можно чисто теоретически решить алгоритмом, использующим решение систем линейных уравнений. А разве за пятьдесят лет у нас ещё остались какие-то иллюзии, что мы можем лучше решать системы линейных уравнений, чем компьютер? На самом деле, лично я после разбора внутреннего устройства AlphaGeometry могу сказать, что она впечатляет меня меньше, чем сверхчеловеческие игроки в го или даже в шахматы. (Возможно, дело просто в том, что я понимаю евклидову геометрию лучше, чем понимаю го или шахматы). Разумеется, я не обладаю достаточными знаниями, чтобы обещать, на что способны или не способны будут другие техники ИИ. Я знаю лишь то, что прямо сейчас, возможно, в подземном кабинете офиса какой-нибудь технологической компании группа исследователей совершила случающееся раз в поколение открытие, которое позволит ей создать всемогущий ИИ, способный решить за месяц все шесть оставшихся задач тысячелетия! Кто может сказать наверняка? Но одно мы знаем точно: AlphaGeometry не стала таким открытием. Судя по тому, что нам известно, у нас ещё есть время, прежде чем машины взбунтуются и уничтожат всё человечество.
