Группа учёных из Google DeepMind вывела на суд сообщества новый исследовательский агент под названием AlphaProof Nexus. По данным исследования, он зафиксировал решение 9 из 353 открытых задач, связанных с именем венгерского математика Пала Эрдёша. Среди оставшихся задач две считались неразрешимыми на протяжении 56 лет. Кроме того, отмечается, что на каждую из девяти найденных формальных решений система тратила несколько сотен долларов. Также агент доказал 44 из 492 открытых гипотез из Онлайн-энциклопедии целочисленных последовательностей (OEIS).

Авторы подчёркивают, что речь идёт не просто о поиске числовых ответов, а о применении крупных языковых моделей для формализации доказательств. В рамках исследования проверяют пригодность подхода не только для олимпиад, но и для открытых задач исследовательского уровня.

Ключевое отличие AlphaProof Nexus от обычного чат-бота состоит в применении Lean — языка и среды для формализации математических доказательств. Агент выносит доказательства в формальном виде, после чего Lean последовательно проверяет каждый логический шаг. Если система на каком-то этапе обнаруживает ошибку, она получает обратную связь и продолжает поиск. Важен не просто стиль изложения; результат обязан пройти машинную верификацию по строгим правилам логики.

В рамках архитектуры работают несколько ИИ-агентов, которые параллельно ищут решения, оценивают различные подходы и при необходимости уточняют доказательства. В самой сложной конфигурации их работу координирует эволюционный алгоритм, а для отдельных этапов поиска применяется система автоматического доказательства теорем AlphaProof — созданная на базе обучения с подкреплением.

Сравнение с более простым режимом, где доказательства сначала генерируются языковой моделью, а затем проверяются в Lean, показало: этот простой агент тоже справился со всеми девятью задачами Эрдёша. Однако на наиболее сложных местах такая схема обходилась дороже, что свидетельствует о том, что итоговый успех определяется не только мощностью языковой модели, но и эффективной организацией процесса доказательства.

Авторы отмечают, что потенциал AlphaProof Nexus выходит за пределы задач Эрдёша и OEIS: система помогла решить открытое задание в алгебраической геометрии, улучшила оценки в выпуклой оптимизации и помогла обнаруживать ошибки в формализациях математических утверждений в научной литературе. Её применяют в исследованиях по теории графов и квантовой оптике.

Несмотря на достигнутые успехи, подавляющее большинство открытых задач Эрдёша ей пока не поддалось. Преимущества наблюдаются в областях с существующей крупной базой формализованных результатов и там, где сложные рассуждения можно разделить на подзадачи. Также сохраняются ограничения языковых моделей: результаты поиска могут заметно варьироваться между попытками, а задачи, требующие разработки обширной новой теории, остаются вне досягаемости системы.

Авторы утверждают, что формальные доказательства теоретически могут стать способом вовлечь искусственный интеллект в реальную математическую работу, а не только выдавать готовые ответы.