Lean4AgenticRL / TreeOPSD / FC-SWE 合读：Agentic RL 信用分配的结构化路线三连 精读

论文 1：Lean4AgenticRL: Advancing Agentic RL with Verifiable Multi-level Process Rewards（arXiv:2610.22448） 链接：https://arxiv.org/abs/2610.22448 ｜ 代码：https://github.com/RickySkywalker/Lean4AgenticRL ｜ 机构：AWS + UIUC ｜ 时间：2026-10-15

论文 2：Tree-Aware Posterior Distillation for Long-Horizon Agentic Reinforcement Learning（arXiv:2610.23181） 链接：https://arxiv.org/abs/2610.23181 ｜ 机构：清华 + 腾讯（基础模型部） ｜ 时间：2026-10-16

论文 3：FC-SWE: Failure-Conditioned RL for Long-Horizon Software Engineering Agents（arXiv:2610.07898） 链接：https://arxiv.org/abs/2610.07898 ｜ 机构：NVIDIA + 清华 ｜ 时间：2026-10-06

一、论文背景

1.1 共同的时代背景：Agentic RL 的"最后一公里"是信用分配

要理解这三篇论文为什么值得放在一起读，得先从一个所有做 Agent 强化学大的团队都撞过的墙说起。

什么是 Agentic RL？ 简单说，就是让 LLM 以"智能体"的方式工作——反复地思考、调用工具（读文件、跑命令、搜网页）、观察结果、再思考——然后用强化学习提升这套行为。训练信号通常来自 RLVR（Reinforcement Learning with Verifiable Rewards，可验证奖励的强化学习）：任务最后能不能通过测试、答案对不对，机器可以自动判定，不需要人类打分。DeepSeek-R1、GLM-5 等模型的训练都建立在这套范式上。

墙在哪里？ 在长时序（long-horizon）任务里，agent 可能要执行几十上百步才走到终点，而 RLVR 的奖励只在终点发一次。这带来一个经典难题——信用分配（credit assignment）：一条轨迹成功了，是第 3 步的定位文件做对了，还是第 47 步的修复策略做对了？失败的轨迹里难道就没有任何有价值的步骤吗？标准 GRPO 把轨迹级优势"广播"到每一个 token：成功轨迹里的冗余步骤跟着沾光，失败轨迹里的有效步骤跟着遭殃。轨迹越长，这个错配越严重，训练信号的信噪比越低。

用一个类比：这就像一个班级期末只交一次总成绩，老师无法知道每个学生（每个中间步骤）谁在认真学习。要提升全班水平，你需要的是"过程性评价"——但过程性评价谁说了算？怎么防止学生刷分？

1.2 三篇论文各自切入的具体痛点

论文 1（Lean4AgenticRL） 的出发点是：现有的过程奖励要么只看单个工具调用（视角太碎，一个工具调用常常和任务目标没有直接对应），要么靠 LLM judge 打分（会被策略"刷分"，即 reward hacking）。作者来自 AWS 与 UIUC，此前的 Lean4Agent 系列工作已经用 Lean 4 形式化语言给 agent 工作流建模，这篇则把形式化验证从"运行时检查"推进到"训练信号"。这是该团队路线的自然延伸。

论文 2（TreeOPSD） 抓住的是两个纠缠在一起的问题：其一，终端奖励在回合（turn）级别稀疏且高方差；其二，工程实践中一个 rollout batch 会被切成多个 mini-batch 顺序更新，第一个 mini-batch 更新完参数后，后面的 mini-batch 已经"off-policy"了——策略漂移（policy staleness）会持续放大。现有解法要么引入 value 网络（难训练）、要么过程奖励模型（要标注）、要么外部教师蒸馏（要更强模型），都增加了复杂度。清华自动化系与腾讯基础模型部的团队想找一个 critic-free、零标注、零外部教师的方案。

论文 3（FC-SWE） 看到的是一个被所有人浪费掉的信号源：GRPO 采样一组轨迹，失败的 patch 会收到 verifier 的诊断输出——失败的测试名、报错堆栈、traceback——然后这些信息就被扔掉了，下一条轨迹重新从零开始。可是对人类程序员来说，报错信息才是修改代码最值钱的输入。NVIDIA 与清华的团队问：能不能把"失败后看着诊断信息重试"这件事本身变成训练分布的一部分？

1.3 为什么合读：一个问题的三种结构化答案

三篇论文的公约数可以浓缩成一句话：终端稀疏奖励如何变成可验证的中间信号？ 但它们选择的结构完全不同：

• Lean4AgenticRL 走"定义"路线：用依赖类型形式语言预先定义"什么是好的中间状态"（工作流阶段的前后置条件），奖励来自对定义的机械检查；
• TreeOPSD 走"反事实"路线：不定义任何东西，用共享前缀的树结构做受控实验——同一前缀分出多条后继，后继的成败差异就是这个回合的因果贡献；
• FC-SWE 走"证据"路线：不细分中间步骤，而是把终局失败的诊断证据注入下一次尝试的上下文，让策略自己学会解读证据。

定义、反事实、证据——这三条路线恰好覆盖了信用分配问题解空间的三种基本取向，因此合读的价值远大于单读。

二、论文定位和关联工作

2.1 各自的定位坐标

Lean4AgenticRL 位于"形式化方法 × Agentic RL"的交叉点，这个交叉点此前几乎没人走过。相关工作分两支：(1) Agentic RL 过程奖励——AgentPRM、ToolRL、隐式步骤奖励等，大多绑定低层工具调用或依赖 LLM judge；(2) 可验证 agent 系统——LangChain 类型检查、VeriGuard 工具验证、Lean4Agent 工作流形式化，但它们只做运行时检查或事后审计，从不参与训练。本文是第一个把依赖类型形式化验证变成开放式 Agentic RL 训练奖励的框架，其直接前身 Lean4Agent 只支持固定工作流，本文把它推广到一般 harness。

