Learning GR(1) Specifications from Traces

Stellen Sie sich vor, Sie versuchen einem Roboter beizubringen, wie er sich verhalten soll, aber Sie können die Regeln nicht aufschreiben, weil Sie sie nicht kennen. Stattdessen haben Sie eine Videokamera, die den Roboter aufzeichnet. Sie zeigen der Kamera eine Reihe von Clips, in denen der Roboter einen großartigen Job gemacht hat (die „guten“ Spuren), und eine Reihe von Clips, in denen er abgestürzt ist oder sich seltsam verhalten hat (die „schlechten“ Spuren). Ihr Ziel ist es, ein Regelbuch zu schreiben, das die guten Clips perfekt von den schlechten trennt. Dies ist die Welt des Specification Mining: das Durchforsten von Daten, um die verborgenen Gesetze zu finden, die ein System regieren.

Aber es gibt einen Haken: In der realen Welt folgen Systeme wie selbstfahrende Autos oder Fabrikroboter nicht einfach nur Regeln; sie reagieren auf ihre Umgebung. Wenn die Umgebung (wie eine regnerische Straße oder ein Mensch, der einen Knopf drückt) etwas tut, muss das System darauf reagieren. Dies nennt man ein reaktives System. Um solche Systeme sicher zu machen, verwenden Informatiker eine spezielle Art von Logik, die GR(1) heißt. Betrachten Sie GR(1) als einen strengen Vertrag: „Wenn die Umgebung verspricht, sich gut zu verhalten (Annahmen), dann verspricht das System, seinen Job zu erledigen (Garantien).“ Wenn Sie diesen Vertrag richtig aufsetzen, können Sie automatisch einen Roboter bauen, der mathematisch garantiert funktionieren wird. Wenn Sie ihn falsch aufsetzen, könnte der Roboter scheitern oder, noch schlimmer, die Mathematik könnte sagen, dass der Robot unmöglich zu bauen ist, obwohl er es eigentlich sein könnte.

Das Problem ist, dass das Finden des richtigen Vertrags schwierig ist. Bestehende Werkzeuge versuchen oft, die Regeln zu erraten, indem sie jeden möglichen Satz in der Sprache der Logik untersuchen. Das ist so, als würde man versuchen, eine bestimmte Nadel im Heuhaufen zu finden, indem man jedes einzelne Strohhalm-Stück im Universum überprüft. Es dauert ewig, und oft liefert Ihnen das Werkzeug eine Regel, die zwar okay aussieht, aber eigentlich eine Falle ist – sie trennt die guten Clips von den schlechten, aber es ist eine Regel, der ein Roboter niemals folgen könnte.

Hier kommt das Paper ins Spiel. Die Forscher, angeführt von Sam Nicholas Kouteili und seinem Team, haben ein neues Werkzeug namens GR1MINE entwickelt. Anstatt wahllos zu raten, kennt GR1MINE die Form des Vertrags im Voraus. Es kennt das Skelett der GR(1)-Regel: „Wenn die Umgebung X tut, dann muss das System Y tun.“ Es muss nur noch herausfinden, was X und Y tatsächlich sind.

Um dies zu erreichen, verwendeten sie einen cleveren Trick mit einem „SAT-Solver“, der wie ein superschneller Rätsellöser funktioniert. Stellen Sie sich vor, Sie versuchen, eine LEGO-Burg zu bauen, aber Sie wissen nicht, welche Steine Sie verwenden sollen. Anstatt eine ganze Burg zu bauen, zu testen und dann wieder abzureißen, um es erneut zu versuchen, baut GR1MINE einmal das Gerüst der Burg. Dann versucht es verschiedene Kombinationen von Steinen innerhalb dieses Gerüsts. Wenn eine Kombination fehlschlägt, merkt sich der Solver, warum sie fehlgeschlagen ist, und nutzt dieses Gedächtnis, um tausende andere schlechte Kombinationen sofort zu überspringen. Dies wird als „inkrementelles Lösen“ bezeichnet.

Das Team testete sein Werkzeug an 120 verschiedenen Rätseln (Benchmarks), die aus realen Hardware- und Robotik-Herausforderungen stammen. Die Ergebnisse waren beeindruckend. Wenn die Rätsel aus Standard-GR(1)-Regeln bestanden, löste GR1MINE alle 60 von ihnen. Im Gegensatz dazu lösten die bisher besten Werkzeuge etwa die Hälfte oder ein Drittel davon. Noch beeindruckender war, dass GR1MINE auf diesen spezifischen Rätseln über 30-mal schneller war als die generischen Werkzeuge.

Doch der wahre Zauber geschah, als sie das Werkzeug an Rätseln testeten, die keine perfekten GR(1)-Regeln waren. Selbst als die ursprünglichen Regeln chaotisch waren und nicht in das ordentliche Template passten, gelang es GR1MINE immer noch, für 38 von 60 dieser chaotischen Fälle eine funktionierende, realisierbare Regel zu finden. Die anderen Werkzeuge hatten Schwierigkeiten und fanden nur sehr wenige funktionierende Regeln, und diejenigen, die sie fanden, waren oft „unrealisierbar“ – das heißt, mathematisch unmöglich für einen Roboter zu befolgen.

Kurz gesagt: GR1MINE findet nicht nur eine Regel, die Gut von Schlecht trennt; es findet eine Regel, nach der ein Roboter tatsächlich leben kann. Indem es sich an die bekannte Struktur von GR(1) hält und intelligente Gedächtnistricks verwendet, um Doppelarbeit zu vermeiden, hat das Team gezeigt, dass wir komplexe, sichere Verträge für Roboter viel schneller und zuverlässiger als bisher automatisch entdecken können. Sie haben nicht nur eine Nadel im Heuhaufen gesucht; sie haben einen Magneten gebaut, der nur die richtigen Nadeln anzieht.