Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications

Este artigo apresenta uma abordagem que estende a mineração de especificações a tipos de dados mais ricos, unificando a síntese de transformações de dados e especificações temporais via TSL$_f$ para gerar programas reativos com maior eficiência de amostragem e robustez em comparação a métodos tradicionais baseados em abstração booleana.

O essencial

Imagine que você tem um amigo que é um gênio jogando videogame, mas ele nunca te explicou como ele joga. Você só vê ele jogando: ele anda, pula, evita buracos e chega na meta.

A maioria dos sistemas de Inteligência Artificial (IA) atuais tenta aprender copiando esses movimentos, como um macaco aprendendo a imitar. Se o jogo mudar um pouco (o buraco se move, o tamanho do mapa muda), o "macaco" fica perdido porque ele só memorizou os passos, não a lógica por trás deles.

Este artigo apresenta uma abordagem diferente, chamada "Mineração de Especificações". Em vez de apenas copiar os movimentos, o sistema tenta descobrir a receita secreta ou as regras do jogo que o gênio está seguindo.

Aqui está a explicação simplificada, usando analogias do dia a dia:

1. O Problema: A Tradução Ruim (Bool vs. Dados Reais)

Antes, os computadores tentavam entender o jogo transformando tudo em "Sim" ou "Não" (verdadeiro/falso).

• A analogia: Imagine que você quer ensinar alguém a cozinhar, mas só pode usar a palavra "Sim" ou "Não".
  • "O tomate está vermelho?" -> Sim.
  • "A cebola está picada?" -> Sim.
  • Mas como você explica "Corte a cebola em 3 pedaços" ou "Adicione 2 colheres de sal"? Você teria que transformar cada número em uma lista gigante de "Sim/Não" (ex: "O número 2 é verdadeiro? Não. O número 3 é verdadeiro? Sim..."). Isso torna a receita confusa, enorme e cheia de erros.

O novo método do artigo permite que o computador entenda os números e as transformações diretamente. Ele entende que "x + 1" é uma regra, não apenas uma sequência de luzes acesas e apagadas.

2. A Solução: Duas Etapas Mágicas

O sistema funciona como um detetive em duas fases:

Fase 1: Descobrindo as Ferramentas (A Cozinha)

O computador olha para os registros do jogo (trilhas de dados) e pergunta: "Quais ferramentas o jogador usou para mudar o estado?"

• Ele usa uma técnica chamada Síntese Guiada por Sintaxe (SyGuS).
• A analogia: Imagine que você vê uma massa de bolo mudar de forma. O computador testa hipóteses: "Será que foi um batedor? Seria um cortador? Será que alguém adicionou açúcar?". Ele tenta encontrar a função matemática exata (como +1 ou -1) que explica a mudança de um passo para o outro. Ele descobre que o jogador não apenas "moveu", mas "moveu para a direita somando 1 à coordenada X".

Fase 2: Descobrindo a História (O Roteiro)

Com as ferramentas descobertas, o computador agora tenta escrever a história do jogo usando uma linguagem especial chamada TSLf.

• A analogia: Em vez de dizer "O jogador está na casa 1, depois na casa 2", o sistema escreve a regra: "Sempre que você estiver perto de um buraco, pare. Eventualmente, você deve chegar à meta."
• Isso cria duas regras principais:
  1. Segurança (Safety): O que você nunca deve fazer (ex: "Nunca pise no buraco").
  2. Vitalidade (Liveness): O que você precisa fazer eventualmente (ex: "Chegue na meta").

3. O Resultado: Um Jogador que Entende, não apenas Memoriza

Os autores testaram isso em jogos simples do OpenAI (como FrozenLake, onde você desliza em um lago de gelo e evita buracos).

• Os métodos antigos (Imitação): Se você treina um sistema antigo em um mapa com buracos na esquerda, ele aprende a ir para a direita. Se você mudar o jogo e colocar os buracos na direita, ele continua indo para a direita e cai no buraco. Ele é um "macaco" que só sabe o que viu.
• O novo método (Mineração TSLf): O sistema descobre a regra: "Evite qualquer coisa que seja um buraco, independente de onde ele esteja."
  • Resultado: O sistema aprendeu com pouquíssimos exemplos (menos de 20 jogos) e conseguiu vencer em 100% dos novos mapas que ele nunca viu antes, mesmo com tamanhos e posições diferentes.

4. Por que isso é importante?

Imagine que você está ensinando um robô a dirigir.

• Abordagem antiga: O robô vê você virar à esquerda em um semáforo e aprende a virar à esquerda sempre que vê um semáforo. Se o semáforo mudar de lugar ou o trânsito mudar, ele pode bater.
• Abordagem deste artigo: O robô descobre a regra: "Pare no vermelho, siga no verde, e evite carros." Com essa regra, ele pode dirigir em qualquer cidade do mundo, mesmo que nunca tenha estado lá, porque ele entende a lógica, não apenas o caminho.

Resumo em uma frase

Este trabalho ensina computadores a não apenas "imitar" o que veem, mas a "descobrir as regras do jogo" (matemática e lógica) por trás das ações, permitindo que eles aprendam muito mais rápido e se adaptem a situações novas, como um humano faria, em vez de agir como um macaco repetidor.

Resumo técnico

Resumo Técnico: Mineração de Transformações de Dados e Especificações Temporais

1. O Problema

A mineração de especificações (derivação automática de propriedades lógicas a partir de traços de execução) é fundamental para capturar o comportamento de sistemas e automatizar a verificação. No entanto, as abordagens existentes (como as baseadas em LTLf - Linear Temporal Logic on finite traces) sofrem de limitações críticas:

• Abstração Booleana: Elas tratam todos os eventos como variáveis booleanas. Para lidar com dados complexos (ex: coordenadas, inteiros), é necessário "bit-blast" (converter dados em bits) ou criar manualmente predicados, o que aumenta o tamanho das fórmulas e introduz relações semânticas espúrias.
• Falta de Consciência de Dados: Elas não conseguem expressar propriedades que dependem da evolução de variáveis (ex: "mover x para a célula acima do obstáculo mais próximo") de forma nativa, limitando a generalização em ambientes dinâmicos.
• Ineficiência de Amostragem: Métodos de aprendizado passivo (como Imitation Learning) exigem milhares de exemplos para generalizar, pois aprendem mapeamentos locais estado-ação em vez de regras temporais e relacionais globais.

2. Metodologia

Os autores propõem uma abordagem unificada que combina síntese de funções e mineração de especificações temporais sobre tipos de dados ricos. O pipeline consiste em três etapas principais:

A. Descoberta de Funções (Function Discovery)

• O sistema utiliza Síntese Guiada por Sintaxe (SyGuS) para inferir automaticamente as funções que explicam a evolução das variáveis ao longo do tempo.
• Um algoritmo bottom-up (de baixo para cima) e ganancioso é utilizado:
  1. Gera candidatos de transições (input-output) para cada variável em cada passo de tempo.
  2. Usa um solver SyGuS (CVC5) para sintetizar funções que satisfazem essas transições.
  3. Agrupa e funde conjuntos de restrições para encontrar um conjunto mínimo de funções que cobre todos os traços, eliminando funções espúrias (ex: funções que funcionam apenas para um par de dados específicos).

B. Lógica Temporal TSLf

• Introduzem TSLf (Temporal Stream Logic on finite prefixes), uma interpretação de prefixo finito da TSL.
• Diferencial: Diferente do LTLf, o TSLf separa o controle dos dados. Ele suporta nativamente:
  • Atualizações Funcionais: Termos como [s ← f(s1, ...)] que descrevem como uma variável é atualizada no próximo passo de tempo.
  • Predicados de Primeira Ordem: Permite raciocinar sobre relações entre dados (ex: igualdade, aritmética linear) sem convertê-los em booleanos.
• Semântica: Define traços bem-formados onde cada variável tem uma única atualização por passo de tempo (exceto no final) e inclui um predicado END exclusivo para o último passo.

C. Mineração de Especificações e Síntese

• Com as funções descobertas, os traços brutos são "elevados" para traços de aplicação de funções (TSLf traces).
• O problema de mineração é decomposto em duas partes para garantir a síntese de controladores reativos robustos:
  1. Liveness (Vivacidade): O que eventualmente deve acontecer (ex: alcançar o objetivo).
  2. Safety (Segurança): O que sempre deve ser mantido (ex: evitar buracos/obstáculos).
• Utiliza-se uma extensão da ferramenta Bolt para minerar fórmulas minimais que discriminam traços positivos de negativos.
• Finalmente, a especificação minerada é sintetizada em um controlador reativo (transdutor de estado finito) usando a ferramenta Issy.

3. Principais Contribuições

1. Algoritmo de Síntese Bottom-Up: Um método para descobrir conjuntos de funções que cobrem traços de execução completos, utilizando uma estratégia de troca de entrada (input-swapping) para refinar as hipóteses.
2. Framework TSLf: A introdução de uma semântica de traços finitos para a Lógica de Fluxo Temporal, permitindo mineração de especificações sobre transformações de dados e tipos não booleanos.
3. Aprendizado de RL Simbólico: Demonstração de que é possível sintetizar programas reativos generalizáveis a partir de especificações mineradas, superando métodos de aprendizado passivo em eficiência de amostras e robustez.

4. Resultados e Avaliação

A abordagem foi avaliada no conjunto de benchmarks OpenAI-Gymnasium ToyText (FrozenLake, CliffWalking, Taxi, Blackjack), comparando-se com baselines de aprendizado passivo (Alergia, Behavioral Cloning/Redes Neurais, Árvores de Decisão) e mineração LTLf com bit-blast.

• FrozenLake (Grid World):

  • O método TSLf alcançou 100% de precisão em configurações não vistas (variação de posições de buracos e tamanhos de grade) usando apenas 24 traços (12 positivos, 12 negativos).
  • Baselines de imitação estagnaram entre 70-85% mesmo com 1000 amostras e falharam completamente em mudanças de configuração fixa.
  • As especificações mineradas capturaram relações invariantes (ex: "evitar coordenadas iguais às dos buracos"), permitindo generalização, enquanto o bit-blast produziu fórmulas semânticamente vazias.

• CliffWalking:

  • O TSLf generalizou perfeitamente para variações na altura do precipício e tamanho do tabuleiro.
  • Baselines falharam ao tentar generalizar de configurações fixas para dinâmicas alteradas, pois memorizaram mapeamentos locais em vez de regras temporais.

• Taxi (Objetivos Temporais Ordenados):

  • O ambiente exige uma sequência temporal: pegar o passageiro e depois ir ao destino.
  • O TSLf minerou a especificação sequencial correta com poucos exemplos.
  • Baselines de imitação falharam (<32%) por não conseguirem codificar a estrutura temporal "primeiro A, depois B" em políticas de estado único.

• Blackjack (Ambiente Estocástico):

  • Embora não tenha estrutura espacial, o TSLf conseguiu minerar estratégias de segurança (quando "parar" ou stand) baseadas em limiares de cartas, alcançando 100% de aderência à estratégia com poucas amostras.

5. Significado e Impacto

Este trabalho representa um avanço significativo rumo a um paradigma de Aprendizado por Reforço (RL) puramente simbólico.

• Eficiência de Amostragem: O método é ordens de magnitude mais eficiente em termos de amostras que métodos baseados em gradientes ou imitação passiva.
• Generalização Robusta: Ao aprender especificações relacionais e temporais (o "porquê" e "como" do comportamento) em vez de mapeamentos estado-ação (o "o que" fazer), o agente generaliza para cenários nunca vistos durante o treinamento.
• Interpretabilidade: As especificações mineradas são fórmulas lógicas humanas, oferecendo transparência sobre a política aprendida, ao contrário de "caixas pretas" como redes neurais.
• Futuro: Abre caminho para agentes que interagem com o ambiente, mineram especificações de suas experiências e refinam seu comportamento iterativamente através de síntese formal.