Lean4AgenticRL: LAR-27B atinge 77,3% no TerminalBench-2.1 com recompensas formais

A equipe por trás do Lean4AgenticRL propôs uma forma de treinar agentes baseados em LLM não só pelo resultado final, mas também pela qualidade dos passos intermediários, que são verificados formalmente por meio de um esquema em Lean4. Com base no framework, foram treinados os modelos LAR-9B e LAR-27B. A versão maior atingiu 77,3% no TerminalBench-2.1. Em média, os modelos superaram o modelo base em 9,89% e o melhor modelo de porte comparável conhecido pelos autores em 5,07%.

O problema: o agente aprende pela nota final

Tarefas agênticas em desenvolvimento de software e no uso do terminal são longas. O agente lê o repositório, executa comandos, edita arquivos, roda testes, volta atrás e tenta de novo. As LLMs atuais para esses cenários costumam passar por um RL de ajuste fino em larga escala. Segundo a descrição dos autores, nele predomina a outcome reward: a recompensa pelo resultado, como a aprovação em testes.

Esse sinal tem uma falha evidente. Ele chega só no fim e não diz qual das dezenas de etapas foi acertada e qual foi desnecessária. As chamadas de ferramentas, no nível inferior, e as fases do fluxo de trabalho, no nível intermediário, quase não recebem recompensa própria. Na avaliação dos autores, isso torna o treinamento menos eficiente.

Como funciona o Lean4AgenticRL

A abordagem se baseia na formalização em Lean4. Os autores afirmam que este é o primeiro framework em que recompensas de processo em vários níveis, voltadas ao RL agêntico aberto, se apoiam em um esquema único em Lean4. A cadeia funciona assim.

Primeiro, é construído um problem-specific workflow, ou seja, um fluxo de trabalho sob medida para a tarefa. Ele precisa equilibrar as capacidades próprias do agente e a controlabilidade: o agente não fica preso a trilhos rígidos, mas recebe uma estrutura que permite verificar seu comportamento.

Em seguida, o workflow é formalizado e as recompensas são distribuídas em vários níveis. Isso permite verificar as ações do agente dentro de uma estrutura universal (harness). O treinamento usa GRPO com normalização por etapas do workflow. A ideia é comparar e calcular a média do sinal dentro de cada etapa, e não sobre toda a trajetória de uma vez.

Principais parâmetros do trabalho:

• framework: Lean4AgenticRL, com recompensas em três níveis (chamada de ferramenta, etapa do workflow e resultado final);
• algoritmo: workflow-stage-normalized GRPO;
• modelos: LAR-9B e LAR-27B;
• melhor resultado: 77,3% do LAR-27B no TerminalBench-2.1;
• ganho sobre o modelo base: 9,89% em média;
• vantagem sobre o segundo melhor modelo de porte comparável: 5,07%.

O que os números mostram

Os 77,3% no TerminalBench-2.1 parecem um resultado forte para um modelo de 27 bilhões de parâmetros. Mas o resumo do artigo não traz os detalhes necessários para uma avaliação precisa. O modelo base não é nomeado. O conjunto completo de benchmarks usado no cálculo da média não é informado. Não está claro se os 9,89% e os 5,07% são pontos percentuais ou valores relativos. Também não se diz qual é, exatamente, o «segundo melhor modelo». Enquanto o texto completo do artigo não for analisado, é melhor tratar esses números como uma afirmação dos autores, e não como uma comparação independente.

Ainda assim, a direção é clara. Se as recompensas por etapa puderem ser obtidas de forma verificável, sem um modelo de recompensa treinável e sem a avaliação ruidosa de outra LLM, o sinal de processo fica mais barato e mais confiável. É nisso que se apoia a aposta nos métodos formais.

O que as equipes devem fazer com isso

Para quem faz ajuste fino de agentes em tarefas de SWE e de terminal, a principal conclusão é de engenharia: vale olhar para a estrutura da trajetória, e não apenas para o pass/fail final. Mesmo sem Lean4, é útil marcar as etapas típicas (exploração, edição, verificação) e medir o progresso por elas.

Vale esperar o texto completo e, caso os autores publiquem, o código e os pesos do LAR-9B/27B. Aí será possível checar quanto trabalho a formalização do workflow exige para uma nova classe de tarefas e se o ganho se mantém fora dos benchmarks de terminal. O custo dessa anotação é que vai definir se a abordagem se tornará uma ferramenta de trabalho ou ficará como demonstração de pesquisa.