FoSeRL: Formal Sequential Robustness Certification for Reinforcement Learning Policies

Sara Taheri; Deep Kumar Ganguly; Jan Křetínský; Majid Zamani

cs.LGOct 3, 2026

FoSeRL: Formal Sequential Robustness Certification for Reinforcement Learning Policies

Authors: Sara Taheri, Deep Kumar Ganguly, Jan Křetínský, Majid Zamani

Organizations: LMU Munich, Germany · TUM, Munich, Germany · Masaryk University, Brno, Czech Republic · CU Boulder, USA

Abstract

Even a few action perturbations can substantially degrade the performance of a deployed decision policy. Certifying the resulting return loss is challenging in stochastic environments, where returns vary even without an attack. We introduce FoSeRL, a framework for certifying deployed RL policies against precommitted, temporally sparse action attacks. The deployed policy is unchanged, with no smoothing or retraining. Certification requires a resettable simulator supporting shared randomness and independent one-step successor queries, but no analytical dynamics model. FoSeRL certifies that an attacked episode loses no more than a prescribed amount of return relative to the same episode unattacked, with at least a target probability and at a user-specified confidence level. Both runs share the initial state and randomness, so the measured loss reflects the attack, not the episode; carrying the running return gap as a state coordinate makes it the terminal value, reducing trajectory-level certification to terminal safety. Time-dependent barrier conditions on the augmented state bound the terminal failure probability: satisfied exactly, they certify every admissible precommitted attack; learned from sampled trajectories and verified on held-out data, they certify the same guarantee under a specified attack-episode setting. Across six stochastic continuous-control environments and three RL policy families (TD3, SAC, and PPO), FoSeRL certifies non-trivial cardinality--magnitude robustness frontiers, achieves substantially larger certified budgets than policy smoothing, and reveals marked robustness differences among policies with comparable nominal performance.

Figures & tables

Panel of Figure 1 — Figure 1: Matched nominal and attacked executions share episode randomness; their accumulated return gap becomes the terminal degradation certified by FoSeRL.

Figure 2: Illustrative Ant rollouts for SAC and PPO in a separate $T\!=\!500$ experiment. Each row shows a nominal rollout, an accepted FoSeRL budget, and a larger uncertified attack at $K/T\!=\!10\%$ . The lower trace shows the running gap $z(t)/\alpha$ ; at $T$ , $z(T)=D_{\mathrm{traj}}$ , and $1$ marks the terminal tolerance. Videos for this and additional case studies are available at this link .

Panel of Figure 3 — Figure 3: Certified degradation tolerance versus attack budget across different settings. Larger tolerances expand the certified budget, whereas denser temporal attacks generally contract the robustness frontier. Markers denote individually verified specifications and connecting lines are visual guides only. ( $\rho=0.90$ , $\beta=0.001$ )

Panel of Table 1 — Table 1: Representative formal certificates at selected $(K/T,\alpha_{\%})$ settings. Direct certification, policy smoothing (PS), and FoSeRL are compared by $b_{\mathrm{cert}}$ , $\rho_{\mathrm{cert}}$ , and runtime (RT, seconds). Direct uses the corresponding benchmark attack and norm specification, whereas PS is evaluated under its native $\ell_{2}$ perturbation setting. All results use $\rho\!=\!0.90$ and $\beta\!=\!0.001$ . FoSeRL remains non-trivial where PS fails (Failures are denoted by “–”).

Appendix figures & tables10 assets

Supplementary material from the paper’s appendix.

Appendix

Parameter	Inv. Pend.	ACC	Unicycle	Hopper	HalfCheetah	Ant
Model	Custom	Custom	Custom	Gym v5	Gym v5	Gym v5
$n_{\mathrm{obs}}$	3	3	3	11	17	105
$n_{x}$	2	3	3	12	18	29
$n_{a}$	1	1	2	3	6	8
$\Delta t$	0.05	0.10	0.10	0.008	0.05	0.05
$T$	200	300	500	1000	500	1000

Appendix

