On the Ability of Transformers to Verify Plans

1. O Problema

Os modelos de linguagem grandes (LLMs) baseados em Transformers demonstraram capacidades notáveis em várias tarefas, mas seu desempenho em planejamento de IA (AI planning) tem sido inconsistente. Embora consigam gerar planos para instâncias pequenas ou semelhantes às de treinamento, eles frequentemente falham ao generalizar para planos mais longos ou para instâncias com um número maior de objetos (vocabulário expandido).

A literatura atual carece de uma análise teórica clara sobre por que e quando os Transformers conseguem generalizar em tarefas de planejamento. A maioria das falhas é atribuída a problemas empíricos (como perder o estado do mundo ou propor ações inaplicáveis), sem uma compreensão formal das limitações expressivas dos modelos. O foco deste trabalho é especificamente na verificação de planos: dado um problema de planejamento e um plano candidato, determinar se o plano resolve corretamente o problema. O desafio central é a generalização de comprimento: um modelo treinado apenas em planos curtos consegue verificar planos arbitrariamente longos? E consegue lidar com um número de objetos (vocabulário) maior no teste do que no treino?

2. Metodologia

Os autores adotam uma abordagem teórica baseada na teoria da linguagem formal e na complexidade computacional, combinada com validação empírica.

• Abordagem Teórica (C-RASP e C-RASP):*

  • O trabalho baseia-se no framework C-RASP (Counting RASP), que mapeia a expressividade dos Transformers para linguagens formais. Sabe-se que tarefas expressíveis em C-RASP[Pos] permitem generalização de comprimento para Transformers com codificações posicionais absolutas (APE).
  • Inovação Principal (C-RASP):* Para abordar o cenário onde o número de objetos cresce no tempo de teste (vocabulário infinito/expansível), os autores introduzem o C-RASP*. Esta é uma extensão do C-RASP projetada para garantir generalização de comprimento mesmo com o crescimento simultâneo do tamanho da sequência e do tamanho do vocabulário.
  • O C*-RASP utiliza Funções de Produto e um modelo de aprendizado chamado Symbolic Limit Transformer. Ele impõe restrições de invariância à tradução (interações dependem apenas de diferenças relativas, não de IDs absolutos de objetos) e localidade (interações decaem além de uma certa distância).
  • A classe C*-RASP permite verificar se um problema de planejamento pode ser resolvido por um algoritmo que não depende da memorização de IDs específicos de objetos, mas sim de padrões estruturais.

• Definição de Subclasses de Planejamento:
  Os autores analisam a verificabilidade de planos em diferentes subclasses de domínios de planejamento:

  1. Delete-Free: Ações apenas adicionam fatos (não removem).
  2. Well-Formed (Bem-formado): Cada efeito de uma ação altera necessariamente o valor de verdade de um fato (não há efeitos nulos ou redundantes).
  3. STRIPS: Formalismo padrão sem efeitos condicionais.
  4. Conditional Effects: Ações com efeitos que dependem do estado atual.

• Experimentos Empíricos:

  • Foram criados três domínios sintéticos para validar a teoria: Heavy Grippers (robô com garra), Colors (adicionar/remover cores de sacos) e Lights Out (quebra-cabeça de luzes).
  • Para cada domínio, foram geradas variantes "Bem-formadas" (Well-formed) e variantes padrão (STRIPS ou com efeitos condicionais).
  • Modelos GPT-2 foram treinados em planos de 11 a 100 ações e testados em planos de 101 a 200 ações, com variações no número de objetos.

3. Principais Contribuições

1. Introdução do C-RASP:* Um novo framework teórico que estende a análise de generalização de comprimento para cenários com vocabulário variável (número crescente de objetos), provando que a generalização é garantida se a tarefa for expressível nesta linguagem.
2. Caracterização Teórica da Verificação de Planos:
   • Positivo: A verificação de planos em domínios Delete-Free ou Well-Formed pertence à classe C*-RASP. Isso implica que os Transformers podem, teoricamente, aprender a verificar planos longos e com muitos objetos, generalizando perfeitamente.
   • Negativo: A verificação de planos em domínios STRIPS gerais ou com Efeitos Condicionais não pertence a C*-RASP (e muitas vezes reduz-se a linguagens como FlipFlop ou PARITY, que são intratáveis para generalização de comprimento em Transformers).
3. Prova de Generalização: Estabelecem que a expressibilidade por um Symbolic Limit Transformer é uma condição necessária e suficiente para a generalização de comprimento no modelo de aprendizado proposto.
4. Validação Empírica: Os experimentos confirmam rigorosamente a teoria: os modelos atingem precisão próxima de 100% em variantes bem-formadas (mesmo com vocabulário crescente), mas falham (desempenho ao nível de acaso) em variantes com efeitos condicionais ou STRIPS não bem-formados.

4. Resultados Chave

• Domínios Bem-Formados e Delete-Free: Os modelos conseguiram generalizar com sucesso para planos mais longos e com mais objetos do que os vistos durante o treinamento. A precisão manteve-se alta (próxima de 1.0) no conjunto de teste OOD (Out-of-Distribution).
• Domínios STRIPS e com Efeitos Condicionais:
  • No domínio Lights Out com efeitos condicionais, o modelo falhou em generalizar, mesmo com um conjunto fixo de objetos, caindo para o nível de acaso.
  • No domínio Colors (variante STRIPS), a precisão caiu drasticamente à medida que o comprimento do plano aumentava, diferentemente da variante bem-formada que manteve alta precisão.
• Impacto da Reformulação: O trabalho demonstra que reformular um problema complexo (como Lights Out com efeitos condicionais) para uma forma bem-formada (expandido em um número exponencial de ações, mas sem condicionais) torna o problema solucionável e generalizável por Transformers.

5. Significado e Implicações

• Explicação Teórica para Falhas: O artigo fornece uma explicação fundamental para a inconsistência observada em tarefas de planejamento com LLMs: não é apenas uma questão de dados ou arquitetura, mas de propriedades estruturais do domínio. Se a dinâmica do problema exige rastrear o "último estado" de forma não-local (como em STRIPS geral ou efeitos condicionais), os Transformers falham na generalização.
• Diretrizes para Prática: Para aplicar Transformers em planejamento, é crucial reformular os problemas para garantir que sejam bem-formados ou delete-free. Isso sugere que a engenharia de domínio (como a criação de compiladores de planejamento que transformam problemas condicionais em bem-formados) é essencial para o sucesso de modelos baseados em LLMs.
• Avanço Teórico: O framework C*-RASP e o conceito de Symbolic Limit Transformer abrem novas fronteiras para a análise teórica de como modelos de deep learning lidam com vocabulários infinitos e generalização estrutural, indo além da verificação de planos para outras tarefas de raciocínio simbólico.

Em resumo, o paper estabelece que a capacidade de um Transformer generalizar na verificação de planos depende criticamente da estrutura do domínio de planejamento. Domínios com propriedades de "bem-formação" permitem generalização perfeita, enquanto domínios com efeitos condicionais ou lógica de STRIPS não restringida são intratáveis para generalização de comprimento e vocabulário nesses modelos.