Lean4AgenticRL

Lean4AgenticRL trains 9B and 27B agent models with Lean4-verified process rewards, and the authors report 77.3% on TerminalBench-2.1

Posted on arXiv on Oct 19, 2026 (source: arxiv.org).

Ruida Wang, Gerald Friedland, Tong Zhang and Chris Kong propose Lean4AgenticRL, which formalizes an agent's problem-specific workflow in Lean4 so tool calls and workflow stages can be verified and rewarded during reinforcement learning, not just final outcomes, using a workflow-stage-normalized GRPO. They use it to train LAR-9B and LAR-27B. The paper reports that LAR-27B scores 77.3% on TerminalBench-2.1 and that the models beat their base models by 9.89% on average and the next-best model of comparable size the authors know of by 5.07%. The paper has not yet been peer-reviewed.