TreeOPSD 的定位是"树结构策略优化"谱系中的优化算法创新。Tree-of-Thought、MCTS 类方法在推理期用树做规划；TreeRL、TreePO、ARPO 等在线方法把树带进 RL 做探索或局部分析。论文明确说自己的贡献"在于如何优化已获得的树，而不在于树在哪里分支"——树采样沿用的是 initialize-then-expand 方案（每条初始轨迹随机抽 N 个锚点分支新后缀）。与 GRPO/GSPO 的区别是粒度（回合 vs 轨迹/序列），与 TreePO 的区别是核心机制（有限目标残差匹配 vs 固定信用线性上升）。理论上它接的是 Policy Mirror Descent 与 KL 正则策略优化的脉络，把"求解 KL 正则邻近问题"与"向目标投影"显式解耦。

FC-SWE 处在"反馈利用与迭代精修"传统中。Self-Refine/Reflexion 用反馈但不更新权重；RISE/SCoRe 学多轮自我修正；RLEF 用公开测试反馈做多轮代码 RL——这是与 FC-SWE 最接近的前身。FC-SWE 的差异化在于三点：恢复按"每条失败轨迹"触发（而非任务级）、从原始仓库状态重启（携带的只有失败证据而非交互历史）、每条轨迹保留自己的 verifier 结果参与优化（而非只优化最后一条）。与 LaMer（把后续结果计入回报）、PivoARL（从错误状态重试）的对比也围绕这些设计选择展开。

2.2 三篇之间的隐含对话

有意思的是，三篇论文互相引用了对方的"问题"却给出不同答案。Lean4AgenticRL 的 related work 里批评的"分层信用分配依赖高度相似的轨迹或树搜索"正是 TreeOPSD 的方法论土壤；TreeOPSD 强调"不需要 LLM judge、不需要过程标注"暗指 Lean4AgenticRL 这类依赖标注的方法的工程成本；FC-SWE 则干脆不在步骤层面做任何切分，用一句"verifier 反馈含有宝贵诊断信息"绕开了整个切分难题。它们像三个盲人摸同一头象：摸到的是定义之腿、反事实之耳、证据之鼻。

在评测层面，FC-SWE 的 SWE-bench Verified 也是 Lean4AgenticRL 的主战场之一（41.7%@1 vs LAR 系列 64%+/84%+，但模型规模与 harness 不同，不可直接比）；TreeOPSD 的 Deep Research 设定则展示了这套方法在搜索型任务上的泛化性，与另两篇的 SWE/终端任务互补。

三、问题定义

3.1 论文 1：开放式任务的多级可验证奖励

给定问题陈述 S、环境 E（通常是一个容器）、通用工作流 W，目标是训练一个在开放环境（无固定工作流约束的 harness，如 Claude-code、Terminus-2）中执行的 LLM agent 策略。难点在于：如何为这种开放式执行定义"中间过程奖励"，使得它（a）与任务目标对齐而非只与工具调用对齐，（b）可机械验证而非依赖不可靠的打分，（c）不能被策略通过仪式性行为"刷"到。

形式化地说，本文需要一套奖励函数族 {α, β, γ}：α 是轨迹级 outcome 奖励（verifier 判定，±1）；β 是工作流阶段级奖励（每个阶段是否达成其声明的目标）；γ 是工具调用级奖励（纯惩罚型守卫）。核心问题是如何让 β"可验证"——这就要求先解决两个子问题：如何把自由格式的 agent 执行切分成有意义的工作流阶段（步骤-阶段对齐问题），以及如何在开放 harness 上跑形式化验证（Lean4Agent 只支持固定工作流的限制）。

3.2 论文 2：回合级信用的免标注获取与离策略稳定

在 ReAct 式多轮交互中，轨迹分布是 π(a_t|H_{t-1}) 与环境转移的乘积，只有策略生成的 token 参与梯度。给定稀疏终端奖励 R(H_T) ∈ [0,1]，问题有两个：

问题 A（信用稀疏）：如何在不引入 value 网络、过程标注、外部教师的前提下，把终端奖励变成回合级稠密信号？

问题 B（策略陈旧）：一个 rollout batch 内做 E 个序贯 mini-batch 更新时，第 e 个 mini-batch 面对的 π_θ 已偏离采样时的 π_θold。重要性采样比值在高维下方差爆炸，裁剪只限制步长却不定义"应该停在哪里"。如何构造一个优化目标，使得更新在到达某个有限目标时自动停止、过冲后自动反向？

3.3 论文 3：结局依赖的恢复链如何进 GRPO

把"失败触发的恢复"形式化为结局依赖恢复链（outcome-dependent recovery chain）：对每个 issue，初始轨迹总是被执行（q_{c,1}=1），恢复轨迹只在前一轨迹失败时存在（q_{c,r} = (1-y_{c,r-1})·q_{c,r-1}）。这带来两个必须显式回答的设计问题：

问题 A（奖励归属）：一条 [失败, 成功] 的链，训练奖励应该记 [0, 1]（轨迹局部）、[1, 1]（链广播）还是 [⊥, 1]（只训最后一条）？

问题 B（对比组构造）：GRPO 的优势是组内相对比较。恢复链下，同一 issue 的轨迹集合是结局依赖的——成功的链只有 1 条轨迹，失败的链有 2 条。哪些轨迹进入优势估计的比较组？未执行的占位槽如何处理？

