Lean4AgenticRL : LAR-27B atteint 77,3% sur TerminalBench-2.1 grâce à des récompenses formelles

L'équipe de Lean4AgenticRL propose d'entraîner des agents LLM non seulement sur leur résultat final, mais aussi sur la qualité de leurs étapes intermédiaires, vérifiées formellement via un schéma Lean4. Les modèles LAR-9B et LAR-27B ont été entraînés avec ce framework. La version la plus grande atteint 77,3% sur TerminalBench-2.1. En moyenne, les modèles dépassent le modèle de base de 9,89%, et le meilleur modèle de taille comparable connu des auteurs de 5,07%.

Le problème : l'agent apprend à partir du score final

Les tâches agentiques en développement logiciel et en usage du terminal sont longues. L'agent lit un dépôt, lance des commandes, modifie des fichiers, exécute des tests, revient en arrière et réessaie. Les LLM actuels destinés à ces scénarios passent généralement par un réentraînement RL à grande échelle. Selon les auteurs, c'est l'outcome reward qui y domine : une récompense portant sur le résultat, par exemple la réussite des tests.

Ce signal a un défaut évident. Il arrive à la fin et n'indique pas, parmi des dizaines d'étapes, lesquelles étaient utiles et lesquelles superflues. Les appels d'outils, au niveau le plus bas, et les étapes du workflow, au niveau intermédiaire, ne reçoivent presque aucune récompense propre. Pour les auteurs, cela rend l'entraînement moins efficace.

Comment fonctionne Lean4AgenticRL

L'approche repose sur une formalisation en Lean4. Les auteurs affirment qu'il s'agit du premier framework où des récompenses de processus multiniveaux, pour le RL agentique ouvert, s'appuient sur un schéma Lean4 unique. La chaîne se déroule ainsi.

D'abord, on construit un problem-specific workflow, c'est-à-dire un processus de travail adapté à la tâche. Il doit trouver un équilibre entre les capacités propres de l'agent et le contrôle qu'on peut exercer sur lui : l'agent n'est pas enfermé sur des rails rigides, mais il dispose d'une structure qui permet de vérifier son comportement.

Ensuite, le workflow est formalisé et les récompenses sont réparties sur plusieurs niveaux. Cela permet de vérifier les actions de l'agent au sein d'un harness universel. L'entraînement utilise GRPO avec normalisation par étape du workflow. L'idée est de comparer et de moyenner le signal à l'intérieur d'une étape, et non sur l'ensemble de la trajectoire d'un coup.

Paramètres clés du travail :

• framework : Lean4AgenticRL, récompenses à trois niveaux (appel d'outil, étape du workflow, résultat final) ;
• algorithme : workflow-stage-normalized GRPO ;
• modèles : LAR-9B et LAR-27B ;
• meilleur résultat : 77,3% pour LAR-27B sur TerminalBench-2.1 ;
• gain par rapport au modèle de base : 9,89% en moyenne ;
• avance sur le deuxième meilleur modèle de taille comparable : 5,07%.

Ce que montrent les chiffres

Avec 77,3% sur TerminalBench-2.1, un modèle de 27 milliards de paramètres semble afficher un résultat solide. Mais l'abstract ne donne pas les détails nécessaires pour l'évaluer précisément. Le modèle de base n'est pas nommé. L'ensemble complet des benchmarks utilisés pour calculer la moyenne n'est pas indiqué. On ne sait pas si les 9,89% et les 5,07% sont exprimés en points de pourcentage ou en valeurs relatives. On ne sait pas non plus de quel modèle il s'agit quand on parle du « deuxième meilleur ». Tant que le texte complet de l'article n'a pas été analysé, mieux vaut lire ces chiffres comme une déclaration des auteurs, et non comme une comparaison indépendante.

La direction, elle, est claire. Si les récompenses par étape peuvent être obtenues de façon vérifiable, sans reward-model entraîné et sans l'évaluation bruitée d'un autre LLM, le signal de processus devient moins coûteux et plus fiable. C'est sur ce pari que reposent les méthodes formelles.

Que peuvent en faire les équipes

Pour ceux qui réentraînent eux-mêmes des agents sur des tâches SWE et terminal, la leçon principale est d'ordre ingénierie : il faut regarder la structure de la trajectoire, et pas seulement le pass/fail final. Même sans Lean4, il est utile d'annoter les étapes types (exploration, modification, vérification) et de mesurer la progression sur chacune.

Il vaut la peine d'attendre le texte complet et, si les auteurs les publient, le code et les poids de LAR-9B/27B. On pourra alors vérifier combien de travail demande la formalisation du workflow pour une nouvelle classe de tâches, et si le gain se transfère au-delà des benchmarks de terminal. Le coût de cette annotation déterminera si l'approche devient un outil de travail ou reste une démonstration de recherche.