Новости

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Отчет о сердце машины

Редакция «Машинное сердце»

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

Для ИИ математическая олимпиада больше не является проблемой.

В четверг искусственный интеллект Google DeepMind совершил подвиг: использовал ИИ для решения реального вопроса Международной математической олимпиады этого года, IMO, и остался всего в одном шаге от завоевания золотой медали.

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

Ранее в этом месяце штатный профессор Калифорнийского университета в Лос-Анджелесе Теренс Тао только что провел математическую олимпиаду по искусственному интеллекту (AIMO Progress Award) с призом в миллион долларов. Неожиданно уровень решения задач ИИ поднялся до этого уровня еще до июля.

ИМХО, задавайте вопросы одновременно и правильно отвечайте на самые сложные вопросы.

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

На конкурсе IMO в этом году AlphaProof и AlphaGeometry 2, разработанные командой DeepMind, совместно достигли важного прорыва.

Среди них AlphaProof — это система обучения с подкреплением для формальных математических рассуждений, а AlphaGeometry 2 — улучшенная версия системы решения геометрии DeepMind AlphaGeometry.

Этот прорыв демонстрирует потенциал общего искусственного интеллекта (AGI) с расширенными возможностями математического мышления для открытия новых областей науки и технологий.

Итак, как система искусственного интеллекта DeepMind участвовала в конкурсе IMO?

Проще говоря, эти математические задачи сначала вручную переводятся на формальный математический язык, чтобы система ИИ могла их понять. В официальном конкурсе участники-люди подают свои ответы в два сеанса (два дня) с ограничением времени на каждый сеанс в 4,5 часа. Система искусственного интеллекта, состоящая из AlphaProof+AlphaGeometry 2, решила одну проблему за несколько минут, но на решение других проблем ушло три дня. Хотя если строго следовать правилам, у системы DeepMind вышел тайм-аут. Некоторые люди предполагают, что это может потребовать большого количества взлома методом грубой силы.

По словам Google, AlphaProof решила две задачи по алгебре и одну задачу по теории чисел, определив ответы и доказав их правильность. В их число входит самая сложная задача конкурса, которую на IMO в этом году решили только пять участников. А AlphaGeometry 2 доказывает геометрическую проблему.

Решение, предоставленное ИИ: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html.

Золотой медалист ИМО и медалист Филдса Тимоти Гауэрс и двукратный золотой медалист ИМО д-р Джозеф Майерс, председатель Комитета по отбору задач IMO 2024, оценивали решения, полученные с помощью комбинированной системы, в соответствии с правилами подсчета очков IMO.

Каждый из шести вопросов оценивается в 7 баллов, максимальная общая сумма баллов — 42 балла. Система DeepMind получила окончательную оценку 28, что означает, что все четыре задачи, которые она решила, получили высшие баллы, что соответствует наивысшему баллу в категории серебряных медалей. Порог золотой медали в этом году составил 29 очков, и 58 из 609 игроков официальных соревнований завоевали золотые медали.

На этом графике показана производительность системы искусственного интеллекта Google DeepMind по сравнению с конкурентами-людьми на IMO 2024. Система набрала 28 баллов из 42, достигнув уровня серебряного призера соревнований. Кроме того, в этом году 29 очков могут принести золотую медаль.

AlphaProof: формальный метод рассуждения

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

Среди них формальные языки предоставляют важные преимущества для формальной проверки правильности доказательств математических рассуждений. До сих пор это имело ограниченное применение в машинном обучении, поскольку объем данных, написанных человеком, был очень ограничен.

Напротив, методы, основанные на естественном языке, несмотря на доступ к большим объемам данных, производят промежуточные шаги рассуждения и решения, которые кажутся разумными, но неправильными.

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

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

Чтобы обучить AlphaProof, Google DeepMind доказал или опровергнул миллионы математических задач, охватывающих широкий спектр трудностей и тем, за несколько недель до соревнований IMO. Во время соревнований также применяется цикл обучения для усиления доказательства самостоятельно сгенерированных вариантов задач соревнования до тех пор, пока не будет найдено полное решение.

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

Более конкурентоспособная AlphaGeometry 2

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

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

До соревнований этого года AlphaGeometry 2 могла решить 83% всех исторических задач по геометрии IMO за последние 25 лет по сравнению со всего лишь 53% у ее предшественницы. В IMO 2024 AlphaGeometry 2 решила проблему 4 в течение 19 секунд после ее формализации.

Пример вопроса 4 требует доказать, что сумма ∠KIL и ∠XPY равна 180°. AlphaGeometry 2 предлагает построить точку E на линии BI так, чтобы ∠AEB = 90°. Точка E помогает придать смысл средней точке L отрезка AB, тем самым создавая множество пар подобных треугольников, таких как ABE ~ YBI и ALE ~ IPC, для доказательства вывода.

Google DeepMind также сообщает, что в рамках работы IMO исследователи также экспериментируют с новой системой мышления на естественном языке, основанной на Gemini, и современной системой мышления на естественном языке, надеясь достичь расширенных возможностей решения проблем. Система не требует перевода вопросов на формальный язык и может комбинироваться с другими системами искусственного интеллекта. В ходе проверки вопросов конкурса IMO в этом году он «показал большой потенциал».

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

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

Исследовательская команда

В Google заявили, что новое исследование было поддержано Международной математической олимпиадой, а кроме того:

Разработкой AlphaProof руководили Томас Хьюберт, Риши Мехта и Лоран Сартран; в число ключевых участников входили Хуссейн Масум, Аджа Хуанг, Миклош З. Хорват, Том Захави, Вивек Виерия, Эрик Визер, Джессика Юнг, Лей Ю, Янник Шрекер, Джулиан Шритвизер, Оттавия Бертолли, Борха Ибарц, Эдвард Локхарт, Эдвард Хьюз, Марк Роуленд и Грейс Марганд.

Среди них Аджа Хуанг, Джулиан Шритвизер, Янник Шрекер и другие члены также были основными членами газеты AlphaGo 8 лет назад (2016 г.). Восемь лет назад стала известна программа AlphaGo, созданная на основе обучения с подкреплением. Восемь лет спустя обучение с подкреплением снова проявляется в AlphaProof. Кто-то в кругу друзей посетовал: RL так вернулся!

Работу над AlphaGeometry 2 и выводом на естественном языке возглавляет Тхан Луонг. Разработкой AlphaGeometry 2 руководили Триу Тринь и Юрий Червони, при этом значительный вклад внесли Мирек Ольшак, Сяоменг Ян, Хоанг Нгуен, Джунхюк Юнг, Доусен Хван и Марсело Менегали.

Кроме того, Дэвид Сильвер, Куок Ле, Хассабис и Пушмит Кохли отвечают за координацию и управление всем проектом.

Справочное содержание:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/