Technische Samenvatting: Schalen van observatiebewuste planning in onzekere domeinen

Probleemdefinitie

Het artikel behandelt het Optimale Observatieprobleem (OOP) in de context van Partially Observable Markov Decision Processes (POMDP's). De kern van de technische uitdaging ligt in het bepalen welke sensormogelijkheden (observaties) op een agent in onzekere domeinen moeten worden ingezet om te waarborgen dat een taak haalbaar is, zonder prohibitieve hardware- of verwerkingskosten te veroorzaken.

Formeel, gegeven een onderliggend Markov Decision Process (MDP) $M$, een budget $B$, en een beloningstijl $\tau$, vraagt het OOP of er een observatiefunctie $obs$ bestaat (die toestanden afbeeldt op een verzameling observaties met kardinaliteit $\le B$) zodanig dat de minimale verwachte beloning van het resulterende POMDP $\le \tau$ is.

Hoewel het algemene OOP onbeslisbaar is, richt het artikel zich op twee beslisbare fragmenten:

1. Sensor Selectie Probleem (SSP): Een variant waarbij observaties binair zijn (aan/uit) voor specifieke locatiesensoren.
2. Positieve Observatieprobleem (POP): Een variant die positionele strategieën overweegt (acties hangen alleen af van de huidige observatie, niet van de geschiedenis).

Vorig werk van Konsta et al. [19] formaliseerde deze problemen en reduceerde ze tot Typede Parametrische Markovketens (tpMC's), die werden opgelost via SMT-gebaseerde parametersynthese. Deze aanpak kampt echter met schaalproblemen bij grotere instantiegroottes.

Methodologie

De auteurs stellen een tweeledige aanpak voor om de oplossing van OOP-fragmenten te schalen:

1. Verbeteringen aan SMT-gebaseerde Parametersynthese

Op basis van de tpMC-reductie uit [19] verfijnen de auteurs de SMT-encoding om de prestaties van de solver te verbeteren (specifiek met Z3):

• Natieve Booleaanse Encoding: In plaats van reële parameters beperkt tot $\{0,1\}$ te gebruiken, vervangen de auteurs deze door native Booleaanse variabelen. Dit maakt gebruik van SAT-propagatie en vermindert de overhead van niet-lineaire rekenkunde.
• Beperkingenverlichting:
  • Budgetherstel: Een twee-trapsbenadering "verlicht-en-repareer" waarbij de solver eerst een oplossing vindt die de budgetbeperking negeert, en vervolgens probeert deze te verfijnen om aan het budget te voldoen.
  • Invariant Bovenlimiet: Het vervangen van exacte Bellman-vergelijkingen door ongelijkheden ($v_s \ge \text{Bellman}(v_s)$). Dit zoekt een conservatieve overbenadering van de verwachte beloning, wat voldoende is voor haalbaarheidscontroles waarbij de drempel $\tau$ niet noodzakelijk de optimale minimumwaarde is.
• Volgorde van Asserties: Empirische tests toonden aan dat de volgorde van SMT-asserties de prestaties significant beïnvloedt; de auteurs identificeerden een optimale volgorde die andere permutaties overtreft.

2. Heuristische Decompositie via POMDP-Orakels

Omdat het oplossen van de volledige tpMC-encoding voor elke kandidaat-observatiefunctie inefficiënt is, introduceren de auteurs een decompositieparadigma. In plaats van het globale optimalisatieprobleem direct op te lossen, doorzoeken ze de ruimte van observatiefuncties met behulp van "orakels" om kandidaten te evalueren.

• Orakels: Het artikel maakt gebruik van twee soorten orakels om een kandidaat-observatiefunctie te evalueren:
  1. SMT-Orakel: Een vereenvoudigde tpMC-encoding waarbij observatievariabelen zijn vastgezet, wat de complexiteit verlaagt.
  2. PMC-Orakel: Integratie met de probabilistische modelchecker Storm om verwachte beloningen te evalueren.
• Atomaire Onderscheidbaarheidsgroepen: De auteurs definiëren equivalentierelaties tussen toestanden op basis van hun "optimale handtekeningen" (de verzameling optimale acties in het onderliggende MDP). Toestanden met identieke optimale handtekeningen vormen atomaire onderscheidbaarheidsgroepen.
• AG-algoritme (Heuristische Enumeratie):
  • Het algoritme partitioneert de verzameling atomaire onderscheidbaarheidsgroepen in observatieklassen.
  • Het hanteert een rangschikkingsheuristiek gebaseerd op equivalentiescores (hoeveel toestanden in een klasse een gemeenschappelijke optimale actie delen) en strategiebeperkingen (hoeveel actieprobabiliteiten kunnen worden vastgezet op 0 of 1).
  • Het algoritme evalueert kandidaten in aflopende volgorde van veelbelovendheid. Als een kandidaat aan de drempel voldoet, retourneert het de oplossing; anders gaat het door naar de volgende.
  • Deze aanpak is correct en compleet voor specifieke topologieën (Lijn, Labyrint, Rooster) onder bepaalde budgetvoorwaarden, hoewel deze over het algemeen incompleet is omdat het atomaire groepen niet splitst.

Belangrijkste Bijdragen

1. Geoptimaliseerde SMT-encodings: De auteurs ontwikkelden native Booleaanse encodings en invariant-verlichtingen die de prestaties van de oorspronkelijke parametersynthese-aanpak verbeteren met ongeveer 3 ordes van grootte in runtime en het oplossen van instanties mogelijk maken die ~75 keer groter zijn.
2. Decompositieparadigma: Ze introduceerden een nieuwe methode voor het oplossen van OOP-instanties door het probleem te decomponeren in de enumeratie van observatiefuncties die via orakels worden geëvalueerd, in plaats van een monolithisch SMT-probleem op te lossen.
3. Heuristische Enumeratie (AG-algoritme): Een specifiek algoritme dat staatsequivalentie en optimale actiehandtekeningen benut om de zoekruimte te prioriteren. Deze methode verbetert de geavanceerde SMT-aanpak met 3 ordes van grootte in runtime en schaalt tot instanties die 100 keer groter zijn.
4. Empirische Validatie: Uitgebreide benchmarks op standaardmodellen (Rooster, Labyrint, Lijn) tonen aan dat de voorgestelde methoden de baseline uit [19] en de eigen intermediaire SMT-verbeteringen van de auteurs aanzienlijk overtreffen.

Resultaten

Het artikel presenteert experimentele resultaten die de oorspronkelijke aanpak [19], de geavanceerde SMT-aanpak (Sectie 3) en de heuristische decompositie-aanpak (Sectie 5) vergelijken:

• Runtime: Het AG-algoritme vermindert de oplostijd met factoren van $10^3$ ten opzichte van de geavanceerde SMT-methode. Bijvoorbeeld, een Rooster-instantie (G(20)) die bij SMT een time-out kreeg of ~30 seconden duurde, werd door AG in milliseconden opgelost.
• Schaalbaarheid:
  • SMT-Verbeteringen: Loste instanties op met tot ~10.000 toestanden (Lijn) en ~1.296 toestanden (Rooster) voor deterministische strategieën, vergeleken met respectievelijk ~377 en ~96 in de baseline.
  • AG-Decompositie: Loste instanties op met tot 200.001 toestanden (Lijn) en 160.801 toestanden (Rooster) voor deterministische strategieën.
• Gestochastische Strategieën: De verbeteringen zijn ook significant voor gestochastische strategieën, hoewel deterministische strategieën over het algemeen grotere schalingsfactoren opleveren vanwege de effectiviteit van Booleaanse encoding.

Betekenis en Claims

Het artikel beweert dat door het combineren van symbolische (SMT) en sub-symbolische (heuristische decompositie/orakelgebaseerde) technieken, het mogelijk is om de oplossing van beslisbare fragmenten van het Optimale Observatieprobleem te schalen naar maten die eerder als onhandelbaar werden beschouwd.

De auteurs benadrukken dat hun werk de focus verschuift van het oplossen van de volledige tpMC-encoding naar het intelligent doorzoeken van de ruimte van observatiefuncties. Ze stellen dat hun op heuristieken gebaseerde enumeratie-algoritme correct is en, voor de bestudeerde specifieke topologieën (Lijn, Labyrint, Rooster), compleet lijkt te zijn voor budgetten groter dan of gelijk aan het minimale positionele budget.

Het artikel concludeert bescheiden, met de opmerking dat hoewel de huidige resultaten significant zijn, toekomstig werk de voorspelbaarheid verder kan verbeteren via Z3-tactieken, parametersynthesetools kan uitbreiden en Reinforcement Learning-technieken kan toepassen die worden geïnitieerd door de voorgestelde heuristieken. De auteurs claimen niet het algemene onbeslisbare OOP te hebben opgelost, maar hebben de state-of-the-art voor zijn beslisbare fragmenten aanzienlijk vooruitgebracht.