Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Maestro научилась отличать трудный шаг доказательства от ложной леммы или ошибочного плана и выбирать для каждого случая разную реакцию. В препринте University of Illinois Urbana-Champaign, AWS AI Labs и Georgia Institute of Technology, который не прошёл рецензирование и содержит замеры самих авторов, система доказала 34 из 48 теорем arXivLean против 19 у обычного агента. Для команд, которые строят проверяемые LLM-системы, работа переносит акцент с выбора модели на управление неудачными попытками.
Почему повторное дробление заводит доказательство в тупик
Агент редко пишет длинное доказательство Lean с первой попытки. Поэтому существующие системы делят исходную цель на вспомогательные леммы, отправляют их отдельным агентам и снова дробят те леммы, которые не удалось доказать.
Одинаковый сигнал «не получилось» скрывает разные причины. Агенту может не хватать вспомогательного факта, сама лемма может быть ложной, а вся ветвь доказательства — опираться на неудачную идею. Если система всегда отвечает новым разбиением, она подробно развивает план, который не может привести к результату.
Maestro заменяет это правило общей координацией. Рабочие агенты действуют в копиях единого проекта Lean: доказывают открытые цели, предлагают разбиение на леммы или ищут другой подход. При неудаче они возвращают не только статус, но и описание испробованных путей, недостающих фактов, предполагаемых контрпримеров и уровня проблемы — внутри текущей леммы или выше в плане.
Постоянный координатор видит все отчёты и редактирует общий проект. Он может уточнить задание одному агенту, добавить общую лемму для нескольких ветвей, исправить ложное утверждение либо удалить целое поддерево и построить его заново. Уже доказанные факты при этом можно сохранить, если они не зависят от отвергнутой идеи.
В одном разборе Maestro выбрала неподходящую конструкцию для контрпримера к четырнадцатой проблеме Гильберта. Координатор удалил 22 связанные с ней леммы, включая 19 уже доказанных, сохранил независимые результаты и сменил конструкцию. После такого отступления доказательство завершилось через 1,4 часа — действие, которое система с планом, способным только разрастаться, выполнить не может.
Контрпример возвращает на исправление не доказательство, а код
Та же схема работает при генерации проверяемого кода. Входом служат неизменяемая спецификация Lean, определения и условия задачи. Агент сначала пишет реализацию, после чего другие агенты пытаются доказать, что она соответствует спецификации.
Неудачное доказательство здесь тоже допускает несколько объяснений. Ошибка может находиться в рассуждении, во вспомогательной лемме или в самой программе. Если рабочий агент строит проверенный в Lean контрпример, координатор определяет, что нарушена спецификация, и возвращает реализацию агенту-программисту вместе с конкретным входом, на котором она ломается.
В задаче AlgoVeri на алгоритм проталкивания предпотока две модели сначала написали стандартную реализацию, которая прошла созданные агентом тесты. Спецификация иначе обрабатывала граф, где одна дуга перечислена повторно. Ошибка проявилась только при доказательстве: агент нашёл граф, на котором программа нарушала требование, после чего координатор отправил код на исправление и заново построил обязательства для проверки.
Этот цикл отличается от обычного исправления по результатам тестов. Спецификация остаётся стабильным контрактом, а доказательство исследует все допустимые входы, а не только заранее выбранные примеры. Практический шаблон здесь шире Lean: исполнитель должен сообщать координатору причину сбоя и проверяемое свидетельство, а координатор — уметь пересматривать решение на том уровне, где возникла ошибка.
Координация меняет архитектуру агента, но не отменяет проверку на своей задаче
Maestro проверяли с четырьмя ведущими LLM на семи математических и трёх программных наборах задач. В сравнение вошли исследовательские теоремы, олимпиадная математика, проверка готовых реализаций и синтез кода. На простых программных задачах обычные агенты уже близки к насыщению, поэтому заметнее всего разница проявилась в длинных доказательствах и более сложной проверке программ.
Главное контролируемое сравнение — с Claude Code или Codex на той же базовой модели. Простое рекурсивное дробление почти не улучшило результат обычного агента, тогда как Maestro закрывала больше целей. Значит, прибавку даёт не само распараллеливание лемм, а возможность сопоставить неудачи разных ветвей, остановить бесполезный поиск и изменить план выше места сбоя.
Сравнения с опубликованными доказателями нужно читать осторожнее: там различаются базовые модели, вычислительные бюджеты и версии наборов задач. Для архитектурного решения важнее другое наблюдение работы — управляющая оболочка улучшала результат у разных моделей и применяла один цикл как к математике, так и к коду.
Командам не обязательно менять выбранную LLM, чтобы проверить этот подход. Если агентный процесс уже разбивает задачу на шаги, план стоит хранить как изменяемое состояние, собирать структурированные причины неудач и разрешать координатору отменять решения выше текущего шага. Но результаты Lean не доказывают такой же выигрыш в произвольном рабочем процессе: перенос требует формальной спецификации или другого механизма, который надёжно проверяет контрпримеры и итог.
Источники
Иллюстрация: рисунок из статьи «Maestro: Agentic Formal Proof Development by Coordination», Haoyu Li, Zeren Shui, Yuhao Zhang и др., CC BY 4.0
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
