AlphaProof Nexus использует Lean, язык и среду для записи математических доказательств. Агент предлагает доказательство в строгом виде, после чего Lean проверяет каждый логический шаг.
Если проверка находит ошибку, агент получает обратную связь и продолжает поиск. Убедительного объяснения недостаточно: результат должен пройти машинную проверку по заданным логическим правилам.
На отдельных этапах используется AlphaProof, система автоматического доказательства теорем на основе обучения с подкреплением. Такой метод обучения позволяет системе менять действия после оценки результата.
Авторы сравнили эту архитектуру с более простым агентом. Он чередует создание доказательства языковой моделью и его проверку в Lean, причём на самых трудных задачах его применение обходилось дороже.
AlphaProof Nexus применяли и в других областях математики. Она помогла решить открытую задачу в алгебраической геометрии, улучшить оценку в выпуклой оптимизации и найти ошибки в формализации утверждений из научной литературы.
Её также используют в исследованиях по теории графов и квантовой оптике. При этом большинство открытых задач Эрдёша агент решить не смог.
Нынешние результаты сосредоточены в областях с развитой библиотекой формализованных математических результатов. Сложные рассуждения там удаётся разделить на отдельные подзадачи.
AlphaProof Nexus сохраняет ограничения языковых моделей. Результаты поиска могут заметно различаться между попытками, а задачи, для которых нужна обширная новая теория, остаются за пределами её возможностей.
Авторы исследования считают, что формальные доказательства могут позволить использовать искусственный интеллект в математической работе, а не только для получения ответов.
Подробности опубликованы на странице ixbt.com.