注意这两个问题在标准 GRPO 里根本不存在——正是"把恢复纳入训练"这个决定 itself 制造了它们。这篇论文的方法部分基本就是对这两个问题的回答。

四、问题解法

4.1 论文 1：Lean4AgenticRL——形式化定义驱动三级奖励

框架分三步（对应论文 Figure 1 的 a/b/c）。

第一步：问题特定工作流（PSWF）agent 系统。 采用 plan-then-execute 范式：规划 agent 先探索环境，写一份针对当前问题的自然语言工作流 W_S（包含相关源文件、疑似根因、修复与验证步骤），执行 agent 再按 W_S 解题。这一步的目的是在"固定工作流的可控性"与"ReAct 自由执行的灵活性"之间取平衡——既给后续验证提供了结构，又不限制 agent 的探索空间。消融显示仅加 PSWF（不训练）就能把 Qwen-3.5-9B 的 SWE-Bench-Verified 从 42.4% 提到 44.0%。

第二步：工作流形式化与多级奖励标注。 这是方法核心：

1. 形式化：用一个更强的标注 LLM（DeepSeek-V4-Pro、Claude-Opus 等）把自然语言 W_S 翻译成 Lean4Agent 框架下的形式化工作流 F(S)W = {(v_i, ρ_pre, ρ_post)}——一张有向图，每个阶段节点带前置/后置条件谓词。类比 Hoare 三元组 {前置} 程序 {后置}：进入阶段时什么必须成立、离开时什么必须达成，都被写成可检查的谓词。

2. 阶段切分：另一个标注 LLM 逐个读取执行轨迹的每一步（局部窗口 τ_{i-1}, τ_i, τ_{i+1}），决定该步属于 STAY（仍在当前阶段）/ ADVANCE（进入下一阶段）/ LOOP_BACK（沿声明的环边回到某阶段）。因为每次判定只依赖局部窗口而非全轨迹，切分可扩展到超长轨迹。论文对标注忠实度做了系统评估：谓词标注失败率 8.03%、阶段切分 6.21%、轨迹验证 4.84%，且该错误率下训练稳定不受影响。

3. β 奖励（中游）：阶段 i 的后置条件成立则 β_i = +1，否则 −1。可直接判定的谓词用 Lean 或 Python 代码检查；需语义解释的谓词由"证据接地的 LLM judge"判定（判断必须引用观察到的证据，区分 agent 的声称与实际执行结果——比如"声称测试通过"不构成"测试运行过"的证据）。

4. γ 奇奖励（下游）：纯惩罚型符号守卫，针对六类 reward hacking 模式：连续重复同一命令（第 3 次起罚）、空操作命令链（exit/true/sleep）、常量输出（echo/cat 常量串）、纯打印脚本（语法树只含字面量 print 的代码）、中间无动作步（只推理不执行）、阶段内无进展重执行。由 Lean + Python 检查器自动评估。关键设计：γ ∈ {−1, 0}，只罚不奖——策略无法通过刷 γ 本身获利，它只能封堵刷 β 的路径。

第三步：workflow-stage-normalized GRPO。 融合公式（r^(0) = α + (0.2+0.3·I{α=1})·β；γ=−1 时取 min(−1, r^(0))）里有两个精心设计的门控：β 的系数上限 0.5，保证过程奖励永远不能压过 outcome；β 只作用于组通过率为 0% 或 ≥75% 的组——这些组的 outcome 梯度本来就弱（全失败组无正向信号、近全成功组无差异信号），过程奖励在这里补位而非添乱。训练流程（附录 C 的伪代码）：规划阶段 token 用纯 outcome 奖励 α；执行阶段用融合奖励跑 workflow-stage-normalized GRPO。整个奖励管线由单一 Lean4Agent 形式框架管理，挂在统一 reward server 上做异步扩展（基于 SLIME + OpenClaw-RL，batch 32 × group 32，上下文 128K、单响应 8K 封顶）。

一个容易忽略的细节是优势归一化公式（Eq. 6）里的双重均值结构：外层对组内 G 条轨迹取平均、内层对每条轨迹内部的 m 个阶段取平均，再对阶段内 n 步取平均。这意味着一个"阶段多但每阶段步数少"的轨迹与一个"阶段少但每阶段步数多"的轨迹，总梯度贡献被拉平——轨迹长度不再直接决定话语权。这在长轨迹动辄数百步的终端任务里是稳定训练的必要条件：否则最长的轨迹（往往是卡住打转的）会主导梯度。

4.2 论文 2：TreeOPSD——反事实树备份 + 闭合解有界教师

方法是一个漂亮的"两步解耦"（对应论文 Eq. 7）：

目标构造（每棵树做一次）：

1. initialize-then-expand 建树：行为策略 π_θold 先采 M 条完整轨迹，每条均匀抽 N 个非终端锚点，从每个锚点前缀分支出一条新后缀，合并共享前缀得 K = M(N+1) 条终端轨迹的树。关键工程考虑：分支后继的期望生成成本约为完整轨迹的一半，所以 (M, N)=(4, 2) 的树与 GRPO G=8 的采样预算期望匹配——公平对比的前提。

2. 树备份得回合信用：终端奖励标准化成 A_k 后，按行为策略似然权重递归备份：内部节点 i 的 V_i = Σ_c ω_{i,c}·V_c。直觉：固定前缀、只变后继，后继的成败差就是前缀末尾这个回合的"因果贡献"。每个唯一回合只在树中计一次（共享前缀不重复）。

