Learning GR(1) Specifications from Traces

Stel je voor dat je een robot probeert te leren hoe hij zich moet gedragen, maar je kunt de regels niet opschrijven omdat je niet weet wat ze zijn. In plaats daarvan heb je een videocamera die de robot opneemt. Je laat de camera een heleboel fragmenten zien waarin de robot het geweldig heeft gedaan (de "goede" sporen) en een heleboel fragmenten waarin hij crashte of vreemd gedrag vertoonde (de "slechte" sporen). Je doel is om een regelboek te schrijven dat de goede fragmenten perfect van de slechte scheidt. Dit is de wereld van specification mining: het doorzoeken van data om de verborgen wetten te vinden die een systeem beheersen.

Maar er is een addertje onder het gras. In de echte wereld volgen systemen zoals zelfrijdende auto's of fabrieksrobots niet alleen regels; ze reageren op hun omgeving. Als de omgeving (zoals een regenachtige weg of een mens die op een knop drukt) iets doet, moet het systeem daarop reageren. Dit wordt een reactief systeem genoemd. Om deze systemen veilig te maken, gebruiken informaticus een speciaal soort logica genaamd GR(1). Denk aan GR(1) als een strikt contract: "Als de omgeving belooft zich goed te gedragen (aannames), dan belooft het systeem zijn werk te doen (garanties)." Als je dit contract goed krijgt, kun je automatisch een robot bouwen die wiskundig gegarandeerd werkt. Als je het fout krijgt, kan de robot falen, of erger nog, de wiskunde kan zeggen dat de robot onmogelijk te bouwen is terwijl dat eigenlijk wel kan.

Het probleem is dat het vinden van het juiste contract moeilijk is. Bestaande tools proberen vaak regels te raden door naar elke mogelijke zin in de taal van de logica te kijken. Dit is alsof je probeert een specifieke naald in een hooiberg te vinden door elk stukje stro in het universum te controleren. Het duurt eeuwig, en vaak geeft de tool je een regel die er wel oké uitziet, maar die eigenlijk een valstrik is—het scheidt de goede fragmenten van de slechte, maar het is een regel die geen enkele robot ooit zou kunnen volgen.

Dit is waar het paper om draait. De onderzoekers, onder leiding van Sam Nicholas Kouteili en zijn team, hebben een nieuwe tool gebouwd genaamd GR1MINE. In plaats van willekeurig te gokken, kent GR1MINE de vorm van het contract vooraf. Het kent het skelet van de GR(1)-regel: "Als de omgeving X doet, dan moet het systeem Y doen." Het hoeft alleen nog maar uit te zoeken wat X en Y precies zijn.

Om dit te doen, gebruikten ze een slimme truc met een "SAT-solver", die lijkt op een supersnelle puzzeloplosser. Stel je voor dat je een LEGO-kasteel probeert te bouwen, maar je weet niet welke stenen je moet gebruiken. In plaats van een heel kasteel te bouien, te testen, en dan weer af te breken om het opnieuw te proberen, bouwt GR1MINE eerst het frame van het kasteel. Daarna probeert het verschillende combinaties van stenen binnen dat frame. Als een combinatie mislukt, onthoudt de solver waarom het mislukte en gebruikt die herinnering om direct duizenden andere slechte combinaties over te slaan. Dit wordt "incremental solving" genoemd.

Het team testte hun tool op 120 verschillende puzzels (benchmarks) afkomstig van echte hardware- en robotica-uitdagingen. De resultaten waren opmerkelijk. Wanneer de puzzels bestonden uit standaard GR(1)-regels, loste GR1MINE alle 60 van hen op. In tegenstelling hiermee losten de vorige beste tools slechts ongeveer de helft of een derde van hen op. Nog indrukwekkender was dat GR1MINE meer dan 30 keer sneller was dan de generieke tools op deze specifieke puzzels.

Maar de echte magie gebeurde toen ze het testten op puzzels die geen perfecte GR(1)-regels waren. Zelfs toen de oorspronkelijke regels rommelig waren en niet in het nette sjabloon pasten, slaagde GR1MINE er nog steeds in om voor 38 van de 60 van die rommelige gevallen een werkende, realiseerbare regel te vinden. De andere tools worstelden en vonden slechts een klein aantal werkende regels, en de regels die ze wel vonden waren vaak "onrealiseerbaar"—wat betekent dat ze wiskundig gezien onmogelijk voor een robot te volgen waren.

Kortom, GR1MINE vindt niet alleen een regel die goed van slecht scheidt; het vindt een regel waar een robot echt naar kan leven. Door vast te houden aan de bekende structuur van GR(1) en slimme geheugentrucs te gebruiken om dubbel werk te voorkomen, hebben het team laten zien dat we complexe, veilige contracten voor robots veel sneller en betrouwbaarder kunnen ontdekken dan voorheen. Ze hebben niet alleen een naald in de hooiberg gevonden; ze hebben een magneet gebouwd die alleen de juiste soort naalden aantrekt.