COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management

O artigo apresenta a aplicação da ferramenta COOL-MC para verificar e explicar políticas de aprendizado por reforço na gestão de estoques de plaquetas, demonstrando como a combinação de verificação probabilística e explicabilidade garante decisões transparentes e seguras em cadeias de suprimentos de saúde críticas.

O essencial

Imagine que você é o gerente de um banco de sangue. Sua tarefa mais importante é garantir que sempre haja plaquetas (um tipo de célula do sangue) disponíveis para pacientes que precisam de transfusão, como vítimas de acidentes ou pessoas com câncer.

Mas aqui está o grande problema: as plaquetas são como flores frescas. Elas duram apenas 5 dias. Se você tiver muitas, elas estragam e você joga fora (o que é um desperdício de recurso caro e escasso). Se você tiver poucas, pacientes podem morrer por falta de sangue (o que é uma tragédia).

O desafio diário é: Quantas caixas de plaquetas devo pedir hoje? Pedir demais é desperdício; pedir de menos é risco de vida.

O "Gênio" de Computador (IA)

Para resolver isso, os pesquisadores usaram uma Inteligência Artificial chamada Aprendizado por Reforço (RL). Pense nela como um "aluno" que joga um videogame milhões de vezes.

• Se ele pede de menos e o paciente morre (na simulação), ele leva uma "punição".
• Se ele pede de mais e as plaquetas estragam, ele também leva uma "punição".
• Com o tempo, o computador aprende a jogar perfeitamente, criando uma estratégia (uma política) para pedir a quantidade exata.

O Problema: O computador aprendeu a jogar muito bem, mas ele é uma "caixa preta". Ele toma decisões, mas ninguém sabe por que ele decidiu pedir 14 caixas hoje em vez de 10. Em um hospital, os médicos não podem confiar em uma "caixa preta" que pode errar sem aviso.

A Solução: O "Detetive" COOL-MC

É aqui que entra o COOL-MC, a ferramenta apresentada neste artigo. Pense no COOL-MC como um detetive forense ou um tradutor que entra na mente do computador para explicar o que ele está pensando.

O COOL-MC faz três coisas principais:

1. O Mapa do Tesouro (Verificação):
   Em vez de tentar analisar todas as possibilidades do universo (o que seria impossível), o COOL-MC desenha apenas o "mapa" das situações que o computador realmente vai encontrar. Ele usa esse mapa para calcular matematicamente: "Qual a chance de faltar sangue nos próximos 200 dias?"

   • Resultado: O computador aprendeu a ter apenas 2,9% de chance de faltar sangue e 1,1% de chance de ter excesso (que vai para o lixo). Isso é muito seguro!

2. O Raio-X (Explicação):
   O detetive COOL-MC faz perguntas ao computador: "O que você está olhando para decidir?"

   • Eles descobriram que o computador ignora coisas que os humanos acham importantes, como "dia da semana" ou "pedidos pendentes".
   • Em vez disso, ele foca obsessivamente na idade das plaquetas. Ele sabe exatamente quais caixas estão prestes a vencer e quais são frescas. É como se ele tivesse um radar para a "data de validade".

3. O "E Se...?" (Análise Contrafactual):
   O COOL-MC permite fazer testes de "E se?".

   • Pergunta: "E se, em vez de pedir 14 caixas, pedíssemos apenas 6?"
   • Resposta do Detetive: "Não faz diferença! O computador só pede 14 quando o estoque está super cheio e seguro. Se você reduzir o pedido, ele ainda estará seguro."
   • Isso mostra que o computador não está sendo "teimoso", mas sim inteligente e cauteloso.

A Analogia do Chuveiro

Imagine que você está tomando um banho e precisa ajustar a temperatura.

• O RL (IA) é um robô que aprendeu a ajustar a torneira perfeitamente para não queimar nem congelar você.
• O COOL-MC é o técnico que entra, olha o robô e diz: "Olha, ele não está olhando para o relógio (dia da semana). Ele está olhando apenas para a temperatura da água que já está saindo. Se você mudar a torneira para 'água fria' (reduzir o pedido) quando a água já está morna, ele vai se adaptar e você não vai sentir diferença. Mas se você tirar o sensor de temperatura (idade das plaquetas), ele vai te queimar!"

Por que isso é importante?

Antes, os hospitais tinham medo de usar IAs porque não entendiam como elas pensavam. Com o COOL-MC, os gerentes de banco de sangue podem:

1. Verificar matematicamente que a IA é segura.
2. Entender que a IA está focada no que importa (a validade das plaquetas).
3. Confiar na decisão da máquina, sabendo que ela foi "auditada" por um detetive digital.

Em resumo, o artigo mostra que é possível ter uma Inteligência Artificial superinteligente gerenciando vidas, desde que tenhamos as ferramentas certas para abrir a "caixa preta" e garantir que ela está fazendo o bem.

Resumo técnico

1. O Problema

A gestão de estoques de plaquetas representa um desafio crítico de segurança na cadeia de suprimentos de saúde devido a três fatores principais:

• Vida útil curta: As plaquetas expiram em apenas 5 dias.
• Demanda incerta: A demanda diária é estocástica e difícil de prever.
• Conflito de objetivos: Os bancos de sangue devem equilibrar o risco de escassez (que pode colocar vidas em risco) com o risco de desperdício (devido ao vencimento do estoque).

Embora o Aprendizado por Reforço (RL) tenha demonstrado capacidade de aprender políticas de pedido eficazes para este Processo de Decisão de Markov (MDP), as políticas resultantes (geralmente redes neurais) são "caixas-pretas". Isso impede a adoção em domínios críticos de segurança, pois os gestores não conseguem entender por que uma decisão foi tomada, nem garantir formalmente que a política não violará restrições de segurança (como esgotar o estoque com alta probabilidade).