3. 仿射映射成教师：q_i = 1/2 + V_i/τ。这是全文最优雅的一步——为什么这么简单的映射是对的？因为 (a) 由 Samuelson 不等式，标准化优势 |V_i| ≤ (K−1)/√K，凸备份保持该界，于是 τ = (K−1)/(ρ√K) 保证所有 q_i ∈ [1/2−ρ, 1/2+ρ]，无需任何裁剪即天然有界；(b) 定理 1 证明这个仿射映射与树备份可交换：父节点的教师恰是子教师的前向 KL 重心，所以"先备份再映射"与"先映射再备份"等价，共享前缀可无损压缩成单次评分；(c) 附录 B.1 证明它是唯一满足对称性与半径校准的凸组合交换映射。

分布匹配（每个 mini-batch 重算）：

学生回合后验定义为 p_θ,i = σ(s_θ,i)，其中 s_θ,i 是当前策略对行为策略的按回合长度归一化的对数似然比（几何均值比值取 log）。长度归一化消除了长回合与短回合的方差差；σ 映射把无界的比值变成有界的 Bernoulli 参数（在线策略点 r=1 时 p=1/2）。训练损失是 Forward-KL(Q★_i ‖ P_θ,i) 的 token 加权和。

两个定理给出全部保证：定理 2(i) 在行为策略处（s=0），蒸馏梯度精确退化为树策略梯度——第一步更新与经典方法完全一致；定理 2(ii) 漂移校正项 −τ(p_θ,i − 1/2) 是加性的、Lipschitz、一致有界的，没有乘性重要性比值 e^s 的指数爆炸；定理 2(iii) 残差 Γ_i = τ(q_i − p_θ,i) 在学生到达目标时归零、过冲后反向——像一根弹簧，拉向目标、到达即松弛、拉过头往回弹。附录还证明了标量收缩性（步长合理时不单调过冲）与参数漂移上界。

消融设计很有教育意义：pointwise 信用（V_c 本身）优于 listwise 中心化（V_c − V_i），因为中心化会把两个都有用的孩子变成一升一降；odds 映射优于 logistic 映射 q = σ(V/τ’)，因为后者不满足备份交换性，父梯度会出系统误差。

从实现视角看整个算法（Algorithm 1）出奇地轻：目标构造阶段只比 GRPO 多一步"从锚点分支后缀"的采样调度；分布匹配阶段每回合只算一个标量 s_θ,i（对数似然比均值），损失梯度权重 τ(p_θ,i − q_i)/L_x 直接挂在现有 PPO 式训练器的 token 梯度上。没有新网络、没有新标注管线、没有对 verifier 的额外调用——所有额外计算是前向传播中顺带得到的似然值。这也是它能直接套在 Qwen3-1.7B 到 30B-A3B 多个规模上复现的原因（附录 D.1：1.7B 26.88、Llama-3.2-3B 35.58，同样全胜）。

4.3 论文 3：FC-SWE——失败证据条件化的恢复链训练

方法围绕第 3.3 节两个问题的回答展开：

恢复机制：attempt r 失败后，控制器记录其 patch 与诊断 verifier 输出，把仓库恢复原始任务状态（防止瞬态文件/进程/工具状态泄漏），然后把 issue + 失败 patch + verifier 输出格式化（30K token 携带上限、6K 字符 verifier 摘录、3K 字符失败片段）成 attempt r+1 的上下文。提示词明确允许保留、修改或放弃上一个方案。主配置 G=8 链 × R=2 次尝试。

对问题 A 的回答——轨迹局部奖励：r_{c,r} = y_{c,r}（每条轨迹拿自己 patch 的验证结果），三种可能序列 [1,⊥]（首试成功）、[0,1]（恢复成功）、[0,0]（双败）。反事实对照：链广播会把 [0,1] 记成 [1,1]，让被拒绝的 patch 因为后来者的成功获得正奖励——这是在训练"碰运气"；只训最后一条则会丢掉失败行为提供的对比度。

对问题 B 的回答——活跃集优势估计：比较组 V_x = 同一 issue 下所有实际执行过的（初始 + 恢复）轨迹，用与 GRPO 相同的 leave-one-out 基线做标准化；未执行的占位行（静态批处理需要 256 行 transport tensor，其中未激活的行是 padding 不是轨迹）不进奖励统计也不进损失。这样 [0,1] 链中恢复成功者获正优势、先前失败者获负优势，跨尝试的比较得以保留。论文坦承：比较组是结局依赖的，这个更新不继承"基线与动作无关"的标准无偏性保证——这是把恢复纳入训练的固有代价。

训练与部署细节：训练用 R2E-Gym 的 4,518 个任务（十个仓库，与 SWE-bench Verified 无仓库重叠），rollout 由 OpenHands CodeActAgent 生成、评测用 SWE-agent harness——训练与评测用不同 harness 本身就是一个值得注意的选择，它说明恢复能力可以跨 harness 迁移而非过拟合到某个界面。每步 16 任务 × 8 初始链 = 128 条初始轨迹，失败最多再激活 128 条恢复轨迹；物理上分配 256 行 transport tensor（含 padding），静态批处理下异步权重同步。上下文 64K、每次尝试最多 100 次模型-工具交互、学习率 1e-6 常数无预热、裁剪 ε_l=0.2/ε_h=0.28、无 KL 参考。报告的 FC-SWE 检查点（step 67）由多个验证集（含 SWE-bench Verified 的固定 100 题子集）选出。

