Найдены варианты решения для девяти «вечных» математических задач
Специалисты Google DeepMind адаптировали систему математического искусственного интеллекта AlphaProof для поиска решений открытых задач и подготовки строгих алгоритмов проверки теорем, пишет Science.
Что удалось сделать
Система нашла решения девяти задач, сформулированных венгерским математиком Палом Эрдешем. Разработанная агентная система самостоятельно ищет способы решения сложных математических проблем и записывает строгие доказательства на языке Lean. Она решила девять из 353 открытых задач Эрдеша и доказала 44 из 492 гипотез, связанных с Онлайн-энциклопедией целочисленных последовательностей.
Кто работал
Работу выполнила группа исследователей под руководством научного сотрудника DeepMind Сварата Чадхури. Основой стала нейросеть AlphaProof, способная решать сложные математические задачи на уровне призёров и победителей Международной олимпиады по математике.
Как устроена система
AlphaProof создаёт алгоритмы на языке программирования Lean, который применяется в математике для проверки доказательств теорем, и использует их для анализа логических построений. Для расширения возможностей систему объединили с большими языковыми моделями Google.
Новая архитектура анализирует условие задачи, записанное на языке Lean, после чего множество независимых субагентов ищет решение. Субагенты используют AlphaProof, чтобы формулировать новые идеи на языке Lean, проверять их и оценивать перспективность дальнейшего применения.
Результаты
Исследователи проверили подход на открытых проблемах Эрдеша, задачах Онлайн-энциклопедии целочисленных последовательностей и других математических вопросах. Интеграция AlphaProof с большими языковыми моделями сократила число попыток и расход вычислительных ресурсов по сравнению с использованием только языковых моделей; авторы работы также указали на возможность применять схожий метод в квантовой оптике и теории графов.
Справка
Пал Эрдеш — один из самых продуктивных математиков XX века, автор более 1500 работ; он часто формулировал задачи в виде открытых проблем, за решение которых предлагал денежные премии.
Онлайн-энциклопедия целочисленных последовательностей (OEIS) — база данных, содержащая сотни тысяч числовых последовательностей с описаниями и ссылками на литературу.
Lean — интерактивный помощник доказательств, разработанный в Microsoft Research; он позволяет формально проверять математические утверждения, что исключает ошибки, возможные при традиционных доказательствах на бумаге.
AlphaProof была представлена в 2024 году и показала результат уровня серебряного призёра Международной олимпиады по математике.
Напомним, что OpenAI решила сотни математических задач: математики обеспокоены планами публикации.