Skip to content

Experiments

Experiment notebooks share helper code from src/experiments/safety_runs.py. Those helpers build monitors, synthesize shields, construct certified libraries, wrap PettingZoo environments, run repeated seeds, and export metrics.

Experiment Flow

  1. Pick an environment and named global formula.
  2. Build a concrete environment and safety model.
  3. Compile global or per-agent monitor automata.
  4. Synthesize ordinary local shields for shielded baselines.
  5. Build the certified library for Contract-IPPO and Contract-IQL.
  6. Train selected algorithms for each seed.
  7. Export metrics, timings, contract events, and plots.

Certified Library Parameters

The most common contract synthesis controls are:

  • contract_depth,
  • contract_max_candidates,
  • contract_max_profiles,
  • contract_max_active_per_agent,
  • contract_max_atomic_props,
  • contract_max_states,
  • contract_use_model_local_alphabet,
  • contract_use_temporal_form_heuristic,
  • contract_use_model_seed_formulas,
  • contract_candidate_labels.

These control the certification search. They are not reward hyperparameters. The default experiment notebooks use the normal search-built local-obligation path: use_contract_candidates=false and contract_use_model_local_alphabet=true. contract_candidate_labels is an optional normal-search frontier override; it is different from the separate hand-authored candidate-contract profile path used for debugging.

The notebooks also make the ranking priors explicit. They default to contract_use_temporal_form_heuristic=true, which is the preferred ordering prior for normal runs, and contract_use_model_seed_formulas=false, which is the no-seed headline audit setting. If the goal is to maximize reward rather than produce no-seed evidence, enable model seed formulas only as an explicitly labeled seeded-prior ablation and compare it against the no-seed run.

The benchmark notebooks currently default to num_runs=3, total_timesteps=1_000_000, and num_envs=1. By default they run Shielded-IPPO, Contract-IPPO, Shielded-IQL, Contract-IQL, Shielded-MAPPO, and Shielded-PQN-VDN, while the unshielded, constrained, and Joint PPO baselines are available behind their run_* flags.

Reading Results

A good comparison includes both reward and safety. Contract results should be compared against ordinary shielded baselines and unshielded or constrained baselines. Useful questions are:

  • Did the run keep safety_violations_mean at zero?
  • Did the shielded and contract learners keep the mask-diagnostic metrics at zero?
  • Did the selected contract profile change during training?
  • Did Contract-IPPO or Contract-IQL improve return over Shielded-IPPO or Shielded-IQL?
  • Is the selected profile interpretable from its local LTL formulas?

Generated timing files help separate training cost from contract synthesis cost.

Batch Submission Scripts

For Slurm-style batch runs, the helper scripts under notebooks/experiments/scripts submit the script-style marimo notebooks through the local submit helper or sbatch.

bash notebooks/experiments/scripts/csh.sh num_runs=3
bash notebooks/experiments/scripts/csh_env.sh flatland a30 num_runs=1
bash notebooks/experiments/scripts/csh_env_seeds.sh rware a16 run_joint_ppo_shielded=True
bash notebooks/experiments/scripts/csh_env_resume.sh flatland a16 num_runs=3
bash notebooks/experiments/scripts/csh_vis.sh num_runs=3

csh.sh submits all environments to their configured partitions. csh_env.sh submits one environment split across algorithm bundles and owns the run_* flags itself. csh_env_seeds.sh submits one job per run number while keeping the full num_runs export window, so a default three-seed command writes *_0.np, *_1.np, and *_2.np from three separate jobs. csh_env_resume.sh submits only algorithms whose expected run exports are still incomplete, forcing resume mode without restarting complete run sets. csh_vis.sh submits visualization-only jobs with just_vis=True and defaults to min_plot_runs=1, so it plots each algorithm with at least one loadable export inside the requested num_runs window. Pass min_plot_runs=None for strict complete-run plotting. Set DRY_RUN=1 to print commands without submitting them.