Counting Worlds Branching Time Semantics for post-hoc Bias Mitigation in generative AI

Título: Semântica de Ramificação de Contagem de Mundos para Mitigação Post-hoc de Viés em IA Generativa

1. O Problema

Sistemas de Inteligência Artificial Generativa (como LLMs e geradores de imagens) tendem a amplificar os vieses presentes em seus dados de treinamento. Embora existam estratégias de mitigação no momento da inferência (inference-time), a maioria delas é empírica e carece de garantias formais.
O desafio central abordado pelo artigo é a necessidade de:

• Verificar formalmente se uma série de saídas geradas por uma IA respeita uma distribuição de probabilidade desejada para um atributo protegido (ex: gênero, raça) em qualquer ponto do processo de geração.
• Prever a probabilidade de que a série permaneça dentro de limites aceitáveis à medida que novas saídas são geradas.
• Determinar, de forma lógica e quantitativa, quantas e quais saídas devem ser removidas (post-hoc) para restaurar a equidade (fairness) na série final, sem a necessidade de re-treinamento do modelo.

2. Metodologia: A Lógica CTLF

Os autores propõem uma nova lógica modal chamada CTLF (Computational Tree Logic com Contagem de Mundos), adaptada para raciocinar sobre séries de eventos probabilísticos. A metodologia baseia-se em três pilares principais:

• Semântica de Contagem de Mundos (Counting Worlds Semantics):

  • O espaço de possibilidades é modelado como uma árvore de mundos, onde cada "mundo" representa um resultado possível em um passo específico da geração.
  • Diferente da lógica temporal linear tradicional (LTL), a CTLF utiliza uma estrutura de árvore (ramificada) para representar todas as extensões possíveis de uma série de saídas.
  • Cada caminho na árvore representa uma sequência completa de eventos.

• Operadores Modais Específicos:
  A lógica introduz operadores que permitem verificar propriedades estatísticas e temporais:

  • $\square_q \phi$ (Contagem Passada): Verifica se, no estado atual, o evento $\phi$ ocorreu pelo menos $q \times m$ vezes (onde $m$ é o número de saídas até o momento).
  • $\blacksquare_q \phi$ (Possibilidade de Contagem): Verifica se existe alguma série possível (dentro de uma distribuição definida) onde $\phi$ ocorreu pelo menos $q \times m$ vezes.
  • $\bigcirc_q \phi$ (Existência de Caminho): Verifica se existe pelo menos uma série completa onde $\phi$ ocorre $q \times n$ vezes.
  • $\triangleright_q \phi$ (Probabilidade Futura): Calcula a probabilidade de que o próximo evento seja $\phi$, dado o estado atual e a distribuição.
  • $\nabla_q \phi$ e $\dagger_q \phi$ (Propriedades de Caminho): Analisam se uma série completa satisfaz uma frequência mínima e qual a probabilidade de completar a série mantendo a distribuição desejada a partir de um ponto específico.

• Modelo Formal:
  O sistema define um modelo $M = (W, W^1, W^n, R_e, R_f, V)$, onde:

  • $W$ é o conjunto de mundos (resultados possíveis).
  • $R_e$ é uma relação de "ancestralidade" (passado).
  • $R_f$ é uma relação de "parentalidade" (futuro/ramificação).
  • $\Phi_\Sigma$ associa caminhos completos a uma distribuição de probabilidade alvo $\Sigma$.

3. Contribuições Principais

1. Formalização Lógica de Mitigação de Viés: A primeira proposta de usar lógica temporal ramificada com contagem de mundos para verificar e mitigar viés em tempo de execução (inferência) e post-hoc.
2. Capacidade de Previsão e Intervenção: O framework permite não apenas detectar que o viés já ocorreu, mas prever se a série pode ser corrigida no futuro e calcular exatamente quantos itens devem ser removidos para atingir a distribuição alvo.
3. Abordagem Post-hoc com Garantias Formais: Oferece um método para "limpar" uma série de saídas geradas (ex: removendo imagens ou textos enviesados) com base em cálculos lógicos rigorosos, garantindo que o subconjunto restante atenda aos critérios de equidade.
4. Exemplo Didático: Ilustração prática com geração de imagens de "engenheiros", mostrando como a lógica calcula odds (probabilidades) e decide quando intervir para corrigir uma distribuição de gênero desbalanceada (ex: de 75% masculino para 50/50).

4. Resultados e Exemplos

O artigo apresenta um exemplo de "mundo de brinquedo" (toy example) com 6 gerações de imagens:

• Cenário de Detecção: Em um ponto intermediário da geração (ex: 4ª imagem), a lógica verifica se a proporção atual de gêneros ainda permite atingir a meta de 50/50 no final.
• Cenário de Mitigação: Se a série gerada até o momento já excedeu a cota máxima permitida para um grupo (ex: 3 homens em uma meta de 50/50 para 6 itens), a lógica identifica que qualquer geração subsequente de um homem deve ser removida.
• Cálculo de Probabilidade: A lógica consegue determinar que, em certo estado, a probabilidade de completar a série de forma justa é de 50% ($\dagger_{1/2}$), indicando que uma única saída "errada" nas próximas etapas pode inviabilizar a correção.
• Validação: O modelo demonstra que é possível definir um subconjunto $O' \subset O$ (subconjunto mitigado) que satisfaz a distribuição desejada, removendo apenas os elementos necessários.

5. Significado e Impacto

• Transição do Empírico para o Formal: O trabalho preenche uma lacuna crítica ao fornecer garantias matemáticas para estratégias de mitigação de viés, que atualmente são majoritariamente heurísticas.
• Eficiência Operacional: Ao permitir a detecção precoce de desvios e a previsão de viabilidade de correção, evita o desperdício de recursos computacionais gerando saídas que já estão fadadas a serem injustas.
• Aplicabilidade Prática: Os autores planejam implementar essa lógica na ferramenta MIRAI Toolbox, permitindo sua aplicação em sistemas reais de texto-para-imagem e LLMs.
• Futuro: O trabalho abre caminho para modelos adaptativos onde as probabilidades de transição são atualizadas em tempo real (cadeias de Markov paramétricas) e para a integração de pesos nas transições para maior precisão.

Em resumo, a CTLF oferece uma estrutura teórica robusta para monitorar, prever e corrigir vieses em sistemas de IA generativa, transformando a mitigação de viés de um processo de "tentativa e erro" em um procedimento de verificação formal e controlável.