Table 2: Complete experimental specification for the six FoSeRL case studies. For each environment, we report the environment and policy configuration, attack specification, degradation-tolerance grid, certificate architecture, and synthesis/verification sample budgets.

N_{s}

and

M_{s}

denote the synthesis episodes and successor samples, while

N

and

M

denote the corresponding formal-verification sample counts. All formal runs target

\rho=0.90

with

\beta=\beta_{0}=0.001

Figure 5: FoSeRL certified-budget retention $b_{\mathrm{cert}}/b_{\mathrm{emp}}$ across temporal attack-density bins. Points denote individual reported specifications and the blue line connects bin medians.

Figure 6: Complete empirical and certified robustness profiles for all retained RL-policy experiments. Each environment–policy setting is shown as a paired panel: the upper plot gives the FoSeRL-certified frontier and the lower plot the corresponding empirical pre-verification reference. Curves represent the tested temporal attack densities $K/T$ ; the horizontal axis is the attack magnitude $b$ , and the vertical axis is the normalized degradation tolerance $\alpha_{\%}$ . Formal FoSeRL certificates target reliability $\rho=0.90$ with per-specification confidence parameter $\beta=0.001$ . Across settings, larger degradation tolerances generally support larger attack budgets, while denser temporal attacks tend to reduce the admissible magnitude. The gap between the empirical and certified frontiers varies across environments and policies, revealing setting-dependent verification conservatism. Markers denote individually tested specifications; connecting lines are visual guides only and do not certify interpolation or untested budgets.

Figure 7: Fraction of reported settings with a nonzero certified budget for FoSeRL and policy smoothing (PS), grouped by environment–policy pair.

Environment	Policy	$\mathbf{b_{\max}}$	$\mathbf{K}$	$\mathbf{K/T}$	$\bm{\alpha_{\%}}$	$\mathbf{b_{\mathrm{emp}}}$	$\mathbf{b_{\mathrm{cert}}}$		Norm. gap
Environment	Policy	$\mathbf{b_{\max}}$	$\mathbf{K}$	$\mathbf{K/T}$	$\bm{\alpha_{\%}}$	$\mathbf{b_{\mathrm{emp}}}$	FoSeRL	PS	Norm. gap
Inverted Pendulum ( $T=200$ )	SAC	4	7	3.5%	5%	4.00	4.00	0.0198	0.9951
			16	8%	2.5%	2.60	2.00	0.0129	0.4968
			16	8%	5%	3.47	3.00	0.0132	0.7467
			27	13.5%	1%	1.02	0.65	0.0000	0.1625
			27	13.5%	2.5%	1.84	1.50	0.0101	0.3725

Appendix

Table 3: Detailed FoSeRL–policy-smoothing (PS) comparison on aligned environment–policy settings. For each setting, we report the search limit

b_{\max}

, attack cardinality

K

and density

K/T

, normalized degradation tolerance

\alpha_{\%}

, empirical design reference

b_{\mathrm{emp}}

, and the certified budgets returned by FoSeRL and PS. The normalized gap is

\left|b_{\mathrm{cert}}^{\mathrm{FoSeRL}}-b_{\mathrm{cert}}^{\mathrm{PS}}\right|/b_{\max}

. A zero PS entry indicates that no nonzero budget was certified at that specification.

Figure 8: Inverted pendulum (SAC), at $K=27$ (top block) and $K=40$ (bottom), $\alpha=2.5\%$ of $S_{\mathrm{env}}$ , $\rho_{\mathrm{target}}=0.90$ , $\beta=10^{-3}$ . Each block shows the nominal rollout, the rollout at FoSeRL’s certified budget, and a rollout beyond it, with the attacked pole in colour against the nominal in grey. The budget bar contrasts the two certificates; note the scopes differ, smoothing being worst-case over $\|\delta\|_{2}\leq b\sqrt{n_{a}K}$ and FoSeRL distributional under the declared attack law. $D/\alpha$ is signed, so a marginally negative value ( $-0.07$ , top middle) indicates an attack realisation that slightly helped that episode. The third panel of each block is one of the $20\%$ ( $K=27$ ) and $34\%$ ( $K=40$ ) of episodes that breach beyond the certified budget; breaching outside the certified region is the certificate behaving as specified.