与 GRPO 基线对齐的严谨性：论文的 GRPO 实现用了 leave-one-out 基线（b_c 为其它 G−1 条轨迹奖励的均值）而非原版 GRPO 的组均值——这使基线与被评轨迹统计独立，也让 FC-SWE 的活跃集优势估计可以无缝继承同一个公式（Eq. 7 只是换了求和的集合）。两种方法共享运行时惩罚、损失归一化、解码配置，差异被压缩到恢复机制与奖励/分组两个设计维度。这种"共享一切、只改一处"的对照哲学贯穿全文实验。

4.4 三种机制的直观图景

如果用一张图来概括三篇方法的几何差异：Lean4AgenticRL 像在轨迹上打"里程碑"——预先立好一串带条件检查的路标（工作流阶段），走过每个路标都核对是否达标（β），另有巡警检查有没有作弊动作（γ）；TreeOPSD 像做"对照实验"——同一开头写多个续篇，续篇的成败统计出开头的价值，然后像弹簧一样把策略拉向（但不推过）统计出的目标位置；FC-SWE 像发"错题本"——每次考试错题附标准解析重考，考多了自然学会看解析改错。里程碑要预知地形（结构先验），对照实验要多花笔墨（采样预算），错题本要容忍重考（verifier 访问）。三者的成本结构与适用地形不同，但没有一个是另一个的特例——这正是"结构化路线三连"的含义。

值得对照思考的是三篇论文对"额外采样成本"的三种态度。TreeOPSD 用期望预算匹配（分支后缀成本约为完整轨迹一半，(4,2) 树 ≈ G=8 全轨迹）把成本严格对齐到 baseline；Lean4AgenticRL 的额外成本花在标注 LLM 上（形式化 + 切分 + judge，一 1200 轨迹的忠实度评估背后是 3.2 万条谓词标注的抽查），换取的是奖励的零采样开销；FC-SWE 的恢复轨迹则是"按需支出"——只有失败才花钱，且这笔钱同时买了训练信号和（测试期的）第二机会。三种货币（采样、标注、执行）的汇率因场景而异：推理任务 token 便宜 verifier 贵 → 树方案划算；SWE 任务环境执行贵但测试基建现成 → 证据方案划算；工作流结构稳定的领域 → 定义方案的一次性标注投资可摊销。

五、评估指标与实验证据

5.1 论文 1 的实验设计

主实验：SWE-Bench-Verified（500 题，mean@3）+ TerminalBench-2.0/2.1（89 题，mean@5），基座 Qwen-3.5-9B / Qwen-3.8-27B（TMax-15k + SWE-ReBench 混合数据，64 H200，9B 训 160 步/160 小时、27B 训 120 步/240 小时）。对手是同规模最强开源模型。LAR-9B 64.2%/32.8%/29.5%，LAR-27B 84.2%/68.2%/77.3%（TB-2.1），家族平均超基座 +9.89%、超同规模第二好 +5.07%（配对 p 值 3.5e-3 到 <10^-10）。9B 模型在 SWE-V 上甚至超过 31B 的 Gemma-4。

为什么这套设计能证明论点：(1) 与纯 outcome GRPO 的训练动力学对照（同数据同框架 OpenClaw-RL）隔离了奖励设计的贡献——GRPO 在 SWE 上 15 步后回落到初始水平、在终端任务上大幅震荡，本方法 30 步全程稳定上升且 10/30 步内即超过 GRPO 最优检查点；(2) 消融三件套各击一处：去 PSWF（-1.6%）、去 γ（56.0%→49.4%，且 γ 捕获的重复命令暴增 66.8%、总工具调用 +18.7%——证明没有 γ 时策略确实学会刷 LLM judge）、案例研究展示 α 恒为 −1 的任务上 β 正确率从 2/8 → 4/7 → 5/6 → 5/5 的爬升（过程奖励在 outcome 失效处提供信号）；(3) 跨模型复现（Qwen-3.6-27B +4.0/+8.0pp、DeepSeek-V4-Flash-304B TB-2.1 +5.6pp）排除了特定基座的偶然性。

5.2 论文 2 的实验设计

主实验：两个设定 × 两个规模——Multi-Hop QA（HotpotQA 训练，4 基准 EM 平均）与 Deep Research（OpenResearcher 训练，BrowseComp-Plus/BC/GAIA/xbench），Qwen3-4B 与 Qwen3-30B-A3B-Thinking。30B 上 Deep Research 平均：TreeOPSD 21.20 vs GRPO 16.23（+4.97）vs TreePO 17.59（+3.61）；Multi-Hop QA 45.93 vs 44.80。5 训练种子下 44.13±0.16 / 15.45±0.39，次序在每个种子中保持。

为什么这套设计能证明论点：精髓在于 TreePO 这个受控对照——它与 TreeOPSD 用同样的树、同样的 V_i、同样的优化块，唯一差别是"固定信用系数 V_i/L_x"还是"残差匹配"。所以 TreeOPSD−TreePO 的差（Deep Research 4B +2.38、30B +3.61）纯粹是有限目标机制的贡献。且增益集中在长程设定（Deep Research 后续 mini-batch 更多处于 off-policy 状态，正是有限目标该发力的地方；Multi-Hop QA 上两者接近——因为 5 轮封顶的短程任务里策略漂移本来就小），这个"增益-条件"匹配本身就是机制生效的证据。等训练时间对比（附录 D.3）显示 TreeOPSD 在 GRPO 的总训练时间内始终领先，排除了"多花计算"的解释。交互轮数分析显示 TreeOPSD 评估时使用更多助手轮次（学会了更深的搜索行为）。

5.3 论文 3 的实验设计

主实验：SWE-bench Verified 全 500 题 × 3 解码种子，SWE-agent harness，verifier-assisted 协议（所有方法同等访问 benchmark 测试反馈）。Base（Qwen3.5-4B）27.9%@1 → GRPO 38.9%@1/48.5%@2/恢复率 15.7% → FC-SWE 41.7%@1/52.8%@2/恢复率 19.0%。

