Learning GR(1) Specifications from Traces

Immagina di cercare di insegnare a un robot come comportarsi, ma non puoi scrivere le regole perché non sai quali siano. Inveve, hai una videocamera che registra il robot. Mostri alla telecamera un sacco di clip in cui il robot ha fatto un ottimo lavoro (le tracce "buone") e un sacco di clip in cui si è schiantato o si è comportato in modo strano (le tracce "cattive"). Il tuo obiettivo è scrivere un libro di regole che separi perfettamente le clip buone da quelle cattive. Questo è il mondo della specificazione mineraria (specification mining): scavare nei dati per trovare le leggi nascoste che governano un sistema.

Ma c'è un problema. Nel mondo reale, i sistemi come le auto a guida autonoma o i robot industriali non si limitano a seguire le regole; essi reagiscono al loro ambiente. Se l'ambiente (come una strada piovosa o un essere umano che preme un pulsante) fa qualcosa, il sistema deve rispondere. Questo è chiamato un sistema reattivo. Per rendere sicuri questi sistemi, gli informatici utilizzano un tipo speciale di logica chiamata GR(1). Pensa al GR(1) come a un contratto rigoroso: "Se l'ambiente promette di comportarsi bene (assunzioni), allora il sistema promette di svolgere il suo compito (garanzie)". Se ottieni questo contratto correttamente, puoi costruire automaticamente un robot che è matematicamente garantito per funzionare. Se lo ottieni in modo errato, il robot potrebbe fallire, o peggio, la matematica potrebbe dire che il robot è impossibile da costruire anche quando in realtà potrebbe esserlo.

Il problema è che trovare il contratto giusto è difficile. Gli strumenti esistenti spesso cercano di indovinare le regole guardando ogni possibile frase nel linguaggio della logica. Questo è come cercare un ago specifico in un pagliaio controllando ogni singolo pezzo di paglia dell'universo. Ci vuole un'eternità e, spesso, gli strumenti ti forniscono una regola che sembra andare bene ma che è in realtà una trappola: separa le clip buone da quelle cattive, ma è una regola che nessun robot potrebbe mai seguire.

È qui che entra in gioco il paper. I ricercatori, guidati da Sam Nicholas Kouteili e dal suo team, hanno costruito un nuovo strumento chiamato GR1MINE. Invece di indovinare casualmente, GR1MINE conosce già la forma del contratto in anticipo. Conosce lo scheletro della regola GR(1): "Se l'ambiente fa X, allora il sistema deve fare Y". Deve solo capire cosa sono effettivamente X e Y.

Per farlo, hanno usato un trucco intelligente che coinvolge un "SAT solver", che è come un risolutore di puzzle super veloce. Immagina di dover costruire un castello LEGO, ma non sai quali mattoncini usare. Invece di costruire un intero castello, testarlo e poi demolirlo per riprovare, GR1MINE costruisce il telaio del castello una volta per tutte. Poi, prova diverse combinazioni di mattoncini all'interno di quel telaio. Se una combinazione fallisce, il solver ricorda perché è fallita e usa questa memoria per saltare istantaneamente migliaia di altre combinazioni errate. Questo si chiama "risoluzione incrementale" (incremental solving).

Il team ha testato il proprio strumento su 120 diversi puzzle (benchmark) tratti da sfide reali di hardware e robotica. I risultati sono stati sorprendenti. Quando i puzzle erano composti da regole GR(1) standard, GR1MINE ne ha risolti tutti i 60. Al contrario, i precedenti migliori strumenti ne risolvevano circa la metà o un terzo. Ancora più impressionante, GR1MINE era oltre 30 volte più veloce degli strumenti generici su questi puzzle specifici.

Ma la vera magia è accaduta quando lo hanno testato su puzzle che non erano regole GR(1) perfette. Anche quando le regole originali erano disordinate e non si adattavano al modello pulito, GR1MINE è comunque riuscito a trovare una regola funzionante e realizzabile per 38 casi su 60 di questi casi disordinati. Gli altri strumenti hanno faticato, trovando pochissime regole funzionanti, e quelle che hanno trovato erano spesso "non realizzabili", ovvero matematicamente impossibili da seguire per un robot.

In breve, GR1MINE non si limita a trovare una regola che separi il buono dal cattivo; trova una regola che un robot può effettivamente vivere. Attenendosi alla struttura nota del GR(1) e usando trucchi intelligenti di memoria per evitare di rifare il lavoro, il team ha dimostrato che possiamo scoprire automaticamente contratti complessi e sicuri per i robot molto più velocemente e in modo più affidabile rispetto al passato. Non hanno solo cercato un ago nel pagliaio; hanno costruito un magnete che attira solo il tipo di aghi giusti.