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

AI summary

Overview

Research area: Reinforcement learning for LLM agents (agentic RL), with formal verification via the Lean 4 proof assistant; applied to software engineering and terminal-usage tasks.

Technical level: Advanced — assumes familiarity with GRPO-style policy optimization, agent harnesses, and dependent-type formal verification.

Scope: The paper introduces Lean4AgenticRL, a framework that derives verifiable high-, mid-, and low-level process rewards inside a unified Lean 4 schema and uses them to train the LAR-9B/27B model family.

What This Paper Is About

Current large-scale agentic RL for LLMs mostly relies on a single outcome reward at the end of a long trajectory, which cannot distinguish useful intermediate actions from redundant or wrong ones. Existing attempts at process rewards typically score individual tool calls, which can miss broader workflow progress and degrade training when a single call has no direct link to the task goal. The paper's goal is to unify outcome, workflow-stage, and toolcall rewards in one verifiable framework so that agent training gets denser and more reliable signals on open-ended tasks like SWE and terminal usage.

Key Contributions

1. Lean4AgenticRL framework: To the authors' knowledge, the first framework that derives multi-level process rewards within Lean — described as a uniform dependent-type verifiable language — for agentic RL in open-ended domains.
2. Problem-specific workflow (PSWF) system: A plan-then-execute paradigm that balances the agent's own capability against execution controllability, plus a generalization of the existing agent verification framework from fixed workflows to general harness systems.
3. Workflow formalization and multi-level reward annotation: Natural-language plans are formalized into Lean4Agent-style stages with pre- and post-conditions, trajectories are segmented into those stages, and three reward levels (α outcome, β workflow-stage, γ toolcall) are annotated.
4. Workflow-stage-normalized GRPO: A GRPO variant that computes advantages by grouping steps that align to the same general workflow stage across rollouts, rather than aligning raw tool calls. This trains the released LAR-9B/27B models.

Main Findings

• Benchmark results: LAR-27B reaches 84.2% on SWE-Bench-Verified, 68.2% on TerminalBench-2.0, and 77.3% on TerminalBench-2.1. LAR-9B reaches 64.2%, 32.8%, and 29.5% respectively on the same three benchmarks.
• Gains over base models (9B): LAR-9B improves on its base model by 20.2%, 13.5%, and 13.4% on SWE-Bench-Verified, TerminalBench-2.0, and TerminalBench-2.1, with a paired p-value of the average improvement below 10⁻¹⁰.
• Gains over comparable models (9B): LAR-9B surpasses the second-best model of comparable size by 10.7%, 5.6%, and 1.9% on those benchmarks (p = 3.5 × 10⁻³).
• Gains over base models (27B): LAR-27B raises the baseline by 1.2%, 3.5%, and 7.7% on the three benchmarks (p = 0.044).
• Aggregate improvement: Across the three evaluated benchmarks, the models outperform their base models by 9.89% on average and the second-best comparable-size model by 5.07% on average.
• Small model beats larger ones: LAR-9B exceeds the larger Gemma-4-31B on SWE-Bench-Verified (64.2% vs 61.0%) and performs on par with it on TerminalBench-2.0 (32.8% vs 33.9% — the paper describes this as on par).
• Training stability vs. plain GRPO: In matched comparisons on Qwen-3.5-9B, GRPO improved for the first 15 steps on the SWE task but deteriorated to roughly its initial level by step 20, while Lean4AgenticRL improved steadily across all 30 steps. On terminal usage, GRPO fluctuated with a pronounced mid-task degradation; Lean4AgenticRL kept a clear upward trend.
• Training efficiency: Lean4AgenticRL surpassed the best GRPO checkpoint within 10 steps on SWE and 30 steps on terminal usage.
• Ablation — problem-specific workflow: Removing PSWF lowered Qwen-3.5-9B's SWE-Bench-Verified resolution rate from 44.0% to 42.4%, with failures traced to insufficient repository exploration and misattributed root causes.
• Ablation — toolcall reward γ: Removing γ reduced performance by 6.6% (56.0% with γ vs 49.4% without). Without γ, repeated commands captured by γ increased by 66.8% versus the base model and total tool calls rose 18.7% versus full Lean4AgenticRL, consistent with reward hacking of the LLM-as-judge predicates via echo and repeated read-only or placeholder commands.
• Case study (regex-chess, LAR-27B on TerminalBench-2.1): The outcome reward α stayed at −1 for the step-40, step-80, and step-120 checkpoints and could not distinguish them, while the fraction of stages with β = +1 rose from 2/8 to 4/7 to 5/6 before the task was solved at step 120 (5/5).

Methodology in Plain English

The method has three stages.

1. Plan, then execute. For each problem, the agent runs in a harness (Claude-code or Terminus-2) and first explores the environment to write a natural-language, problem-specific workflow — a stage-by-stage plan. It then executes that plan, with the planning trajectory kept in context to avoid re-exploring. This keeps the agent controllable without a rigid fixed script.

