Resumo Técnico: Síntese e Verificação de Programas Transformer

Declaração do Problema

Transformers, a arquitetura fundamental dos Modelos de Linguagem de Grande Escala (LLMs), são notoriamente difíceis de analisar formalmente. Embora sejam expressivos e paralelizáveis, verificar suas propriedades é indecidível, e sua extensão com Cadeias de Pensamento (Chain of Thoughts) os torna completos no sentido de Turing. Para abordar isso, pesquisadores desenvolveram linguagens declarativas como RASP (Restricted Access Sequence Processing Language) e sua variante C-RASP (Counting RASP) para capturar o comportamento dos transformers com semântica precisa.

No entanto, apesar da conexão teórica entre C-RASP e transformers, duas lacunas críticas permanecem:

1. Verificação: Não há um método automático para verificar programas C-RASP. Verificar se um C-RASP reconhece uma linguagem trivial é indecidível no caso geral, e não existe nenhuma ferramenta prática para analisar propriedades como equivalência ou inclusão de linguagens.
2. Síntese: Não há nenhum método conhecido para aprender ou sintetizar automaticamente um programa C-RASP a partir de exemplos. Abordagens existentes dependem do treinamento de redes neurais e da extração de regras, que frequentemente falham em produzir traduções implementáveis ou exigem pressupostos idealizados.

Este artigo aborda esses desafios desenvolvendo as primeiras técnicas automáticas para verificação e síntese de programas C-RASP.

Metodologia

1. Verificação via Redução para Lustre

Os autores estabelecem uma conexão formal entre C-RASP e Lustre, uma linguagem de fluxo de dados síncrona usada para sistemas embarcados.

