PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Ruida Wang, Gerald Friedland, Tong Zhang, Chris Kong

arXiv:2610.22448v1cs.LG

TL;DR

Long agent traces receive sparse outcome rewards that cannot distinguish useful intermediate actions from redundant or erroneous ones. Lean4AgenticRL formalizes multi-level rewards for open-ended agentic RL and trains models that outperform comparable-size alternatives across three benchmarks.

  • Problem

    Sparse outcome rewards for long-horizon agentic tasks cannot distinguish useful intermediate actions from redundant or erroneous ones.

    Source: §4.1 · p. 9

  • Method

    Lean4AgenticRL formalizes workflows for general harnesses, unifies outcome, workflow-stage, and toolcall rewards, and optimizes policies with workflow-stage-normalized GRPO.

    Source: §1 · p. 2, §2.4 · p. 5, §5 · p. 9

  • Results

    Across three benchmarks, LAR models outperform their base models by 9.89% and comparable-size second-best models by 5.07% on average.

    Source: §3.3 · p. 7

  • Takeaways & Limitations

    The authors conclude that Lean4AgenticRL provides more effective agentic RL for continuously optimizing models that have already undergone extensive post-training.

    Source: §3.3 · p. 7

    Verifiability depends on externally bounding agent behavior and does not inspect the LLM’s internal computation.

    Source: A LIMITATIONS · p. 16

Abstract

from arXiv · show

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.

1 INTRODUCTION

Agentic RL for long-horizon software and terminal tasks often relies on outcome rewards that do not distinguish useful intermediate actions. Lean4AgenticRL formalizes workflows and multi-level rewards in Lean4, then uses them to train models that outperform comparable-size models across evaluated benchmarks.

1 INTRODUCTION

  • Outcome rewards can fail to distinguish useful intermediate actions, while toolcall-only rewards may miss broader workflow progress.This motivates unifying outcome, workflow-stage, and toolcall rewards in a verifiable framework.Source: §1 · p. 1, Figure 1 · p. 2
  • Lean4AgenticRL uses a plan-then-execute problem-specific workflow, formalizes it for general harnesses, and annotates trajectories with outcome, workflow-stage, and toolcall rewards.The workflow-stage-normalized GRPO algorithm trains with these multi-level rewards.Source: §1 · p. 2, Figure 1 · p. 2
  • The framework derives multi-level process rewards in Lean and extends agent verification from fixed workflows to general harness systems.The authors describe it as the first such framework to their knowledge.Source: §1 · p. 2
  • 9.89% average improvement over base models and 5.07% over comparable-size second-best models; LAR-27B reaches 77.3% on TerminalBench-2.1.The comparison covers three evaluated benchmarks.Source: §1 · p. 3
  • The authors present formal verification as a new perspective for agentic RL and open-source their code and model.They frame the framework as a basis for future studies of formal methods in modern RL.Source: §1 · p. 3

2 METHODOLOGY

Lean4AgenticRL formalizes problem-specific workflows and agent behavior in Lean to assign outcome, workflow-stage, and toolcall rewards. It trains LAR-9B/27B with workflow-stage-normalized GRPO.

2.1 PRELIMINARIES

  • The paper defines an LLM agent as cycling between reasoning and tool-based actions, and verifies workflow-stage completion through predicate-based preconditions and postconditions.The workflow is represented as stages connected by allowed transitions, with a stage verified when its post-condition holds after execution.Source: §2.1 · p. 3

2.2 PROBLEM-SPECIFIC WORKFLOW AGENT SYSTEM

  • The PSWF system balances fixed-workflow control with ReAct-style flexibility by planning from task exploration and then executing the resulting stage-wise plan.The planning trajectory is included during execution to avoid repeated exploration; the plan can specify relevant files, suspected causes, and repair and verification steps.Source: §2.2 · p. 3, §2.2.1 · pp. 3–4, §2.2.2 · p. 4

2.3.1 GENERALIZING AGENT VERIFICATION SYSTEM WITH PSWF

  • The framework extends verification to open-ended harnesses by formalizing each problem-specific workflow and assigning execution steps to reachable stages using a local context window.Revisits in loops and branches receive separate stage instances, and the local-window segmentation is intended to scale to ultra-long trajectories.Source: §2.3.1 · p. 4

2.3.2 WORKFLOW-STAGE MID-LEVEL REWARD ANNOTATION

  • Workflow-stage rewards β verify whether each stage meets its post-condition, using Lean or Python for decidable predicates and an LLM judge for semantic interpretation.The authors describe this reward as intermediate between toolcall-level and outcome-level rewards.Source: §2.3.2 · pp. 4–5

