Искусственный интеллект Google чуть не завоевал золотую медаль IMO: решение задачи за 19 секунд шокировало жюри, геометрические способности превзошли человеческие

DeepMind новейшая математическая модель завоевала серебряную медаль на Международной математической олимпиаде (IMO), показав выдающиеся результаты. Модель идеально решила 4 из 6 задач, и ей не хватило всего 1 балла до золотой медали. Особенно впечатляющим было решение задачи №4, где модель дала ответ всего за 19 секунд, поразив человеческое жюри скоростью и качеством решения.

AlphaProof

AlphaProof - это система, способная доказывать математические утверждения на формальном языке Lean. Она сочетает в себе предварительно обученную большую языковую модель с алгоритмом обучения с подкреплением AlphaZero.

Чтобы преодолеть ограничения формальных языков в машинном обучении из-за ограниченных данных, написанных человеком, исследователи преодолели разрыв между естественным языком и формальными утверждениями путем:

  1. Дообучения модели Gemini для автоматического перевода формулировок задач на естественном языке в формальные утверждения
  2. Создания большой библиотеки формализованных задач различной сложности

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

AlphaGeometry 2

AlphaGeometry 2 - это нейро-символическая гибридная система, обученная с нуля с использованием языковой модели Gemini. Она может решать более сложные геометрические задачи, чем ее предшественник, включая задачи с движением объектов, углами, отношениями и уравнениями расстояний.

Ключевые улучшения включают:

  1. Обучение на синтетических данных, на порядок превышающих объем предыдущей версии
  2. Символьный движок, работающий на два порядка быстрее, чем раньше
  3. Новый механизм обмена знаниями, позволяющий использовать продвинутые комбинации различных деревьев поиска для решения более сложных задач

AlphaGeometry 2 продемонстрировала впечатляющие возможности, решив 83% геометрических задач IMO за последние 25 лет, по сравнению с 53% у предшественника. На IMO этого года она решила Задачу 4 всего за 19 секунд после получения формализованного вопроса.

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