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

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

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

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

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

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

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

AlphaGeometry 2: Интеграция БВК и символического ИИ для решения геометрических задач

AlphaGeometry 2 – это последняя итерация серии AlphaGeometry, предназначенная для решения геометрических задач с повышенной точностью и эффективностью. Основываясь на фундаменте своего предшественника, AlphaGeometry 2 использует нейро-символический подход, который объединяет большие языковые модели (БВК) с символическим ИИ. Это объединение сочетает правило-ориентированную логику с предсказательной способностью нейронных сетей для определения вспомогательных точек, необходимых для решения геометрических задач. БВК в AlphaGeometry предсказывает новые геометрические конструкции, в то время как символический ИИ применяет формальную логику для генерации доказательств.

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

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

AlphaProof и AlphaGeometry 2 на IMO

В этом году на Международной математической олимпиаде (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 на Международной математической олимпиаде являются заметным шагом вперед в способности ИИ решать сложные математические задачи. Обе системы продемонстрировали результаты на уровне серебряной медали, решив четыре из шести сложных задач, демонстрируя значительные достижения в формальном доказательстве и решении геометрических задач. Несмотря на их достижения, эти системы ИИ все еще зависят от человеческого ввода для перевода задач на формальный язык и сталкиваются с проблемами интеграции с другими системами ИИ. Будущие исследования направлены на дальнейшее улучшение этих систем, потенциально включая рассуждение на естественном языке для расширения их возможностей по решению математических задач.