2.3.3 TOOLCALL LOW-LEVEL REWARD ANNOTATION

  • Penalty-only toolcall rewards flag repetition, noop commands, and constant-shell behavior to counter reward hacking that can exploit workflow-level predicates.The toolcall reward is −1 for violations and 0 otherwise, avoiding positive reward that could overwhelm other rewards.Source: §2.3.3 · p. 5

2.4 LEAN4AGENTICRL TRAINING

  • Workflow-stage-normalized GRPO combines outcome and stage rewards, limits process-reward use to groups with 0% or at least 75% pass rates, and normalizes advantages across workflow stages.The framework trains LAR-9B/27B on software-engineering and general terminal-usage tasks.Source: §2.4 · pp. 5–6, §2.5 · p. 6

3 EXPERIMENT

The experiments evaluate LAR-9B/27B on SWE and terminal-use benchmarks, comparing them with similar-size models and testing Lean4AgenticRL against outcome-reward GRPO. The results report cross-benchmark gains, training-dynamics differences, ablation effects, and denser stage-level signals in a case study.

3.1.1 TASK AND BENCHMARK

  • Evaluation uses SWE-Bench-Verified and TerminalBench-2.0/2.1, with mean@3 for SWE and mean@5 for terminal tasks, against similar-size open-weight models.Baselines ran with the highest reasoning effort and longest supported context; Terminus-2 was used for terminal tasks and Claude-code for SWE.Source: §3.1.1 · p. 6, §3.1.2 · p. 6

3.2 IMPLEMENTATION DETAILS

  • Training uses Qwen-3.5-9B and Qwen-3.8-27B with TMax-15k and SWE-ReBench, using asynchronous RL built on SLIME and OpenClaw-RL.The 9B and 27B models were trained for 160 and 120 steps, respectively.Source: §3.2 · pp. 6–7

3.3 MAIN RESULTS

  • 9.89% and 5.07%: LAR models outperform their base models and the second-best comparable-size models, respectively, on average across three benchmarks.The reported comparison covers SWE-Bench-Verified, TerminalBench-2.0, and TerminalBench-2.1.Source: Table 1 · p. 7, §3.3 · p. 7
  • At 9B, LAR-9B improves on its base across all three benchmarks and surpasses comparable-size peers; at 27B, LAR-27B also raises its base on all three.LAR-27B reaches 84.2% on SWE-Bench-Verified and 77.3% on TerminalBench-2.1; LAR-9B’s gains over its base are 20.2%, 13.5%, and 13.4%, respectively, while its gains over the second-best comparable-size model are 10.7%, 5.6%, and 1.9%.Source: §3.3 · p. 7

3.4 COMPARED WITH DIRECT RL TRAINING

  • Lean4AgenticRL outperforms outcome-reward GRPO throughout training on both tasks and reaches the best GRPO checkpoint within 10 SWE steps and 30 terminal-task steps.GRPO deteriorates after early SWE gains and fluctuates on terminal usage, while Lean4AgenticRL improves steadily on both.Source: Figure 2 · p. 7, §3.4 · p. 8

3.5.1 DROPPING PROBLEM-SPECIFIC WORKFLOW

  • Without PSWF, Qwen-3.5-9B’s SWE resolution rate falls from 44.0% to 42.4%, with failures involving insufficient repository exploration and file localization.The experiment evaluates PSWF without training in the Claude-code harness.Source: §3.5.1 · p. 8

3.5.2 DROPPING γ REWARDS

  • Removing γ reduces model performance by 6.6%, increases repeated commands by 66.8%, and raises tool calls by 18.7% relative to full Lean4AgenticRL.The authors report that without γ, ritualistic commands can exploit LLM-judge predicates and inflate response length.Source: §3.5.2 · p. 8

3.6 CASE STUDY

  • In the regex-chess case, β-positive stages rise from 2/8 to 4/7 and 5/6 before the task is solved at step 120, when the fraction is 5/5.The binary outcome reward α remains −1 for the first three checkpoints, while β identifies intermediate failures and successes.Source: §3.6 · pp. 8–9

4 RELATED WORK

Prior agentic RL work uses outcome rewards, toolcall-level process rewards, or task-specific verifiers, leaving open challenges for long-horizon, open-ended tasks. Lean4AgenticRL combines multi-level verifiable rewards with a unified formal framework for general agent executions.

4.1 AGENTIC REINFORCEMENT LEARNING

  • Sparse outcome rewards assign identical credit across long-horizon steps, while toolcall-level signals can miss broader progress; prior hierarchical methods rely on similar trajectories or tree search.Task-specific symbolic or algorithmic oracles have generally been used in controlled environments.Source: §4.1 · p. 9

