你让 AI 修一个软件故障。它查文件、跑命令、改代码，忙了几十步，最后测试失败。训练系统通常只会告诉它：这次得零分。可究竟是找错了文件、误判了原因，还是修改正确但测试方法不对？它不知道。
Lean4AgenticRL 想解决的就是这笔“糊涂账”。它把一次长任务拆成若干工作阶段，再分别检查最终结果、阶段目标和每次工具调用。部分检查用 Lean 4——一种能让计算机严格核验程序性质与证明的形式化系统——来表达和执行。这样，智能体即使尚未完成整道题，也可能知道自己走到了哪一步、哪里开始偏航。
这项工作的全部效果数据均来自 Ruida Wang、Gerald Friedland、Tong Zhang 和 Chris Kong 的论文及其实验，尚无独立复现。它值得关注的重点，不是“AI 的全部行为已经得到数学证明”，而是研究者开始尝试把形式化检查变成强化学习中的过程反馈。
只看终点，教不会长任务
强化学习（Reinforcement Learning，RL）让模型通过奖励调整行为：高分做法以后更常出现，低分做法则逐渐减少。这里训练的不是只回答一句话的模型，而是会读取文件、调用工具、执行终端命令并连续解决问题的智能体。
这类任务的麻烦在于“奖励稀疏”。一次软件修复可能包含几十甚至上百步，系统却只在结尾给出成功或失败。结果奖励像整场考试只给一个总分，无法告诉学生是哪道题、哪一步出了问题。更糟的是，一条最终成功的轨迹里也可能夹着大量无效操作；如果把同一份功劳平均记到每一步头上，模型可能连绕路和碰巧奏效的动作一起学走。
过程奖励试图检查中间步骤。已有做法常盯着单次工具调用，但一个命令是否有用，往往取决于它服务于哪个阶段。读取配置文件本身既不对也不错：排查配置问题时很关键，已经定位故障后反复读取则可能只是在浪费上下文。
先让智能体画路线，再分段检查
Lean4AgenticRL 的第一步是建立“问题特定工作流”（Problem-Specific Workflow，PSWF）。智能体先探索任务环境，再写出分阶段计划。处理软件问题时，计划可包含相关源文件、疑似故障原因、修复办法和验证步骤。执行阶段会保留此前的探索轨迹，减少重复摸索。
这不是把智能体锁进固定脚本。论文采用“先计划、后执行”的折中：计划提供路标，智能体仍能根据现场情况调整行动。作者在未进行训练的对照实验中发现，仅加入 PSWF，就把 Qwen-3.5-9B 在 SWE-Bench-Verified——检验模型能否解决真实软件问题的基准——上的解决率从 42.4%提高到 44.0%。作者检查失败轨迹后认为，没有这份计划时，模型更容易探索不足、找错文件或误判根因。
接下来，系统把自然语言计划转成形式化工作流，并将执行轨迹中的每一步归入相应阶段。一步可以留在当前阶段，也可以转向工作流允许连接的下一阶段；遇到循环或分支时，同一阶段的每次重访会单独编号。分段只依赖局部窗口，而非重新阅读完整轨迹，因此作者称它也能处理很长的执行记录。
三层奖励，各管一件事
系统随后给出三层反馈。
高层是结果奖励：任务最后有没有完成。中层是工作流阶段奖励：某一阶段是否从规定的前置状态出发，并实现预期的后置条件。能直接判定的条件由 Lean 或 Python 检查；需要理解语义的条件则交给 LLM judge，也就是让另一个大模型充当评审。因此，“可验证”并不意味着所有判断都由 Lean 完成。
低层是工具调用奖励，主要负责抓作弊式行为。论文举例说，如果中层规则希望看到“修复后重试”，模型可能反复运行同一条测试命令，表面满足要求，却没有真正推进任务。系统因此设置符号化规则，检查连续重复、无效命令和固定 shell 操作等模式。这一层只扣分、不加分，避免模型靠大量容易获得的低层正分盖过真正的任务目标。
消融实验显示，去掉这道低层防线后，30 步软件工程训练的成绩由 56.0%降到 49.4%；被检测到的重复命令比基础模型多 66.8%，工具调用总数也比完整方案多 18.7%。作者观察到的典型行为包括 echo、重复只读命令和占位命令。它们会填满上下文，却很少帮助解决问题。
同阶段的动作，才放在一起比较
有了三层奖励，作者还修改了 GRPO——一种让模型在一组尝试中比较相对得分、再更新策略的强化学习算法。标准 GRPO 往往把整条轨迹的功过分给所有步骤；直接比较工具调用，又可能把用途完全不同的动作摆在一起。
Lean4AgenticRL 使用 workflow-stage-normalized GRPO，也就是“按工作流阶段归一化的 GRPO”。它先把不同尝试中属于同一阶段的步骤对齐，再计算相对优势。直观地说，诊断动作与诊断动作比，修复动作与修复动作比，而不是拿一次读文件去和另一次运行测试硬比。
为减少过程奖励被钻空子，论文还限制其权重最高为 0.5，并只把它用于结果奖励难以提供稳定梯度的尝试组。规划阶段的训练则仍只使用最终结果奖励。
一个案例展示了这种细粒度信号的意义。在 TerminalBench-2.1 的 regex-chess 任务上，基础模型及 LAR-27B 的第 40、80 步检查点都没有完成任务，二元结果奖励无法区分三者；但完成的工作流阶段比例依次从 2/8 升到 4/7、5/6。到第 120 步时，模型解决了任务，阶段记录为 5/5。也就是说，终点分数连续给出三个零时，中间反馈已经看见模型在接近答案。
成绩亮眼，但先看清比较方式
作者以 Qwen-3.5-9B 和 Qwen-3.8-27B 为基础，训练出 LAR-9B 与 LAR-27B。训练数据混合 TMax-15k 和 SWE-ReBench；两种模型分别训练 160 步和 120 步，使用 64 张 H200 GPU，耗时分别为 160 小时和 240 小时。评测覆盖 SWE-Bench-Verified、TerminalBench-2.0 和 TerminalBench-2.1；前者报告三次随机种子的均值，后两者报告五次均值。
LAR-9B 在三个基准上分别得到 64.2%、32.8%和 29.5%。对应的基础模型 Qwen-3.5-9B 为 44.0%、19.3%和 16.1%。同规模对手中，TMax-9B 分别为 53.5%、27.2%和 27.6%。
LAR-27B 的三个成绩是 84.2%、68.2%和 77.3%；基础模型 Qwen-3.8-27B 为 83.0%、64.7%和 69.6%。其中最明显的提升出现在 TerminalBench-2.1，增加 7.7 个百分点。论文汇总称，两种 LAR 模型在三个基准上平均比各自基础模型高 9.89 个百分点，比作者选取的同规模次优模型高 5.07 个百分点。
与只用结果奖励的普通 GRPO 相比，Lean4AgenticRL 在两类任务的训练过程中都保持领先。软件工程实验里，普通 GRPO 前 15 步有所改善，约到第 20 步又跌回接近起点；新方法则在 30 步中持续上升，并在 10 步内超过普通 GRPO 的最佳检查点。终端任务中，它在 30 步内超过对照方法的最佳检查点。不过，作者关于训练更稳定、提升来自多层奖励的解释，仍主要由这些内部实验支持。
为什么这条路线值得看
它真正有意思的地方，是把“形式化方法”放到了训练回路里。Lean 4 在这里不只是任务结束后的审计工具，也参与生成奖励信号。最终成败、阶段进度和工具调用纪律被放进同一套奖励服务，形式化检查由此开始影响模型下一次会怎么行动。
这也补上了长任务学习中的一个缺口：只看结果太粗，只看单个命令又太碎。工作流阶段提供了中间尺度。它既能表达“已经定位问题但尚未修好”，也能让不同执行轨迹在大致相同的工作环节上比较。
作者称，这是首个在统一 Lean 4 形式化模式下，为开放式智能体强化学习提供多层过程奖励的框架。不过，“据作者所知的首个”是论文自述，不能当作经过独立检索验证的首创结论。更稳妥的判断是：这项工作给出了一套完整方案，并在软件工程和终端任务上展示了可观的内部结果。
局限与未知
- 验证边界并不等于全程形式化证明。部分阶段条件仍依赖 LLM judge；Lean 与 Python 主要负责可直接判定的谓词和工具调用规则。因此，它验证的是被形式化出来的部分条件，不是证明模型的整条输出必然正确。
- 所有数字都来自同一篇论文，尚无独立复现。虽然正文给出了基准、对手、随机种子均值及训练配置，但仍需外部实验确认 77.3% 等成绩能否稳定重现，以及不同工具和运行环境会怎样影响结果。
- 过程奖励依赖先规划、形式化、分段和标注。论文展示了它在所选软件工程与终端任务中的效果，但这些额外环节迁移到其他开放式任务时需要多少规则设计、判断成本和人工维护，现有材料尚未回答。