BAPR: When Robots Learn to "Forget" — Machine-Verified Safety for AI in a Shifting World
Imagine you're a robot that spent a month mastering flat-ground walking. Then one day someone swaps your world to ice: friction drops from 0.8 to 0.1. Every action you take is based on a now-false assumption — "the ground beneath me is stable."
- A standard RL agent keeps using old experience and only slowly (possibly after hundreds of thousands of iterations) notices the world changed.
- A robust RL agent (e.g., RE-SAC) stays cautious always — wasting performance during 99% of stable time.
- Expected run length: h̄ = Σ h·ρ(h)
- When the environment is stable, BOCD's posterior concentrates on large h and h̄ is high. After a change point, the posterior jumps to small h and h̄ plummets.
- BAPR uses the deviation of h̄ from its exponential moving average: λ_w = max(0, h̄/(H-1) − ēma)
- BAPR: 20,679 ± 3,402
- ESCP (context-conditioned): 4,600 ± 4,406
- SAC (standard): 17,171 ± 194
- Remove RMDM (mode-recognition module): performance drops 47% — the most critical component
- Remove BOCD: −21%
- Q-dependent β_eff (the counterexample design): −10% — validating the counterexample's practical harm
- Remove adaptive β: −9%
- Theory-to-implementation gap. The contraction theorem covers an abstract mixture operator Σρ(m)T^m with M independent Q-functions; the implementation uses a single shared critic with context embeddings. The claimed "conservative" approximation is quantitatively bounded in ApproxContraction.lean, but the exact bridging logic isn't fully clear.
- End-to-end convergence. Like all Bellman-contraction proofs in deep RL, the result is a per-step property — contraction for any fixed belief snapshot ρ. Full end-to-end convergence of the non-stationary training loop remains open.
- False-negative rate. Is 41% acceptable in safety-critical settings? If changes are subtle (L≈1), detection latency grows as O(1/log L) and may exceed metastable periods — the environment changes again before detection completes.
- Walker2d/Hopper ceiling. All 14 configuration sweeps failed to break through. BAPR lacks an explicit mechanism for stale replay data; a natural improvement would be cleansing or down-weighting the buffer after a detected change point — unexplored in the paper.
- Title: BAPR: Bayesian amnesic piecewise-robust reinforcement learning for non-stationary continuous control
- Authors: Yifan Zhang, Liang Zheng
- Affiliation: Central South University
- arXiv: 2605.16170
- Submitted: 2026-05-15
- Areas: Machine Learning (cs.LG), Artificial Intelligence (cs.AI), Formal Verification (cs.LO)
- Code: https://github.com/erzhu419/BAPR
- Core claim: For continuous control in piecewise stationary environments, BAPR unifies Bayesian online change-point detection (BOCD) with robust ensemble RL. Key theoretical contributions are the γ-contraction proof of the BAPR operator and its counterexample (belief-dependent Q-values degrade the contraction factor to γ+λΔ, enabling divergence), all formally verified in Lean 4 (1,145 lines, 22 theorems, 0 sorry). Detection latency O(log(1/δ)); the policy automatically maximizes conservatism after change points (β_eff ≤ β_base, machine-verified) and smoothly relaxes as confidence recovers. Experiments across four non-stationary MuJoCo environments show BAPR's worst Ant seed beats ESCP's best with zero distribution overlap; ablations confirm RMDM as the most critical component (−47% when removed).
In May 2026, two researchers at Central South University (Yifan Zhang and Liang Zheng) proposed a third path: BAPR. Its philosophy: act boldly when stable, become instantly alert at abrupt change, and prove this behavior is safe with mathematics.
What makes this paper fascinating is something almost no ML paper dares to do: the core theorems are proven in Lean 4 — 1,145 lines of code, 22 machine-verified theorems, zero sorry placeholders.
1. The Problem: When the World Changes the Rules
RL assumes stationarity — today's reward function and physics equal tomorrow's. True in labs, rarely in the real world: a self-driving car trained in normal weather meets a blizzard; a warehouse robot trained on standard loads gets an unexpectedly heavy shelf; a medical AI trained on adults is deployed in pediatrics.
These share a structure: piecewise stationary environments — long stable periods punctuated by sudden change at unknown times. Standard RL is blindsided; robust RL is permanently over-conservative; context-conditioned methods (e.g., ESCP) offer adaptation but no formal safety guarantees, and collapse in high-dimensional settings (27-dim observations, 8-dim actions).
2. BAPR's Three Layers of "Freezing"
BAPR's core design can be summarized in one word: freeze.
1. Frozen aleatoric penalty (κ) — RE-SAC subtracts a constant κ from Q-values to counteract environmental stochasticity. Freezing it avoids circular dependence (adjusting κ using the very Q-values κ protects would break convergence guarantees). 2. Frozen epistemic penalty (Γ_epi) — measured by the standard deviation of a Q-network ensemble; ensemble parameters are fixed during training, for the same reason. 3. Frozen belief distribution (ρ) — unique to BAPR. The Bayesian Online Change-point Detection (BOCD) module maintains ρ, a belief over "time since last change point." Within one Bellman-operator step, ρ is frozen: Q-updates are weighted by ρ, but Q never influences ρ.
3. The Counterexample: When Beliefs Depend on Q, Everything Collapses
The paper's most insightful part is a counterexample, also machine-verified in Lean 4.
Suppose you let ρ depend on Q-values — intuitively reasonable, since sudden Q fluctuations might indicate change. Math says otherwise: the Bellman operator's contraction factor becomes γ + λΔ, where Δ is the reward gap between modes. When γ + λΔ ≥ 1, the operator no longer contracts — Banach fixed-point reasoning fails, Q-values may never converge, and the agent can enter divergent oscillations.
Crucially, this is not a pathological edge case: real reward gaps between modes (e.g., "normal driving" vs. "blizzard") can be large, easily pushing γ + λΔ past 1. Lean 4 rigorously verifies this (T_bad_not_contraction, T_bad_expansion) with the contraction factor computed exactly as γ + λΔ — a sharp boundary: contraction on one side, divergence on the other, no gray zone.
Freezing ρ is not a design preference; it's a mathematical necessity.
4. Adaptive Conservatism: The Art of "Amnesia"
Freezing ρ guarantees single-step contraction; BAPR then adjusts behavior after change points via "Bayesian Amnesia":
The verified safety guarantee (also in Lean 4):
β_eff ≤ β_base for all λ_w ≥ 0
BAPR is never *less* conservative than the static robust baseline. False detections only cause temporary over-conservatism, never unsafety — a beautiful "one-way safety valve." After surprise, the agent selectively "forgets" old experience, becomes extremely cautious, then gradually relaxes as confidence recovers.
5. Detection Speed: A Few Iterations Suffice
Detection latency is bounded by O(log(1/δ)), derived from a likelihood-ratio argument: after a change point, posterior ratios grow geometrically, PR(n) = L^(2n)/r₀, requiring n ≥ log(r₀/δ)/(2 log L).
With typical parameters (L≈2, uniform prior, δ=0.05), theoretical latency is ~2–3 iterations. Experimentally (Ant-v2, K=4 modes), BOCD's median detection delay is 13 iterations, 90th percentile 22. Honestly noted: 9 of 22 mode switches went undetected within 50 iterations — a 41% empirical false-negative rate, expected for weakly separable modes. BAPR's response is graceful degradation: undetected, it falls back to the static robust RE-SAC baseline, retaining basic safety.
6. Experiments: Overwhelming Advantage on Ant
Four MuJoCo environments (Hopper, HalfCheetah, Walker2d, Ant), each with intra-episode mode switches.
On Ant (27-dim observations, 8-dim actions, K=4 discrete modes):
BAPR's worst seed (17,872) exceeds ESCP's best seed (9,824) — zero distribution overlap. ESCP nearly collapses because recovering mode information from raw 27-dim observations is extremely hard, whereas BAPR's μ(z) channel — discrete mode clusters discovered online via k-means — lets the critic condition on a consistent indicator when modes recur.
Ablations:
An honest negative result: on Walker2d and Hopper, all methods hit a ~550 reward ceiling — bipedal/unipedal balance policies can't fully solidify before mode switches, and the replay buffer retains "toxic" data from previous modes. This is a general limitation of current piecewise-stationary RL, not BAPR-specific.
7. What I'm Not Sure About
8. Takeaway
BAPR's biggest impact isn't the algorithm — it's the methodology of formal verification.
Typical ML theorem proofs live in paper appendices, rarely checked by anyone but the authors. This paper instead writes every theorem as Lean 4 code and lets the machine verify: 22 theorems, 1,145 lines, zero sorry. If you doubt it, run the compiler yourself — Lean doesn't lie.
The machine-verified counterexample is especially valuable: humans may err in derivations, but when the Lean compiler says "Q.E.D.," that's a fact, not an opinion. With formal proofs, we know our reasoning is error-free at that precise abstraction level; the remaining theory-to-reality gap can be quantified and progressively narrowed.
BAPR isn't perfect — the 41% false-negative rate, the Walker2d ceiling, and missing end-to-end convergence are real limitations. But it embodies an attitude rarely seen in ML papers: not settling for "beat the baseline," but understanding why, under what conditions, and with what mathematical guarantees.
When an algorithm stays safe in a shifting world, and that safety is guaranteed by machine-verified theorems rather than intuition, that's a different tier of trustworthiness — perhaps worth more attention than a 5-percentage-point performance gain.
---