Изображение сгенерировано ИИ.
Две новые модели искусственного интеллекта AlphaProof и AlphaGeometry, разработанные Google DeepMind, успешно решили четыре из шести задач престижной Международной математической олимпиады (IMO). Используя продвинутую систему логических рассуждений, они завоевали эквивалент серебряной медали, продемонстрировав беспрецедентный для ИИ успех в решении задач такого типа.
IMO проводится раз в год с 1959 года и является крупнейшим и старейшим международным математическим соревнованием. Чтобы принять в нем участие, молодые математики со всего мира (доуниверситетского уровня) тренируются, иногда в течение тысяч часов. Соревнование включает в себя решение шести чрезвычайно сложных задач по алгебре, комбинаторике (область математики, занимающаяся подсчетом и упорядочиванием объектов), геометрии и теории чисел.
С недавних пор IMO также стал эталоном для оценки способностей систем искусственного интеллекта к расширенному мышлению. Однако до сих пор они далеки от навыков логического мышления, необходимых для решения сложных и общих математических задач. Последние требуют сложного иерархического планирования, а также определения подцелей, проверки ответов и опробования новых методов.
С другой стороны, когда речь идет о математике, ИИ сталкивается с огромной нехваткой обучающих данных. «Зачастую проще обучить модель математике, если у вас есть возможность проверить ее ответы (на формальном языке), но формальных данных по математике в сети сравнительно меньше, чем данных по естественному языку (неформальному языку)«, — рассказала MIT Review Кэти Коллинз, исследователь из Кембриджского университета, специализирующаяся на математике и ИИ.
Чтобы восполнить эти пробелы, компания Google DeepMind разработала AlphaProof и AlphaGeometry 2. Участвуя в конкурсе IMO в этом году, обе модели показали впечатляющие результаты. «Ни одна из разработанных на сегодняшний день систем такого типа не способна решать задачи с таким высоким процентом успеха и таким высоким уровнем сложности«, — говорит Пушмит Кохли, вице-президент по исследованиям Google DeepMind.
Сложная система проверки
AlphaProof — это система, основанная на обучении с подкреплением, которая сама обучается доказывать математические утверждения на формальном языке программирования Lean. Для того чтобы ИИ мог легче обрабатывать данные, их необходимо было перевести на формальный математический язык. В отличие от обработки на естественном языке, обработка на формальном языке позволяет эффективно проверять точность математических рассуждений. Подходы на основе естественного языка, с другой стороны, могут генерировать правдоподобные, но, как правило, неверные ответы.
Математические данные на естественном языке были автоматически переведены в формальный язык с помощью усовершенствованной версии Gemini, самого мощного генеративного ИИ Google. В результате была создана большая библиотека формальных математических задач различной сложности. Затем Gemini был объединен с алгоритмом обучения с подкреплением AlphaZero, который ранее освоил игры в шахматы, сёги и го.
Эти две модели были объединены для создания AlphaProof, который генерирует ответы-кандидаты, а затем выполняет процесс обратной связи, чтобы доказать или опровергнуть их точность. По мере проверки ответов система становится все более эффективной, что позволяет впоследствии решать более сложные задачи. Этот цикл обучения повторялся в течение нескольких недель перед соревнованиями.
Компьютерная графика процесса цикла обучения с подкреплением AlphaProof: около миллиона неформальных математических задач переводятся на формальный математический язык сетью формализаторов. Затем разрешающая сеть ищет доказательства или опровержения этих задач, постепенно обучаясь с помощью алгоритма AlphaZero решать более сложные задачи. © Google DeepMind
AlphaGeometry 2 — это улучшенная версия AlphaGeometry, модели, предназначенной для решения математических задач, связанных с движением объектов и уравнений с углами, соотношениями и расстояниями. Новая модель основана на движке, который в два раза быстрее своего предшественника, и обучена на гораздо большем количестве синтетических данных, что позволяет решать гораздо более сложные геометрические задачи.
Не дотянули до золотой медали, набрав 28 баллов из 42
Во время соревнования ответы моделей оценивали и отмечали два выдающихся математика: Тимоти Гауэрс, золотой медалист IMO и обладатель медали Филдса, и Джозеф Майерс, двукратный золотой медалист IMO и председатель комитета по выбору задач IMO 2024. Как и студентам, системам искусственного интеллекта было отведено две сессии по 4,5 часа на решение шести конкурсных задач.
Одну из задач системы решили всего за несколько минут, а на решение других ушло до 3 дней. AlphaProof решил две задачи по алгебре и одну задачу по теории чисел, определив ответ и доказав его правильность. Последняя задача была самой сложной на конкурсе, и ее решили всего пять участников. AlphaGeometry 2 решила одну из задач по геометрии, а две другие задачи по комбинаторике остались без ответа.
График, показывающий результаты работы искусственного интеллекта Google DeepMind в сравнении с человеческими конкурентами на IMO 2024. ИИ набрал 28 баллов из 42, что соответствует уровню серебряного призера соревнований. © Google DeepMind
Каждая из шести задач оценивается в семь баллов, поэтому максимально возможный результат — 42. Золотую медаль можно получить, набрав 29 баллов. Вместе две системы набрали 28 баллов, не дотянув до золотой медали. Это первый случай, когда система искусственного интеллекта достигла такого уровня производительности в конкурсе IMO. «Как математик, я считаю, что это очень впечатляет и представляет собой значительный прогресс по сравнению с тем, что было возможно раньше«, — сказал Гауэрс на пресс-конференции.
Этот новый результат может проложить путь к сотрудничеству человека и ИИ в математических исследованиях. Это также может позволить расшифровать способ, которым наш мозг решает эти задачи, — аспект, который до сих пор остается во многом непонятным.
