Специалисты Google DeepMind адаптировали систему математического искусственного интеллекта AlphaProof для поиска решений открытых задач и подготовки строгих алгоритмов проверки теорем. Как сообщает ТАСС со ссылкой на статью в журнале Science, система нашла решения девяти задач, сформулированных венгерским математиком Палом Эрдешом.
Разработанная агентная система самостоятельно ищет способы решения сложных математических проблем и записывает строгие доказательства на языке Lean. Она решила девять из 353 открытых задач Эрдеша и доказала 44 из 492 гипотез, связанных с Онлайн-энциклопедией целочисленных последовательностей.
Работу выполнила группа исследователей под руководством научного сотрудника DeepMind Сварата Чадхури. Основой стала нейросеть AlphaProof, способная решать сложные математические задачи на уровне призеров и победителей Международной олимпиады по математике.
AlphaProof создает алгоритмы на языке программирования Lean, который применяется в математике для проверки доказательств теорем, и использует их для анализа логических построений. Для расширения возможностей систему объединили с большими языковыми моделями Google.
Новая архитектура анализирует условие задачи, записанное на языке Lean, после чего множество независимых субагентов ищет решение. Субагенты используют AlphaProof, чтобы формулировать новые идеи на языке Lean, проверять их и оценивать перспективность дальнейшего применения.
Исследователи проверили подход на открытых проблемах Эрдеша, задачах Онлайн-энциклопедии целочисленных последовательностей и других математических вопросах. Интеграция AlphaProof с большими языковыми моделями сократила число попыток и расход вычислительных ресурсов по сравнению с использованием только языковых моделей; авторы работы также указали на возможность применять схожий метод в квантовой оптике и теории графов.