Probabilistic Shielding¶

The shield sits between a policy and the environment. The policy proposes an action; the shield either certifies it under the current budget or executes a safer replacement.

Offline Bundle Construction¶

The learned path loads wm/env_transition_graph.pkl and om/iop_stack.pt, then builds one focal MDP per opponent reasoning level. For each level, sound value iteration computes lower and upper bounds on the minimum probability of eventually reaching an unsafe state.

Unsafe nodes are fixed to one, an almost-sure safe set is fixed to zero, lower bounds rise, upper bounds fall, and missing probability mass goes to an explicit unsafe sink. Runtime decisions use the conservative upper bounds. For every floor f, the bundle also stores the robust floor-wise certificate W_f: the value that must hold against every level l >= f at once.

The result is cached as:

shield/transition_shield_bundle.pkl
shield/transition_shield_bundle_player_<i>.pkl   # additional shielded roles

Cache identity includes the graph and opponent checkpoint metadata, focal agent, environment state/action shape, safety implementation, value-iteration parameters, and shield semantics version.

Runtime State and Decision¶

The ordinary TransitionShield leaves every base action space unchanged. By default, it augments the focal observation with two scalars:

flatten(base observation) || current safety budget || opponent-level floor

At each step it checks the proposed pure action against every retained opponent level. A feasible proposal is kept. Otherwise the shield chooses the highest aggregated predicted reward among budget-admissible actions, with lower aggregated risk as a tie-breaker. Bayesian expected reward is the default; minimum reward across retained levels is available as an ablation. The shield then projects successor budgets, executes the action, and sets the next budget from the realized successor. Missing state, action, or successor coverage is treated conservatively.

IPPO samples only within the shield's admissible set: the trainer masks the policy logits with the shield's action mask before sampling. A frozen shielded policy is therefore evaluated with the same masks.

The optional parameterized wrapper instead learns a pairwise primitive-action distribution, successor-budget allocation, or both. Its robust projections are environment dynamics, so PPO stores and scores the policy's exact augmented action rather than the subsequently sampled primitive action.

Opponent-Level Floor¶

The floor is monotone within one shield instance. When the opponent posterior supports a higher level for shield_patience consecutive successful updates, the floor rises by one. The candidate evidence counter survives environment resets; shield_patience=0 raises eagerly. The default is 64.

The posterior mode is unstable early in training, so at patience 64 the floor reaches the top level within a few thousand steps in most environments. Larger patience delays the first raise. A predeclared floor-patience screen and follow-up sweep (64 against 512, 1024, 2048, and 4096) are reported as ablations; see the patience screen protocol.

This is the default shield_opponent_mode=monotone_floor. Experiments can also select all_levels, which never removes a level, or bayesian_mixture, which uses the posterior-weighted transition and appends the posterior to the focal observation. Bayesian mixing is a model-relative ablation rather than a worst-case guarantee over each opponent level. shield_reward_mode=bayesian is the default reward ranking; robust ranks by minimum reward across the levels considered. In both cases reward only ranks actions that already pass the safety constraint.

credible_floor is a middle ground: it chooses the largest monotone suffix containing the configured posterior mass, then remains worst-case robust over every level in that suffix. With the default summable schedule, the 5% tail budget is spread over all opponent observations; fixed instead gives a 5% pointwise suffix without a 5% infinite-horizon guarantee. This claim depends on calibrated level posteriors, monotone true level progression, and the usual learned-model/coverage assumptions. The posterior-tail allowance is additive to the shield's reachability budget rather than automatically deducted from max_risk.

Coordinated Multi-Role Shielding¶

MultiAgentTransitionShield protects two or more agents in the same environment step. Each protected role owns a separate TransitionShield controller, opponent model, posterior, monotone floor, and carried budget. The wrapper:

1. evaluates every role's proposal from the same pre-state,
2. resolves every replacement,
3. steps the base game once with the final joint action, and
4. updates every controller from that realized transition, using the executed primitive joint action rather than any pre-projection proposal.

Nesting single-role wrappers is not equivalent. The outer wrapper would see another agent's augmented proposal rather than its executed action, and the result would depend on wrapper order.

Congestion and Markov Stag Hunt expose this through shielded_agent_ids=player_0,player_1, which currently requires shield_action_mode=pure. Each extra role needs its own opponent model, trained with focal_idx=<i> (see Opponent Modelling). The Congestion campaign shields both vehicles. Per-agent episode rows are exported to tables/<artifact>_per_agent_episodes.csv.gz.

Each role's certificate is still a certificate inside its own learned model. Shielding the modelled opponent changes its live policy, so a joint run is empirical evidence about joint shielding rather than a new arbitrary-opponent theorem.

Padded Certificates¶

shield_padding_radius=r certifies every action against a total-variation ball of radius r around each retained level's row instead of the row itself. If the world-model error plus the opponent gap stays within r, the anytime guarantee then covers the shield that actually runs; that bound is still an assumption, not something padding establishes. See Guarantees and Robustness for the construction and its reporting labels.

Learned and True-Policy Shields¶

The learned shield freezes a bundle derived from the learned world and opponent models. TruePolicyTransitionShield (IPPO-TrueShielded) instead uses the exact transition graph and periodically rebuilds its bundle from the live opponent policies. It needs no WM or OM artifacts.

TrueShielded is an oracle reference, reported beside the primary methods: it has information no deployed agent has. Comparing it with the learned shield separates world- and opponent-model error from the shielding rule itself. Run it for every environment and agent count you report.

The exact arbitrary-opponent certificate is different again. It does not weight opponent actions by any policy; it takes the worst one in every row.

Telemetry¶

minimal debug mode reports overrides, proposed/final risk, floor, levels considered, missing coverage, and decision reason. verbose mode adds per-action risks, mixture values, budgets, successor projections, convergence gaps, state keys, and a bounded in-memory trace. LabelledEnv aggregates the main shield fields into each EpisodeLog. Credible-floor telemetry also reports the scheduled allowance, posterior mass excluded/retained by the irreversible floor, posterior-tail constraint misses, and the nominal summable additive risk quantity. These are posterior diagnostics, not delta_cov.