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