Learning¶

The learning experiments compare reward and safety across ordinary, constrained, shielded, and contract-aware algorithms.

Baselines¶

The repository includes independent and centralized-training baselines:

• IPPO and IQL as unshielded learners,
• IPPO-Lagrangian and IQL-Lagrangian as cost-constrained learners,
• ICPO as a constrained policy optimization baseline,
• MAPPO, Joint PPO, and PQN-VDN as additional cooperative MARL baselines,
• Shielded-IPPO, Shielded-IQL, Shielded-MAPPO, and Shielded-PQN-VDN.

The shielded baselines enforce ordinary local shields. They are useful for measuring how much reward is lost when each agent must be safe against arbitrary teammate behavior.

Contract Learners¶

Contract-IPPO and Contract-IQL use certified contract profiles. They receive a certified library built before training. Each library contains:

• generated candidate local LTL formulas,
• certified contract profiles,
• compiled monitors and shield templates,
• a certification trace for debugging.

The library builder tries the all-t profile first, but that profile is only kept if it certifies. In most current benchmarks the first usable profile already contains formulas that imply or realize the global safety property.

During training, the active profile is passed through reset options. The wrapper then emits masks for the selected profile.

Profile Selection¶

The default selector is a discounted UCB bandit. It tries unvisited certified profiles, records recent team return, and then balances exploitation with exploration.

The selector is not a safety mechanism. It only chooses among profiles that have already been certified.

Metrics To Inspect¶

The most important metrics are:

• episode_return_mean and reward_mean,
• safety_violations_mean,
• contract_profile_index,
• contract_profile_changed,
• contract_permissiveness.

shield_interventions_mean and shield_interventions_agent_fraction_mean are mask diagnostics retained in the export schema. They should remain zero in normal mask-aware shielded and contract runs.

Contract exports also include contract_events, contract_vote_events, and the serialized contract_library.

Interpreting Reward Optimality¶

Contract learners should be judged against ordinary shielded learners, not only against unsafe baselines. A reward-optimal contract run has three properties:

• the global safety metrics remain at zero,
• the selected profile is certified and interpretable,
• return improves over the matching Shielded-IPPO or Shielded-IQL run with the same formula, environment settings, seeds, and training budget.

Current local evidence is strongest for Flatland and Car Platoon, where saved Contract-IPPO and Contract-IQL runs outperform the matching Shielded baselines with zero safety violations. Level-Based Foraging has a positive Contract-IPPO signal against zero-reward Shielded-IPPO, but Contract-IQL still needs a fresh run and likely exploration work. Connector, Pressure Plate, CookingZoo, and RWARE all have certified coordination profiles but need paired reward exports before making a dominance claim.