Key points
- Problem: Standard RL assumes stationarity. In piecewise-stationary environments (long stable periods, then sudden regime switches like road → ice, clear weather → blizzard), standard RL keeps using stale policies, while robust RL (e.g., RE-SAC) is permanently conservative and wastes performance during stable periods.
- BAPR's approach: Bayesian online change-point detection (BOCD) plus robust ensemble RL, with three "frozen" layers—frozen aleatoric penalty (κ), frozen epistemic ensemble penalty (Γ_epi), and a frozen belief distribution ρ over run-lengths. Freezing ρ inside the Bellman step prevents circular dependence between the critic and the belief it protects.
- The killer counterexample (machine-verified): If the belief ρ is allowed to depend on Q-values, the operator's contraction factor degrades from γ to γ + λΔ (Δ = reward gap between modes). When γ + λΔ ≥ 1, contraction fails entirely—Q-values can oscillate or diverge. The theorems
T_bad_not_contractionandT_bad_expansionestablish a sharp boundary, so freezing ρ is a mathematical necessity, not a design taste. - Adaptive conservatism ("Bayesian Amnesia"): Expected run-length h̄ drops sharply after a detected change; BAPR uses its deviation from an exponential moving average to raise a conservativeness penalty. The machine-verified safety guarantee is β_eff ≤ β_base for all λ_w ≥ 0—false alarms can only cause temporary over-conservatism, never reduced safety.
- Detection speed: O(log(1/δ)) theoretical bound; ~2–3 iterations under typical parameters (L≈2, δ=0.05). Empirically, median detection latency of 13 iterations on Ant-v2 (90th percentile: 22). Honest caveat: 9 of 22 mode switches went undetected within 50 iterations (~41% false negatives); BAPR degrades gracefully to the static robust baseline in those cases.
- Experiments: Four MuJoCo environments with intra-episode regime switches. On Ant (27-dim observations, 8-dim actions, K=4 modes):
- BAPR: 20,679 ± 3,402
- ESCP (context-conditioned): 4,600 ± 4,406 (collapses in high dimensions)
- SAC (standard): 17,171 ± 194
- BAPR's *worst* seed (17,872) beats ESCP's *best* seed (9,824)—zero distribution overlap.
- Ablations: Removing the regime-identification module (RMDM) cuts performance by 47%; removing BOCD costs 21%; a Q-dependent β_eff (the counterexample's design) costs 10%; removing adaptive β costs 9%.
- Theory-to-implementation gap: the contraction theorem covers an abstract mixture operator with M independent critics; the implementation uses a single shared critic with context embeddings, bridged by an "approximate contraction" bound whose exact logic is hard to fully verify.
- End-to-end convergence: the guarantee is per-step (for a fixed belief snapshot); full non-stationary training-loop convergence remains open.
- 41% false-negative rate: questionable for safety-critical settings, especially with weakly separable regimes (L≈1), where detection latency grows as O(1/log L).
- Walker2d/Hopper ceiling: *no* method exceeds ~550 return; replay buffers retain "toxic" data from previous regimes. BAPR has no mechanism to flush or down-weight stale buffer data—an obvious future improvement.
- Title: BAPR: Bayesian amnesic piecewise-robust reinforcement learning for non-stationary continuous control
- Authors: Yifan Zhang, Liang Zheng (Central South University)
- arXiv: 2605.16170 (submitted 2026-05-15)
- Areas: cs.LG, cs.AI, formal verification (cs.LO)
- Code: https://github.com/erzhu419/BAPR
Honest limitations discussed in the analysis
Why the formal verification matters
The most striking aspect is methodological: all 22 theorems—including the counterexample—are encoded in Lean 4 (1,145 lines, zero sorry), so anyone can re-run the proofs. When the Lean compiler says Q.E.D., that is a fact, not an opinion. This does not erase the theory-to-practice gap (function approximation, sampling noise), but it makes the remaining gap explicit, quantifiable, and steadily shrinkable.