Resumo Técnico: Do It for HER: Especificação de Recompensa em Lógica Temporal de Primeira Ordem em Aprendizado por Reforço

Problema

O Aprendizado por Reforço (RL) depende de sinais de recompensa para guiar o comportamento do agente, mas a engenharia de recompensas continua sendo um processo heurístico e trabalhoso. Um desafio significativo surge quando as tarefas são inerentemente não-markovianas, exigindo recompensas dependentes de histórico que as funções de recompensa markovianas padrão não conseguem capturar efetivamente. Embora a Lógica Temporal Linear com traços finitos (LTLf) tenha sido empregada com sucesso para especificar tais tarefas, ela é limitada a predicados booleanos. Essa restrição exige "funções de rotulagem" manuais para mapear espaços de estados contínuos ou heterogêneos (ex: coordenadas de valores reais, IDs de objetos, pesos) para símbolos proposicionais discretos. Em cenários complexos do mundo real, como robótica ou gestão de processos de negócio, esse codificação manual é frágil, não reutilizável e falha em aproveitar a rica estrutura dos dados contínuos. Além disso, especificações baseadas em lógica resultam frequentemente em recompensas esparsas, tornando o aprendizado difícil sem mecanismos adicionais, como modelagem de recompensa (reward shaping) ou replay de experiência de retrospectiva (hindsight experience replay).

Metodologia

Os autores propõem um framework utilizando Lógica Temporal Linear Modulo Theories sobre traços finitos (LTLfMT) para superar as limitações de expressividade da LTLf.

1. Estrutura Teórica: LTLfMT

Em vez de átomos booleanos, a LTLfMT utiliza fórmulas de primeira ordem interpretadas sobre teorias arbitrárias (ex: Aritmética Real Não-Linear, bancos de dados relacionais).

• Sintaxe: O framework define uma gramática onde os átomos proposicionais são substituídos por termos de primeira ordem e predicados ($\alpha$) envolvendo variáveis, constantes e funções. Estes são combinados via lógica de primeira ordem ($\lambda$) e, em seguida, envolvidos em operadores temporais ($\phi$), de forma semelhante à LLtf padrão.
• Fragmento Tratável: Reconhecendo que a LTLfMT completa é indecidível, os autores identificam um fragmento específico adequado para RL. Eles removem os operadores de "olhar à frente" ($\bigcirc, \sim\bigcirc$) da camada de termos, argumentando que restrições temporais sobre a coleta de dados são desnecessárias para a especificação da recompensa. Isso deixa a decidibilidade dependente apenas da teoria subjacente.
• Tradução para Autômatos: Para permitir o RL padrão, os autores propõem uma estratégia de proposicionalização. Uma fórmula $\phi$ no fragmento LTLfMT é traduzida em uma fórmula LTLf padrão $\phi'$ através da substituição de subfórmulas de primeira ordem por letras proposicionais distintas. Um solver de Satisfatibilidade Modulo Theories (SMT) atua como uma função de rotulagem universal, avaliando essas subfórmulas em cada passo de tempo para determinar os valores de verdade das letras proposicionais.
• MDP de Produto: A fórmula proposicionalizada é convertida em um Autômato Finito Determinístico (DFA). Este DFA é combinado com o ambiente original para formar um MDP de Produto, onde o espaço de estados é o produto cartesiano do estado do ambiente e o estado do autômato. Isso transforma o problema de recompensa não-markoviana em um problema markoviano solucionável por algoritmos de RL padrão.

2. Abordagem da Escassez de Recompensa: CRM-HER

Para lidar com a esparsidade inerente aos objetivos baseados em lógica, o artigo combina duas técnicas dentro da estrutura do MDP de Produto:

• Experiências Contrafatuais para Máquinas de Recompensa (CRM): Esta técnica gera transições artificiais substituindo o estado atual do DFA por outros estados alcançáveis no autômato, criando efetivamente cenários de "e se" para densificar o sinal de recompensa.
• Replay de Experiência de Retrospectiva (HER): O HER melhora a eficiência de amostragem ao rotular trajetórias falhas com objetivos que foram de fato alcançados durante esses episódios.
• Integração: Os autores adaptam o HER para o MDP de Produto definindo o "objetivo" como um estado específico no espaço do produto (um estado que dispara uma transição para um estado aceitante). Eles propõem uma abordagem combinada (CRM-HER) onde o HER é aplicado tanto às trajetórias reais quanto às trajetórias contrafatuais geradas pelo CRM. Isso aproveita a natureza estruturada dos objetivos de primeira ordem para gerar automaticamente especificações de objetivos sem intervenção manual.

Principais Contribuições

1. LTLfMT para Especificação de Recompensa: O artigo introduz um framework que estende a LLtf para LTLfMT, permitindo que as especificações de recompensa sejam escritas diretamente sobre domínios de dados contínuos e heterogêneos usando teorias de primeira ordem, eliminando a necessidade de funções de rotulagem manuais.
2. Identificação de um Fragmento Tratável: Os autores definem um fragmento específico de LTLfMT que é livre de problemas de decidibilidade (assumindo que a teoria subjacente seja decidível) e permite a tradução eficiente para autômatos via solvers SMT.
3. Abordagem Unificada CRM-HER: O artigo apresenta um novo método para combinar Experiências Contrafatuais e Replay de Experiência de Retrospectiva no contexto de recompensas especificadas por lógica, especificamente adaptado para a estrutura de MDP de Produto derivada da LTLfMT.
4. Validação Empírica: O framework é avaliado em ambientes de controle contínuo (Parking e Reacher) usando Aritmética Real Não-Linear (NRA). Os experimentos demonstram que a abordagem proposta, particularmente a combinação CRM-HER, supera as linhas de base (DDPG padrão, CRM-apenas e HER-apenas) em tarefas com objetivos complexos e esparsos.

Resultados

Experimentos foram conduzidos usando Gradientes de Política Determinística Profunda (DDPG) em um ambiente de Parking modificado e um ambiente Reacher.

• Desempenho da Linha de Base: O DDPG padrão aplicado ao MDP de Produto teve grande dificuldade, muitas vezes falhando em aprender uma política de sucesso em tarefas complexas (ex: parking_1, parking_2) devido à esparsidade da recompensa.
• CRM vs. HER: O CRM sozinho melhorou o desempenho em tarefas onde a estrutura do autômato era o principal gargalo, mas ofereceu benefícios limitados quando o próprio objetivo era difícil de ser descoberto. O HER sozinho teve bom desempenho em cenários de descoberta de objetivos, mas não aproveitou totalmente a estrutura do autômato.
• Superioridade do CRM-HER: A abordagem combinada CRM-HER alcançou consistentemente o melhor ou o segundo melhor desempenho em todas as tarefas. Notavelmente, na tarefa mais complexa (parking_2), o CRM-HER foi o único método capaz de aprender uma política de sucesso. Os resultados sugerem que a sinergia entre o raciocínio contrafatual (explorando a estrutura do autômato) e a experiência de retrospectiva (explorando a generalização de objetivos) é fundamental para resolver tarefas complexas de recompensa esparsa em domínios contínuos.

Significância e Alegações

O artigo afirma que a LTLfMT oferece uma alternativa mais expressiva e reutilizável à LTLf para a especificação de recompensas, particularmente em domínios com dados contínuos ou heterogêneos. Ao deslocar a complexidade da codificação das funções de rotulagem manuais para solvers SMT prontos para uso, o framework reduz a intervenção humana e aumenta a velocidade de definição de novas tarefas.

Os autores enfatizam que sua abordagem facilita naturalmente a aplicação de HER em RL baseado em lógica. Como a especificação da recompensa é baseada em fórmulas de primeira ordem, as variáveis usadas na fórmula podem servir diretamente como base para definições de objetivos no HER, evitando a necessidade de engenharia de objetivos ad-hoc. O artigo conclui que esta integração de lógica simbólica, resolução SMT e técnicas modernas de RL (CRM e HER) fornece um caminho robusto para especificar e aprender comportamentos complexos e não-markovianos em configurações de controle contínuo, pavimentando o caminho para trabalhos futuros em restrições de segurança e aprendizado multitarefa.