Technisch overzicht: Contract-gebaseerde Compositionele Shielding voor Veilige Multi-Agent Reinforcement Learning

Probleemstelling

In coöperatieve Multi-Agent Reinforcement Learning (MARL) is het waarborgen van veiligheid tijdens training en implementatie uitdagend wanneer globale veiligheidsrestricties niet unilateraal door een enkele agent kunnen worden afgedwongen. In "veilige coördinatieproblemen" hangt de toelaatbaarheid van de actie van een agent af van de niet-stationaire beleid van zijn teamgenoten. Standaardbenaderingen vertrouwen vaak op gecentraliseerde shielding, die een globale veilige actierelatie berekent, of op unilaterale (gefactoriseerde) masking, waarbij elke agent onafhankelijk zijn acties beperkt op basis van worst-case aannames over anderen.

De paper identificeert een kritieke beperking in unilaterale masking: het werpt vaak optimale veilige gedragingen weg die coördinatie vereisen. Zoals geïllustreerd in het motiverende voorbeeld van de paper (Figuur 1), als de veilige actie van Agent A afhankelijk is van het feit dat Agent B een specifieke actie kiest, zal een puur unilaterale mask de actie van Agent A verbieden om veilig te blijven tegen alle mogelijke acties van Agent B. Dit leidt tot een "conservatieve Cartesiaanse decompositie" die veilige, hoog-belonende gecoördineerde gezamenlijke acties uitsluit. Het doel is om decentrale executie te bereiken (waarbij agenten handelen op basis van lokale informatie) terwijl men team-optimale veilige gedragingen herstelt zonder terug te vallen op gecentraliseerde runtime-controle.

Methodologie

De auteurs stellen Contract-Based Compositional Shielding voor, een framework dat een gedeelde globale veiligheidsspecificatie deelt in lokale temporele contracten. De methodologie bestaat uit drie hoofdfasen:

1. Formeel Framework en Aannames

• Globale Specificatie: Veiligheid wordt gedefinieerd door een enkele globale formule $\Phi_{safe}$ in het veiligheidsfragment van Linear Temporal Logic ($LTL_{safe}$).
• Lokale Contracten: De globale specificatie wordt gedecomposed in een tupel van lokale verplichtingen $C = \langle \phi_i \rangle_{i=1}^n$, waarbij elke $\phi_i$ een $LTL_{safe}$-formule is over de lokale alfabet van agent $i$.
• Circulaire Assume-Guarantee: In tegenstelling tot eerdere werken die acyclische afhankelijkheidsstructuren vereisen, staat deze aanpak circulaire aannames toe. Agent $i$ neemt aan dat alle andere agenten $j \neq i$ hun verplichtingen $\phi_j$ nakomen. Deze circulariteit wordt niet opgelost door een vaste volgorde, maar door de gehele tupel simultaan te certificeren.

2. Shield Synthese (Offline)

Het syntheseproces construeert een bibliotheek van gecertificeerde contracten:

• Automata Constructie: Elke lokale verplichting $\phi_i$ wordt gecompileerd naar een deterministische veiligheidsautomaton $A^C_i$ met een set "slechte toestanden" die schendingen vertegenwoordigen.
• Contract Product: Een globale productautomaton wordt geconstrueerd over de toestandsruimte $S \times Q_1 \times \dots \times Q_n$.
• Fixed-Point Certificering: De auteurs berekenen een grootste vast punt (de "rechthoekige winnende regio" $Win^\square_C$) met behulp van een assume-guarantee predecessor operator. Deze regio vertegenwoordigt toestanden waarvanuit een niet-lege Cartesiaanse product van lokale actiemaskers (een "rechthoek") behouden kan worden zodanig dat:
  1. De gezamenlijke actie binnen de winnende regio blijft.
  2. Er geen slechte toestanden worden bereikt.
• Certificeringscriteria: Een contract-tupel is "gecertificeerd" als:
  1. De conjunctie van lokale verplichtingen semantisch de globale veiligheidsdoelstelling impliceert ($C \models^\uparrow \Phi_{safe}$).
  2. De initiële toestand van het systeem binnen de berekende winnende regio ligt.
• Projectie: Zodra gecertificeerd, wordt de winnende regio geprojecteerd om lokale actiemaskers voor elke agent te genereren. Deze maskers zijn "lokaal mask-identificeerbaar", wat betekent dat een agent zijn toegestane acties kan bepalen met behulp van alleen zijn lokale observatiegeschiedenis en de actieve contract-identifier, zonder de maskers van andere agenten te reconstrueren.

3. Leren en Selectie (Online)

• Bibliotheek Constructie: Vóór de training wordt een begrensde zoektocht uitgevoerd die kandidaat contract-tupels enumereert (beperkt door formule-diepte en een eindige taal). Elke kandidaat wordt getest op certificering. De set succesvolle tupels vormt de Gecertificeerde Bibliotheek ($\mathcal{L}_{cert}$).
• Bandit Selector: Tijdens de training selecteert een niet-stationair multi-armed bandit algoritme welk contract uit de bibliotheek moet worden afgedwongen voor een gegeven trainingsblok.
  • Elk contract fungeert als een "arm".
  • De selector optimaliseert voor team return terwijl veiligheid wordt gegarandeerd.
  • Het gebruikt een Discounted Upper Confidence Bound (D-UCB) strategie om zich aan te passen aan het niet-stationaire karakter van het leerproces (naarmale de policies verbeteren, verandert de waarde van verschillende contracten).
