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