Искусственный интеллект DeepMind достиг уровня серебряной медали на Международной математической олимпиаде 2024 года

AlphaProof и AlphaGeometry 2

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

Методологии обучения AlphaProof и AlphaGeometry 2

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

Выступление на ММО 2024

На Международной математической олимпиаде 2024 года AlphaProof успешно решил две задачи по алгебре и одну задачу по теории чисел, а AlphaGeometry 2 решил одну геометрическую задачу. Их совместные решения принесли в общей сложности 28 баллов из 42 возможных, что эквивалентно результату серебряной медали и всего на один балл меньше порога золотой медали. Примечательно, что AlphaGeometry 2 решил свою задачу всего за 19 секунд, продемонстрировав свою замечательную эффективность. Задачи были вручную переведены на формальный математический язык для систем ИИ, и решения занимали от нескольких минут до трех дней.

Значение достижения

Этот рубеж представляет собой значительный скачок вперед в способности ИИ справляться со сложными математическими рассуждениями, задачей, которая ранее была сложной для машин. Успех AlphaProof и AlphaGeometry 2 демонстрирует, что ИИ теперь может выполнять логические рассуждения высокого уровня, абстрагирование и иерархическое планирование, необходимые для решения задач ММО. Особенно примечательно, что системы ИИ создавали удобочитаемые доказательства и использовали классические правила геометрии, аналогично участникам-людям. Это достижение было признано экспертами-математиками, в том числе Филдсовским лауреатом Тимом Гауэрсом, который выразил удивление способностью ИИ находить «волшебные ключи», открывающие сложные задачи. Производительность систем приближается к показателям обладателей золотых медалей среди людей: AlphaGeometry 2 решает 83% всех исторических геометрических задач ММО за последние 25 лет, что является значительным улучшением по сравнению с 53% успеха его предшественника.

Будущий потенциал ИИ в математике

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