• Tradução: Um programa C-RASP é traduzido para um nó Lustre. A tradução mapeia regras C-RASP para variáveis Lustre (fluxos booleanos e inteiros).
  • Operadores de Contagem: O operador de contagem C-RASP #φ (contando posições onde φ é verdadeiro) é simulado em Lustre usando variáveis inteiras auxiliares que acumulam valores sobre um fluxo infinito.
  • Finito vs. Infinito: Como C-RASP opera sobre palavras finitas e Lustre sobre fluxos infinitos, a entrada é codificada como um fluxo infinito com um marcador específico de fim de fluxo (#) e um marcador de eternidade (Ω).
• Verificação de Modelo: Uma vez traduzido, propriedades como equivalência de linguagem, inclusão e vacuidade são verificadas usando verificadores de modelo de última geração (especificamente Kind2) acoplados a solucionadores SMT otimizados (CVC5, Z3).
• Complexidade: A tradução é polinomial em tamanho, desde que os parâmetros de intervalo no operador #rs,re sejam codificados em unário.

2. Síntese via Recozimento Simulado

O artigo propõe um algoritmo de busca local baseado em recozimento simulado para sintetizar programas C-RASP a partir de exemplos positivos e negativos.

• Espaço de Estados: A busca é restrita a uma "forma de programa" fixa definida pelo número de regras booleanas ($N_b$), regras de contagem ($N_c$) e um limite em constantes numéricas ($K$).
• Operadores de Mutação: O algoritmo explora o espaço de estados aplicando mutações sintáticas ao programa atual. Estas incluem:
  • Ressamplagem: Substituir inteiramente o lado direito de uma regra.
  • Micro-mutações: Mudanças locais como trocar conectivos lógicos, alternar negação ou inverter a estricção de comparações.
  • Restrições: As mutações são restritas a fragmentos de sintaxe rasos (por exemplo, profundidade-2 para expressões de contagem) para enviesar a busca em direção a modelos simples e interpretáveis.
• Função Objetivo: A função de pontuação $E(P)$ prioriza a minimização de classificações incorretas ($\lambda_{mis}$), seguida pela penalização de regras inacessíveis ($\lambda_U$) e o tamanho total da árvore de sintaxe abstrata ($\lambda_S$).
• Dinâmica de Recozimento: O algoritmo aceita soluções piores com uma probabilidade dependente de um cronograma de temperatura de resfriamento, permitindo que ele escape de ótimos locais.

3. Aplicações Integradas

Os autores integram esses dois componentes em um framework unificado que suporta duas aplicações:

1. Minimização de Programas Transformer: Dado um programa C-RASP, o sistema sintetiza um programa estruturalmente menor e equivalente. Ele alterna entre busca local e verificação de equivalência; contraexemplos do verificador orientam a busca.
2. Aprendizado Constrained: Dada uma especificação parcial (um programa C-RASP $P_{spec}$) e exemplos rotulados, o sistema sintetiza um programa que se ajusta aos exemplos e está incluído na linguagem de $P_{spec}$ ($L(P) \subseteq L(P_{spec})$).

Contribuições Principais

1. Primeiro Método Automático de Verificação: O artigo apresenta a primeira técnica para verificar automaticamente programas C-RASP reduzindo-os a Lustre e utilizando verificação de modelo. Isso permite a verificação de equivalência de linguagem, inclusão e vacuidade.
2. Primeiro Método Automático de Síntese: Os autores introduzem um algoritmo de busca local (recozimento simulado) capaz de sintetizar programas C-RASP diretamente a partir de exemplos, contornando a necessidade de treinamento intermediário de redes neurais.
3. Implementação e Benchmarking: Uma ferramenta unificada em Scala foi implementada e avaliada contra uma suíte de benchmarks da literatura, incluindo linguagens regulares, baseadas em contagem e estilo livre de contexto.

Resultados Experimentais

Os autores avaliaram sua ferramenta em uma suíte de benchmarks incluindo linguagens como Dyck-1, Majority e várias máquinas de Tomita.

• Eficiência: A ferramenta sintetizou com sucesso programas C-RASP corretos para a maioria dos benchmarks dentro de um tempo limite de 300 segundos. Por exemplo, sintetizar um programa para Dyck-1 levou aproximadamente 3,92 segundos, enquanto AnBnCn levou 80,05 segundos.
• Precisão: A síntese alcançou alta precisão de treinamento e avaliação (frequentemente 100%) em linguagens dentro do poder expressivo do C-RASP.
• Comparação com Transformers: O artigo observa que, para certos benchmarks, treinar um transformer (por exemplo, GPT-2 via HuggingFace) para alcançar a linguagem correta poderia levar várias horas, enquanto a ferramenta de síntese C-RASP completou a tarefa em segundos.
• Limitações: Como esperado da teoria da expressividade, linguagens além do poder do C-RASP (por exemplo, Parity, Tomita 3, Tomita 5) não puderam ser aprendidas com alta precisão, com as melhores precisões de treinamento permanecendo abaixo de 80%.

Significado e Alegações

O artigo posiciona o C-RASP não apenas como uma ferramenta teórica para entender a expressividade dos transformers, mas como um modelo substituto interpretável. Ao fornecer métodos automáticos para verificação e síntese, os autores argumentam que o C-RASP pode ser analisado usando métodos formais (FXAI), fechando a lacuna entre a natureza de "caixa preta" das redes neurais e a necessidade de explicabilidade.

O significado reside em:

• Decidibilidade na Prática: Embora a verificação geral seja indecidível, a redução para Lustre fornece um caminho prático e automatizado para verificar comportamentos específicos e do mundo real de transformers.
• Síntese Direta: O método de síntese oferece uma rota direta para gerar programas interpretáveis sem a instabilidade ou opacidade do treinamento de redes neurais profundas.
• Otimização: A capacidade de minimizar programas de transformers existentes e aprendê-los sob restrições demonstra a utilidade do C-RASP para refinamento de programas e aplicações críticas de segurança.

Os autores concluem que seu trabalho estabelece as bases para a análise formal de transformers, com direções futuras incluindo verificação de robustez e a incorporação de mecanismos de Cadeia de Pensamento (CoT).