为什么这套设计能证明论点：这篇论文的实验纪律值得称道，四个层层递进的对照：

1. 同预算反馈 vs 重采样（Figure 4a）：这是全文最关键的一张图。Base 与 GRPO 上，反馈式重试的恢复率低于独立重采样（11.6% vs 13.7%；15.7% vs 18.6%）——印证了文献里"弱模型自我修正反而有害"的发现；只有 FC-SWE 反转（19.0% vs 17.0%）。这排除了"收益来自多一次机会"的解释，把收益钉死在"学会了利用失败证据"上。

2. 上下文内容消融（Figure 4b）：只给失败 patch 15.7%（还不如不给的 17.0%——差 patch 是误导），加 verifier 证据到 19.0%（+3.3pp）——证明值钱的是诊断信息而非 patch 本身。

3. 训练期上下文消融：去掉训练期失败上下文（保留重试机制），恢复率从 19.0% 跌到 12.6%、Resolved@2 从 52.8% 跌到 47.9%——纯重试机制解释不了收益。

4. 奖励设计消融：共享奖励变体恢复率 17.7% vs 20.4%（单种子），再去掉运行时惩罚则在线成功率从 76.6% 崩到 2.3%（训练崩溃）。

测试时外推：训练只见过 2 次尝试，但 K=11 时达 70.7% vs GRPO 67.3%——恢复能力泛化到远超训练时程的预算。token 效率：达到 50% 分辨率，FC-SWE 3.15M tokens/题 vs GRPO 4.39M vs Base 8.22M。案例研究（astropy 与 django 两例）给了定性证据：GRPO 面对失败反馈重复原 patch，FC-SWE 读懂"测试失败是因为 warning 意外出现"而删掉 warning。

六、效果优势的根源解释

按"方法差异 → 机制变化 → 指标提升"的因果链逐篇拆解。

6.1 Lean4AgenticRL：为什么形式化定义能涨 9.89%？

方法差异：奖励从"轨迹级 ±1 单信号"变成"α(±1) + β(±1×≤0.5 系数) + γ(纯罚)“三级融合，且 β 的归一化单位从"整条轨迹"细化到"同通用工作流阶段跨 rollout”。

机制变化一：弱梯度组获得有效信号。 GRPO 里组内全失败（通过率 0%）时所有优势相同，梯度≈0——这些恰恰是最有学习潜力的样本。本文的门控设计让 β 恰好只在 0% 与 ≥75% 组生效：全失败组现在能看到"哪个阶段做对了"（案例：regex-chess 任务 α 恒 −1 的三个检查点上 β 正确率 2/8→4/7→5/6，第 120 步任务解开时 5/5）。机制上，这把"0 信息组"变成了"过程信息组"。近全成功组同理——outcome 无差异但阶段质量有差异。

机制变化二：阶段归一化修正了比较粒度。 位置对齐的工具调用比较（先前工作的做法）比较的是"第 k 步 vs 第 k 步"，但不同轨迹的第 k 步可能服务于完全不同的目的。以工作流阶段分组后，比较的是"定位阶段 vs 定位阶段"、“修复阶段 vs 修复阶段”——同目的行为之间的优势差才是干净的信号。这解释了训练动力学的差异：GRPO 在 SWE 上 15 步后回落（错配信号最终把策略带偏），本方法单调上升。

机制变化三：γ 封死了刷分路径，保住了 β 的信噪比。 依赖 LLM judge 的过程奖励天然有被 hack 的风险（agent 发现重复跑测试命令就能满足"反复修复重试"谓词）。γ 的六条符号规则由代码检查器执行、无法欺骗；纯惩罚设计让 γ 不构成新的 hack 目标。消融显示去掉 γ 后重复命令 +66.8%——策略确实立刻找到了 judge 的漏洞——而完整系统里几乎观察不到刷分行为。因果关系是链式的：γ 守住 β，β 才能持续提供干净的过程信号，三级奖励的整体增益才成立。

跨模型一致性（Qwen-3.6-27B、DeepSeek-V4-Flash-304B 均显著提升）进一步说明增益来自方法而非基座特性。

6.2 TreeOPSD：为什么闭合解教师能在长程上多拿 4.97 分？

方法差异：与 TreePO 唯一的区别是——固定信用系数 V_i/L_x（一个采集时定死的线性上升方向）换成对冻结教师 q_i 的残差匹配 τ(q_i − p_θ,i)。

机制变化一：更新从"方向"变成"目的地"。 固定信用只指定初始上升方向，序贯 mini-batch 每一步都在同一方向推——如果第 1 个 mini-batch 已经把某回合推过了合理位置，后面 3 个 mini-batch 继续推（过冲）。残差 Γ_i 在到达 r★_i 时归零、过冲反向：同一批数据支持多次更新而不累积过冲。数学上，蒸馏损失每一步的下降恰等于邻近 RL 目标的上升（Fenchel-Young 对偶），优化是单调有界的。指标对应：增益集中在 Deep Research（回合多、批内更新块多、漂移大）而非 Multi-Hop QA（≤5 轮、漂移小）——机制预测与数据吻合。

机制变化二：pointwise 信用保留了共享价值。 组内中心化（listwise，GRPO 式）会删掉所有孩子共享的分量：两个孩子都有用时，中心化后一升一降，总概率不涨。树备份的 pointwise 信用 V_c 允许把所有有用回合一起抬高。数值研究（Figure 7b）与训练曲线都验证了这一点。这在"采样兄弟只覆盖续写空间一小部分"的 LLM 场景里是实质差异——你采到的几个续写可能个个都比平均值好，中心化方法却无法整体提升它们。

