Technische Samenvatting: Waardefuncties als Supermartingale Certificaten

Probleemstelling

De verificatie van stochastische systemen tegen $\omega$-reguliere eigenschappen (inclusief Linear Temporal Logic, LTL) over algemene toestandsruimten (eindig, aftelbaar oneindig en continu) berust doorgaans op supermartingale certificaten. Dit zijn reële functies die specifieke bewijsregels voldoen en dienen als wiskundige garanties voor de bijna-zekere voldoening van een specificatie. Het synthetiseren van deze certificaten is echter uitdagend; bestaande methoden vertrouwen vaak op beperkte optimalisatie, wat niet goed schaalt naar grote of continue toestandsruimten.

Daartegenover staat dat Reinforcement Learning (RL) breed wordt toegepast voor het synthetiseren van policies voor $\omega$-reguliere taken. Hoewel RL-methoden de kans op voldoening kunnen maximaliseren, missen ze doorgaans formele garanties dat een getrainde (niet-optimale) policy de specificatie met een bepaalde waarschijnlijkheid voldoet, met name buiten eindige toestands- en actieruimten. Er bestaat een kloof tussen de theoretische machinerie van supermartingale verificatie en de praktische machinerie van RL-policy evaluatie.

Methodologie

Dit artikel vestigt een nieuwe theoretische verbinding tussen de waardefunctie van een policy in een gedisconteerde RL-setting en Streett supermartingale certificaten. De kernhypothese is dat onder specifieke beloningsontwerpen de waardefunctie $V^\pi$ van een policy $\pi$ die een LTL-specificatie bijna-zeker voldoet, een geldige Streett supermartingale codeert.

De auteurs stellen twee afzonderlijke beloningsontwerpen voor om dit te bereiken:

1. Beloningsontwerp 1 (Kennis van Absorberende Sets):

   • Vereiste: Kennis van de absorberende sets geïnduceerd door de policy (specifiek de grootste absorberende deelverzameling van het complement van de unie van de Streett-paar sets).
   • Mechanisme: De beloning wordt ingesteld op 1 wanneer het proces de doelset $B$ of een absorberende set betreedt van waaruit noch $A$ noch $B$ opnieuw bezocht kan worden.
   • Theoretische Basis: De waardefunctie $V^\pi$ vertegenwoordigt de verwachte gedisconteerde som van deze beloningen. Door het certificaat $W(s) = C - V^\pi(s)$ te definiëren (waarbij $C$ een constante is gerelateerd aan de discontfactor), bewijzen de auteurs dat $W$ voldoet aan de Streett supermartingale condities: het neemt strikt af in verwachting wanneer men in $A \setminus B$ is (door uniforme grenzen op hittijden) en blijft elders niet-toenemend.

2. Beloningsontwerp 2 (Alleen Specificatiekennis):

   • Vereiste: Alleen kennis van de specificatie (het Streett-paar $(A, B)$), zonder de noodzaak van kennis over de specifieke absorberende sets van de policy.
   • Mechanisme: Dit ontwerp maakt gebruik van een toestandsafhankelijke discontfactor $\Gamma(s)$ en een beloningsfunctie die positieve beloningen toekent voor het bezoeken van $B$ en negatieve beloningen voor het bezoeken van $A \setminus B$.
   • Theoretische Basis: De discontfactor wordt ingesteld op $\gamma < 1$ wanneer beloningen niet nul zijn en op 1 anders. Onder een "positieve recurrentie-grens" aanname (die het verwachte aantal stappen in $A$ vóór het raken van $B$ beperkt), codeert de waardefunctie eveneens een supermartingale. De ratio van positieve naar negatieve beloningen wordt afgestemd om ervoor te zorgen dat het certificaat niet-negatief en strikt afnemend blijft waar vereist.

Beide benaderingen worden bewezen te gelden voor eindige, aftelbaar oneindige en continue toestandsruimten. De bewijzen steunen op lemma's die waardefuncties relateren aan eerste hittijden en de verwachte een-staps veranderingen in waarde.

Belangrijkste Bijdragen

• Theoretische Brug: Het artikel bewijst dat de waardefunctie van een policy die een LTL-specificatie voldoet een geldig Streett supermartingale certificaat is onder passende beloningsontwerpen (Theorem 1 en 2).
• Twee Beloningsschema's: De auteurs bieden twee verschillende methoden aan voor het construeren van deze beloningen: één die gebruikmaakt van policy-specifieke absorberende sets (Theorem 1) en één die uitsluitend steunt op de structuur van de specificatie met toestandsafhankelijke discounting (Theorem 2).
• Generaliteit: De resultaten zijn niet beperkt tot eindige MDP's; ze zijn van toepassing op algemene toestandsruimten, waarmee zij een gat vullen in de bestaande RL-gebaseerde verificatie die vaak een gebrek heeft aan formele garanties voor oneindige of continue ruimten.
• Experimentele Validatie: De auteurs valideren de theorie op eindige Markov Beslissingsprocessen (MDP's) met behulp van een grid-world omgeving. Zij synthetiseren certificaten voor diverse LTL-specificaties die het Manna-Pnueli hiërarchie beslaan, verifiëren de supermartingale bewijsregels en controleren de voldoeningskansen met de PRISM model checker.

Resultaten

• Experimentele Verificatie: In de grid-world experimenten hebben de voorgestelde beloningsontwerpen succesvol geldige certificaten gesynthetiseerd voor policies die aan de specificaties voldeden (waarschijnlijkheid van voldoening = 1.0). Voor policies die de specificaties niet voldeden, faalden de bewijsregels (ongeldige certificaten) en bevestigde PRISM dat de voldoeningskansen strikt kleiner dan 1 waren.
• Consistentie: De experimentele resultaten komen perfect overeen met de theoretische garanties, wat aantoont dat de waardefunctie-benadering zowel voldoende als niet-voldoende policies correct identificeert.
• Beperkingen in Experimenten: De huidige experimenten zijn beperkt tot eindige MDP's waarbij waardefuncties exact berekend kunnen worden via lineaire systemen. Het artikel merkt op dat het uitbreiden hiervan naar oneindige/continue ruimten met parametrische benaderingen (bijv. neurale netwerken) een onderwerp is voor toekomstig werk.

Betekenis en Claims

Het artikel claimt een "geprincipierde route naar certificaat-synthese via RL" te openen. Door het probleem van het vinden van supermartingale certificaten (traditioneel een probleem van beperkte optimalisatie) te herformuleren als een probleem van policy evaluatie gevolgd door een certificaat check, suggereren de auteurs een pad om verificatie te schalen naar grote en continue toestandsruimten met behulp van data-gedreven RL-methoden.

De auteurs benadrukken dat hoewel de theorems voldoende voorwaarden bieden voor de waardefunctie om een certificaat te zijn, het certificaat zelf geldig is als de bewijsregels standhouden, ongeacht of de aannames van de theorems (zoals uniforme hittijdgrenzen) onafhankelijk geverifieerd zijn. Dit maakt een praktische workflow mogelijk: een policy trainen, de waardefunctie schatten en de supermartingale condities direct verifiëren.

Het artikel positioneert dit werk als een fundamentele stap richting gecertificeerde reinforcement learning, waarbij getrainde policies formeel geverifieerd kunnen worden voor $\omega$-reguliere eigenschappen buiten eindige toestandsruimten, waardoor de kloof tussen de schaalbaarheid van RL en de strengheid van formele verificatie wordt overbrugd.