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

📄 arXiv: 2610.22448v1 📥 PDF

作者: Ruida Wang, Gerald Friedland, Tong Zhang, Chris Kong

分类: cs.LG

发布日期: 2026-10-15

💡 一句话要点

提出Lean4AgenticRL以解决多层次过程奖励不足的问题

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 智能强化学习 多层次奖励 Lean4形式化 软件工程 模型训练

📋 核心要点

  1. 现有的智能强化学习方法主要依赖高层次的结果奖励，忽视低层次和中层次的奖励，导致训练效果不佳。
  2. 本文提出Lean4AgenticRL框架，通过多层次过程奖励和Lean4形式化，增强代理的智能能力和可控性。
  3. 实验结果显示，Lean4AgenticRL训练的LAR-27B模型在TerminalBench-2.1上达到了77.3%的准确率，超越了同类模型。

📝 摘要（中文）

提升大型语言模型（LLMs）在复杂软件工程和终端使用问题上的智能能力是一个紧迫的挑战。目前的最先进LLMs主要依赖高层次的结果奖励，忽视了低层次工具调用和中层次工作流阶段奖励，导致训练效果不佳。为此，本文提出了Lean4AgenticRL，这是首个将多层次过程奖励与统一的Lean4形式化框架结合的开放式智能强化学习（RL）框架。Lean4AgenticRL通过构建问题特定的工作流系统，平衡代理在执行过程中的能力和可控性，为进一步的验证奠定基础。我们的工作流形式化和多层次奖励注释方法使得代理行为的验证成为可能，并通过工作流阶段归一化的GRPO算法提供更有效的智能RL支持。实验表明，使用Lean4AgenticRL训练的模型在性能上优于同类模型。

🔬 方法详解

问题定义：本文旨在解决当前智能强化学习方法中对多层次过程奖励的忽视，导致训练效果不理想的问题。现有方法主要依赖高层次的结果奖励，缺乏对低层次工具调用和中层次工作流阶段的关注。

核心思路：Lean4AgenticRL框架的核心思想是将多层次过程奖励与Lean4形式化相结合，以增强代理的智能能力和可控性。通过建立问题特定的工作流系统，代理能够在执行过程中更好地平衡自身能力与可控性。

技术框架：Lean4AgenticRL的整体架构包括三个主要模块：问题特定的工作流系统、工作流形式化和多层次奖励注释方法。首先，构建工作流系统以支持代理的能力和可控性；其次，进行工作流形式化以便于代理行为的验证；最后，提供多层次奖励以支持更有效的智能强化学习。

关键创新：Lean4AgenticRL的最大创新在于首次将多层次过程奖励与Lean4形式化结合，形成一个统一的框架。这一设计使得代理在执行过程中能够获得更全面的反馈，从而提升学习效果。

关键设计：在技术细节上，Lean4AgenticRL采用了工作流阶段归一化的GRPO算法，并在奖励设计中引入了多层次的奖励机制，以确保代理在不同阶段都能获得适当的反馈。

🖼️ 关键图片

fig_0
img_1
img_2

📊 实验亮点

实验结果表明，使用Lean4AgenticRL训练的LAR-27B模型在TerminalBench-2.1上达到了77.3%的准确率，平均超越基线模型9.89%，并且比第二名的同类模型高出5.07%。这些结果展示了将形式化方法与开放式智能强化学习结合的潜力。

🎯 应用场景

Lean4AgenticRL框架在软件工程和终端使用等复杂任务中具有广泛的应用潜力。通过增强代理的智能能力和可控性，该框架可以帮助开发更高效的自动化工具和智能系统，推动人工智能在实际应用中的发展与落地。

📄 摘要（原文）

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.