Neuro-Symbolic Injection of LTLf Constraints in Autoregressive Reinforcement Learning Policies

Resumo Técnico: Injeção Neuro-Simbólica de Restrições LTL$_f$ em Políticas de Aprendizado por Reforço Autorregressivas

Declaração do Problema
No Aprendizado por Reforço (RL) offline, agentes aprendem políticas exclusivamente a partir de conjuntos de dados pré-coletados, sem interação online. Embora abordagens recentes de modelagem de sequência, como Trajectory Transformers (TT) e Decision Transformers (DT), tenham enquadrado o RL com sucesso como um problema de geração de sequência, elas tipicamente otimizam apenas a recompensa cumulativa. Isso cria uma lacuna crítica em domínios de segurança crítica (ex: robótica, navegação autônoma) onde as políticas devem aderir a restrições de alto nível e temporalmente estendidas. A otimização baseada em recompensa padrão não consegue garantir que uma política satisfaça requisitos de lógica temporal complexos, como "eventualmente alcançar o objetivo enquanto sempre evita perigos", especialmente quando as violações não podem ser corrigidas via exploração de tentativa e erro em um cenário offline.

Metodologia
Os autores propõem um framework neuro-simbólico que injeta restrições de Lógica Temporal Linear sobre traços finitos (LTL$_f$) diretamente no processo de treinamento de políticas baseadas em transformers autorregressivos. A metodologia central envolve três componentes principais:

1. Compilação de LTL$_f$ para DFA: Especificações temporais de alto nível são compiladas em Autômatos de Estados Finitos Determinísticos (DFAs). Essa tradução permite que as restrições lógicas sejam representadas como sistemas de transição de estados que podem processar sequências de tokens.
2. Perda de Lógica Diferenciável: Para integrar esses autômatos discretos na otimização contínua de redes neurais, os autores empregam uma representação diferenciável.
   • Sinais de Satisfação Suave (Soft Satisfaction Signals): Em vez de amostragem rígida (hard sampling), o framework utiliza amostragem Gumbel-Softmax para gerar vetores de tokens diferenciáveis, próximos de one-hot, durante o treinamento.
   • Integração DeepDFA: Esses tokens suaves são alimentados em um "DeepDFA", uma relaxação neural do DFA padrão. Este módulo calcula um sinal de satisfação probabilístico indicando a probabilidade de a trajetória gerada satisfazer a fórmula LTL$_f$.
   • Regularização: Uma função de perda de lógica ($L_\phi$) é derivada do log-probabilidade negativa de satisfação. Esta é combinada com a perda padrão de modelagem de sequência supervisionada ($L_{\mathcal{D}}$) via uma soma ponderada: $L = \alpha L_\phi + (1 - \alpha) L_{\mathcal{D}}$, onde $\alpha$ é um parâmetro de compensação (trade-off).
3. Agnosticismo de Arquitetura: O framework é projetado para ser agnóstico ao modelo dentro da classe de modelos de sequência autorregressivos. Ele utiliza um "adaptador de lógica" compartilhado para lidar com mapeamentos de token-para-símbolo e execuções (rollouts) de DFA, tornando-o aplicável tanto a arquiteturas TT quanto DT sem alterar suas estruturas subjacentes.

Principais Contribuições
O artigo delineia três contribuições primárias:

• Framework Neuro-Simbólico Unificado: Um método para injetar restrições LTL$_f$ em políticas de RL offline baseadas em transformers usando módulos baseados em autômatos que são agnósticos à arquitetura.
• Stack de Avaliação Canônica: Um pipeline consistente de avaliação de fim de episódio que alinha a serialização do conjunto de dados, o mapeamento de token-para-símbolo e a avaliação lógica, prevenindo desalinhamentos semânticos entre o treinamento e a avaliação da lógica temporal.
• Análise Empírica: Uma avaliação sistemática em domínios de navegação demonstrando as trocas (trade-offs) entre o desempenho da tarefa (return) e a satisfação de restrições sob diferentes níveis de orientação lógica.

Resultados Experimentais
O framework foi avaliado no ambiente de navegação ColourBomb, testando dois tipos de especificação: Segurança Invariante ($G(\neg \text{bomb})$) e Alcançar-enquanto-Seguro ($G(\neg \text{bomb}) \land F(\text{goal})$).

• Decision Transformers (DT):
  • DTs vanilla (sem regularização de lógica) falharam completamente, atingindo células de bomba e falhando em alcançar objetivos.
  • A introdução da regularização de lógica com um parâmetro de compensação alto ($\alpha = 0.8$) alcançou 100% de satisfação para ambas as especificações de segurança e alcançar-enquanto-seguro.
  • Crucialmente, esta configuração de alta restrição também melhorou o retorno médio (de -1.460 para -0.780) ao eliminar falhas catastróficas (impactos em bombas), demonstrando que a satisfação de restrições pode alinhar-se com o desempenho em configurações offline.
• Trajectory Transformers (TT):
  • TTs vanilla mostraram conformidade de segurança parcial, mas baixo alcance de objetivos.
  • A regularização de lógica melhorou as taxas de satisfação e reduziu as taxas de impacto em bombas. Para a tarefa de segurança invariante, $\alpha = 0.8$ produziu os melhores resultados. Para a tarefa mais complexa de alcançar-enquanto-seguro, um peso menor ($\alpha = 0.1$) proporcionou o equilíbrio ideal, melhorando tanto a satisfação quanto o retorno em comparação com o baseline.
  • Os autores observam que, embora melhorias tenham sido observadas, elas foram mais moderadas em TTs em comparação com DTs, uma discrepância deixada para investigação futura.

Significância e Alegações
O artigo afirma que integrar o conhecimento de fundo simbólico diretamente no objetivo de aprendizado — em vez de modificar a representação dos dados ou depender de modelagem de recompensa (reward shaping) — é uma direção promissora para melhorar a confiabilidade da política em RL offline de segurança crítica.

As principais alegações sobre a significância do método incluem:

• Injeção Direta de Restrições: Ao contrário de abordagens que dependem de blindagem (shielding, que requer modelos explícitos do ambiente) ou modelagem de recompensa (que pode ser difícil de projetar), este método injeta o conhecimento de lógica temporal diretamente na perda de treinamento.
• Generalidade: O framework suporta fórmulas LTL$_f$ arbitrárias, estendendo-se além do "fragmento de segurança" para incluir vivacidade (liveness) e combinações temporais complexas.
• Preservação de Desempenho: Os resultados sugerem que impor restrições lógicas estritas não necessariamente degrada o desempenho da tarefa; nos cenários testados, isso de fato melhorou os retornos ao prevenir resultados catastróficos que modelos vanilla encontravam frequentemente.

Os autores mantêm um tom modesto, reconhecendo que a abordagem é atualmente limitada a cenários offline e que as melhorias observadas em TTs foram menos pronunciadas do que em DTs. Eles identificam como trabalho futuro a extensão da avaliação para outros benchmarks, arquiteturas de modelos e a realização de comparações abrangentes de ponta a ponta com frameworks estabelecidos de Safe RL.