2. Metodologia

O artigo aplica a ferramenta COOL-MC, que integra RL, verificação de modelos probabilísticos e explicabilidade de RL. A metodologia segue quatro etapas principais:

A. Modelagem do MDP

O problema é modelado como um MDP inspirado em Haijema et al., com:

• Estado: Representado por 8 características: dia da semana, 5 classes de idade do estoque (plaquetas com 1 a 5 dias de vida restante), pedidos pendentes e uma fase de decisão.
• Ações: Níveis de pedido (0 a 30 unidades agregadas).
• Dinâmica: Demanda segue uma distribuição Poisson truncada. O sistema opera em duas fases diárias: decisão de pedido (não determinística) e realização da demanda estocástica (com FIFO para atendimento e descarte de itens vencidos).
• Recompensa: Penaliza escassez e desperdício com uma razão de custo de 5:1 (escassez é 5x mais custosa que o desperdício).

B. Treinamento da Política

Uma política de RL foi treinada utilizando o algoritmo PPO (Proximal Policy Optimization) com uma rede neural feedforward (3 camadas ocultas de 256 neurônios) por 25.000 episódios.

C. Construção do DTMC Induzido

Em vez de verificar o MDP completo (que sofre da maldição da dimensionalidade), o COOL-MC constrói uma Cadeia de Markov de Tempo Discreto (DTMC) induzida pela política treinada.

• O algoritmo explora apenas os estados alcançáveis sob a política específica, resolvendo a não-determinística.
• Isso reduz drasticamente o espaço de estados (de ~1,68 milhão para ~5.200 estados), tornando a verificação formal viável.

D. Verificação e Explicação

Sobre o DTMC induzido, são aplicadas duas abordagens:

1. Verificação Formal (PCTL): Uso da lógica temporal probabilística (PCTL) no verificador Storm para calcular probabilidades exatas de propriedades de segurança (ex: "Qual a probabilidade de atingir estoque zero em 200 passos?").
2. Explicabilidade:
   • Poda de Características (Feature Pruning): Remove-se uma entrada da rede neural (ex: "dia da semana") e re-verifica-se a política para medir o impacto na segurança.
   • Permutação de Importância: Avalia a relevância local de características em estados específicos.
   • Rótulos de Ação: Anotação de estados com a ação escolhida para permitir consultas formais sobre o comportamento de decisão.
   • Análise Contrafactual: Substituição de ações específicas (ex: trocar pedidos médios por pequenos) para simular cenários "e se" sem retreinar o modelo.

3. Principais Contribuições

• Primeira Verificação Formal: Este é o primeiro estudo a aplicar verificação formal e explicabilidade a uma política de RL para gestão de estoques de plaquetas.
• Pipeline COOL-MC Aplicado: Demonstra a eficácia da ferramenta COOL-MC em um cenário de saúde real, combinando verificação de segurança com explicabilidade causal.
• Análise Estrutural vs. Métricas Agregadas: Vai além da simples métrica de custo esperado, fornecendo garantias probabilísticas exatas e insights sobre como a política toma decisões (ex: quais características do estoque ela prioriza).

4. Resultados Chave

• Desempenho de Segurança: A política treinada alcançou uma probabilidade de escassez (stockout) de 2,9% e uma probabilidade de estoque cheio (risco de desperdício) de 1,1% dentro de um horizonte de 200 passos.
• Eficiência Computacional: A construção do DTMC induzido reduziu o espaço de estados em mais de 99,6% em comparação com o MDP completo, permitindo a verificação formal onde métodos tradicionais falhariam.
• Explicabilidade e Fatores Críticos:
  • Distribuição de Idade: A política ignora quase completamente o "dia da semana" e "pedidos pendentes". Ela foca quase exclusivamente na distribuição de idade do estoque.
  • Prevenção de Escassez: As características de estoque mais fresco (idades 4 e 5) são as mais críticas para evitar a escassez. Removê-las aumentou a probabilidade de falta de estoque em mais de 1000%.
  • Prevenção de Desperdício: O estoque mais antigo (idade 1) é o fator dominante para evitar o excesso de estoque.
• Análise de Ações:
  • A política emprega uma estratégia diversificada, mas 7 quantidades de pedido nunca são selecionadas.
  • Análise Contrafactual: Substituir pedidos médios/grandes (14 unidades) por pedidos menores (6 unidades) em 11,8% dos estados não alterou significativamente as probabilidades de segurança. Isso indica que esses pedidos maiores ocorrem em estados com "amortecedores" de estoque suficientes, onde a redução não compromete a segurança.

5. Significado e Impacto

O trabalho demonstra que é possível integrar RL em cadeias de suprimentos de saúde críticas sem sacrificar a transparência ou a segurança.

• Confiança e Adoção: Ao fornecer garantias formais (probabilidades exatas de falha) e explicações claras (quais dados a IA está usando), o COOL-MC supera a barreira da "caixa-preta", facilitando a adoção por gestores de bancos de sangue.
• Auditoria e Segurança: Oferece uma ferramenta para auditar políticas antes da implantação, permitindo que os gestores verifiquem se a política atende a requisitos de segurança específicos e se é robusta a variações nos dados de entrada.
• Generalização: A abordagem sugere um caminho para aplicar verificação formal e explicabilidade em outros domínios de saúde e logística onde o RL é promissor, mas o risco de falha é inaceitável.