You train a robot to walk on a treadmill. The belt is smooth rubber. The gait is coordinated, weight transfer is correct, energy consumption is 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 static, 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 mode. From rubber belt to ice. From ice to sand.
Standard reinforcement learning faces a fundamental dilemma here.
⚖️ Too Conservative vs. Too Aggressive
You can use a globally conservative policy. It can walk on any surface, but walks well on none. 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 switched to ice—before it has detected the change—it walks on ice with treadmill parameters and falls hard.
The switching delay between these modes is fatal. You want to be aggressive on the treadmill and conservative on ice. The problem: you don't know the exact moment the switch happens. By the time you notice, 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.
Taking it apart:
- Bayesian: it uses Bayesian Online Changepoint Detection (BOCD) to assess "is the current environment still the same regime?"
- Amnesic: after a change is detected, it deliberately *forgets* experience from the old regime to make room for learning the new one.
- Piecewise-Robust: it stays robust within each segment and transitions smoothly between segments.
The policy's conservatism is driven by this belief. Right after a switch, the policy enters maximum-conservatism mode—safety first. As more data accumulates under the new mode, conservatism relaxes smoothly back toward the adaptive mode. The detection delay bound is O(log(1/δ))—exponentially fast.
🔧 What Else They Did: Lean 4 Verification
An unusual feature of the paper: the 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 of "assumption A implies conclusion B," the computer either accepts it or tells you where the hole is. No middle ground. No "it's correct because the reviewers didn't spot the flaw."
They verified the convergence properties of the BAPR operator. The operator is a γ-contraction mapping—repeated application converges to a unique fixed point. They found a precise boundary condition: when the belief depends on the Q-function, the contraction factor becomes γ + λΔ, and contraction fails—i.e., it diverges—exactly when γ + λΔ ≥ 1.
Such a boundary condition might be a one-page argument in informal math, but their Lean 4 verification took 1,145 lines of code and 22 theorems, with no "sorry" placeholders (in Lean, if you omit part of a proof you must write a sorry; they have none).
🤷 What I Don't Know
Several uncertainties remain.
First, BAPR assumes that during training, a simulator provides a "mode ID" for the current dynamics. Mode labels aren't needed at deployment. The question: going from label-supervised training to label-free deployment, will the context-conditioning module's learned mode representations overfit to the simulator's regime set? What happens at deployment when a genuinely new regime appears? My guess is it maps the new mode to the nearest known one, but I don't know how well that generalizes.
Second, the Lean 4 verification covers only the abstract operator's properties, not the full algorithm's implementation. The authors themselves say the verified results carry over to the practical algorithm only "via frozen-parameter design intuition." The real implementation—with numerical error, approximations, and random seeds—may not exactly match the verified abstraction. This "verification gap" is a common and important issue in formal methods; I'm unsure how much it matters in practice.
Third, the paper claims O(log(1/δ)) detection delay but gives no concrete constant—and constants often matter enormously in online detection. A detector with constant 100 versus one with constant 5, both O(log(1/δ)), behave very differently in practice.
Still, the core idea is elegant: a *belief about the environment's regime* directly drives the policy's level of conservatism, with convergence guaranteed mathematically even before changes are 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.