ИИ-агент ProofCouncil решил 6 из 10 открытых математических задач турнира FirstProof
Группа исследователей разработала ProofCouncil — математического агента на основе большой языковой модели (LLM), способного автономно решать открытые задачи. Результаты работы описаны в препринте на arXiv.
ProofCouncil использует архитектуру «автор-критик»: одна часть генерирует решение, другая проверяет и улучшает его. Такой подход имитирует реальную математическую практику, что позволяет добиться более высокого качества.
Агент участвовал во втором раунде челленджа FirstProof, где нужно было решить 10 реальных открытых задач из разных областей математики. Решения оценивали рецензенты. ProofCouncil успешно справился с 6 задачами — они были признаны верными или требовали лишь незначительных правок. Это лучший результат среди всех команд.
Помимо турнира, авторы протестировали агента на 30 открытых задачах, собранных у математиков-исследователей. Из 21 полученного отзыва 5 решений признаны полностью верными, ещё 2 — многообещающими после финальной проверки, а 8 содержат полезный частичный прогресс.
Разработчики также выпустили библиотеку для создания подобных агентов, которую опубликовали в открытом доступе. Это позволяет другим исследователям дорабатывать и адаптировать подход для своих задач.
По данным arXiv, ProofCouncil демонстрирует, что LLM-агенты могут не только находить решения, но и самостоятельно формулировать доказательства. Развитие таких инструментов способно ускорить работу математиков и помочь в решении сложнейших проблем.
