ИИ AlphaGeometry может выиграть олимпиаду по математике

До сих пор компьютеры не смогли доказать сложные математические утверждения. Но теперь ИИ AlphaGeometry удалось решить десятки задач с олимпиады по математике.

Международная Математическая Oлимпиада (IMO), пожалуй, самое престижное студенческое соревнование. Ежегодно студенты со всего мира соревнуются за заветные бронзовые, серебряные и золотые медали (в 2023 году в них приняли участие 112 стран) — и вскоре программы искусственного интеллекта смогут с ними конкурировать.

Команда под руководством Трие Х. Трина из Google DeepMind и Нью-Йоркского университета 17 января 2024 года представила в журнале Nature новую программу искусственного интеллекта под названием AlphaGeometry, которая успешно выполнила 25 из 30 задач по геометрии из прошлых олимпиад по математике. Это означало, что уровень успеха ИИ был такой же, как и у лучших участников-людей, которые смогли выиграть золотую медаль в соревновании. AlphaGeometry также нашла более общее решение проблемы, поднятой IMO в 2004 году, которая ранее ускользала от экспертов.

«Математические олимпиады — самые престижные в мире соревнования по решению теорем», — пишут Трин и его коллеги в своей публикации. В течение двух дней каждому студенту предстоит поработать над тремя задачами из разных математических областей. Иногда проблемы настолько сложны , что их не могут решить даже специалисты. Задачи обычно имеют короткие и элегантные решения, но требуют большого творчества. Это делает их особенно интересными с точки зрения исследований ИИ. До сих пор даже крупные языковые модели, такие как GPT-4 от OpenAI, не справлялись с такими задачами.

Одной из причин, почему программы ИИ до сих пор терпят неудачу в высшей математике, является отсутствие наборов данных. Большие языковые модели, такие как GPT-4, обучаются на десятках гигабайт текстовых файлов, что соответствует примерно 20 миллионам заполненных страниц формата А4. Несмотря на большой объем математической работы, перевод доказательства на понятный компьютеру язык программирования, такой как Lean, требует много работы. В области геометрии это чрезвычайно сложно, поскольку доказательства обычно еще труднее формализовать. Хотя существуют языки программирования, разработанные специально для геометрии, они вряд ли допускают методы из других областей. Поэтому, если доказательство требует промежуточного шага, на котором появляются комплексные числа (с корнями из отрицательных значений), этот язык геометрии использовать нельзя.

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

ИИ приходит на помощь

Однако таких методов недостаточно для решения задач уровня олимпиад по математике. Поставленные там проблемы обычно требуют большего, чем простое применение простых выводов. «Решающее значение имеет введение новых концепций доказательства», — пишут Трин и его команда. Например, если вы хотите что-то доказать о треугольнике, иногда необходимо ввести новые точки и линии, не упомянутые в задаче. Именно это введение новых вспомогательных объектов для подхода к доказательству того, что большая модель языка искусственного интеллекта, подобная GPT, должна взять верх.

Языковые модели генерируют тексты, постепенно выводя слова в соответствии с распределением вероятностей. Из-за огромных объемов данных, с которыми они обучаются, программам искусственного интеллекта, таким как ChatGPT, иногда удается осмысленно отвечать на вопросы и даже вести диалоги, похожие на человеческие. Исследователи теперь могли использовать специальную базу данных для обучения AlphaGeometry математическим задачам и доказательствам. Однако большая программа на языке ИИ не должна изучать дедуктивные этапы доказательства. Эту работу продолжают выполнять специализированные дедуктивные алгоритмы. Скорее, модель ИИ должна сосредоточиться на поиске полезных вспомогательных конструкций.

Если вы дадите AlphaGeometry задачу, дедуктивный алгоритм сначала выводит различные свойства из описанной системы. Если утверждение, которое необходимо доказать, не включено, языковая модель создает вспомогательную конструкцию. Например, она может решить добавить четвертый пункт. Это дает дедуктивному алгоритму новую информацию, которую он может использовать для получения дальнейших свойств геометрического объекта. Это можно повторять до тех пор, пока ИИ и дедуктивная программа не придут к желаемому выводу.

«Метод звучит правдоподобно и в некотором смысле похож на подготовку участников Международной математической олимпиады», — говорит медалист Питер Шольце, который в прошлом трижды выигрывал золотую медаль IMO. Для проверки AlphaGeometry четверо ученых выбрали 30 геометрических задач, которые появлялись на олимпиадах по математике с 2000 года. В то время как стандартная программа, ранее использовавшаяся для решения геометрических задач («метод Ву»), правильно обработала только десять задач, а GPT-4 не справилась ни с одной, AlphaGeometry удалось решить 25 из них. Как заявляют исследователи, ИИ превосходит большинство участников IMO, выполняя в среднем 15,2 из 30 задач. Обладателям золотых медалей же удается выполнить в среднем 25,9 заданий. Однако кандидаты-люди работают не только над геометрическими задачами: задачи IMO также охватывают другие области математики, такие как алгебра, теория чисел и комбинаторика.

Когда исследователи проверили доказательства, сгенерированные ИИ, они заметили, что в задании 2004 года программа не использовала всю информацию, предоставленную в задании. Таким образом, AlphaGeometry решила более общую задачу, чем представленная. Также было показано, что сложные задачи (с которыми участники IMO справлялись плохо) обычно требовали от ИИ предоставления более длительных доказательств. Это означает, что машина, похоже, испытывает трудности с теми же задачами, что и люди.

У AlphaGeometry пока не было реальных шансов принять участие в Международной олимпиаде по математике: поскольку задачи по геометрии обычно составляют лишь треть поставленных задач, ИИ не может заранее набрать достаточное количество баллов для поступления. Но Трин и его коллеги подчеркивают, что их подход можно применить и к другим математическим областям. «Я ожидаю, что очень скоро появятся модели ИИ, которые будут конкурентоспособны на олимпиаде.