Математики остаются такими же как и раньше, а модели ИИ умнеют

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

Компания представила AlphaProof, модель обучения с подкреплением, способную к формальному математическому мышлению, и AlphaGeometry 2, улучшенную версию существующей системы решения геометрических задач компании. В DeepMind заявили, что для разработки искусственного общего интеллекта, или AGI, потребуется развитое математическое мышление.

Чтобы протестировать обе модели, DeepMind задал им задачи Международной математической олимпиады этого года. Это старейшее и наиболее престижное соревнование для молодых математиков, проводимое ежегодно с 1959 года. Он состоит из шести исключительно сложных вопросов по алгебре, комбинаторике, геометрии и теории чисел. Исследовательская группа применила две модели к шести задачам, и вместе они решили четыре из них, достигнув того же уровня мастерства, что и серебряный призер. AlphaProof решил две задачи по алгебре и одну задачу по теории чисел, а AlphaGeometry 2 решил задачу по геометрии. Оставшиеся две задачи комбинаторики остались нерешенными. AlphaProof работает путем доказательства математических утверждений на формальном языке Lean. Он построен с использованием предварительно обученной языковой модели AlphaZero, алгоритма обучения с подкреплением, который ранее сам себя обучил игре в шахматы, сеги и Го. Формальные языки позволяют представлять математические уравнения таким образом, чтобы их правильность можно было проверить, но для алгоритмов искусственного интеллекта доступно ограниченное количество данных, записанных человеком. Напротив, большие языковые модели, использующие естественный язык вместо формального, могут вызывать галлюцинации, предоставляя правдоподобные, но ошибочные ответы даже при большом объеме данных, сгенерированных человеком. “Мы установили мост между этими двумя взаимодополняющими сферами, доработав модель Gemini для автоматического перевода формулировок задач на естественном языке в формальные выражения, создав большую библиотеку формальных задач различной сложности”, — заявили исследователи DeepMind. Gemini — это крупнейшая и наиболее функциональная модель Google для работы с большими языками, а также разработчик чат-бота Gemini. Он способен поддерживать беседу, отвечать на вопросы, расширенно генерировать текст, обобщать текст и генерировать код. Исследователи обучили AlphaProof тому, как с его помощью можно было доказать и опровергнуть миллионы потенциальных задач в широком диапазоне математических тем и трудностей. Тот же цикл обучения был применен во время соревнований для самостоятельной генерации вариантов конкурсных задач до тех пор, пока не было найдено решение. AlphaGeometry 2 — это также гибридная модель, основанная на Gemini и нейросимвольной системе, которая была обучена с нуля с использованием на порядок большего количества синтетических данных, чем ее предшественница AlphaGeometry. “Это помогло модели решать гораздо более сложные геометрические задачи, включая задачи о перемещении объектов и уравнения углов, соотношений или расстояний”, — говорят исследователи. По словам команды, символьный движок в модели также работает в два раза быстрее, чем его предшественник. Он использует специализированный механизм обмена знаниями для поиска геометрических решений с использованием деревьев поиска для понимания сложных задач. Благодаря этим усовершенствованиям AlphaGeometry 2 успешно решила 83% всех задач по геометрии IMO за последние 25 лет, по сравнению с 53%-ным показателем, достигнутым предыдущей моделью. По словам исследователей, модель решила задачу 4 в течение 19 секунд после ее формализации. Команда также экспериментировала с логикой на естественном языке, построенной с помощью Gemini. Система не требует перевода задач на формальный язык и, следовательно, может быть легко объединена с другими системами искусственного интеллекта. Исследователи заявили, что она была протестирована на задачах IMO этого года, и “результаты оказались многообещающими”.