Разработан подход на базе больших языковых моделей, который позволил автоматически формализовать данные и подготовить базу из 80 млн математических проблем

МОСКВА, 12 ноября. /ТАСС/. Специалисты из компании Google DeepMind раскрыли принципы работы нейросети AlphaProof, не уступающей победителям международных математических олимпиад в способности решать задачи и доказывать теоремы. Ключом к ее успеху стало создание ИИ-инструментов для "перевода" человеческих математических проблем на легко понимаемый нейросетями язык, пишут исследователи в статье, опубликованной в журнале Nature.

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

Научная команда Deepmind уже более десяти лет лидирует в разработке систем искусственного интеллекта. Так, им удалось создать первую систему ИИ, победившую человека в настольной игре го, а следующие ее версии освоили шахматы и компьютерные игры, а также научились решать некоторые биологические, физические и математические задачи. Год назад специалисты Deepmind создали системы AlphaGeometry и AlphaProof, способные решать сложные задачи по геометрии и математике на уровне призеров и победителей Международной олимпиады по математике.

Виртуальный "учитель" математики для нейросети

Ключом к этому успеху, как пишет нобелевский лауреат и сооснователь Google Deepmind Демис Хассабис, стало использование "игровых" подходов, ранее примененных при создании системы ИИ AlphaZero, и специального алгоритма на базе большой языковой модели Gemini. Он позволил системе AlphaProof использовать уже существующие онлайн-платформы и инструменты, которыми математики пользуются для проверки доказательств теорем, в процессе обучения и при подготовке решений к поставленным перед ней задачам.

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

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