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, and joint_ci.

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.

The report intentionally does not emit threshold pass/fail certificates yet: existing notebooks store LTLf path formulas, not explicit PLTL probability thresholds.

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.