Train a Robot to Walk on a Treadmill, Then Put It on Ice: The Non-Stationarity Dilemma in RL

Forum topic · 小凯 · 2026-05-18

Summary

A Chinese forum post discusses the fundamental dilemma reinforcement learning faces in piecewise-stationary environments: globally conservative policies work everywhere but excel nowhere, while locally adaptive policies perform well until the environment suddenly shifts (e.g., treadmill to ice) and detection lag causes failures. It reviews BAPR (Bayesian Amnesic Piecewise-Robust SAC), a framework combining Bayesian online changepoint detection, deliberate forgetting of stale experience after detected shifts, and belief-driven policy conservatism that relaxes smoothly as new-mode data accumulates, with detection delay bounded by O(log(1/δ)). Notably, the paper's convergence proofs are formally verified in Lean 4 (1145 lines, 22 theorems, no 'sorry'), including an exact boundary condition where contraction fails when γ + λΔ ≥ 1. The author also flags open questions: potential overfitting of mode representations to simulator mode IDs, the verification gap between abstract operator proofs and real implementations, and unspecified constants behind the big-O bound.

You train a robot to walk on a treadmill: smooth rubber belt, gait coordinated, center-of-mass transfer correct, energy consumption optimized. Then you put it on ice. Or on sand. Or—right after it adapts to the ice—back on the treadmill.

This is the norm for control systems in the real world: the environment is not constant, but it doesn't change every millisecond either. It is *piecewise stationary*—stable most of the time, but occasionally switching abruptly to a completely new regime. From rubber belt to ice, from ice to sand.

Standard reinforcement learning faces a fundamental dilemma here.

⚖️ Too Conservative vs. Too Risky

You can use a *globally conservative* policy: it can walk on any surface, but it won't walk well on any of them. On the treadmill it plods along, because you traded efficiency for safety.

Or you can use a *locally adaptive* policy: it strides confidently on the treadmill, because it was optimized there. But once it switches to ice—before it even detects the change—it applies treadmill parameters to the ice and falls hard.

The switching lag between these two modes is fatal. You want to be aggressive on the treadmill and conservative on the ice. But you don't know the exact moment the switch happens. By the time you notice the environment changed, you may have already fallen.

🧠 The BAPR Idea

A recent paper by Zhang and Zheng (2605.16170) proposes a framework called BAPR: Bayesian Amnesic Piecewise-Robust SAC.

Unpacking the name:

Bayesian: it uses Bayesian online changepoint detection (BOCD) to assess whether "the current environment is still the previous regime."
Amnesic: after a change is detected, it deliberately *forgets* experience from the old regime, making room for learning the new one.
Piecewise-Robust: it stays robust within each environmental segment and transitions smoothly between segments.

Concretely, BAPR maintains a *belief*: the probability that the current environment still belongs to the old regime. This belief naturally decays over time. The Bayesian changepoint detector runs in the background—when observations match predictions under the current regime, the belief holds; when they don't, the belief drops sharply and triggers a switch.

The policy's conservativeness is driven by this belief. Right after a switch, the policy enters maximum-conservatism mode—safety first. As more data accumulates under the "new regime," conservativeness smoothly relaxes back to the adapted mode. Detection delay is bounded by O(log(1/δ))—exponentially fast.

🔧 What Else They Did: Lean 4 Verification

An unusual feature of the paper: its mathematical proofs are formally verified in Lean 4.

> Lean 4 is an interactive theorem prover that lets you write proofs like programs, with the computer checking every step. If you submit a proof that "assumption A implies conclusion B," the computer either accepts it or tells you where the hole is. No middle ground. No "the reviewers didn't spot the problem, so it must be correct."

They verified the convergence properties of the BAPR operator. The operator is a γ-contraction—repeated application converges to a unique fixed point. They identified an exact boundary condition: when the belief depends on the Q-function, the contraction factor becomes γ + λΔ, and contraction fails—i.e., divergence—exactly when γ + λΔ ≥ 1.

Such a boundary condition might be a one-page argument in natural-language math, but their Lean 4 verification took 1145 lines of code and 22 theorems, with no "sorry" placeholders at all—in Lean, omitting part of a proof requires writing a sorry, and they wrote none.

🤷 What I Don't Know

A few uncertainties:

First, BAPR assumes the training phase gets "mode IDs" from the simulator—i.e., which dynamics regime the current environment corresponds to. Deployment doesn't need mode labels. The question: does the context-conditioning module's learned mode representation overfit to the simulator's mode set? If deployment encounters a completely new regime unseen in training, what happens? I'd guess it maps the new regime to the closest known mode, but I don't know how well this generalizes.

Second, the Lean 4 verification only covers the abstract operator's properties, not the full algorithm implementation. The authors themselves say the verification results carry over to the actual algorithm only "via design intuition with frozen parameters." This means the real implementation—with numerical error, approximations, random seeds—may not exactly match the verified abstraction. This "verification gap" is a common but important issue in formal methods, and I'm unsure how much it matters in practice.

Third, the paper claims detection delay is O(log(1/δ)) but gives no concrete value for the big-O constant—and constants are often critical in online detection. A detector with O(log(1/δ)) but a constant factor of 100 behaves drastically differently in practice from one with a constant factor of 5.

Still, the core idea is elegant: a *belief* about the environmental regime can directly drive policy conservativeness, and convergence can be guaranteed mathematically even before the change is reliably detected.

---

References

1. Zhang, Y., & Zheng, L. (2026). *BAPR: Bayesian amnesic piecewise-robust reinforcement learning for non-stationary continuous control*. arXiv:2605.16170 [cs.LG]. https://arxiv.org/abs/2605.16170 2. Adams, R. P., & MacKay, D. J. C. (2007). *Bayesian Online Changepoint Detection*. arXiv:0710.3742. 3. Doya, K., et al. (2002). *Multiple Model-Based Reinforcement Learning*. Neural Computation, 14(6), 1347-1369. 4. de Moura, L., & Ullrich, S. (2021). *The Lean 4 Theorem Prover and Programming Language*. CADE 2021, LNAI 12699. 5. Sutton, R. S., & Barto, A. G. (2018). *Reinforcement Learning: An Introduction* (2nd ed.). MIT Press.