Lean4AgenticRL：用 Lean4 形式化多层过程奖励，提升智能体强化学习

导语

让大语言模型真正承担软件工程和终端操作任务，难点并不只在于给出最终答案。智能体需要理解任务、选择工具、处理反馈，并在多个阶段持续修正行动。现有智能体强化学习通常以最终结果作为主要奖励，对工具调用是否合理、工作流是否按预期推进等中间行为关注不足，训练信号因此较为稀疏。

arXiv 论文提出的 Lean4AgenticRL，尝试用 Lean4 形式化方法补上这一环节。论文资料显示，该框架训练了 LAR-9B 和 LAR-27B 两个规模的模型，目标是提升模型处理软件工程及一般终端任务的能力。

核心要点

• 把过程奖励拆成多个层级。 框架不只评估任务是否完成，还关注低层工具调用与中层工作流阶段，从而为智能体提供更细致的反馈。
• 先建立问题专属工作流。 Lean4AgenticRL 会围绕具体问题构建工作流，在模型自主决策能力与执行过程可控性之间取得平衡，为后续验证提供结构化基础。
• 引入统一的形式化验证方案。 论文将工作流形式化，并通过通用 harness 系统对智能体行为进行验证和奖励标注，使不同阶段的行为能够被纳入同一套框架。
• 配合阶段归一化 GRPO。 多层奖励被用于 workflow-stage-normalized GRPO，以减少不同工作流阶段之间奖励尺度差异可能带来的训练影响。
• 报告了终端任务上的结果。 LAR-27B 在 TerminalBench-2.1 上达到 77.3%。论文还称，LAR-9B/27B 相比基础模型平均提升 9.89%，并比作者所知的同规模第二优模型高 5.07%。

意义与局限

这项工作的价值，在于把“智能体做得对不对”进一步拆解为“每一步是否合理、每个阶段是否完成、最终结果是否达成”。对于软件工程和终端使用这类长流程任务，细粒度反馈理论上能够帮助模型更早发现偏离，并减少只在任务结束后才获得奖励的问题。

Lean4 的引入也提供了一个较清晰的研究方向：形式化方法不再只用于验证程序或数学证明，也可以参与开放式智能体行为的监督。不过，现有材料主要给出了框架设计和总体实验结果，尚不足以判断该方法在更多任务类型、不同工作流设计或更大模型上的稳定性。工作流如何构建、验证成本如何控制，以及多层奖励是否会限制模型的自主探索，仍是后续值得观察的问题。

总体来看，Lean4AgenticRL 将形式化验证、过程奖励和智能体强化学习连接起来，为解决长链条工具使用中的奖励稀疏问题提供了一个值得关注的方案。

来源：arXiv