Level-Based Foraging¶

Level-Based Foraging models agents collecting food that may require cooperative loading. The contract benchmark uses a small one-food setting where synchronized loading is useful but unsafe solo loading must be avoided.

Global Safety Formula¶

The default experiment formula is:

avoid_failed_loads = G(!{agent}_failed_load)

In the two-agent experiment, this specializes to:

(G(!agent_0_failed_load)) &
(G(!agent_1_failed_load))

The global monitor rejects any trace containing a failed load for any agent.

Local Alphabets¶

For the default two-agent cooperative-load experiment, the exhaustive contract-local alphabets are:

agent_0:
  agent_0_coop_load_ok
  agent_0_failed_load
  agent_1_failed_load

agent_1:
  agent_1_coop_load_ok
  agent_0_failed_load
  agent_1_failed_load

The diagnostic alphabet can also expose joint_load_ready, food availability, food completion, load attempts, successful loads, adjacency, partner-readiness, and solo-load facts.

Emitted Labels¶

The safety model emits labels for:

• food availability, location, level, and completion,
• agent positions,
• load attempts and successful or failed loads,
• cooperative-load protocol status,
• food adjacency and whether a partner is adjacent to the same food,
• solo-load ability and partner-needed facts.

Contract Intuition¶

Joint LOAD can be high-reward but risky if an agent cannot rely on a teammate being ready. Certified profiles can include cooperative-load obligations or other readiness commitments, reducing the conservatism of robust local factorised shielding. In the current default search, joint_load_ready is diagnostic-only so synthesis does not learn an anti-reward obligation to avoid the loading phase. Contract shielding can outperform the matching Shielded-* baseline when a cooperative-load obligation lets the team take the safe joint LOAD action that an ordinary local shield would mask under worst-case teammate behavior.

Current Contract Profiles¶

With the current core alphabet and experiment synthesis parameters, the no-seed normal search-built feasibility audit certifies 2 nontrivial LBF profiles, 1 of which adds obligations beyond the failed-load formula APs. The canonical reward-relevant profile is profile_0002; it adds a cooperative-load commitment:

agent_0:
G(!agent_0_failed_load & !agent_1_failed_load) &
G(agent_0_coop_load_ok)

agent_1:
G(!agent_0_failed_load & !agent_1_failed_load)

joint_load_ready stays out of the default core alphabet and remains diagnostic-only, which prevents normal search from producing anti-reward profiles such as G(!joint_load_ready). The agent_i_coop_load_ok family is the contract signal most likely to beat ordinary shielding: it separates unsafe solo load attempts from coordinated load attempts, so an agent can take reward-producing LOAD actions with less robust-shield conservatism. The newest local Contract-IPPO exports show positive reward while Shielded-IPPO stays at zero. Older Contract-IQL artifacts can contain larger runtime menus than the canonical no-seed report, so the paired IPPO/IQL experiments should be rerun before treating the edge as final.

Reward-optimality status: high for IPPO pending flagged rerun, weak for IQL. Ordinary shielding masks LOAD at joint-load-ready states because solo or mismatched loading can fail. A cooperative-load contract can permit the safe joint load. The IPPO artifacts show that mechanism beginning to pay off; Contract-IQL remains near zero and should be treated as an exploration or profile-selection issue until rerun.

Reward Function¶

The default experiment is a one-food cooperative loading task:

force_coop = true
normalize_reward = true
penalty = 1.0
player levels = 1, 1
food level = 2

Rewards are only assigned by the loading logic. Each step starts every player's reward at 0. When one or more players choose LOAD while adjacent to the same food, the environment sums the levels of the participating loaders.

If the participating level is below the food level, each participating loader receives -penalty; in the default experiment that is -1.0. If the participating level is high enough, each participating loader receives:

r_i = player_level_i * food_level

With normalize_reward=true, this is divided by:

sum_participating_player_levels * total_spawned_food_level

For the default two-level-1-agents and one-level-2-food setup, a successful joint load gives each agent 0.5. Movement, waiting, collisions, and invalid load actions that are converted to NONE carry no direct reward.

Spaces¶

For the default cooperative-load experiment (field_size=(5, 5), n_agents=2, max_num_food=1, vector observations):

Source Links¶

• Environment implementation
• Formula module
• Labelled safety model
• Experiment notebook