Probabilistic Shielding¶

The shield sits between a discrete-action 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.

The result is cached as:

shield/transition_shield_bundle.pkl

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 accessible 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 considered levels is available as an ablation. The shield projects successor budgets, executes the action, and sets the next budget from the realized successor. Missing state, action, or successor coverage is treated conservatively.

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.

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.

Learned and True-Policy Shields¶

The learned shield freezes a bundle derived from the learned world and opponent models. TruePolicyTransitionShield instead uses an exact transition graph and periodically rebuilds its bundle from the live opponent policies. It is an evaluation baseline, not a dependency of learned shielding.

Exact Anytime Arbitrary-Opponent Audit¶

The optional run_exact_anytime_diagnostic stage makes a stronger but narrower statement. It keeps every exact (state, focal action, joint opponent action) transition row and takes the worst opponent action, rather than weighting rows by a learned or live opponent policy. An independent raw-edge pass verifies the robust Bellman inequalities, reset support, probability mass, unsafe labels, environment binding, and artifact hashes.

A report marked certified bounds eventual unsafe reachability for one focal agent and one episode, from every reset in an exhaustively declared support, against arbitrary opponent actions in the serialized exact graph bound to the matching environment contract. A certified_on_declared_reset_support report is the same conditional statement for an incomplete or unknown reset support. Here delta_cov=0; it does not cover dynamics or reset states outside the graph. An infeasible report means the converged certificate's robust reset demand exceeds max_risk and must not be used as a runtime guarantee. Read the reported solver gap when interpreting it as evidence about the optimum.

This audit is off by default and performs no RL training or rollouts. Exact graph construction can still be expensive on large gridworlds; see the experiment workflow for environment-specific reporting guidance.

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.