Разработка нейросети AlphaProof: новый уровень в математическом искусственном интеллекте

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

Ключевым фактором успеха стала разработка инструментов искусственного интеллекта для "перевода" математических задач с человеческого языка на формат, понятный нейросетям. Согласно статье в журнале Nature, команда DeepMind формализовала более 80 миллионов математических проблем, что позволило обучить AlphaProof на обширной базе данных.

DeepMind, лидер в области разработки систем искусственного интеллекта, уже добился значительных успехов: от создания первой ИИ-системы, победившей человека в игре «го», до решения биологических, физических и математических задач. Год назад DeepMind представила системы AlphaGeometry и AlphaProof, способные решать сложные задачи по геометрии и математике на уровне призеров Международной олимпиады по математике.

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

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

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

Ключевые особенности AlphaProof:

1. Решение олимпиадных задач: В 2024 году AlphaProof (вместе с другой моделью DeepMind, AlphaGeometry 2) успешно решила четыре из шести задач Международной математической олимпиады (IMO), что соответствует уровню серебряного призера среди людей-участников.

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

3. Формальный язык Lean: AlphaProof обучается и генерирует доказательства на формальном языке Lean, который позволяет компьютеру автоматически проверять правильность математических рассуждений, обеспечивая высокий уровень достоверности.

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

Источник: vk.com

Комментарии: