Learning GR(1) Specifications from Traces

Imagine que você está tentando ensinar um robô como se comportar, mas não consegue escrever as regras porque não sabe quais são elas. Em vez disso, você tem uma câmera de vídeo gravando o robô. Você mostra à câmera vários clipes onde o robô fez um ótimo trabalho (os rastros "bons") e vários clipes onde ele bateu ou agiu de forma estranha (os rastros "ruins"). Seu objetivo é escrever um livro de regras que separe perfeitamente os clipes bons dos ruins. Este é o mundo da mineração de especificação: escavar através de dados para encontrar as leis ocultas que governam um sistema.

Mas há um porém. No mundo real, sistemas como carros autônomos ou robôs de fábrica não apenas seguem regras; eles reagem ao seu ambiente. Se o ambiente (como uma estrada chuvosa ou um humano apertando um botão) faz algo, o sistema deve responder. Isso é chamado de sistema reativo. Para tornar esses sistemas seguros, cientistas da computação usam um tipo especial de lógica chamada GR(1). Pense no GR(1) como um contrato rigoroso: "Se o ambiente prometer se comportar bem (suposições), então o sistema promete fazer o seu trabalho (garantias)." Se você acertar esse contrato, pode construir automaticamente um robô que é matematicamente garantido que funcionará. Se você errar, o robô pode falhar, ou pior, a matemática pode dizer que o robô é impossível de ser construído quando, na verdade, ele poderia ser.

O problema é que encontrar o contrato certo é difícil. As ferramentas existentes geralmente tentam adivinhar as regras olhando para cada frase possível na linguagem da lógica. Isso é como tentar encontrar uma agulha específica em um palheiro verificando cada pedaço de palha no universo. Leva uma eternidade e, muitas vezes, a ferramenta lhe dá uma regra que parece estar ok, mas que é na verdade uma armadilha — ela separa os clipes bons dos ruins, mas é uma regra que nenhum robô conseguiria realmente seguir.

É aqui que entra o artigo. Os pesquisadores, liderados por Sam Nicholas Kouteili e sua equipe, construíram uma nova ferramenta chamada GR1MINE. Em vez de adivinhar aleatoriamente, o GR1MINE conhece a forma do contrato antecipadamente. Ele conhece o esqueleto da regra GR(1): "Se o ambiente fizer X, então o sistema deve fazer Y." Ele só precisa descobrir o que X e Y realmente são.

Para fazer isso, eles usaram um truque inteligente envolvendo um "solver SAT", que é como um resolvedor de quebra-cabeças super-rápido. Imagine que você está tentando construir um castelo de LEGO, mas não sabe quais peças usar. Em vez de construir um castelo inteiro, testá-lo e depois derrubá-lo para tentar novamente, o GR1MINE constrói a estrutura do castelo uma única vez. Então, ele tenta diferentes combinações de peças dentro dessa estrutura. Se uma combinação falha, o solver lembra por que falhou e usa essa memória para pular sobre milhares de outras combinações ruins instantaneamente. Isso é chamado de "resolução incremental".

A equipe testou sua ferramenta em 120 quebra-cabeças diferentes (benchmarks) retirados de desafios reais de hardware e robótica. Os resultados foram impressionantes. Quando os quebra-cabeças eram feitos de regras GR(1) padrão, o GR1MINE resolveu todos os 60 deles. Em contraste, as melhores ferramentas anteriores resolveram apenas cerca de metade ou um terço deles. Mais impressionante ainda, o GR1MINE foi mais de 30 vezes mais rápido que as ferramentas genéricas nesses quebra-cabeças específicos.

Mas a verdadeira magia aconteceu quando eles testaram a ferramenta em quebra-cabeças que não eram regras GR(1) perfeitas. Mesmo quando as regras originais eram bagunçadas e não se encaixavam no modelo limpo, o GR1MINE ainda conseguiu encontrar uma regra realizável e funcional para 38 de 60 desses casos bagunçados. As outras ferramentas tiveram dificuldades, encontrando muito poucas regras funcionais, e as que encontraram eram frequentemente "irrealizáveis" — ou seja, matematicamente impossíveis de serem seguidas por um robô.

Em resumo, o GR1MINE não apenas encontra uma regra que separa o bom do ruim; ele encontra uma regra pela qual um robô pode realmente viver. Ao aderir à estrutura conhecida do GR(1) e usar truques inteligentes de memória para evitar refazer o trabalho, a equipe mostrou que podemos descobrir contratos complexos e seguros para robôs de forma muito mais rápida e confiável do que antes. Eles não apenas encontraram uma agulha no palheiro; eles construíram um ímã que só atrai o tipo certo de agulha.