A Contractive Feedback Semantics for Reinforcement Learning

Resumo Técnico: Uma Semântica de Feedback Contrativo para Aprendizado por Reforço

Declaração do Problema
O Aprendizado por Reforço (RL) padrão é tipicamente formalizado como programação dinâmica em Processos de Decisão de Markov (MDPs) fechados. Nesta visão, uma política é fixada, um operador de Bellman é definido, e a função valor é estudada como o ponto fixo desse operador. Embora eficaz, essa abordagem obscurece a realidade estrutural de que a transição de um passo é um componente aberto com interfaces de entrada/saída, um canal de recompensa e uma continuação. O valor de horizonte infinito emerge apenas quando a continuação é realimentada no componente. Teorias existentes frequentemente carecem de uma linguagem composicional para analisar rigorosamente se substituições locais (por exemplo, em sistemas modulares, filtros de estado de crença ou avaliações off-policy) permanecem válidas dentro de sistemas circundantes arbitrários. O artigo aborda a necessidade de uma semântica que trate componentes de RL como objetos abertos e tipados, onde o feedback é explícito e composicional.

Metodologia
O artigo propõe uma visão composicional onde um processo de decisão de um passo é tratado como um componente estocástico aberto, e a avaliação de política de horizonte infinito é obtida fechando um laço de feedback contrativo. A metodologia repousa sobre três princípios semânticos:

1. Princípio do Feedback: O valor de horizonte infinito é o resultado de alimentar uma saída de continuação de volta em um componente de um passo. O desconto torna esse feedback "protegido" (contrativo), garantindo que o valor do laço fechado seja unicamente definido pelo teorema do ponto fixo de Banach.
2. Princípio Contextual: Componentes são comparados em suas interfaces. Se dois componentes induzem transformadores tipados próximos, sua diferença deve permanecer controlada após a inserção em um circuito de decisão maior.
3. Princípio do Contrato: Requisitos de correção (segurança, risco, recursos) são limites superiores em uma álgebra ordenada. Esses limites devem compor-se localmente, elevando-se de subcomponentes para sistemas conectados maiores via transformadores monótonos e pontos fixos mínimos.

O desenvolvimento técnico utiliza:

• Camada Estocástica: Núcleos de Markov como morfismos na categoria Stoch.
• Camada de Valor (Métrica): Espaços de Banach de funções mensuráveis limitadas ($B(S)$) para retornos descontados aditivos, utilizando contração $\gamma$.
• Camada de Valor (Ordem): Retículos completos enriquecidos por quantales para garantias ordenadas (risco, segurança), utilizando mapas monótonos $\omega$-contínuos.
• Semântica de Traço: Um "traço de Banach protegido" onde a operação de traço é definida apenas para mapas cujo fio de feedback é uniformemente contrativo, realizado como um ponto fixo único.

Principais Contribuições e Resultados

1. Semântica de Bellman Traçada Protegida:
   O artigo formula componentes de decisão descontados abertos (ODDCs) e prova que a avaliação de política é o traço de Banach protegido de um circuito de feedback admissível. Não assume uma operação de traço global em mapas arbitrários; em vez disso, restringe o traço à classe admissível de circuitos protegidos onde o fator de desconto garante contração.

2. Composicionalidade Tipada:
   Os autores provam que operações de conexão correspondem a operações estruturais em transformadores de Bellman:

   • Conexão em Série: Corresponde à composição de funções de transformadores de continuação, com contabilidade explícita de desconto (recompensas de estágios posteriores são descontadas mais profundamente).
   • Conexão em Paralelo: Corresponde ao tensoramento (produto) de transformadores, preservando estruturas de valor aditivas/separáveis sob independência.
   • Feedback: Corresponde a um traço de ponto fixo protegido.

3. Equivalência Contextual (Congruência):
   O artigo define uma métrica de operador em bolas de valor invariantes e prova que a equivalência aproximada é preservada por contextos lineares bem tipados admitidos (contextos onde o "buraco" é usado exatamente uma vez).

   • Resultado: Se dois componentes têm um erro local de operador $\epsilon$, o erro no valor final de ponto fixo do circuito composto é limitado por $L(C) \cdot \frac{1}{1-\kappa(C)} \cdot \epsilon$, onde $L(C)$ é o ganho do contexto e $\kappa(C)$ é o módulo de contração. Isso fornece constantes de sensibilidade explícitas e computáveis para propagação de erro.

4. Abstração Coalgebráica:
   O framework conecta-se à teoria de representação tratando MDPs como coalgebras.

   • Abstração Exata: Prova que homomorfismos comutantes (preservando recompensas e núcleos de transição) produzem preservação exata de valor via entrelaçamento de operadores.
   • Abstração Aproximada: Quantifica a distorção de valor sob comutação aproximada (diferença de recompensa limitada e diferença de transição em variação total), fornecendo limites explícitos de norma sup que se propagam através de contextos de circuito.

5. Contratos de Quantale:
   O artigo introduz uma camada para especificações de segurança, risco e recursos usando contratos com valores em quantales.

   • Resultado: Sob semântica de transformadores de contrato monótonos $\omega$-contínuos, limites indutivos locais (pré-pontos fixos) elevam-se através de conexões em série, paralelas e de feedback para garantias globais via raciocínio de ponto fixo mínimo. Isso separa o raciocínio de ponto fixo métrico (para recompensas) do raciocínio de ordem (para restrições).

6. Extensões e Verificações de Sanidade:
   O framework é mostrado para cobrir:

   • Levantamento de Estado de Crença: MDPs Parcialmente Observáveis (POMDPs) são tratados como elevando o objeto de estado para o espaço de crença, aplicando a mesma semântica de ponto fixo.
   • Avaliação Off-policy: Mudanças de medida de trajetória são analisadas como mudanças composicionais de medida, com derivadas de Radon–Nikodym fatorando-se sob decomposições específicas de circuito.
   • Não Estacionariedade: Operadores variantes no tempo são rastreados via métricas de deriva de operador, produzindo limites sobre o erro de rastreamento de ponto fixo.

Significado e Alegações
O artigo alega explicitamente não ser um novo algoritmo de aprendizado, um estudo empírico ou uma proposta de uma categoria monoidal traçada global para todos os morfismos de RL. Em vez disso, seu significado reside em uma reformulação teórica da semântica de RL em torno de feedback contrativo.

A alegação central é que a avaliação descontada de Bellman admite uma semântica de feedback contrativo na classe admissível de circuitos protegidos. Essa perspectiva produz:

• Congruência Contextual: Erros locais de operador permanecem controlados em circuitos circundantes, com limites explícitos.
• Limites de Abstração Explícitos: Preservação e distorção de valor são derivadas de propriedades de comutação coalgebráica.
• Segurança Composicional: Especificações de segurança e risco podem ser verificadas localmente e elevadas composicionalmente.

O artigo argumenta que essa visão expõe a estrutura composicional suprimida pela notação padrão de MDP fechado, fornecendo uma base rigorosa para sistemas de decisão modulares, filtragem de estado de crença e avaliação off-policy onde substituições locais devem ser validadas dentro de contextos arbitrários.