📖 AI 总结

该论文针对当前大语言模型在复杂软件工程与终端任务中智能体强化学习训练效果受限的问题，指出现有方法多依赖高层结果奖励，而忽视底层工具调用与中层工作流阶段的奖励信号。为此，作者提出Lean4AgenticRL框架，首次将多层级过程奖励统一建立在Lean4形式化模式之上，通过构建问题特定的工作流系统、工作流形式化与多级奖励标注方法，在通用执行框架内实现智能体行为验证，并结合工作流阶段归一化的GRPO算法进行训练。基于该框架训练的LAR-9B/27B模型在实验中优于同规模领先模型，其中LAR-27B在TerminalBench-2.1上达到77.3%，平均较基座模型提升9.89%，较已知同规模次优模型高出5.07%。结果表明，将形式化方法引入开放式智能体强化学习具有显著潜力。

🔑 关键词速览