Проблема ИИ в серьезной науке не в отсутствии «интеллекта», а в его вопиющей хрупкости при масштабировании. Как только дело доходит до автоформализации длинных математических доказательств, системы начинают сыпаться: контекст плывет, зависимости путаются, а попытка исправить локальную ошибку превращается в эффект домино, разрушающий всю логическую цепочку. По словам Юаньхэ Чжана и группы исследователей из Уорикского университета и института RIKEN, главная беда не в сложности отдельной леммы, а в управлении сотнями взаимозависимых деклараций. Модель может подправить определение, чтобы закрыть дыру в одном месте, и тем самым молча аннулировать всю последующую логику. На выходе получается текст, который выглядит формально верным, но математически бесполезен.
Для решения этой задачи исследователи представили LeanMarathon — мультиагентную систему для работы в среде Lean 4. В центре архитектуры стоит «Blueprint» (чертеж), который служит единственным источником истины и жестким скелетом доказательства. Вместо того чтобы полагаться на удачный промпт, система координирует работу четырех специализированных агентов:
Архитектор: выстраивает общую структуру и иерархию доказательства.
Аудитор: проводит критический анализ и верификацию логических переходов.
Исполнитель: занимается непосредственным выводом и доказательством конкретных лемм.
Редактор: отвечает за «ремонт» и устранение локальных противоречий.
Этот оркестратор превращает одну хрупкую многочасовую сессию генерации в серию восстанавливаемых транзакций, где каждый шаг верифицируется через состязательную проверку.
Результаты и эффективность
Эффективность подхода проверили на четырех задачах Эрдёша из свежих научных публикаций. В трех автономных запусках LeanMarathon успешно формализовал все семь целевых теорем с вердиктом «nosorry» — это значит, что в доказательствах не осталось пробелов, а работа охватила 258 лемм. По оценке команды разработчиков, этот кейс доказывает: надежный AI-ассистент в науке требует не просто «умных» моделей, а жестких архитектурных каркасов, способных удерживать логику на длинной дистанции.
Мы видим четкий тренд: эпоха болтливых чат-ботов в серьезном бизнесе и науке заканчивается, уступая место верифицируемым автономным системам.
Для техлидов это важный сигнал: если ваша задача требует стопроцентной точности в течение длительного времени, забудьте о масштабировании контекстного окна или бесконечном тюнинге промптов. Будущее за жестким разделением ролей между агентами и внедрением состязательного аудита. Индустриальная надежность ИИ начинается там, где заканчивается вера модели на слово и начинается тотальная проверка каждой логической связки.