This is the official repository for Lean4AgenticRL: Advancing Agentic RL with Verifiable Multi-level Process Rewards. We achieved 77.3% on TerminalBench-2.1 using only 27B model, achieving state-of-the-art of the model in similar size.
Teaser Video
Lean4AgenticRL-video.mp4
| Model | Size | SWE-Bench-Verified | TB-2.0 | TB-2.1 |
|---|---|---|---|---|
| OpenThinker-Agent-V1 | 8B | 15.7% | 1.9% | - |
| Qwen-3.5-9B | 9B | 44.0% | 19.3% | 16.1% |
| TMax-9B | 9B | 53.5% | 27.2% | 27.6% |
| Gemma-4-12B | 12B | 23.2% | 15.3% | 27.0% |
| Qwen-3.6-27B | 27B | 70.0% | 45.6% | 40.5% |
| TMax-27B | 27B | 70.0% | 49.9% | 44.9% |
| Qwen-3-Coder-30B | 30B | 49.2% | 24.5% | - |
| Gemma-4-31B | 31B | 61.0% | 33.9% | 43.0% |
| Qwen-3.8-27B | 27B | 83.0% | 64.7% | 69.6% |
| Our models | ||||
| LAR-9B | 9B | 64.2% | 32.8% | 29.5% |
| LAR-27B | 27B | 84.2% | 68.2% | 77.3% |
Bold and underlined scores indicate the best and second-best results, respectively, among the compared models of similar size.
Evaluation: SWE-Bench-Verified uses mean@3 with Claude-code; TerminalBench-2.0 and 2.1 use mean@5 with Terminus-2.
We introduce Lean4AgenticRL, which, to the best of our knowledge, is the first framework that grounds multi-level process rewards in a unified Lean4 formalization schema for open-ended agentic RL. Lean4AgenticRL first builds a problem-specific workflow system that balances the agent's own capability with controllability during execution, laying the foundation for further verification. Subsequently, our workflow formalization and multi-level reward annotation methods enable the verification of agent behavior within a general harness system. The framework 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 capabilities. LAR-27B achieves 77.3% on TerminalBench-2.1, representing state-of-the-art performance among models of similar size. On average, our models outperform the base model by 9.89% and surpass the second-best model of comparable size that we are aware of by 5.07%. These results indicate the potential of integrating formal methods to enhance open-ended agentic RL.
This release contains the PSWF Terminus-2 harness and the TerminalBench-2.1 evaluation kit. Lean4 formalization, reward annotation, RL training, and the other benchmark evaluation pipelines described in the paper are not included in this checkout.
This section shows how to evaluate LAR-27B on TerminalBench-2.1 using Terminus-2 with PSWF.
Requirements: a Linux machine with 8 H200 GPUs, Python 3.12 with venv, Git, Docker with Compose v2 (and permission to run Docker), sudo, nftables (nft), setsid, and an NVIDIA driver and CUDA toolkit supporting CUDA 13. The default 40 concurrent task containers each have limits of 4 CPUs and 40 GiB RAM; choose concurrency appropriate for the host.
Keep model files and the evaluation work directory on a fast local disk outside this source checkout. MODEL must be a local checkpoint directory containing the model weights, config.json, tokenizer.json, and chat_template.jinja.
# Run from the repository root; replace these with absolute local paths.
export MODEL=/path/to/local/disk/LAR-27B
export WORK=/path/to/local/disk/tb21
python3.12 -m venv ~/.venvs/lar-serve
~/.venvs/lar-serve/bin/pip install -r PSWF/EvaluationKit/TB-2.1/requirements/serve.txt ./PSWF/EvaluationKit/TB-2.1
python3.12 -m venv ~/.venvs/lar-eval
~/.venvs/lar-eval/bin/pip install -r PSWF/EvaluationKit/TB-2.1/requirements/eval.txt ./PSWF/Harness/Terminus-2 ./PSWF/EvaluationKit/TB-2.1
# Download the checkpoint before applying the tokenizer patch.
~/.venvs/lar-eval/bin/hf download amazon/LAR-27B --local-dir "$MODEL"
~/.venvs/lar-eval/bin/python -m pswf_harbor_patches --tokenizer-dir "$MODEL"# Initialize the TB-2.1 containers
~/.venvs/lar-eval/bin/python -m tb21_eval.prepare --work-dir "$WORK"
sudo ~/.venvs/lar-eval/bin/python -m tb21_eval.netguard up --work-dir "$WORK"
~/.venvs/lar-eval/bin/python -m tb21_eval.netguard probe --work-dir "$WORK"# Run the evaluation
~/.venvs/lar-serve/bin/python -m tb21_eval.serve up --model "$MODEL" --work-dir "$WORK"
~/.venvs/lar-eval/bin/python -m tb21_eval.make_job --model "$MODEL" --work-dir "$WORK" --run-dir "$WORK/runs/x5" --n-attempts 5 --n-concurrent 40
setsid nohup ~/.venvs/lar-eval/bin/harbor run -c "$WORK/runs/x5/job.json" --env-file "$WORK/runs/x5/harbor.env" > "$WORK/runs/x5/harbor.log" 2>&1 &
# ~16 h in the background; score at any time.
# If interrupted: ~/.venvs/lar-eval/bin/python -m tb21_eval.resume --run-dir "$WORK/runs/x5"
~/.venvs/lar-eval/bin/python -m tb21_eval.score "$WORK/runs/x5"The kit runs 89 tasks with a 20,000-second agent budget per attempt. Its default kit scoring policy uses the first round containing at least five attempts and no trial classified as an infrastructure failure for a task, selecting the first five trials by name. A verifier timeout without a recorded reward after pytest starts counts as zero. Other missing or invalid verification evidence, infrastructure failures, and model-guard refusals make that round ineligible; tasks without an eligible round remain pending, and recovery reruns all five attempts. Pending slots count as zero in the displayed mean. The report also shows Harbor's stock reward policy. See the scorer for the classification rules and the harness README for standalone use and tests.
The code is released under the MIT License. Model weights use the separate Apache 2.0 license indicated on the model page.
If you find our work useful, please cite it using the BibTeX entry below. This entry currently links to the PDF hosted on GitHub and will be updated once the arXiv version is available.
@misc{wang2026lean4agenticrl,
title={Lean4AgenticRL: Advancing Agentic RL with Verifiable Multi-level Process Rewards},
author={Ruida Wang and Gerald Friedland and Tong Zhang and Chris Kong},
year={2026},
eprint={2610.22448},
archivePrefix={arXiv},
primaryClass={cs.LG},
url={https://arxiv.org/abs/2610.22448},
}