Panel of Figure 9 — Figure 9: Certified and uncertified regimes on MuJoCo locomotion, the setting in which neither Kumar et al. [2022] nor Mu et al. [2024] report results. Panels show the nominal rollout, the rollout at FoSeRL’s certified budget, and a rollout beyond it, with the running degradation $D/\alpha$ beneath each. Because the two branches share the noise realisation but diverge after the first perturbation, their termination times differ: in 9(a) the nominal episode terminates at $t=980$ while the attacked one at the certified budget survives to the horizon, and beyond the budget it collapses at $t=186$ . Third panels are drawn from the $20\%$ (Hopper) and $29\%$ (HalfCheetah) of episodes that breach outside the certified region.

Method	Formal	Channel	Budget	Fixed $\pi$	Level	Form	Paired	Resolved
Attacks on deployed policies
FGSM on policies [ Huang et al., 2017 ]	✗	obs	$\ell_{p}$	✓	ep	—	✗	✗
Strategically-timed [ Lin et al., 2017 ]	✗	obs	$(K,b)$	✓	ep	—	✗	✗
Critical-point [ Sun et al., 2020 ]	✗	obs	$(K,b)$	✓	ep	—	✗	✗
MAS action attack [ Lee et al., 2020 ]	✗	act	$(K,b)$	✓	ep	—	✗	✗
Robust training: hardens a policy, certifies none

Appendix

Table 4: Related work, and where FoSeRL differs. Formal : a mathematical guarantee rather than an empirical rate (

\circ

: formal bounds used internally, empirical robustness reported). Channel : what the adversary perturbs — act =executed actions, obs =observations, data =training data, dyn =dynamics/disturbance, kern =transition kernel. Budget : geometry of the attack set —

(K,b)

=cardinality and magnitude,

\ell_{p}

=norm ball at every step,

\ell_{0}

=count only, set =uncertainty set. Fixed

\pi

: the guaranteed object is the deployed policy itself, not a smoothed, retrained, robust-argmax or aggregated surrogate. Level : ep =whole episode, st =per state. Form : tail =

\Pr[\cdot\leq\alpha]\geq\rho

, mean =expected return, wc =worst case. Paired : degradation measured against the same episode/model unattacked. Resolved : the output is a function of state (and time), not a scalar. To the best of our knowledge, the cardinality–magnitude budget appears in the attack literature but in no prior certificate . For FoSeRL, this denotes a state–time witness and diagnostics, not certified conditional reliability at each state.

Method	Problem formulation and certified property	Attack model and main assumptions	Comparable to FoSeRL?
Per-state policy smoothing	Per-decision robustness of the policy map: certifies action agreement at individual observations, with no statement about accumulated trajectory degradation	$\ell_{2}$ ball applied per observation; each visited state certified independently, with fresh sampling at every point and no coupling across timesteps	No
Gaussian policy smoothing	Sequential robustness under actuator-channel perturbation: certifies the same event as FoSeRL, $P(D_{\mathrm{traj}}\leq\alpha)\geq\rho$	Worst case over all $\\|\delta\\|_{2}\leq b\sqrt{n_{a}K}$ via a Neyman–Pearson shift bound, paired by a union bound. Requires noise $\mathcal{N}(0,\sigma^{2}I)$ shared by both branches and entering the same channel as the attack; $\tau$ grid fixed on design data	Yes
ReCePS	Robustness of expected return: certifies a lower bound on $\mathbb{E}[J]$ rather than a per-trajectory event	Observation-space $\ell_{2}$ ball of radius $B$ ; guarantee holds on the mean, not per trajectory. Smoothed policy evaluated at inference	No

Appendix

Table 5: Related formal robustness and certification frameworks, compared against FoSeRL. All three provide formal (high-probability) guarantees; they differ in what is certified and under which perturbation model. Methods with a different problem formulation are listed for completeness but are not used as quantitative baselines.

				FoSeRL		Smoothing
