Lean4AgenticRL: LAR-27B набрала 77,3% на TerminalBench-2.1 с формальными наградами

Команда авторов Lean4AgenticRL предложила способ обучать LLM-агентов не только по финальному результату, но и по качеству промежуточных шагов, причём шаги проверяются формально, через схему Lean4. На основе фреймворка обучены модели LAR-9B и LAR-27B. Старшая версия набрала 77,3% на TerminalBench-2.1. В среднем модели превзошли базовую на 9,89%, а лучшую из известных авторам моделей сопоставимого размера на 5,07%.

Проблема: агент учится по итоговому баллу

Агентные задачи в разработке ПО и работе с терминалом длинные. Агент читает репозиторий, запускает команды, правит файлы, гоняет тесты, откатывается и пробует снова. Современные LLM для таких сценариев обычно проходят масштабное RL-дообучение. По описанию авторов, в нём доминирует outcome reward: награда за итог, например за пройденные тесты.

У такого сигнала очевидный недостаток. Он приходит в конце и ничего не говорит о том, какой из десятков шагов был удачным, а какой лишним. Вызовы инструментов на нижнем уровне и стадии рабочего процесса на среднем почти не получают собственной награды. Это, по мнению авторов, делает обучение менее эффективным.

Как устроен Lean4AgenticRL

Подход строится вокруг формализации в Lean4. Авторы утверждают, что это первый фреймворк, где многоуровневые процессные награды для открытого агентного RL опираются на единую схему Lean4. Цепочка выглядит так.

Сначала строится problem-specific workflow, то есть рабочий процесс под конкретную задачу. Он должен сохранять баланс между собственными возможностями агента и управляемостью: агента не сажают на жёсткие рельсы, но дают структуру, по которой можно проверять поведение.

Затем workflow формализуется, а награды размечаются на нескольких уровнях. Это позволяет верифицировать действия агента внутри универсальной обвязки (harness). Для обучения используется GRPO с нормализацией по стадиям workflow. Идея в том, чтобы сравнивать и усреднять сигнал внутри этапа, а не по всей траектории сразу.

Ключевые параметры работы:

• фреймворк: Lean4AgenticRL, награды на трёх уровнях (вызов инструмента, этап workflow, итог);
• алгоритм: workflow-stage-normalized GRPO;
• модели: LAR-9B и LAR-27B;
• лучший результат: 77,3% у LAR-27B на TerminalBench-2.1;
• прирост к базовой модели: в среднем 9,89%;
• отрыв от второй по силе модели сопоставимого размера: 5,07%.

Что показывают цифры

77,3% на TerminalBench-2.1 для модели на 27 млрд параметров выглядит сильным результатом. Но в аннотации нет деталей, которые нужны для точной оценки. Не названа базовая модель. Не указан полный набор бенчмарков, по которым считалось среднее. Не раскрыто, выражены 9,89% и 5,07% в процентных пунктах или в относительных величинах. Не сказано, кто именно «вторая по силе модель». Пока полный текст статьи не разобран, эти цифры лучше читать как заявление авторов, а не как независимое сравнение.

При этом направление понятно. Если награды за шаги можно получать проверяемо, без обучаемой reward-модели и без шумной оценки другой LLM, то процессный сигнал становится дешевле и надёжнее. Именно на этом держится ставка на формальные методы.

Что с этим делать командам

Для тех, кто сам дообучает агентов на SWE и терминальных задачах, главный вывод инженерный: стоит смотреть на структуру траектории, а не только на финальный pass/fail. Даже без Lean4 полезно разметить типовые стадии (разведка, правка, проверка) и мерить прогресс по ним.

Стоит дождаться полного текста и, если авторы выложат, кода и весов LAR-9B/27B. Тогда можно проверить, сколько работы требует формализация workflow под новый класс задач и переносится ли выигрыш за пределы терминальных бенчмарков. Именно стоимость такой разметки определит, станет ли подход рабочим инструментом или останется исследовательской демонстрацией.