机制变化三：回合粒度 + 长度归一化消除了两个偏差。 token 级比值随回合长度指数放大方差（长推理回合 vs 短工具调用），轨迹级广播抹平回合差异。回合级几何均值比值 + σ 后验两者兼治。30B-A3B 上 Deep Research 的 +4.97（vs 4B 的 +3.23 over GRPO）也暗示：模型越强、任务越长，回合级信号的价值越大。

6.3 FC-SWE：为什么失败条件化能反转"自我修正有害"？

方法差异：相对 GRPO 增加了两件事——失败触发的条件化恢复采样，与配套的轨迹局部奖励 + 活跃集优势。

机制变化一：失败证据从"被丢弃"变成"训练分布"。 GRPO 的世界里，失败轨迹只贡献一个 0 标签；诊断输出（哪些测试挂了、什么异常）直接进垃圾桶。FC-SWE 让"读着报错改代码"这个行为模式出现在训练数据里，且通过 RL 选择性强化其中成功的模式。最硬的证据是方向反转：Base/GRPO 上反馈重试比重采样差（-2.1/-2.9pp），FC-SWE 上反超（+2.0pp）——如果收益只是"多一次采样"，FC-SWE 应该与 Base/GRPO 同向；只有"学会了读证据"能解释反转。上下文消融（verifier 证据 +3.3pp，纯 patch −1.3pp）进一步把有效成分定位到诊断信息。

机制变化二：轨迹局部奖励保住了对比结构。 若用链广播奖励，[0,1] 链变成 [1,1]，失败 patch 获得正强化——策略学到的是"先乱写再等队友救"的搭便车行为。局部奖励让每次尝试对自己的 patch 负责，恢复成功者与先前失败者在活跃集中形成正负对比，这组对比恰好是"同样证据下，改与不改的差异"——正是想学的信号。消融中共享奖励使 Resolved@2 掉 3.0pp、恢复率掉 2.7pp 支持这一机制。

机制变化三：干净重置 + 有界证据保证恢复任务的平稳性。 仓库恢复原状意味着恢复轨迹与初始轨迹面对同一环境，二者的可比性不因残留状态被破坏；证据截断防止上下文爆炸。这个设计不直接产生指标，但它是前两个机制成立的前提——没有平稳性，[0,1] 的对比就混入环境噪声。

外推机制：K=11 的 70.7% 说明学到的是"利用证据修正"的通用能力而非"第二次尝试"的固定行为——训练时 R=2，测试时 11 次尝试的链式恢复仍在复利。

6.4 三条因果链的并排总结

七、必要知识反推

读懂这三篇需要的前置知识，按"缺什么补什么"列出：

GRPO 及其变体（三篇共同的基座）：组相对策略优化——对同一 prompt 采样一组轨迹，用组内奖励均值做基线、标准差做归一化，免去 value 网络。必须理解"优势 = 组内相对位置"这个核心，因为三篇论文的改造都发生在这个算子的粒度（阶段/回合/链）或输入（多级奖励/树/恢复组）上。延伸阅读 DeepSeekMath（GRPO 出处）、DAPO（clip-higher 等稳定技巧，论文 1、3 都用了 ε_u=0.28/ε_l=0.2 的非对称裁剪）。

论文 1 特需——Lean 4 与依赖类型：Lean 是基于依赖类型理论的定理证明器，“依赖类型"指类型可以依赖值（如"长度为 n 的列表"是类型），Curry-Howard 对应下"验证证明 = 类型检查”。不需要会写 Lean，但要理解为什么选它而非 LTL/SMT（附录 E 的论证）：嵌套 JSON/工作流图等递归结构需要归纳推理，值依赖类型让前后置条件直接陈述在具体数据上。再补 Hoare 逻辑的直觉（{P} 程序 {Q}）就够读方法部分。

论文 2 特需——重要性采样、KL 正则 RL 与 Bregman 对偶：(1) 离策略修正的经典困境——乘性重要性比值 e^s 的方差随序列长度指数增长（自归一化 IS、截断 IS 是经典应对）；(2) Policy Mirror Descent / 最大后验策略优化（MPO）的"邻近目标 + 投影"两步视角；(3) Forward KL 与 Reverse KL 的区别（均值寻求 vs 众数寻求）、Bregman 散度与 Fenchel 对偶（理解"Fenchel-Young 损失 = 邻近目标的最优间隙"这句话）；(4) Samuelson 不等式（样本标准化值的界 (K−1)/√K）——一个 1968 年的统计学结果成了目标有界性的免费午餐。

论文 3 特需——SWE-bench 生态与反馈学习谱系：SWE-bench Verified 的任务形态（issue + 容器化仓库 → git patch → F2P/P2P 测试判定）；R2E-Gym（训练环境）、OpenHands（rollout）、SWE-agent（评测）的分工；以及"自我修正是否有害"的文献线（Olausson 2024 的"自修不如重采样"发现是 FC-SWE 必须回应的对手）。

通用——ReAct 循环与多轮 RL 的 token 结构：哪些 token 是策略生成的（有梯度）、哪些是环境观察（mask 掉），这个区分是论文 2 回合定义和论文 3 loss 权重设计的地基。

八、通用性灵感

