Lean4AgenticRL: Advancing Agentic RL with Verifiable Multi-level Process Rewards
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. **Lean4Agenti...
| Authors | Ruida Wang, Gerald Friedland, Tong Zhang et al. |
|---|---|
| Primary category | cs.LG |
| Published | 15 October 2026 |
| Last updated at source | 15 October 2026 |
Popularity, last 6 days
0 now. Counts as reported by the source, snapshotted daily by Silytics.
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 24 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.