4.2 VERIFIABLE AGENT SYSTEMS

  • Existing agent verification has served as runtime checking or post-hoc auditing, and Lean4Agent uses predefined fixed workflows rather than general harnesses.Other approaches include workflow linters and verification of tool calls and execution results.Source: §4.2 · p. 9

5 CONCLUSION

Lean4AgenticRL formalizes multi-level process rewards in Lean for open-ended agentic RL, combining problem-specific workflows, general-harness verification, and workflow-stage-normalized GRPO. LAR-9B/27B outperform their base and comparable-size models on the evaluated benchmarks, and the framework points toward further formal-method applications in modern RL.

5 CONCLUSION

  • Lean4AgenticRL derives multi-level process rewards under a unified Lean-based framework for open-ended agentic RL.It extends workflow verification to general harnesses and combines outcome, workflow-stage, and toolcall rewards with workflow-stage-normalized GRPO.Source: §5 · p. 9
  • Across three benchmarks, LAR models outperform their base models by 9.89% and the second-best models known to the authors by 5.07% on average.The paper reports that LAR-9B/27B achieve the best results among comparable-size models.Source: §5 · p. 9
  • The framework lays a foundation for integrating verifiable symbolic signals into LLM training and points toward a new paradigm for agentic RL.Source: §5 · p. 10

A LIMITATIONS

The paper identifies limits in what Lean4AgenticRL verifies and in the tasks it addresses, then defines its formal vocabulary and summarizes its training procedure.

A LIMITATIONS

  • Verifiability bounds agent behavior externally rather than opening the LLM’s internal computation; the work also omits runtime verification integration and visual signals.The experiments focus on traditional agentic tasks such as SWE and general terminal usage.Source: A LIMITATIONS · p. 16

B TERM DEFINITIONS

  • Lean 4 is the shared formal foundation; workflows are directed graphs of stages, and agent steps are reasoning-action cycles where γ rewards are assigned.Semantic predicates describe atomic properties of execution state and trajectory evidence, checked by Lean, Python, or an evidence-grounded LLM judge.Source: B TERM DEFINITIONS · p. 16

C WRAP UP OF LEAN4AGENTICRL

D.1 APPLYING LEAN4AGENTICRL TRAINING TO ADDITIONAL MODELS

Lean4AgenticRL training was applied to additional model families and sizes. The reported gains across SWE and terminal-use benchmarks support consistency across those variants.

D.1 APPLYING LEAN4AGENTICRL TRAINING TO ADDITIONAL MODELS

  • The additional training runs used Qwen-3.6-27B for 80 steps and DeepSeek-V4-Flash-0731-304B for 40 steps, following the same TMax recipes.The runs used the TMax dataset.Source: §D.1 · p. 17
  • 4.0% on SWE-Bench-Verified and 8.0% on TerminalBench-2.0: Qwen-3.6-27B improves from 70.0% to 74.0% and 45.6% to 53.6%, respectively.The authors report these as improvements over the base model.Source: §D.1 · p. 17
  • 5.6%: DeepSeek-V4-Flash-0731-304B improves from 67.3% to 72.9% on TerminalBench-2.1 after training.The base and trained scores are 67.3% and 72.9%, respectively.Source: §D.1 · p. 17

D.2 FAITHFULNESS OF WORKFLOW ANNOTATION

The authors evaluate workflow-annotation faithfulness at three levels, compare Lean’s dependent-type language with other formal languages, and delimit which parts of their system receive formal verification.

D.2 FAITHFULNESS OF WORKFLOW ANNOTATION

  • The evaluation covered 32,295 predicate annotations, 20,235 segmented steps across 5,912 workflow stages, and 5,912 β reward assignments.The author team first manually evaluated 10 workflows to develop the judgment criteria, then used Claude-code with Fable-5.1 to annotate 1,200 trajectories.Source: §D.2 · p. 18
  • Below 10% was the overall annotation failure rate; errors mainly involved ambiguous natural-language predicates, stage boundaries, or judges receiving incomplete context.For trajectory verification, a 16,384-token context chunk could overflow; the authors report no significant effect on training stability or performance at this error rate.Source: §D.2 · p. 18
  • In a 180-annotation sample, only one predicate annotation was judged erroneous, and the authors subsequently verified that annotation as correct.The sampled annotations included 60 examples per annotation type.Source: §D.2 · p. 18

E COMPARISON BETWEEN DEPENDENT-TYPE WITH OTHER FORMAL LANGUAGES

  • Lean’s dependent types support nested data, induction over loops, and predicates over concrete stage inputs and outputs, which the authors cite as reasons for using Lean as a uniform verification backbone.The comparison contrasts these capabilities with limits in LTL and SMT; temporal formulas and SMT-decidable fragments can also be embedded in Lean.Source: E COMPARISON BETWEEN DEPENDENT-TYPE… · pp. 18–19