1. 中间信号的本质是"结构先验"，三篇给出了三种可复用的结构化原语。 当你自己的 Agentic RL 任务面临稀疏奖励时，不必照搬任何一篇，但可以问三个问题：任务有没有可形式化的阶段结构（→ 定义式，适合工作流清晰、谓词可判定的领域，如 SWE、终端操作）？交互是否天然分轮次、且分支采样可行（→ 反事实式，适合搜索、研究、对话类任务，树的分支成本可接受时）？失败是否产生可读的诊断输出（→ 证据式，几乎适用于一切有 verifier 的领域，成本最低）？三条路线的可组合性也值得注意：FC-SWE 的恢复链完全可以跑在 TreeOPSD 的树上（失败分支的 verifier 输出条件化新分支）；Lean4AgenticRL 的 β 也可以给 TreeOPSD 的备份提供非终端节点信号。

2. “有限目标"优于"上升方向”——这个洞察溢出了 RL 领域。 TreeOPSD 的核心贡献是把"推一把"变成"拉向一个可到达的点"。任何迭代优化系统里，只要信号在采集后会被多次使用（数据复用、多 epoch、异步训练），固定系数就会累积过冲。把目标定义成相对于采集时状态的函数、让残差随逼近自动衰减，是一个可以迁移到推荐系统重训练、在线学习、甚至 Agent 记忆更新（防止同一条经验被反复过度强化）的设计模式。

3. 防 reward hacking 的分层思路：机械检查守卫语义判断。 Lean4AgenticRL 的 γ 设计（纯惩罚、符号规则、代码执行、不可欺骗）展示了一个通用架构：凡是依赖 LLM judge 的奖励，都应配一套符号层守卫，把最常见的刷分模式（重复、空转、常量输出）定义为可机械检测的违规。γ 的"只罚不奖"原则尤其精妙——守卫本身不能成为新的优化目标。这个原则直接可迁移到任何用 LLM 评分的训练管线。

4. 反转实验是归因的金标准。 FC-SWE 最有说服力的数据不是 41.7% 而是"-2.1/-2.9 → +2.0"的反转：同一机制（反馈重试）在基线上有害、在方法上有益，一正一反之间，收益的归属再无歧义。设计实验时主动寻找这种"符号反转"条件（机制在对照组应当起反作用），比堆砌更多正数更能钉死因果。

5. 被丢弃的副产品往往是下一个信号源。 GRPO 训练每天丢弃海量 verifier 诊断输出、Lean 检查日志、工具调用返回值。FC-SWE 提醒我们审计自己管线里的"废料流"：什么东西是任务执行必然产生、当前又没进训练信号的？失败堆栈、部分通过的测试比例、工具报错类型……都是候选。

6. 门控式奖励注入：过程奖励只该在 outcome 失效处生效。 Lean4AgenticRL 的"β 仅作用于通过率 0% 或 ≥75% 的组"是一个值得记住的细节：过程奖励与 outcome 奖励不是叠加关系而是互补关系，在 outcome 信号健康（中间通过率）的组里注入过程奖励反而添噪。自己设计混合奖励时，先问"outcome 在哪里失效"，再决定过程信号注入哪里。

7. 理论与工程的互锁可以很便宜。 TreeOPSD 的有界性来自 Samuelson 不等式这个"免费"的统计事实，闭合解来自 KL 惩罚在 log-odds 坐标下的线性导数——没有引入任何新计算，只换了坐标就拿到了停机与自校正性质。遇到不稳定的多 epoch 训练问题时，先找"换个坐标系让约束变免费"的机会，可能比加正则项便宜得多。

8. 三篇论文共同指向的下一个问题：中间信号的"可组合堆栈"。 单独看，每篇只解决一层：Lean4AgenticRL 有最细的粒度（阶段级谓词）但依赖任务结构先验；TreeOPSD 有最干净的理论（零先验、纯反事实）但粒度只到回合；FC-SWE 完全不切分但把信息增量留给了策略自己学。一个自然的愿景是分层混合：阶段级形式化奖励做粗粒度结构、树备份在阶段内做回合级反事实、失败证据条件化处理终局负样本——三者分别对应"计划层"“执行层"“重试层"的信号。当然组合会带来新的设计问题（三级信号的优势如何归一化到同一尺度、树的分支与恢复链如何共享 rollout 基础设施），但这恰是后续研究的空间。

9. 对评测协议的警觉：FC-SWE 的"verifier-assisted"是一面镜子。 FC-SWE 的多尝试结果测的是"有 verifier 反馈辅助的恢复”，不是独立采样的 Pass@K，论文附录 A 花了一整节解释这一点并保证所有对比方法同等访问。这个细节提醒我们：当方法本身改变了"agent 能看到什么”（反馈、记忆、检索），评测协议必须随之显式化，否则跨论文的数字不可比。Lean4AgenticRL 的 mean@3/mean@5 与 TreeOPSD 的 EM 也各有隐含假设（前者含 harness 选择、后者含检索环境），复现或对比前先对齐协议。

尾注：三篇的局限与阅读建议

Lean4AgenticRL 的形式化边界止于 LLM 标注（附录 F 坦承三个标注步骤无法形式保证），且验证是外部约束而非打开 LLM 内部黑箱；TreeOPSD 的基准提升绝对值不大（Multi-Hop QA 上 +1.13 over GRPO），长程设定外的收益有限，且每棵树只服务 E=4 个优化块；FC-SWE 的 R=2 链设计与 verifier-assisted 评测协议（测试时可访问 benchmark 测试反馈）在实际部署中的适用性需要打折扣。三者合读时更应吸收的是其结构思想而非具体数字。

建议阅读顺序：先读 FC-SWE（最短、问题最聚焦、实验归因最干净），再读 TreeOPSD（数学最优雅，附录 B 值得逐行过），最后读 Lean4AgenticRL（系统最庞大，附录 D.2/I 的标注细节是理解工程现实的关键）。