ROVER: Regulator-Driven Robust Temporal Verification of Black-Box Robot Policies

Dit paper presenteert ROVER, een regulator-gedreven methode voor de temporele verificatie van black-box robotbeleid die prioriteitsgebaseerde STL-specificaties en robuustheidsmetrieken gebruikt om iteratief beleid te verbeteren, wat resulteert in aanzienlijk hogere naleving van veiligheidseisen in zowel virtuele als fysieke navigatiescenario's.

De kern

Stel je voor dat je een zelfrijdende robot hebt die je hebt ingehuurd om een taak te doen, zoals racen in een virtueel spel of rondrijden in een magazijn. Het probleem is: je weet niet hoe de robot in zijn hoofd denkt. Hij is een "zwarte doos". Je ziet alleen wat hij doet (de input) en wat hij oplevert (de output), maar je kunt niet naar binnen kijken om te zien welke code of logica hij gebruikt.

In de echte wereld moeten deze robots veilig zijn. Maar hoe controleer je of een zwarte doos veilig is als je niet mag kijken hoe hij werkt?

Dit is waar het onderzoek ROVER (Regulator-Driven Robust Temporal Verification) om de hoek komt kijken. Hier is een uitleg in simpele taal, met een paar creatieve vergelijkingen.

1. De Regisseur en de Acteur

Stel je een filmset voor.

• De Robot (De Acteur): Hij speelt een rol. Hij kan heel goed rennen, maar soms struikelt hij of botst hij tegen muren.
• De Regisseur (De Regulator): Dit is de persoon die de regels opstelt. In het echte leven is dit een overheidsinstantie of een veiligheidscontroleur. De regisseur mag niet in het hoofd van de acteur kijken (geen toegang tot de code). Hij kan alleen kijken naar de opnames (de rijpaden die de robot heeft gemaakt).

De regisseur zegt: "Ik wil niet dat je tegen de muren loopt, en ik wil dat je niet te snel gaat in bochten." Maar hoe vertaal je dat naar een robot die je niet begrijpt?

2. De "Tijdscheidsrechter" (Signal Temporal Logic)

Vroeger keken controleurs alleen naar het eindresultaat: "Is de robot gevallen? Ja/Nee." Dat is te simpel. Een robot kan 99 keer veilig rijden en dan één keer hard tegen een muur knallen. Of hij kan langzaam en gevaarlijk slingeren voordat hij crasht.

ROVER gebruikt een slimme methode genaamd Signal Temporal Logic (STL).

• Vergelijking: Stel je voor dat je een sportverslaggever bent die niet alleen kijkt of een speler heeft gescoord, maar de hele wedstrijd analyseert.
  • Regel 1: "Je mag nooit sneller dan 100 km/u." (Dit is een regel voor het hele tijdsverloop).
  • Regel 2: "Als je in een bocht komt, moet je binnen 5 seconden weer rechtuit gaan." (Dit is een regel over de volgorde van gebeurtenissen).

ROVER vertaalt deze regels naar een taal die de computer begrijpt, zodat hij elke seconde van de rit kan controleren.

3. De "Veiligheids-meter" (Robustness Metrics)

Hoe vertel je de maker van de robot (de ontwerper) wat er mis is? ROVER gebruikt drie specifieke meters:

1. TRV (Gemiddelde Veiligheid): Hoe veilig is de robot over het algemeen? Is hij meestal rustig of schokt hij vaak?
   • Analogie: Is de auto over het algemeen soepel gereden, of schokte hij de hele rit?
2. LRV (De Ergste Fout): Wat was het slechtste moment in de hele rit?
   • Analogie: Zelfs als je 99 keer veilig rijdt, als je één keer bijna een boom raakt, is dat een slechte LRV. Dit vertelt je: "Kijk uit, hier is het gevaarlijkst."
3. AVRV (Gemiddelde Ernst van Fouten): Als de robot fouten maakt, hoe ernstig zijn die fouten gemiddeld?
   • Analogie: Rijdt hij zachtjes tegen de muur (een klein foutje) of botst hij hard (een groot ongeluk)?

4. De Cyclus: Feedback en Verbetering

Dit is het echte krachtige deel van ROVER. Het is geen eenmalige test, maar een iteratief proces:

1. De Regulator kijkt: Hij laat de robot 100 keer een ritje maken.
2. De Regulator meet: Hij gebruikt de meters (TRV, LRV, AVRV) om te zien waar de robot faalt.
3. De Regulator geeft advies: Hij zegt tegen de ontwerper: "Je robot rijdt te snel in bochten (LRV is slecht) en blijft te lang bij obstakels hangen."
4. De Ontwerper past aan: De ontwerper (die de code wel kent) past de beloningen voor de robot aan. Bijvoorbeeld: "Als je te snel in een bocht gaat, krijg je minder punten."
5. Opnieuw testen: De robot leert opnieuw en rijdt nu veiliger.

Wat hebben ze gevonden?

De onderzoekers hebben dit getest in twee situaties:

1. Mario Kart (Virtueel): Een robot die racet. Voor de verbetering viel hij vaak van de weg en reed hij te snel. Na de ROVER-adviezen reed hij veel rustiger en bleef hij veel vaker op de weg.
2. TurtleBot (Echte robot): Een kleine robot die door een kamer moet. Voor de verbetering maakte hij scherpe, onrustige bochten en bleef hij stilstaan bij muren. Na de verbetering reed hij soepeler en kwam hij sneller bij het doel.

Conclusie

ROVER is als een veiligheidsinspecteur die geen toegang heeft tot de motor, maar wel de rijstijl kan analyseren. Door slimme regels over de tijd te stellen en precies te meten waar en hoe erg een robot faalt, kunnen makers hun robots veel veiliger maken, zelfs als ze de interne werking niet volledig begrijpen of controleren.

Het zorgt ervoor dat robots niet alleen "werken", maar dat ze veilig en betrouwbaar werken, net zoals we dat van een chauffeur in het echte leven verwachten.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "ROVER: Regulator-Driven Robust Temporal Verification of Black-Box Robot Policies" in het Nederlands.

Titel

ROVER: Regulator-Driven Robust Temporal Verification of Black-Box Robot Policies (Regulator-gedreven robuuste temporale verificatie van black-box robotbeleid).

1. Het Probleem

De certificering van autonome robots in de echte wereld wordt steeds complexer, vooral omdat veel systemen "black-box" zijn. Dit betekent dat de interne modellen (perceptie, planning, besturing) niet direct door regelgevers (regulators) kunnen worden ingezien of geanalyseerd.

• Beperkingen van bestaande methoden: Traditionele verificatiemethoden voor white-box systemen (zoals bereikbaarheidsanalyse of model checking) vereisen toegang tot de interne dynamica, wat bij black-box systemen ontbreekt. Bestaande black-box validatiemethoden vertrouwen vaak op statistische schattingen van faalkansen of surrogate veiligheidsmaatstaven. Deze benaderingen missen vaak de nuance van temporele veiligheidsvereisten (gedrag dat zich over tijdreeksen afspeelt, zoals persistentie, sequencing en respons).
• De kernuitdaging: Hoe kan men garanderen dat een black-box robotbeleid voldoet aan strikte, tijd-afhankelijke veiligheidsregels (bijv. "blijf binnen de baan", "versnel niet tijdens een scherpe bocht") zonder inzicht in de interne werking van de controller?

2. Methodologie: ROVER

ROVER introduceert een nieuwe, regulator-gedreven aanpak die de verificatie simuleert zoals deze in de praktijk verloopt: een externe autoriteit evalueert het gedrag op basis van waarnemingen.

• Regulator-in-the-Loop: De methode behandelt de autonomie-stack als volledig ondoorzichtig. De "Regulator" observeert alleen uitvoeringssporen (rollout traces) en evalueert deze tegenover temporale veiligheidsvereisten.
• Signal Temporal Logic (STL): De veiligheidsvereisten worden formeel uitgedrukt in STL. Dit stelt de regulator in staat om complexe, tijd-gebonden regels te definiëren (bijv. "altijd binnen de lijnen blijven" of "uiterlijk binnen 60 stappen herstellen na een afwijking").
• Robuustheidsmetrieken: Om de naleving van deze STL-specificaties kwantitatief te meten, gebruikt ROVER drie kernmetrieken gebaseerd op de robuustheidswaarde ($\rho$):
  1. TRV (Total Robustness Value): Meet de gemiddelde prestatie en de totale veiligheidsmarge over alle traces. Een hogere waarde duidt op betere gemiddelde naleving.
  2. LRV (Largest Robustness Value): Meet de ergste afwijking (het minimum van de robuustheidswaarden). Dit identificeert de kritiekste fout in de dataset.
  3. AVRV (Average Violation Robustness Value): Meet de gemiddelde ernst van alleen de traces die de specificatie schenden. Dit helpt bij het begrijpen hoe ernstig de fouten zijn wanneer ze optreden.
