Skip to content

Final Policy Satisfaction Verification

Temporal-game experiments support an opt-in final-policy satisfaction check. It samples the frozen learned joint policy after training, and after NashConv auto-resume when auto-resume is triggered.

Config

Shared experiment keys:

  • calculate_satisfaction: disabled by default.
  • satisfaction_eval_episodes: default 1000.
  • satisfaction_delta: default 0.05.

This stage is independent of NashConv. If enabled, it runs once for every trained run, even when calculate_conv=False or calculate_conv_quick=True.

Guarantee

Each rollout yields a Bernoulli objective-satisfaction indicator. For n i.i.d. rollouts and confidence parameter delta, the Hoeffding half-width is:

sqrt(log(2 / delta) / (2 * n))

The reported interval is clipped to [0, 1] around the empirical probability. For the default n=1000, delta=0.05, the half-width is about 0.043.

The verifier also reports intervals that cover all m agents simultaneously with probability at least 1 - delta. It assigns each agent the fixed Bonferroni error budget delta / m, giving joint half-width:

sqrt(log(2 * m / delta) / (2 * n))

This union-bound guarantee does not require agents' outcomes to be independent. It means that every agent's true satisfaction probability is covered simultaneously; it is not the probability that all objectives hold on the same episode.

Artifacts

Each algorithm export directory writes:

  • satisfaction.npy: raw run payloads.
  • satisfaction_report.json: JSON-safe summary with per-run payloads.

Per-run payloads contain:

  • agent_ids, eval_episodes, eval_seed0, delta, confidence, joint_confidence, and success_threshold.
  • per_agent[agent_id] with successes, p_hat, half_width, ci, joint_half_width, joint_ci, and success_bits (one 0/1 character per evaluation episode, in episode-seed order).
  • probability_thresholds: the resolved PLTLf requirement per agent, {"comparator": ">=" | ">" | "<=" | "<", "value": q}.
  • joint_outcome_counts: rollouts per satisfaction pattern, one character per agent in agent_ids order; all_satisfied_count is the all-ones pattern.
  • exclusivity_violations: rollouts on which two objectives declared mutually exclusive by the spec both held (must be 0; see below).
  • certification: the per-seed certificate (next section).

Summaries contain metrics.num_evaluated_runs and per-agent mean/std/min/max empirical satisfaction plus mean marginal and joint interval endpoints. Legacy payloads without joint fields are normalized in memory from their stored delta, episode count, and point estimates when a JSON report is summarized.

Threshold certification

src/verify/certification.py implements the paper's one-sided threshold certificates and their Bonferroni joint version. An objective P_{cmp q}[phi] is certified by an interval [L, U] when L >= q (>=), L > q (>), U <= q (<=), or U < q (<). A seed profile is jointly certified when every agent passes with its joint_ci; the per-run certification block records per-agent marginal_certified/joint_certified, signed margins (L - q for lower bounds, q - U for upper bounds), the profile's joint_margin (minimum over agents), and max_uniform_lower_threshold = min_i L_i^joint, the largest common q at which P_{>=q} would be jointly certified (reported only when every objective is a lower bound).

Thresholds come from TemporalGameExperimentSpec.probability_thresholds: a (comparator, q) pair for all agents or a mapping from agent id to a pair. The default is (">=", 0.5); the eight curated notebooks pass per-agent values from src/experiments/objective_thresholds.py (objective-thresholds.md). Thresholds are distinct from success_threshold, which only binarises terminal monitor rewards. Legacy runs without stored thresholds are certified with the default when summarized. The report-level certification block aggregates counts of certified seeds (num_jointly_certified_runs, per-agent num_joint_certified_runs); averaged interval endpoints remain descriptive and must not be read as a certificate, since averaged endpoints can pass when no seed does.

Certification applies to one frozen profile and one rollout batch. Selecting the best profile using the same rollouts biases the headline certificate; use the confirmatory batch from checkpoint re-evaluation (checkpoint-reevaluation.md) or a family-wise correction (scripts/certification_summary.py reports both task- and campaign-wide Bonferroni counts over all tested seed profiles).

Mutually exclusive objectives

TemporalGameExperimentSpec.exclusive_objective_groups lists agent groups whose objectives cannot hold on the same rollout. Pursuit declares the guard against each intruder (PURSUIT_EXCLUSIVE_OBJECTIVE_GROUPS; groups naming an absent intruder are skipped) and Territory Role Claim declares its two players. Any co-satisfied rollout is counted in exclusivity_violations and printed as a warning: it means the evaluation rollouts or labels are inconsistent, as happened with the Pursuit horizon bug below.

Episode ends in evaluation rollouts

All verification rollouts (rollout_successes_parallel_*) stop at the first step on which any agent reports termination or truncation (rollout_episode_done), matching the trainers, which reset on the same condition. BoolRewardWrapper.agents also returns [] once the wrapper has ended the episode, until reset.

Before 2026-09-30 the loops ran while env.agents: only. Pursuit's objective wrapper truncates at step 100 but the base PursuitEvasion defaulted to max_steps=10000 and never emptied agents at the wrapper horizon, so evaluation kept stepping and re-emitted terminal monitor rewards on every later step. Guard and intruder bits could then both be 1 on one rollout, inflating Pursuit satisfaction and ApxNashConv (estimates of mutually exclusive objectives summed to as much as 1.83). Training was unaffected. The Pursuit env factory now also aligns the base horizon with the wrapper (base.max_steps = wrapper.max_steps_per_episode; observations do not depend on it). Other curated tasks already had matching horizons; re-evaluating them reproduces their stored counts.

Rollout Resource Management

Final satisfaction and NashConv rollouts reuse one environment instance per rollout batch and reset it for each evaluation episode seed. This is important for native PettingZoo gridworlds: repeatedly constructing and closing a fresh environment for every satisfaction episode can grow process memory until PBS kills the Python kernel with a cgroup OOM. The observed failure mode was a marimo message like "kernel died unexpectedly" partway through * final satisfaction, with the PBS .err file reporting Cgroup mem limit exceeded.

The verifier still samples the same episode seed list. The first seed is used to construct the reusable env, then each episode calls reset(seed=episode_seed) before rollout. If an env does not accept reset seeds, the existing safe_reset fallback preserves the previous behavior of using the env's internal reset sequence.