ИИ на Международной математической олимпиаде: как AlphaProof и AlphaGeometry 2 завоевали серебряную медаль

Математическое мышление — жизненно важный аспект когнитивных способностей человека, способствующий прогрессу научных открытий и технологических разработок. Поскольку мы стремимся разработать общий искусственный интеллект, соответствующий человеческому познанию, крайне важно оснастить ИИ передовыми возможностями математического мышления. Хотя нынешние системы искусственного интеллекта могут решать базовые математические задачи, им сложно справляться со сложными рассуждениями, необходимыми для сложных математических дисциплин, таких как алгебра и геометрия. Однако ситуация может измениться, поскольку Google DeepMind сделал это значительные успехи в развитии математических возможностей систем искусственного интеллекта. Этот прорыв был достигнут Международная математическая олимпиада (IMO) 2024. Основанная в 1959 году, IMO является старейшим и самым престижным математическим соревнованием, бросающим вызов старшеклассникам всего мира с задачами по алгебре, комбинаторике, геометрии и теории чисел. Каждый год команды молодых математиков соревнуются в решении шести очень сложных задач. В этом году Google DeepMind представила две системы искусственного интеллекта: AlphaProof, которая фокусируется на формальных математических рассуждениях, и AlphaGeometry 2, которая специализируется на решении геометрических задач. Этим системам искусственного интеллекта удалось решить четыре задачи из шести, выступив на уровне серебряного призера. В этой статье мы рассмотрим, как эти системы работают для решения математических задач.

AlphaProof: объединение искусственного интеллекта и формального языка для доказательства математических теорем

AlphaProof — это система искусственного интеллекта, предназначенная для доказательства математических утверждений с использованием формального языка. Наклонитесь. Он объединяет Gemini, предварительно обученная языковая модель, с AlphaZero, алгоритм обучения с подкреплением, известный благодаря освоению шахмат, сёги и го.

Модель Gemini переводит формулировки задач на естественном языке в формальные, создавая библиотеку задач с различными уровнями сложности. Это преследует две цели: преобразование неточного естественного языка в точный формальный язык для проверки математических доказательств и использование предсказательных способностей Близнецов для создания списка возможных решений с формальной языковой точностью.

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

Для Международной математической олимпиады (IMO) AlphaProof обучался, доказывая или опровергая миллионы задач, охватывающих различные уровни сложности и математические темы. Это обучение продолжалось во время соревнований, где AlphaProof совершенствовала свои решения, пока не нашла полные ответы на проблемы.

AlphaGeometry 2: интеграция LLM и символического искусственного интеллекта для решения задач геометрии

AlphaGeometry 2 — это последняя версия АльфаГеометрия Серия, предназначенная для решения геометрических задач с повышенной точностью и эффективностью. Созданная на основе своего предшественника, AlphaGeometry 2 использует нейросимволический подход, который объединяет нейронные модели большого языка (LLM) с символическим ИИ. Эта интеграция сочетает в себе логику, основанную на правилах, с прогнозирующей способностью нейронных сетей идентифицировать вспомогательные точки, необходимые для решения задач геометрии. LLM в AlphaGeometry предсказывает новые геометрические конструкции, а символический ИИ применяет формальную логику для генерации доказательств.

Столкнувшись с геометрической задачей, программа AlphaGeometry LLM оценивает множество возможностей, предсказывая конструкции, критически важные для её решения. Эти прогнозы служат ценными подсказками, направляя символьный механизм к точным выводам и приближая к решению. Этот инновационный подход позволяет AlphaGeometry решать сложные геометрические задачи, выходящие за рамки традиционных сценариев.

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

AlphaProof и AlphaGeometry 2 в IMO

В этом году на Международной математической олимпиаде (ИМО) участникам предлагалось решить шесть разноплановых задач: две по алгебре, одну по теории чисел, одну по геометрии и две по комбинаторике. Исследователи Google выразилось эти задачи на формальный математический язык для AlphaProof и AlphaGeometry 2. AlphaProof решила две задачи по алгебре и одну задачу по теории чисел, включая самую сложную задачу конкурса, которую в этом году решили только пять участников-людей. Тем временем AlphaGeometry 2 успешно решила задачу геометрии, хотя и не решила две задачи комбинаторики.

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

Следующий скачок: естественный язык для решения математических задач

AlphaProof и AlphaGeometry 2 продемонстрировали впечатляющий прогресс в решении математических задач с помощью ИИ. Однако эти системы по-прежнему полагаются на экспертов-людей для перевода математических задач на формальный язык для обработки. Кроме того, пока неясно, как эти специализированные математические навыки могут быть внедрены в другие системы ИИ, например, для проверки гипотез, тестирования инновационных решений давно существующих проблем и эффективного управления трудоёмкими аспектами доказательств.

Чтобы преодолеть эти ограничения, исследователи Google разрабатывают систему мышления на естественном языке, основанную на Gemini и их последних исследованиях. Эта новая система призвана расширить возможности решения проблем без необходимости формального языкового перевода и предназначена для плавной интеграции с другими системами искусственного интеллекта.

Выводы

Результаты AlphaProof и AlphaGeometry 2 на Международной математической олимпиаде представляют собой значительный шаг вперёд в развитии возможностей ИИ в решении сложных математических задач. Обе системы продемонстрировали результаты, достойные серебряных медалей, решив четыре из шести сложных задач, продемонстрировав значительный прогресс в формальном доказательстве и решении геометрических задач. Несмотря на свои достижения, эти системы ИИ по-прежнему зависят от человеческого участия при переводе задач на формальный язык и сталкиваются с трудностями интеграции с другими системами ИИ. Дальнейшие исследования направлены на дальнейшее совершенствование этих систем, потенциально интегрируя рассуждения на естественном языке для расширения их возможностей в более широком спектре математических задач.