Lean4AgenticRL: Advancing Agentic RL with Verifiable Multi-level Process Rewards

Lean4AgenticRL. Advancing Agentic RL with Verifiable Multi-level Process Rewards. By Ruida Wang and three others, from Amazon Web Services and the University of Illinois Urbana-Champaign. Published on the fifteenth of October. Its code repository is worked out: about forty-five source files, with a readme and a licence.

Getting large language models to handle complex software engineering and general terminal-usage problems is a pressing challenge, and the current state-of-the-art models usually get there through large-scale agentic reinforcement learning. The weak point is the reward. These training runs mostly rely on high-level outcome rewards: did the task succeed at the end. There is minimal consideration of the low-level reward for an individual tool call, or of the mid-level reward for a stage of the workflow. An agent can make many moves before the outcome is known, and a signal given only at the end makes the training less effective. A good tool call inside a failed attempt earns nothing, and a careless one inside a lucky success is rewarded along with everything else.

Lean4AgenticRL grounds rewards at all three levels in one place: the unified Lean4 formalization schema. To the authors' knowledge, it is the first framework to ground multi-level process rewards in that schema for open-ended agentic RL. The aim is that an agent's behaviour, not only its final result, becomes something that can be verified. If each tool call and each workflow stage can be checked against a formal description, each can also be rewarded on its own terms, instead of waiting for the final outcome.

It proceeds in steps. First it builds a problem-specific workflow system, which balances the agent's own capability against controllability during execution. That balance is what lays the foundation for verification later on. Next come two methods, workflow formalization and multi-level reward annotation, which together let agent behaviour be verified inside a general harness system. Out of that verification come the multi-level rewards, and they feed training through a workflow-stage-normalized variant of the GRPO algorithm. The order matters: an agent's behaviour has to be structured before it can be formalized, and formalized before it can be rewarded at each level.

With this framework the authors train LAR-9B and LAR-27B, a family of models with enhanced agentic capability. Extensive experiments indicate that the models outperform the leading model of similar size. The larger one, LAR-27B, reaches seventy-seven point three percent on TerminalBench-2.1. Averaged across the evaluations, the models beat their base model by nine point eight nine percent, and surpass the second-best model of comparable size the authors know of by five point zero seven percent.

Underneath the numbers is a bet that an agent's work can be checked at every level, from a single tool call up to the finished task, rather than only judged at the end. The authors read their results as a sign of what formal methods could contribute to open-ended agentic reinforcement learning.