Guarantees and Robustness¶

The learned shield's certificate is exact arithmetic over a model: the learned world model composed with the imagined opponent levels. It is a strong statement about that model and, by itself, no statement about the real game. This page sets out what each certificate in the repository claims, what it assumes, and which tool checks or relaxes each assumption.

Every offline tool reads existing artifacts. Commands are collected in Analysis and Audits.

What the Deployed Certificate Says¶

For each retained opponent level l >= f (the monotone floor), OmSh induces a focal-agent kernel P_l(s' | s, a) and certifies the executed action against the worst of them. Within that model, the carried budget is a supermartingale bound on eventual unsafe reachability from reset.

Mapping the model claim to the real game needs a coverage condition at every step:

• A1, world model. The learned kernel is within eps_WM of the true kernel on the rows used.
• A2, opponent. Some retained level l >= f_t is within eps_OM of the real opponent's action law at the current state.

The shield is worst-case over every retained level, but coverage only needs one of them to be close. A2 fails if the opponent resembles no level (misspecification) or if the floor has risen past the level it resembles (overshoot). The unpadded deployed shield assumes eps_WM = eps_OM = 0; the tools below either measure how far that is from true or pay for a positive radius.

Exact Arbitrary-Opponent Certificate¶

run_exact_anytime_diagnostic=true replaces both learned models with the exact graph and replaces the opponent model with the worst opponent action in every row. Because it keeps every (state, focal action, joint opponent action) row, no opponent assumption is needed.

An independent raw-edge validator re-checks the robust Bellman inequalities, reset support, probability mass, unsafe labels, environment binding, and artifact hashes. The report's status determines the claim:

Only a certified status with solver_converged=true, certificate_inductive=true, and reset_feasible=true supports the guarantee. Here delta_cov = 0 relative to the serialized exact graph; the claim does not cover dynamics or reset states outside it. Gathering and Markov Stag Hunt use sampled reset states, so their certificates are conditional on that list.

Bertrand and Chicken build their graph rows by stepping the live simulator, so their certificates are simulator-bound. The gridworld builders use separate successor functions, so a gridworld certificate is relative to the serialized graph until those functions are audited against the simulator.

In the retained suite, the matrix games and Congestion have a surely-safe action from reset, so the certificate is feasible against arbitrary opponent actions. Pursuit is the negative control: an arbitrary opponent can make the reset budget infeasible.

Count-Centred Ambiguity Sets¶

src/shield/ambiguity/ builds a statistically valid set of kernels instead of a point estimate. Each row's set is a total-variation ball around the empirical transition counts, with a time-uniform radius:

U(s, a) = { P on Succ(s, a) : TV(P, P_counts(. | s, a)) <= eps_CS(s, a) }

The radius shrinks with the row's visit count and is 1 (the whole simplex) on unvisited rows. A singleton-support row is structurally known and has radius 0. The miscoverage budget delta_cov is chosen, not measured; it is spread across rows and times, and the shield then runs at p_shield = p_total - delta_cov.

Two rules keep the coverage claim valid:

• the ball is centred on counts, never on the neural kernel; the learned model stays the nominal model for imagination and rewards;
• the support is the legal successor set, including successors not yet observed, so the true kernel is always inside its own ball.

The Stage 2B study (scripts/certified_ambiguity_study.py) measures certificate width and feasibility across sample budgets and delta_cov. The exact graph is consulted only afterwards, as a diagnostic of realized coverage.

Padded OmSh¶

shield_padding_radius=r runs the learned shield against a total-variation ball of radius r around each retained level's row, inside the simplex over that row's listed support:

W_f(s) = min_a  max_{l >= f}  sup_{P in B_r(P_l(. | s, a))}  E_P[W_f]

Padding does not establish coverage; A1 and A2 remain assumptions. What it changes is which assumption the guarantee needs. Let E be the event that, at every step, the world-model error is at most eps_WM and some retained level is within eps_OM of the opponent. With r >= eps_WM + eps_OM (clipped at 1), the triangle inequality puts the true next-state law inside the padded set on E, provided the true transitions are supported on the listed successors. Then P(unsafe) <= p + delta_cov whenever P(E) >= 1 - delta_cov, for the shield that actually runs.

Three parts change together so the certificate stays inductive:

1. the floor bounds become the padded fixed point;
2. each action's cost becomes the padded worst case over retained levels;
3. successor budgets are allocated with a padded egalitarian fill.

r = 0 (the default) is exactly the deployed shield. The on-disk bundle cache stays the point bundle; padding is applied in memory. Padding is rejected with shield_opponent_mode=bayesian_mixture, because the construction is worst-case over every retained level. A padded run is labelled, for example, OmSh-Monotone-Padded-r0.05 with artifact stem ippo_shielded_padded_r0p05, so several radii can share one tagged directory. Campaign summaries report it as a variant, never as the primary OmSh row.

Padding shrinks the admissible set. Where some action keeps its whole listed support safe under every level (the matrix games, Gathering, Markov Stag Hunt, and Congestion), any radius up to 1 stays feasible and only reward is lost; at r = 1, Congestion collapses to the uncoordinated policy. Elsewhere the robustness margin bounds the radius: beyond it the padded reset demand exceeds the budget and the shield is infeasible. Pursuit's margins are only about 0.002, 0.006, and 0.021 at floors 0, 1, and 2.

Robustness Margin¶

scripts/compute_robust_margins.py asks the converse question without training: what is the largest uniform radius whose padded certificate still fits the campaign budget? Per environment, shielded role and floor, it reports:

• the nominal reset demand (radius 0 reproduces the cached bundle);
• the margin, bracketed by sound lower and upper values;
• the row-by-row TV between the learned and exact-world-model bundles, which is the world-model part of eps_WM.

A margin far below the measured world-model error means a uniform padded certificate around the learned kernel is not a usable instantiation at that budget. scripts/pursuit_rate_radii.py gives Pursuit tighter, per-row world-model radii from a time-uniform confidence box on its two slip rates, exploiting that Pursuit's rules are known and only its rates are not.

Closest-Retained-Level Opponent Gap¶

A2 needs, at every step,

g_t = min_{l >= f_t} TV(real opponent law at s_t, pi_l(. | s_t)) <= eps_OM

The real law is each opponent's policy within the action mask it samples under, so a shielded opponent is measured as it actually acts. The gap is available two ways:

• log_opponent_level_gap=true records it during IPPO training on a sample of rollout states, without the heavy traces that verbose_data also enables;
• scripts/measure_opponent_level_gap.py replays a tagged condition's frozen evaluation and measures it on the final policies.

The script also reports how often a level below the floor was strictly closer, which is the overshoot failure mode of A2.

Risk-Dominance Audit¶

The anytime bound only uses coverage through one step inequality: the true expectation of the certificate the shield commits to must not exceed the carried budget. With step excess eta_t = max(0, E_true[W_t] - q_t),

P(unsafe by T) <= p + E[ sum_{t < T} eta_t ]

scripts/audit_certificate_dominance.py evaluates eta_t along the frozen evaluation, using the exact graph and the opponents' frozen masked policies. --kernel learned swaps in the learned world model to separate world-model error from opponent error. Zero observed excess makes the plug-in estimate of the bound equal to p, without any coverage assumption.

This is an audit of one frozen deployment with a sample-average expectation. It is a plug-in estimate, not a certificate known before deployment, and zero observed excess does not prove eta_t = 0 almost surely.

Pure Versus Randomised Shields¶

The theory's permissiveness result is for a randomised shield that samples an action and a successor-budget vector jointly. The deployed shield restricts itself to pure actions, which is sound but not complete. scripts/compute_mixed_values.py solves both operators per floor and reports the reset demand under each, the bound d on their difference, and the permissiveness loss the theorem implies for the pure certificate.

With one retained level their certificate values coincide, and the floor usually reaches the top level early in training. On the campaign bundles the mixed certificate values equal the pure ones (d = 0) in five of the six environments; only Pursuit is looser. Runtime admissible sets can still differ, because a randomised shield can mix actions within one step's budget.

That remaining runtime freedom is what the two-action mixed mode (shield_action_mode=egalitarian_mixed) tests. Spending the whole budget removes the slack that otherwise absorbs opponent-model error: on the campaign seeds it broke the safety gate in Bertrand and Chicken and lost reward in Gathering and Markov Stag Hunt, so it is an ablation rather than the default.

Further Reading¶

• Probabilistic Shielding for the runtime mechanics these certificates sit on.
• Final-Policy Evaluation for the frozen-policy measurements the audits replay.
• Maintainer notes: exact anytime certificate, ambiguity sets, robustness margin and padding, Pursuit slip-rate radii, opponent gap, and randomised shield.