Lean4AgenticRL：通过可验证的多层级过程奖励推进智能体强化学习

arXiv:2610.22448v1 公告类型：新 摘要：增强大语言模型（LLM）的智能体能力，使其能够应对复杂的软件工程（SWE）和一般终端使用问题，是一项亟待解决的挑战。当前最先进的LLM通常会经历大规模智能体强化学习（RL）。然而，它们主要依赖高层次的结果奖励，很少考虑低层次的工具调用奖励和中层次的工作流阶段奖励，导致训练效果不佳。为克服这一局限，我们提出了 **Lean4AgenticRL**。据我们所知，这是首个基于统一 Lean4 形式化方案，为开放式智能体强化学习中的多层级过程奖励提供依据的框架。**Lean4AgenticRL** 首先构建了一个*问题特定的工作流*系统，在执行过程中平衡智能体自身的能力与可控性，为进一步验证奠定基础。随后，我们的工作流形式化方法和多层级奖励标注方法，使得能够在通用执行框架系统中验证智能体行为。该框架通过工作流阶段归一化的 GRPO 算法提供多层级奖励，从而支持更有效的智能体强化学习。借助 **Lean4AgenticRL**，我们训练了 **LAR-9B/27B**，这是一系列具有增强智能体能力的模型。大量实验表明，我们的模型优于同等规模的领先模型。**LAR-27B** 在 TerminalBench-2.1 上达到 **77.3%**。平均而言，我们的模型比基础模型高出 **9.89%**，并比我们所知的同等规模第二优模型高出 **5.07%**。这些结果表明，将形式化方法融入开放式智能体强化学习具有巨大潜力。