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.