Исследователи представили ProofCouncil — многоагентную систему, предназначенную для автоматического решения открытых математических задач. Архитектура объединяет несколько специализированных ИИ-агентов, которые взаимодействуют для генерации, проверки и уточнения математических доказательств. Система демонстрирует значительный прогресс в преодолении ограничений одиночных моделей при работе со сложными логическими выводами и формализацией доказательств в среде Lean.
В основе ProofCouncil лежит итеративный процесс, где агенты выполняют роли «авторов» и «критиков». Автор генерирует гипотезы и шаги доказательства, а критик проверяет их на логическую непротиворечивость и соответствие формальным правилам. Такой подход позволяет минимизировать количество галлюцинаций, характерных для стандартных LLM при решении задач, требующих многошаговой верификации и строгого соблюдения математического синтаксиса.
Система использует возможности формальной верификации, что позволяет не просто предлагать вероятные ответы, а подтверждать их корректность с помощью программных инструментов. Это приближает возможности ИИ к уровню квалифицированных математиков в задачах, где цена ошибки крайне высока, а поиск решения требует перебора огромного пространства вариантов и глубокого анализа условий.
Ключевые факты
- ProofCouncil использует многоагентную архитектуру для разделения процессов генерации и верификации доказательств.
- Система интегрирована с формальным языком доказательств Lean для обеспечения математической строгости.
- Метод позволяет эффективно решать задачи, которые ранее требовали значительных усилий экспертов-людей.
- Архитектура снижает уровень логических ошибок за счет циклической проверки между агентами-критиками.