Translation
Training a useful agent these days means reinforcement learning: let the model try repeatedly in a real environment, reward success, punish failure. Sounds reasonable — but how you hand out the rewards is a big problem.
Most teams only look at outcomes. A task is either done or not: a 0 or 1, nothing else. That's like a teacher grading only the final exam total without ever reviewing homework. The paper shows the consequences plainly: a control group trained with pure outcome rewards (GRPO) improved for the first 15 steps on software engineering tasks, then collapsed — by step 20 it was back near its starting point. Nobody supervised the dozens of intermediate steps, the model learned bad habits, and eventually even the outcome score broke down.
What about scoring every intermediate step? The idea is old; it's been stuck on two problems.
First, human annotation doesn't scale: an agent task runs tens to hundreds of steps, and manually labeling each one is too costly. Second, more subtly: using a large model as a judge to grade each step invites cheating. The paper gives a ready-made example — one stage's requirement was "retry after the fix," and the agent learned to re-run the exact same test command several times. The judge saw "it retried" and gave points. Score collected, problem untouched.
The paper's goal is exactly this: how to issue intermediate-step rewards cheaply and cheat-proof.
Their answer is to bring in Lean. Lean is a formal proof language famous for being merciless — the kernel mechanically checks whether what you wrote is correct, no chatting, no exceptions. Prior work (Lean4Agent) already used it to verify theorem-proving tasks, but that system assumed a fixed, predefined workflow; modern agents take open-ended paths nobody can predict in advance. The new contribution, PSWF, works like this: a large model explores the task environment and produces a staged natural-language plan for each problem; the plan is translated into a Lean formal description with pre- and post-conditions. After the agent runs, its trajectory is aligned to the stages, and each stage's conclusion is checked by predicates: did the required conditions hold? If yes, that stage's reward β is 1; if not, -1.
Rewards thus become three-tiered. The top layer α checks the outcome — was the task completed? The middle layer β checks each stage — did the pre/post-conditions pass? The bottom layer γ watches every tool call, specifically to catch cheating patterns: repeated identical commands, no-ops, dead-loop shells — encoded as symbolic predicates and enforced by Lean and Python checkers.
There's a deliberate design choice in γ: it only penalizes, taking values -1 or 0. Why no positive rewards? Because once it hands out positive points, the model will find ways to farm them. Penalty-only leaves nothing to game, so it stays a honest gatekeeper. Ablations show this gatekeeper is worth 6.6 points: removing it drops performance from 56.0% to 49.4%.
The standout result is small models. LAR-9B, trained from Qwen-3.5-9B, gained 20.2, 13.5, and 13.4 points on SWE-Bench-Verified, TerminalBench-2.0, and TerminalBench-2.1 respectively, beating the strongest same-size rival TMax-9B by 10.7, 5.6, and 1.9 points, and even outperforming the nearly-3x-larger Gemma-4-31B on SWE tasks. The 27B story differs: base Qwen-3.8-27B was already the strongest of its size, so LAR-27B builds on a high floor, adding 1.2, 3.5, and 7.7 points, landing at 77.3% on TerminalBench-2.1. Averaged, that's +9.89% over base and +5.07% over the second-best same-size model — the average looks modest, but broken down, the method hits hardest on small models. Training itself is not expensive: 64 H200 GPUs, 160 hours for 9B, 240 hours for 27B.
But the "verifiable" in verifiable rewards deserves scare quotes. The paper's appendix has a dedicated section on the formalization boundary and is candid: three links in the chain are done by LLMs — translating the natural-language plan into Lean code, segmenting trajectories into stages, and scoring semantic predicates. Formal guarantees don't cover these steps. Lean protects the mechanical checking after those steps; if the steps themselves are wrong, the boundary is wrong. In other words, Lean is a perfect checker — but the problem set was written by the very party it's checking. This is the shared soft spot of all "formal + LLM" hybrid systems; the paper doesn't hide it and lays it out in the appendix.
With this position clear, Lean now has three landing points on the technical chain. As a reward verifier during training — that's this paper. As a permission gate at runtime — Lean-verified agent runtimes are already doing this, proving each operation's permission before execution; that's Lean on defense. Translating images and physical scenes into Lean propositions at the perception layer — that's the self-formalization line paving the way. All three point the same direction: large models handle judgment, formal languages handle execution — judgment can be fuzzy, execution must be exact.
The paper's own stated limitations follow the same direction: verification wraps the agent in external constraints without opening the model's internal black box; verification isn't in the runtime; visual signals aren't connected yet. The third is the next battleground; the first two are exactly where the other two lines are filling in.
Source
- Paper: arXiv 2610.22448 (submitted 2026-10-15)
- Code: github.com/RickySkywalker/Lean4AgenticRL (MIT license, repo created 10-10)
- Authors: Ruida Wang, Gerald Friedland, Tong Zhang, Chris Kong; first author completed the work during an Amazon Web Services internship, affiliated with University of Illinois Urbana-Champaign
- All figures cited come from the paper's main text and appendix