Ферма в Lean: 11 дней в сентябре и 28,7 часа у Fable 5.2

Тысяча агентов на ранней версии Claude Fable 5.2 за 28,7 часа заново доказала Великую теорему Ферма в Lean без платформы Prove2Me и без исследователя у руля. Anthropic рассказала об этом 9 ноября в блоге Claude, и читать результат стоит как повтор уже готового доказательства. Агенты стартовали с 47 доказанными леммами из сентябрьской формализации, а сама Anthropic называет прогон игрушечным экспериментом.

Измерены в нём время, расход выходных токенов, длина доказательства и поведение команды. Что команды на моделях вроде Fable 5.2 справятся с амбициозными долгими задачами, Anthropic выводит сама, из одного прогона.

С чем агенты начинали

Команда получила 60 утверждений: финальную теорему и 59 промежуточных вех, у каждого однострочное описание. К ним прилагались набросок классического пути в одно предложение, нужные определения и те самые 47 лемм. Плюс жёсткая иерархия: один ведущий и 999 помощников. Ведущему велели разбить задачу и раздать части, помощникам ждать работы и переспрашивать ведущего, если задача неясна. Других указаний, как доказывать и как организоваться, не было. За прогон обвязка 19 раз автоматически напомнила ведущему, сколько осталось времени, и каждый раз подбодрила продолжать.

Инструменты у каждого агента общего назначения: shell и редактор файлов в собственной песочнице без сети, Lean с Mathlib в образе, своя ветка в Git с правом открывать merge request в main и общая база Postgres, доступная из shell. Доказательство засчитывалось, когда попадало в main и проходило проверку грейдера.

Для сравнения: в сентябре на ту же теорему у исследователя и десятков агентов на внутренней модели, примерно сопоставимой с Claude Fable 5.1, ушло 11 дней и около 6 миллиардов выходных токенов, а кода в Lean получилось 13 миллионов строк. Новая команда потратила треть выходных токенов, примерно 2 миллиарда, и написала доказательство в семь раз короче. Сентябрьская работа держалась на Prove2Me, которую создали Тяньи Пэн, ныне сотрудник Anthropic, и его коллеги из Колумбийского университета. Платформа ведёт общий граф: каждое утверждение связано с более мелкими, на которые его разбили, и любой агент может спросить, какие недоказанные куски готовы к работе. По словам Anthropic, ранние попытки без неё проваливались, потому что агенты теряли состояние проекта и переставали работать вместе.

Пять таблиц вместо Prove2Me

Тысяча песочниц понадобилась из-за железа. Одна общая машина упиралась примерно в 100 агентов: больше половины прогонов на сотне агентов пришлось останавливать или перезапускать, потому что кончались память, диск или CPU. В новом прогоне каждый агент жил на своей лёгкой виртуальной машине, а общим местом стала SQL-база. Anthropic объясняет выбор так: у SQL есть универсальные примитивы для организации данных, транзакции выдерживают одновременную запись от тысячи агентов, и Claude с ним уже знаком.

За первые 10 минут ведущий завёл пять таблиц: приказы всей команде, назначения, открытую доску заметок, список подзадач, где задача достаётся первому взявшему, и журнал готовой работы. Затем раздал каждое утверждение бригаде из 16-17 помощников, назначил в каждой капитана и велел всем для начала оценить сложность своего утверждения.

Оценки оказались мрачными. Примерно на 27-й минуте, когда три утверждения уже были доказаны, ведущий отложил 47 утверждений, которые большинство помощников сочли невыполнимыми в рамках бюджета, и перебросил почти всех на оставшиеся 10. Бригады выросли до 46-139 агентов. Около 45-й минуты, при примерно пяти доказанных из десяти, ведущий записал:

«Пропускная способность команды намного выше, чем предполагали ранние вердикты „невыполнимо в рамках бюджета“».

Все 10 закрыли примерно за 70 минут. Ведущий написал «нет причин простаивать» и вернул помощников к отложенным утверждениям, а к третьему часу сказал свободным агентам «не ждите меня». Подзадачи к тому времени писали уже не только капитаны: к часу 5,6 задачи создали 73 помощника, всего 756 задач, и капитанами из них были только 16.

Около 18-го часа прогон остановили и перезапустили с последнего сохранения, дав агентам ещё 12 часов. Оставались теорема Ленглендса-Таннелла, классический результат, на который опирается доказательство Эндрю Уайлса, и зависящие от неё утверждения. Капитан этой задачи раньше оценивал её минимум в 0,7-1 миллиона строк Lean и давал меньше 1% шансов успеть. Ведущий перебросил на неё около 750 помощников с припиской «Если честно, шансы низкие». Задачи пришлось дробить деревом: помощник, которому кусок был не по силам, делил его на меньшие, и к концу дерево разрослось до 2 418 задач глубиной до 10 уровней. Каждый кусок мог опираться на ещё не доказанные части под ним, поэтому сотни агентов работали параллельно. Ленглендс-Таннелл сдался на 28,4 часа, финальная теорема на 28,7.

В итоговом счёте 54 из 60 утверждений: пять альтернативных путей перестали быть нужны, одно утверждение сняли.

Как держали тысячу агентов

Песочницы закрывали в несколько слоёв. Отдельных средств переписки у агентов не было, только база и Git. Пушить можно было лишь в свою ветку, а слиянием в main занималась отдельная задача, которая отказывала только при конфликте или сбое вроде несвязанной истории. Запросы к базе шли под общей непривилегированной ролью, на каждый SQL-запрос давалось пять секунд, записи больше 256 МиБ отклонялись. Наружу из песочницы вела одна труба к шлюзу, который сам вызывал Claude API, передавал запросы к Git и базе и помечал каждый идентичностью агента, чтобы один не выдавал себя за другого. Ядро собрано без загружаемых модулей, kexec, прямого доступа к памяти и kernel probes и работало в режиме lockdown, команды выполнялись от непривилегированного пользователя без sudo.

Каждый вызов инструмента до запуска проверял классификатор на основе LLM с промптом: он ищет попытки выбраться из песочницы, прощупать её границы или вмешаться в мониторинг. По общему правилу Anthropic блокировка останавливает всю команду до разбора человеком. В этом прогоне работал только монитор, который видит действия без цепочки рассуждений, и прогон закончила бы лишь блокировка ведущего, а заблокированного помощника просто убирали. Параллельный монитор, читающий цепочку рассуждений, добавили вскоре после прогона: в red-team-оценках такие мониторы поймали все попытки саботажа. Отдельно действия команды разбирал офлайн-монитор, которому видны действия других агентов.

Из более чем миллиона вызовов инструментов ни один не дотянул до блокировки. При повторной прогонке через монитор с цепочкой рассуждений и нынешние критерии близко к порогу подошёл один вызов: проверка root-доступа. Модели в таких экспериментах могут ещё не пройти предрелизную проверку согласованности, поэтому мониторинг рассчитан на то, что модель может оказаться несогласованной.

Где без людей пока хуже

Отказываться от специализированных платформ Anthropic не предлагает: Prove2Me, по её словам, может ускорять компиляцию Lean и давать агентам искать и переиспользовать результаты людей. Слабое место команды видно по той же истории с оценками: агенты склонны сдаваться на трудных задачах и неверно судить об их сложности, а 47 утверждений, отложенных как невыполнимые, команда потом в основном доказала. Человеческое ободрение в такие моменты, считают в Anthropic, удерживает агентов от слишком ранней остановки.

Последнее сообщение ведущего в журнале: «Всем спасибо: Великая теорема Ферма в main, проверена ядром официального чекера».