ИИ от Google DeepMind получил серебряную медаль на Международной математической олимпиаде (International Mathematical Olympiad, IMO) в этом году, впервые поднявшись на пьедестал почета.

IMO считается самым престижным в мире конкурсом для молодых математиков. Правильные ответы на вопросы теста требуют математических способностей, которых обычно не хватает системам искусственного интеллекта.

В январе компания Google DeepMind продемонстрировала AlphaGeometry – систему искусственного интеллекта, которая может отвечать на некоторые вопросы по геометрии на IMO не хуже человека. Однако это было не на реальном конкурсе, и она не смогла ответить на вопросы из других математических дисциплин, таких как теория чисел, алгебра и комбинаторика, что необходимо для получения медали IMO.

Компания Google DeepMind выпустила новый ИИ под названием AlphaProof, который может решать более широкий спектр математических задач, а также улучшенную версию AlphaGeometry, которая может решать больше вопросов по геометрии.

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

На конкурсе в Бате (Великобритания), прошедшем в июле 2024 года, 58 участников завоевали золотую медаль и 123 – серебряную.

“Мы все прекрасно понимаем, что в конечном итоге ИИ будет лучше человека решать большинство математических задач, но темпы совершенствования ИИ захватывают дух, – говорит Грегор Долинар (Gregor Dolinar), президент IMO. – То, что несколько дней назад нам не хватило всего одного балла, чтобы завоевать золотую медаль на IMO 2024, действительно впечатляет”.

На пресс-конференции Тимоти Гауэрс (Timothy Gowers) из Кембриджского университета, который помогал отмечать ответы AlphaProof, сказал, что результаты работы ИИ удивительны и, похоже, что он находит “волшебные ключи” для решения задач так же, как и люди. “Я думал, что эти волшебные ключи, вероятно, немного выходят за рамки возможностей программы, поэтому в одном или двух случаях, когда программа действительно нашла эти ключи, я был очень удивлен”, – сказал Гауэрс.

AlphaProof работает аналогично предыдущим моделям ИИ компании Google DeepMind, способным обыграть лучших игроков в шахматы и Го. Все эти модели ИИ основаны на подходе проб и ошибок, называемом обучением с подкреплением, когда система находит свой собственный способ решения задачи в течение многих попыток. Однако этот метод требует большого набора задач, написанных на языке, который ИИ может понять и проверить, в то время как большинство задач, подобных IMO, написаны на английском языке.

Чтобы обойти эту проблему, Томас Хьюберт (Thomas Hubert) из DeepMind и его коллеги использовали ИИ Gemini от Google – языковую модель, подобную той, что используется в ChatGPT, – для перевода этих задач на язык программирования Lean, чтобы ИИ мог научиться их решать.

“Вначале он сможет решать, возможно, самые простые задачи, а затем научится на основе решения этих простых задач решать более сложные и трудные,” – сказал Хьюберт на пресс-конференции. Кроме того, он создает свои ответы на языке Lean, поэтому их можно мгновенно проверить на правильность.

Хотя производительность системы AlphaProof впечатляет, она работает медленно: на поиск некоторых решений уходит до трех дней вместо 4,5 часов, которые предусмотрены у конкурентов для решения трех вопросов. Она также не смогла ответить на оба вопроса по комбинаторике, которая занимается подсчетом и упорядочиванием чисел. “Мы все еще работаем над тем, чтобы понять причину этого, и надеемся, что это поможет нам улучшить систему”, – сказал Алекс Дэвис (Alex Davies) из Google DeepMind.

По словам Гауэрса, неясно, как AlphaProof приходит к своим ответам и использует ли она ту же математическую интуицию, что и человек, но ее способность переводить доказательства с Lean на английский позволяет легко проверить их правильность.

Результат впечатляет и является важной вехой, говорит Джорди Уильямсон (Geordie Williamson) из Сиднейского университета (Австралия). “Ранее предпринималось множество попыток обучения с подкреплением на формальных доказательствах, и ни одна из них не увенчалась успехом”.

Хотя система, подобная AlphaProof, может быть полезной для практикующих математиков, помогая разрабатывать доказательства, она, очевидно, не может помочь в определении задач для решения и работы над ними, что занимает значительную часть времени исследователей, говорит Ян-Хуэй Хэ (Yang-Hui He) из Лондонского института математических наук.

По словам Хьюберта, его команда надеется, что AlphaProof поможет улучшить большие языковые модели Google, такие как Gemini, за счет уменьшения количества неправильных ответов.

Торговая компания XTX Markets предложила приз в 5 миллионов долларов – так называемую “ИИ-математическую олимпиаду” (AI Mathematical Olympiad, AIMO) – для ИИ, способного завоевать золотую медаль на IMO, но AlphaProof не может участвовать в конкурсе, поскольку не находится в открытом доступе. “Мы надеемся, что достижения DeepMind вдохновят больше команд на участие в AIMO Prize, и, конечно же, будем рады публичной заявке от самой DeepMind”, – сказал Алекс Герко (Alex Gerko) из XTX Markets.

Алекс Уилкинс