Репост из: Data Secrets
Система DeepMind автономно решила еще 9 задач Эрдеша
Стоимость решения каждой задачи составила всего несколько сотен долларов. Но есть нюанс: на самом деле DeepMind прогоняли через агента все 353 формализованные открытые задачи Эрдеша и сожгли гораздо больше ресурсов. Решение останавливали, если агент выходил за рамки 3000 итераций, и в итоге полностью решенных задач оказалось 9.
Статья с заявлением: arxiv.org/pdf/2605.22763v1. Здесь подробно описана архитектура самого агента AlphaProof Nexus, решившего задачи.
В базовом варианте это просто итерационный процесс: агент генерирует доказательство -> отправляет его на формальную проверку в Lean -> анализирует ошибки и пробует снова. Поверх этого также прикручен эволюционный поиск, когда агент перебирает ветки доказательств, хранит и анализирует промежуточные шаги и отбрасывает тупиковые идеи.
Помимо 9 задач Эрдеша (включая, кстати, две, которые были открыты на протяжении 50+ лет), Nexus также доказал 44 открытые гипотезы OEIS.
Кажется, DeepMind первые среди ИИ-лидеров провели настолько масштабный эвал агента на нерешенных задачах. Но точно далеко не последние. Решение открытых проблем уже становится похоже на бенчмарк.
Вот здесь выложили сами доказательства: github.com/google-deepmind/alphaproof-nexus-results
Стоимость решения каждой задачи составила всего несколько сотен долларов. Но есть нюанс: на самом деле DeepMind прогоняли через агента все 353 формализованные открытые задачи Эрдеша и сожгли гораздо больше ресурсов. Решение останавливали, если агент выходил за рамки 3000 итераций, и в итоге полностью решенных задач оказалось 9.
Статья с заявлением: arxiv.org/pdf/2605.22763v1. Здесь подробно описана архитектура самого агента AlphaProof Nexus, решившего задачи.
В базовом варианте это просто итерационный процесс: агент генерирует доказательство -> отправляет его на формальную проверку в Lean -> анализирует ошибки и пробует снова. Поверх этого также прикручен эволюционный поиск, когда агент перебирает ветки доказательств, хранит и анализирует промежуточные шаги и отбрасывает тупиковые идеи.
Помимо 9 задач Эрдеша (включая, кстати, две, которые были открыты на протяжении 50+ лет), Nexus также доказал 44 открытые гипотезы OEIS.
Кажется, DeepMind первые среди ИИ-лидеров провели настолько масштабный эвал агента на нерешенных задачах. Но точно далеко не последние. Решение открытых проблем уже становится похоже на бенчмарк.
Вот здесь выложили сами доказательства: github.com/google-deepmind/alphaproof-nexus-results