做非平稳控制或鲁棒强化学习的团队终于有了一个理论扎实且可验证的方案——BAPR在稳定期和变化期之间自动平衡保守性，Lean 4形式化验证保证了可靠性，值得研究RL安全性的开发者点开。
现实世界的控制系统常面临分段平稳环境，即动态长期稳定后突然发生模式切换。标准鲁棒强化学习方法面临两难：全局保守策略在稳定期性能浪费，而局部自适应策略在未检测到模式变化时可能导致灾难性失败。本文提出BAPR（贝叶斯遗忘分段鲁棒SAC），将贝叶斯在线变化检测（BOCD）与鲁棒集成强化学习统一。BAPR算子是一个γ-压缩映射，通过冻结信念分布加权模式条件贝尔曼算子的凸组合。论文通过Lean 4形式化验证了尖锐边界：当信念依赖于Q函数时，压缩因子变为γ+λΔ，且当γ+λΔ≥1时压缩失败。BOCD驱动自适应保守机制：检测到变化点后策略变得极度保守，随置信度增长平滑放松，检测延迟为O(log(1/δ))。
BAPR: Bayesian amnesic piecewise-robust reinforcement learning for non-stationary continuous control
Real-world control systems frequently operate under \emph{piecewise stationary} conditions, where dynamics remain stable for extended periods before undergoing abrupt regime changes. Standard robust RL methods face a fundamental dilemma: a globally conservative policy wastes performance during stable periods, while a locally adaptive policy risks catastrophic failure when the regime changes undetected. We propose \textbf{BAPR} (Bayesian Amnesic Piecewise-Robust SAC), which unifies Bayesian Online Change Detection (BOCD) with robust ensemble RL. The BAPR operator -- a convex combination of mode-conditional Bellman operators weighted by a frozen belief distribution -- is a $γ$-contraction. A complementary counterexample, machine-verified in Lean~4, establishes a \emph{sharp boundary}: when beliefs depend on the Q-function, the contraction factor becomes $γ+ λΔ$ (where $Δ$ is the mode reward gap), and contraction fails exactly when $γ+ λΔ\geq 1$. We derive a \emph{component-wise} formal error budget for the abstract operator -- every component machine-verified -- bounding post-switch recovery; the budget applies to the abstract mode-mixture operator and inherits to the implemented shared-critic algorithm only through the frozen-parameter design intuition. All results are formally verified with no \texttt{sorry} (1,145 lines across 3 Lean~4 files, 22 machine-verified theorems). BOCD drives an adaptive conservatism mechanism: the policy becomes maximally conservative after detected change-points and smoothly relaxes as confidence grows, with detection delay $O(\log(1/δ))$. A context-conditioning module trained via RMDM loss provides mode-aware representations from simulator-provided mode IDs at training time and requires no mode labels at deployment.