Environment	$K$	$\alpha_{\%}$	$T$	$b_{\mathrm{cert}}$	$\rho_{\mathrm{cert}}$	$b_{\mathrm{cert}}$	$\rho_{\mathrm{cert}}$	Ratio
Pendulum (SAC)	27	2.5%	200	$1.5$	$0.9174$	$1.01\times 10^{-2}$	$0.9000$	$148.5$ – $301.2\times$
Hopper (TD3)	50	2.5%	1000	$1.64$	$0.9724$	$2.00\times 10^{-3}$	$0.9000$	$512.5$ – $1100\times$
HalfCheetah (SAC)	50	10%	500	$0.35$	$0.9132$	$1.70\times 10^{-3}$	$0.9000$	$140$ – $1575\times$

Appendix

Table 6: Formal comparison with the one method addressing the same problem formulation as FoSeRL. All quantities are formally certified rather than empirically estimated, at

\rho_{\mathrm{target}}=0.90

and confidence

1-\beta=0.999

(

\beta=\beta_{0}=10^{-3}

). FoSeRL gives a distributional guarantee; smoothing gives a worst-case guarantee over the

\ell_{2}

ball

\|\delta\|_{2}\leq b\sqrt{n_{a}K}

. One representative cell per environment; the last column is the certified budget ratio over the reported nonzero-PS rows in Table 3

Adversarial Robustness

Adversarial robustness studies how well AI systems withstand deliberately crafted inputs, training-data corruption, and other attacks.

See all 484 papers

Training Verifiably Robust Agents Using Set-Based Reinforcement Learning
Aug 17, 2024Manuel Wendl, Lukas Koller, Tobias Ladner +1RL Control Reinforcement Learning
Technical University of Munich, Germany
Certifying Lower Bounds for Risk-Sensitive Reinforcement Learning under Adversarial State Perturbations
Sep 9, 2026Tong Li, Saunak Kumar Panda, Yisha XiangRisk-Sensitive RL Adversarial Perturbations
Department of Industrial and Systems Engineering, University of Houston, 4302 University Dr, Houston, 77004, TX, USA. · Department of Decision and Information Science, University of Houston, 4302 University Dr, Houston, 77004, TX, USA.
Scenario Generation for Risk-Aware Reinforcement Learning with Probably Approximately Safe Guarantees
Jun 3, 2026Mohit Prashant, Arvind EaswaranControl Barrier Functions Risk-Sensitive RL
Nanyang Technological University

Aug 17, 2024J/K move · Enter open · S save

Training Verifiably Robust Agents Using Set-Based Reinforcement Learning

Manuel Wendl, Lukas Koller, Tobias Ladner, Matthias Althoff

Technical University of Munich, Germany

RL Control Reinforcement Learning Neural Network Robustness Certified Robustness Robust RL

Open paper AskPDF arXiv

Reinforcement learning policies parametrized by deep neural networks have achieved strong performance for continuous control, yet even small input perturbations may lead to unpredictable behavior. This sensitivity limits their use in safety-critical domains, where robustness guarantees are required. Our work addresses this gap between state-of-the-art adversarial training methods and formal verification to train verifiably robust agents. Previous works train networks with individual adversarial perturbations, making them only robust against the specific adversarial attacks used. In contrast, our approach propagates entire perturbed input sets, enclosing all possible adversarial attacks within a single network pass. We leverage this to explicitly penalize the size of the output set (minimizing closed-loop uncertainty) and thereby make the actor robust against all possible attacks. This is realized by the use of set-based policy gradients, where each output within the set has a different gradient, thereby balancing the accuracy and robustness of the network. Doing so, we achieve formal verifiability across different verification frameworks for up to 9 times larger input perturbations compared to standard reinforcement learning and improve certified worst-case performance.

Abstract

Adversarial Robustness

Explore similar work

Training Verifiably Robust Agents Using Set-Based Reinforcement Learning

Certifying Lower Bounds for Risk-Sensitive Reinforcement Learning under Adversarial State Perturbations

Scenario Generation for Risk-Aware Reinforcement Learning with Probably Approximately Safe Guarantees