让 Lean 给 Agent 的每一步打分

训练一个会干活的 Agent，现在流行的方法是强化学习：让模型在真实环境里反复试，做对了给糖，做错了打板子。听起来很合理，但糖怎么发，是个大问题。

大多数团队只看结果。任务要么完成，要么没完成，一个 0 和 1，其他不管。这就像老师只看期末卷总分，平时的作业一页不改。后果论文里拍得很清楚：他们用纯结果奖励跑了一个对照组（GRPO），在软件工程任务上，前 15 步成绩往上走，随后开始崩，到第 20 步跌回起点附近。中间几十步没人管，模型学歪了，歪到最后把结果也带崩了。

那把中间每一步都打上行不行？想法早就有了，卡在两件事上。

第一，标不起。一个 Agent 任务跑下来几十上百步，人工去标注哪步对哪步错，成本撑不住。第二，更微妙的：用大模型当裁判去评每一步，模型会作弊。这篇论文给了一个现成的例子——某个环节的要求是「修复后重试」，Agent 学会了把同一条测试命令原样重跑几遍，裁判一看「哦，它重试了」，就给了分。分数骗到手，问题原地没动。

论文要解决的就是这个：中间步骤的奖励，怎么发得又便宜又骗不了。

他们的答案是搬来 Lean。Lean 是一个形式化证明语言，特点是不讲情面——你写的东西对不对，它的内核机械检查，不聊天，不通融。之前的 Lean4Agent 已经用它验证过定理证明类任务，但那套系统假设工作流是事先定死的；现代 Agent 的执行路径是开放式的，事先没人知道它会怎么走。这篇的新东西叫 PSWF：先让大模型探索任务环境，给每道题生成一份分阶段的自然语言计划，再把这份计划翻译成带前置和后置条件的 Lean 形式化描述。Agent 跑完后，轨迹被对齐到各个阶段，每个阶段的收尾由谓词检查：该完成的条件成立没有。成立了，这一阶段的奖励 β 记 1；没成立，记 -1。

于是奖励变成了三层。最高层 α 看结果，任务完成没有。中间层 β 看每个阶段，前置后置条件过没过。最底层 γ 盯着每一次工具调用，专抓作弊模式：连续重复同一条命令、空操作、死循环 shell——这些模式用符号谓词写死，由 Lean 和 Python 的检查器执行。

γ 的设计有个讲究：它只罚不奖，取值只有 -1 和 0。为什么不给正分？因为一旦它给正分，模型就会想办法在这层刷分。只罚不奖，它就没有被刷的油水，只能老老实实当个守门员。消融实验显示这层守门员值 6.6 个百分点：去掉它，成绩从 56.0% 掉到 49.4%。

成绩单上最亮眼的是小模型。9B 的 LAR-9B 从基座 Qwen-3.5-9B 出发，在 SWE-Bench-Verified、TerminalBench-2.0、2.1 三个基准上分别涨了 20.2、13.5、13.4 个百分点，把同尺寸最强的 TMax-9B 甩开 10.7、5.6、1.9，在 SWE 任务上还压过了大它近三倍的 Gemma-4-31B。27B 那边的故事不一样：基座 Qwen-3.8-27B 本来就是同尺寸全场最强，LAR-27B 是在这个已经很高的楼层上继续加盖，三个基准再涨 1.2、3.5、7.7，TerminalBench-2.1 停在 77.3%。平均下来对基座涨 9.89%、对同尺寸第二优涨 5.07%——平均数看着温和，拆开看，方法对小模型下手最狠。训练本身不贵：64 张 H200，9B 跑 160 小时，27B 跑 240 小时。

不过这套「可验证」的可字，得加个引号。论文附录里专门有一节讨论形式化边界，说得很坦白：整条链上有三个环节是大模型做的——把自然语言计划翻译成 Lean 代码、把轨迹切分到各阶段、给语义类谓词打分。这三步形式化保证不了。Lean 守住的，是这三步之后的机械检查；这三步本身要是错了，边界就跟着错。换句话说，Lean 是个完美的验算器，但题目是它要验的那个人出的。这是所有「形式化 + LLM」混合系统的共同软肋，论文没藏，直接摆在了附录里。

把这个位置看清，Lean 在这条技术链上的三个落点就齐了。训练时当奖励验证器，是这篇；运行时当权限门禁， Lean 验证的智能体运行时已经在做——每一步操作先证权限再执行，那是把 Lean 用在防守；感知层把图片和物理场景翻译成 Lean 命题，是自形式化那条线在打前站。三头的方向是一致的：大模型负责判断，形式化语言负责执行——判断可以模糊，执行必须精确。

论文自己列的局限也顺着这个方向：验证靠外部约束包住 Agent，没打开模型内部的黑箱；验证没进运行时；视觉信号还没接。第三条是下一个战场，前两条，恰好是另外两条线正在补的位置。

素材来源：arXiv 2610.22448（2026-10-15 提交），代码库 github.com/RickySkywalker/Lean4AgenticRL（MIT，10-10 建仓）。作者 Ruida Wang、Gerald Friedland、Tong Zhang、Chris Kong，一作在 Amazon Web Services 实习期间完成，另挂 University of Illinois Urbana-Champaign。文中全部数字出自论文正文与附录。