2. Formalize and score. The plan is translated into a formal workflow: a graph of stages, each with a precondition and a postcondition expressed as predicates. Each execution step is assigned to a stage using a local-window LLM check restricted to currently reachable stages, so segmentation scales to very long trajectories and loops/branches get their own instances. Rewards are then assigned on three levels: a high-level ±1 outcome reward α; a mid-level β = +1/−1 depending on whether a stage's postcondition holds at exit (decidable predicates checked in Lean or Python, semantic ones by an LLM judge); and a low-level γ ∈ {−1, 0} that only penalizes known reward-hacking behaviors such as consecutive repetition, no-op commands, and constant shell usage.

3. Train. Rewards are combined: β is scaled by at most 0.5 and only applied to groups with 0% or ≥75% pass rate — the groups whose outcome gradients are least stable. γ, when it fires, forces the reward down to at most −1. Planning-phase tokens use pure α. Advantages are then normalized per workflow stage across rollouts (rather than per tool call), so steps serving the same stage are compared to each other.

Setup. Models are trained from Qwen-3.5-9B and Qwen-3.8-27B on a mixture of TMax-15k and SWE-ReBench, using asynchronous RL built on SLIME and OpenClaw-RL. The 9B model trains for 160 steps and the 27B for 120 steps, both with batch size 32 and group size 32. Clip-higher uses ε_u = 0.28 and ε_l = 0.2, learning rate 1 × 10⁻⁶, 128K max context with responses capped at 8K tokens, on a 64-H200 GPU cluster taking 160 and 240 hours for the 9B and 27B models. Evaluation uses SWE-Bench-Verified under mean@3 and TerminalBench-2.0/2.1 under mean@5 with randomized seeds; Lean and Mathlib version v4.20.0.

Why This Matters

Research impact. The paper argues that formal verification, which routinely supplies training signals in theorem proving and code verification, can also supply them for agentic RL. It gives a concrete recipe for extending a fixed-workflow verifier to open-ended harnesses, and a way to attack the step-alignment problem in GRPO by grouping on workflow stages. The reported gains on top of already heavily post-trained models suggest multi-level rewards still extract signal that outcome-only RL leaves on the table.

Real-world applications:

• Automated software engineering agents that triage issues, locate relevant files, patch code, and verify fixes.
• Terminal and command-line automation for system administration and DevOps workflows.
• Reward-hacking detection and guardrails for any RL pipeline that relies on LLM-as-judge scoring, via the penalty-only γ predicates.
• Auditable, formal traces of agent behavior for compliance or post-hoc review in high-stakes deployments.

Industry relevance. The work was done with Amazon Web Services researchers alongside University of Illinois Urbana-Champaign, targets tasks with direct commercial value, and the code and models are open-sourced at the linked GitHub repository.

Future Directions

• Opening the black box: The authors note that verifiability still depends on externally bounding agent behavior and does not verify the LLM's internal computation.
• Runtime integration: Verification is used to design rewards but is not integrated into the harness at execution time; doing so is flagged as future work.
• Multimodal agents: The framework currently covers SWE and terminal usage without visual signals, leaving GUI or screenshot-based agent tasks unexplored.
• Benchmark headroom: The paper notes SWE-Bench-Verified is approaching saturation at 27B scale and that TerminalBench-2.0 contains tasks with inaccessible external dependencies, arguing TerminalBench-2.1 is the more reliable comparison at that scale — which raises the question of which benchmarks can still separate future methods.

Target Audience

Researchers and engineers working on RL post-training for LLM agents, especially those building process-reward or credit-assignment methods for long-horizon tasks. It also suits practitioners interested in applying formal methods (Lean, dependent types, pre/post-condition specifications) to machine learning pipelines, and teams building SWE or terminal-automation agents who want concrete evidence on where mid-level rewards and reward-hacking guards pay off. Beginners will find the concepts accessible at a high level, but the reward formulations and GRPO objective require background in RL.

Authors’ abstract

Enhancing the agentic capabilities of Large Language Models (LLMs) to tackle complex software engineering (SWE) and general terminal-usage problems is a pressing challenge. Current state-of-the-art LLMs often go through large-scale agentic Reinforcement Learning (RL). However, they mostly rely on high-level outcome rewards, with minimal consideration of low-level toolcall and mid-level workflow-stage rewards, which makes the training less effective. To overcome this limitation, we propose **Lean4AgenticRL**, which, to the best of our knowledge, is the first framework that grounds multi-level process rewards in the unified Lean4 formalization schema for open-ended agentic RL. **Lean4AgenticRL** first builds a *problem-specific workflow* system that balances the agent's own capability and controllability during execution, laying the foundation for further verification. Subsequently, our workflow formalization and multi-level reward annotation methods enable agent behavior verification within a general harness system. It provides multi-level rewards to support more effective agentic RL with the workflow-stage-normalized GRPO algorithm. Using **Lean4AgenticRL**, we train **LAR-9B/27B**, a family of models with enhanced agentic capability. Extensive experiments indicate that our model outperforms the leading model of similar size. **LAR-27B** achieves **77.3%** on TerminalBench-2.1. On average, our models outperform the base model by **9.89%** and surpass the second-best model of comparable size we know by **5.07%**. These results indicate the potential of integrating formal methods in enhancing open-ended agentic RL.