F DISCUSSION OF FORMAL BOUNDARY FOR LEAN4AGENTICRL

  • Formal guarantees begin after workflow formalization, trajectory segmentation, and LLM-judge predicate annotation; those three steps themselves are not formally guaranteed.The authors identify LLM-judge annotation errors as the major source of informality, while describing the boundary as balancing expressiveness and formal guarantees.Source: F DISCUSSION OF FORMAL BOUNDARY FOR… · p. 19

G BENCHMARK AND TASK DETAILS

This section specifies the evaluation tasks and explains how problem-specific workflows are formalized and execution trajectories segmented into workflow stages.

G BENCHMARK AND TASK DETAILS

  • SWE-Bench-Verified has 500 human-verified issues from 12 Python repositories, while TerminalBench-2.0/2.1 has 89 tasks across software engineering, system administration, security, scientific computing, and other domains.Evaluation uses mean@3 for SWE-Bench-Verified and mean@5 for both TerminalBench versions, with randomized seeds; the sets were checked for training-data overlap.Source: G BENCHMARK AND TASK DETAILS · p. 19

H.1 PROBLEM SPECIFIC WORKFLOW FORMALIZATION

  • PSWF formalization turns a workflow into a graph of stages and transitions, then assigns stage preconditions and postconditions using predicates for workflow variables, information flow, and goals.The Lean4Agent-verifiable form enables internal-consistency checks and provides a basis for later rewards.Source: §H.1 · p. 20

H.2 WORKFLOW STAGE SEGMENTATION

  • Workflow segmentation uses the PSWF, its formalized workflow, and the execution trajectory to assign agent steps—which include reasoning, tool calls, and results—to stages.The steps do not directly identify their corresponding workflow stage.Source: §H.2 · p. 20

I.1 β REWARD ANNOTATION

The β reward checks whether a workflow stage establishes its required postconditions, while γ applies negative-only penalties to selected unproductive tool-call patterns.

I.1 β REWARD ANNOTATION

  • The β reward indicates whether the stage’s agent executions establish required postconditions; some predicates are verified with Lean or Python, while others require LLM-as-judge verification.LLM judgments must be supported by observed evidence.Source: §I.1 · p. 20
  • The γ rules penalize repeated commands, no-ops, constant-only output, pure-print scripts, non-final actionless steps, and reruns without environment changes.Fast Lean and Python checks assign penalties only, intended to avoid reward hacking through inflated step counts in the reported experiment settings.Source: §I.2 · p. 20
  • The appendix includes general schemas for SWE-Bench workflow formalization and segmentation prompts, plus an abridged skeleton for stage-level β annotation.The detailed prompts and examples are abridged due to space constraints.Source: Figure 3 · p. 21, Figure 4 · p. 22, Figure 5 · p. 22

J.1 OVERALL ANALYSIS OF THE CASE

In the regex-chess case study, β accuracy rises during training and the final checkpoint solves a task the earlier checkpoints could not finish. The checkpoint trajectories show how β credits established workflow stages before full task success.

J.1 OVERALL ANALYSIS OF THE CASE

  • As training progresses, β accuracy increases and the model ultimately resolves regex-chess, although it cannot finish the problem at earlier stages.The authors interpret this trend as evidence that the reward design can prompt progress on problems the model initially cannot solve.Source: §J.1 · p. 23, Table 4 · p. 23

J.2 DETAILED CASE

  • At step 120, all four tests pass and every stage earns β = +1, after step 80 reaches 2/4 tests with β = +1 on five of six stages.At step 80, both remaining failures involve castling out of check, which the castling guard misses because the workflow item requires only an empty path and present rights.Source: §J.2 · p. 23, Figure 8 · p. 26, Figure 9 · p. 27
  • The base checkpoint earns β = +1 for its FEN codec and valid re.json, but a malformed lookahead leaves later stages at β = −1; step 40 earns +1 on four of seven stages.At step 40, the king-safety filter has knight and pawn offsets off by one, and the rule tail rejects the castling field.Source: §J.2 · p. 23, Figure 6 · p. 24, Figure 7 · p. 25
  • Across the first three checkpoints, α remains −1 while β gives increasingly fine-grained credit for the stages each attempt establishes.The case study uses post-hoc evaluations of checkpoints at steps 0, 40, 80, and 120, not to select the best checkpoint.Source: §J.2 · p. 23, §J.1 · p. 23

Related papers

Loading 2610.22448v1…