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