• Veiligheidsgarantie: Theorem 3 garandeert dat zolang de selector alleen bij de grenzen van episodes van contract wisselt en altijd een contract uit de vooraf gecertificeerde bibliotheek kiest, het systeem end-to-end veilig blijft.

Belangrijkste Bijdragen

De paper beschrijft vier primaire bijdragen:

1. Decompositie en Compilatie: Een methode om een gedeelde globale $LTL_{safe}$ specificatie te deconstrueren in kandidaat lokale verplichtingen en deze te compileren naar deterministische veiligheidsautomata voor shield synthese.
2. Formele Soundness en Recoverability: Formele garanties voor decentrale shielding gebaseerd op circulaire assume-guarantee redenering en contract-product fixed points. De auteurs bewijzen dat als het optimale veilige deterministische beleid representeerbaar is door een contract in de bibliotheek, het framework dit kan herstellen.
3. Optimalisatie onder Certificering: Een mechanisme gebruikmakend van een begrensde gecertificeerde profielzoektocht en discounted UCB selectie om conservatisme te verminderen. Dit stelt het systeem in staat om contracten te selecteren die hoog-belonende gecoördineerde gedragingen blootleggen zonder de deterministische veiligheid op te offeren.
4. Empirische Evaluatie: Uitgebreide evaluatie over 6 coöperatieve multi-agent omgevingen (inclusief Flatland, RWARE, en Pressure Plate) en 15 algoritmische varianten, wat de effectiviteit van de aanpak aantoont.

Resultaten

De empirische evaluatie vergelijkt de voorgestelde Contract-IPPO en Contract-IQL met standaard MARL algoritmen (IPPO, IQL, MAPPO) en diverse shielding baselines (unilaterale shields, gecentraliseerde shields).

• Prestaties: In omgevingen waar unilaterale gefactoriseerde maskers te conservatief zijn (bijv. RWARE, Pressure Plate, Connector), verbetert de contract-gebaseerde shielding de team reward aanzienlijk, waarbij het convergeert naar de prestaties van gecentraliseerde shields (zoals Shielded-Joint-PPO).
• Veiligheid: Veiligheid wordt structureel afgedwongen; de curves in Figuur 4 meten de behouden return, wat impliceert dat veiligheidschendingen worden voorkomen door de maskers zelf.
• Schaalbaarheid: In de grootste omgevingen overwoog de begrensde zoektocht tot wel 12.001 profielen, waarvan er tot 390 als veilig werden gecertificeerd, wat de haalbaarheid van de offline enumeratie-aanpak aantoont.
• Specifieke Bevindingen: In de "Pressure Plate" omgeving dwongen standaard gefactoriseerde shields de runner om buiten beschermde deurregio's te blijven om veilig te zijn tegen elk mogelijk gedrag van de holder. De contract-gebaseerde aanpak liet de runner toe over te steken door te vertrouwen op de gecertificeerde toezegging van de holders om op hun platen te blijven, waardoor het gecoördineerde optimale gedrag werd hersteld.

Betekenis en Claims

De paper beweert een fundamentele trade-off aan te pakken in veilige MARL tussen decentrale executie en optimale coördinatie.

• Herstel van Coördinatie: De auteurs stellen dat hun methode "team-optimale veilige gedragingen" herstelt die doorga af verloren gaan door puur gefactoriseerde (unilaterale) shields. Door agenten toe te staan te vertrouwen op circulaire aannames die simultaan gecertificeerd worden, vermijdt het systeem de "conservatieve Cartesiaanse decompositie" die veilige gezamenlijke acties wegwerpt.
• End-to-End Veiligheid: Het framework scheidt beloningsadaptatie (leren) van veiligheidsafdwinging (shielding). Het leerproces kan exploreren en optimaliseren binnen de grenzen van vooraf gecertificeerde contracten, wat garandeert dat geen enkel onveilig gedrag wordt toegelaten tijdens training of implementatie.
• Bescheiden Omvang: De paper is bescheiden over haar beperkingen. Er wordt erkend dat het vermogen om het wereldwijde optimum te herstellen afhangt van de representeerbaarheid van het optimale beleid binnen de eindige bibliotheek van lokale contracten. Als de contract-taal niet expressief genoeg is (bijv. de diepte-bound $D$ is te laag) om de noodzakelijke coördinatie te vatten, kan het systeem het wereldwijde optimum niet herstellen. Verder wordt gesuggereerd dat toekomstig werk heuristieken kan verkennen voor het vinden van bijna-optimale contracten zonder volledige enumeratie.

Samenvattend presenteert de paper een rigoureuze, formeel geverifieerde aanpak voor veilige MARL die het mogelijk maakt voor decentrale agenten om effectief te coördineren zonder gecentraliseerde runtime-controle, waarmee de kloof tussen formele verificatie en reinforcement learning optimalisatie wordt overbrugd.