ИИ решил математические задачи Международной олимпиады школьников

«Это, несомненно, очень существенный прогресс», — говорит Джозеф Майерс, математик из Кембриджа, Великобритания, который вместе с лауреатом медали Филдса Тимом Гауэрсом проверил решения и помог выбрать оригинальные задачи для IMO этого года.

DeepMind и другие компании пытаются обучить свои модели давать строгие доказательства трудных математических проблем. Задачи, поставленные на IMO — главном в мире конкурсе для молодых математиков — стали эталоном прогресса на пути к этой цели и стали рассматриваться как «грандиозный вызов» для машинного обучения, заявляет компания.

«Это первый раз, когда система ИИ смогла достичь результатов на уровне медали», — сказал Пушмит Кохли, вице-президент DeepMind, на брифинге для журналистов.

Всего несколько месяцев назад, в январе, система AlphaGeometry DeepMind достигла результатов на уровне медалиста IMO при решении одного типа задач — задач по евклидовой геометрии. Первый ИИ, который выступит на уровне золотой медали IMO, включая задачи по алгебре, комбинаторике и теории чисел, которые обычно считаются более сложными, чем геометрия, получит премию в размере 5 миллионов долларов под названием Премия математической олимпиады ИИ (AIMO). (Премия имеет строгие критерии, такие как открытый исходный код и работа с ограниченной вычислительной мощностью, что означает, что результаты, показанные DeepMind, не будут соответствовать требованиям премии.)

В своей последней работе исследователи использовали AlphaGeometry2 для решения геометрической задачи менее чем за 20 секунд. Новая модель ИИ является улучшенной и более быстрой версией их рекордной системы, говорит сотрудник DeepMind Тханг Луонг.

Для других типов задач команда разработала совершенно новую систему под названием AlphaProof. AlphaProof решила две задачи по алгебре и одну по теории чисел. Она потратила на это три дня. (Участникам IMO дается два сеанса по 4,5 часа каждый на все задачи). ИИ не смог решить две задачи по комбинаторике.

Буквально на прошлой неделе группа исследователей из компаний-разработчиков программного обеспечения Numina и HuggingFace использовали большую языковую модель, чтобы выиграть промежуточный «приз прогресса» AIMO, основанный на упрощенных версиях задач IMO. Компании сделали все свои системы открытыми и доступными для загрузки другими исследователями. Но победители сообщили Nature, что для решения более сложных задач одних языковых моделей, вероятно, будет недостаточно.

Новая ИИ-модель AlphaProof объединяет языковую модель с техникой обучения с подкреплением, используя движок AlphaZero, который компания успешно применила для атак на такие игры, как го. В обучении с подкреплением нейронная сеть обучается методом проб и ошибок. Это хорошо работает, когда ее ответы можно оценить с помощью некоторой объективной метрики. Для этой цели AlphaProof был обучен читать и писать доказательства на формальном языке Lean, который используется в одноименном программном пакете «помощника по доказательству», популярном среди математиков. AlphaProof проверял правильность своих выходных данных, запуская их в пакете Lean, что помогло заполнить некоторые шаги в коде.

Обучение любой языковой модели требует огромных объемов данных, но в Lean было доступно мало математических доказательств. Чтобы преодолеть эту проблему, команда разработала дополнительную сеть, которая попыталась перевести существующую запись миллиона задач, написанных на естественном языке, в Lean — но без включения решений, написанных человеком, говорит Томас Хьюберт, исследователь машинного обучения DeepMind, который был одним из руководителей разработки AlphaProof. «Мы хотели понять, можем ли мы научиться доказывать, даже если мы не обучались на доказательствах, написанных людьми?» (У компании был похожий подход с го, где ее ИИ-модель научилась играть, играя сама с собой).

Многие переводы Lean были достаточно хорошими, чтобы AlphaProof смог начать циклы обучения с подкреплением. Результаты были намного лучше ожиданий, сказал Гауэрс на пресс-конференции. «Многие проблемы в IMO обладают свойством волшебного ключа. Проблема кажется сложной, пока вы не найдете волшебный ключ, который ее открывает», — сказал Гауэрс, который работает в Коллеж де Франс в Париже.

В некоторых случаях AlphaProof, кажется, смог отыскать этот «волшебный ключ», и делал правильные шаги, выбранные из бесконечно большого диапазона возможностей, но как он пришел к решению и поможет ли это ему при реальной математической работе, пока неясно.

Майерс сказал на пресс-конференции, что еще предстоит выяснить, можно ли усовершенствовать эти методы до уровня выполнения исследовательской работы в области математики. Майерс задается вопросом: «Можно ли распространить эти методы на другие виды математики, где может и не быть миллиона задач для обучения?» Ответа пока не знает никто.