• Iteratief Verbeteringsproces:
  1. De Regulator evalueert een black-box beleid en berekent de metrieken (TRV, LRV, AVRV) voor elke STL-regel.
  2. Op basis van deze scores en domeinexpertise (gewichting van regels) worden kwalitatieve aanbevelingen gedaan (bijv. "beleid verbeteren" of "edge-case analyse").
  3. De "Designer" gebruikt deze feedback om de beloningsfunctie (reward function) van het leerproces (bijv. Reinforcement Learning) aan te passen en het beleid opnieuw te trainen.
  4. Het nieuwe beleid wordt opnieuw geëvalueerd om verbetering te valideren.

3. Belangrijkste Bijdragen

1. Formalisatie van Black-Box Certificering: ROVER biedt een formeel onderbouwde, traject-niveau evaluatie voor black-box controllers, onafhankelijk van interne modeltoegang. Dit vult het gat tussen statistische validatie en formele verificatie.
2. Adaptiviteit en Robuustheid: De methode is getest in twee zeer verschillende domeinen: een virtueel racen (Mario Kart SNES) en fysieke robotnavigatie (TurtleBot3). Het bewijst effectief te zijn onder verschillende taakdynamieken.
3. Gerichte Feedback voor Modelverbetering: In plaats van alleen een pass/fail-score te geven, levert ROVER gedetailleerde, kwantitatieve feedback (via TRV, LRV, AVRV) die ontwerpers helpt om specifieke aspecten van het beleid te verbeteren (bijv. het verminderen van ernst van overtredingen of het verhogen van het gemiddelde veiligheidsmarge).

4. Resultaten

De auteurs hebben ROVER toegepast op zes verschillende STL-specificaties in twee scenario's:

• Scenario 1: Virtueel Racen (Mario Kart)

  • Regels: Snelheidslimiet, op de baan blijven, wachten met versnellen tijdens bochten.
  • Resultaat: Na regulator-gestuurde hertraining steeg het percentage geslaagde specificaties gemiddeld met 43,8%.
  • Voorbeeld: Voor de regel "Blijf op de baan" steeg de naleving van 8% naar 99%. De gemiddelde robuustheid (TRV) verbeterde aanzienlijk, en de ernst van overtredingen (AVRV) nam af.

• Scenario 2: Mobiele Robot Navigatie (TurtleBot3)

  • Regels: Geen scherpe bochten, tijdige voltooiing, niet langdurig bij obstakels blijven.
  • Resultaat: De hertraining leidde tot een verbetering in de gladheid van het pad en een betere naleving van de regels.
  • Real-world Validatie: In een fysieke testomgeving toonde het gepolijste model een 27% verbetering in de tevredenheid van "smooth navigation". Hoewel er een "sim-to-real" kloof was (de echte robot maakte meer bochten dan in de simulatie), was het gedrag van het post-verificatiemodel duidelijk veiliger en vloeiender dan het pre-verificatiemodel.

5. Betekenis en Conclusie

ROVER is een belangrijke stap voorwaarts in de veilige implementatie van autonome systemen.

• Praktische Toepasbaarheid: Het sluit aan bij de realiteit van certificeringsprocessen waar regelgevers geen toegang hebben tot de broncode van AI-modellen.
• Kwalitatieve en Kwantitatieve Synergie: Door formele logica (STL) te combineren met robuustheidsmetrieken, kunnen regelgevers niet alleen zeggen of een systeem faalt, maar ook hoe en hoe ernstig het faalt.
• Iteratieve Cyclus: Het paper demonstreert dat deze feedbacklus leidt tot concrete verbeteringen in het gedrag van robots, zowel in simulatie als in de echte wereld.

Beperkingen en Toekomst: Het proces is nog steeds iteratief en vereist menselijke expertise voor het vertalen van natuurlijke taal naar STL. Toekomstig werk richt zich op het automatiseren van deze vertaling met Large Language Models (LLM's) en het uitbreiden van de methodiek naar zeldzame gebeurtenissen en afdekking (coverage).