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