Прорывные модели AlphaProof и AlphaGeometry 2 решают сложные задачи по математике, требующие продвинутой логики.
Искусственный общий интеллект (ИОИ), обладающий развитыми математическими способностями, может открыть новые горизонты в науке и технологиях.
Мы достигли значительного прогресса в разработке систем ИИ, которые помогают математикам получать новые знания, создавать алгоритмы и находить ответы на открытые вопросы. Однако современным системам ИИ по-прежнему сложно решать общие математические задачи из-за ограничений в логическом мышлении и недостатка обучающих данных.
Сегодня мы представляем AlphaProof, новую систему формальной математической логики, основанную на обучении с подкреплением, и AlphaGeometry 2, улучшенную версию нашей системы решения геометрических задач. Вместе эти системы решили четыре из шести задач Международной математической олимпиады (ММО) этого года, впервые достигнув уровня серебряного призера.
Прорывные результаты ИИ в решении сложных математических задач
ММО — старейший, крупнейший и самый престижный конкурс для молодых математиков, который проводится ежегодно с 1959 года.
Каждый год лучшие школьники-математики тренируются, иногда по несколько тысяч часов, чтобы решить шесть исключительно сложных задач по алгебре, комбинаторике, геометрии и теории чисел. Многие лауреаты Филдсовской премии, одной из высших наград для математиков, представляли свои страны на ММО.
В последнее время ежегодная олимпиада ММО также получила широкое признание как серьезная задача в области машинного обучения и желанный ориентир для измерения способности системы ИИ к продвинутой математической логике.
В этом году мы применили нашу комбинированную систему ИИ к задачам конкурса, предоставленным организаторами ММО. Наши решения были оценены по правилам начисления баллов ММО известными математиками: профессором сэром Тимоти Гауэрсом, обладателем золотой медали ММО и Филдсовской премии, и доктором Джозефом Майерсом, двукратным обладателем золотой медали ММО и председателем Комитета по отбору задач ММО 2024 года.
«Тот факт, что программа способна предложить столь неочевидное построение, очень впечатляет и выходит далеко за рамки того, что я считал современным уровнем развития», — профессор сэр Тимоти Гауэрс, обладатель золотой медали ММО и Филдсовской премии.
Сначала задачи были вручную переведены на формальный математический язык, чтобы наши системы могли их понять. В официальном соревновании участники предоставляют ответы в течение двух сессий по 4,5 часа каждая. Наши системы решили одну задачу за несколько минут, а на решение остальных ушло до трех дней.
AlphaProof решил две задачи по алгебре и одну по теории чисел, определив ответ и доказав его правильность. В их числе была и самая сложная задача конкурса, которую на ММО этого года решили только пять участников. AlphaGeometry 2 доказал геометрическую задачу, а две задачи по комбинаторике остались нерешенными.
Посмотрите решения нашей системы на ММО 2024 года
За каждую из шести задач можно получить семь баллов, максимальное общее количество баллов — 42. Наша система набрала 28 баллов, получив максимальный балл за каждую решенную задачу, что соответствует верхней границе категории серебряных медалей. В этом году порог золотой медали начинается с 29 баллов, и его преодолели 58 из 609 участников официального соревнования.
AlphaProof: формальный подход к рассуждениям
AlphaProof — это система, которая учится доказывать математические утверждения на формальном языке Lean. Она сочетает в себе предварительно обученную языковую модель с алгоритмом обучения с подкреплением AlphaZero, который ранее самостоятельно научился играть в шахматы, сёги и го.
Формальные языки дают критическое преимущество: доказательства, использующие математические рассуждения, можно формально проверить на правильность. Однако их использование в машинном обучении до сих пор сдерживалось очень ограниченным объемом данных, написанных человеком.
В отличие от этого, подходы, основанные на естественном языке, могут генерировать правдоподобные, но неверные промежуточные шаги рассуждений и решения, несмотря на доступ к данным на порядки большего объема. Мы навели мост между этими двумя взаимодополняющими сферами, точно настроив модель Gemini для автоматического перевода формулировок задач с естественного языка на формальный язык, создав большую библиотеку формальных задач различной сложности.
При получении задачи AlphaProof генерирует варианты решений, а затем доказывает или опровергает их, перебирая возможные шаги доказательства в Lean. Каждое найденное и проверенное доказательство используется для усиления языковой модели AlphaProof, повышая ее способность решать последующие, более сложные задачи.
Мы обучали AlphaProof к ММО, доказывая или опровергая миллионы задач, охватывающих широкий спектр сложности и математических областей, в течение нескольких недель, предшествовавших соревнованию. Цикл обучения также применялся во время конкурса, подкрепляя доказательства самогенерируемых вариаций конкурсных задач до тех пор, пока не удавалось найти полное решение.
AlphaGeometry 2: более конкурентоспособная версия
AlphaGeometry 2 — это значительно улучшенная версия AlphaGeometry. Это нейро-символическая гибридная система, в которой языковая модель основана на Gemini и обучена с нуля на на порядок большем объеме синтетических данных, чем ее предшественница. Это помогло модели решать гораздо более сложные геометрические задачи, в том числе задачи о движении объектов и уравнения углов, соотношений или расстояний.
AlphaGeometry 2 использует символьный движок, который на два порядка быстрее, чем у предшественника. При появлении новой задачи используется новый механизм обмена знаниями, позволяющий использовать передовые комбинации различных деревьев поиска для решения более сложных задач.
До начала олимпиады этого года AlphaGeometry 2 могла решить 83% всех исторических геометрических задач ММО за последние 25 лет по сравнению с 53%, достигнутыми ее предшественницей. На ММО 2024 года AlphaGeometry 2 решила задачу №4 за 19 секунд после получения ее формализации.
Новые горизонты математических рассуждений
В рамках нашей работы над ММО мы также экспериментировали с системой рассуждений на естественном языке, построенной на основе Gemini и наших последних исследований, чтобы обеспечить передовые навыки решения задач. Эта система не требует перевода задач на формальный язык и может быть объединена с другими системами ИИ. Мы также протестировали этот подход на задачах ММО этого года, и результаты оказались многообещающими.
Наши команды продолжают изучать различные подходы ИИ для развития математических рассуждений и планируют в скором времени опубликовать более подробную техническую информацию об AlphaProof.
Мы рады будущему, в котором математики будут работать с инструментами ИИ для изучения гипотез, пробовать новые смелые подходы к решению давних проблем и быстро выполнять трудоемкие элементы доказательств, а системы ИИ, подобные Gemini, станут более способными к математике и более широким рассуждениям.
Источники: https://gerwin.io/journal/alpha-proof-google и https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/