Axiomatic Foundations of Counterfactual Explanations

Resumo Técnico: Fundamentos Axiomáticos de Explicações Contrafatuais

Problema
O artigo aborda uma lacuna crítica na literatura sobre IA Explicável (XAI). Embora as explicações contrafatuais (respondendo a perguntas do tipo "por que não") tenham emergido como um método convincente para aumentar a confiança em sistemas autônomos, a pesquisa existente sofre de duas limitações principais:

1. Falta de Classificação Sistemática: A maior parte do trabalho existente foca em um único tipo de contrafatual local (adaptado a instâncias individuais) sem estudar sistematicamente tipos alternativos.
2. Negligência de Explicações Globais: Há pouca atenção dedicada às explicações contrafatuais globais, que visam explicar o processo de raciocínio geral de um modelo, em vez de apenas previsões individuais.
   Consequentemente, os compromissos teóricos entre contrafatuais locais e globais, e entre diferentes definições de "proximidade" ou "validade", permanecem mal compreendidos.

Metodologia
Os autores propõem um arcabouço axiomático para definir, comparar e caracterizar explicadores contrafatuais de forma sistemática. Esta abordagem, comum na ciência teórica, constrói um sistema baseado em um conjunto de axiomas claramente declarados (propriedades básicas) para derivar teoremas de representação.

• Configuração Formal: O arcabouço opera sobre uma teoria de classificação $T = \langle F, dom, C \rangle$ (características, domínios, classes) e um classificador $\kappa$. Uma consulta é definida como $Q = \langle T, \kappa, x \rangle$.
• Axiomas: O artigo introduz nove axiomas agrupados em três categorias:
  • Propriedades Gerais: Sucesso (saída não vazia), Não-Trivialidade (não há conjuntos vazios), Equivalência (mesma classe $\to$ mesma explicação) e Viabilidade (explicações são subconjuntos da instância).
  • Propriedades de Razões Necessárias: Essencialidade (explicações contêm apenas literais essenciais) e Validade Cética (remover a explicação garante uma mudança de classe).
  • Propriedades de Razões Suficientes: Novidade (explicações não contêm literais da instância original), Validade Forte (a presença da explicação garante uma mudança de classe) e Validade Fraca (substituir valores pela explicação resulta em uma classe diferente).
• Análise: Os autores utilizam esses axiomas para provar teoremas de impossibilidade (mostrando que certas combinações são incompatíveis) e teoremas de representação (estabelecendo correspondências um-para-um entre subconjuntos de axiomas e famílias de explicadores).

Principais Contribuições
O artigo apresenta seis contribuições primárias:

1. Arcabouço Axiomático: Introduz um arcabouço fundamentado em nove axiomas para definir explicadores contrafatuais.
2. Teoremas de Impossibilidade: Prova que nenhum explicador único pode satisfazer certas combinações de axiomas simultaneamente (ex: Sucesso, Não-Trivialidade e Essencialidade são incompatíveis).
3. Caracterização de Conjuntos Compatíveis: Caracteriza totalmente todos os conjuntos compatíveis de axiomas.
4. Teoremas de Representação: Estabelece correspondências um-para-um entre subconjuntos específicos de axiomas e cinco famílias distintas de explicadores, revelando cinco tipos fundamentalmente diferentes de contrafatuais:
   • Razões Necessárias Globais (GNR): Combinações de característica-valor que distinguem uma classe de todas as outras (satisfazem Essencialidade, Não-Trivialidade).
   • Razões Necessárias Locais Céticas (SNR): Subconjuntos de uma instância que a distinguem de todas as outras instâncias com uma decisão diferente (satisfazem Viabilidade, Validade Cética).
   • Razões Suficientes Globais (GSR): Combinações de característica-valor cuja presença garante uma classe diferente (satisfazem Validade Forte).
   • Razões Suficientes Locais Céticas (SSR): Novos valores de características não presentes na instância que garantem uma decisão diferente (satisfazem Novidade, Validade Forte).
   • Razões Suficientes Locais Crédulas (CSR): Combinações de característica-valor que distinguem uma instância de alguma instância com uma decisão diferente (satisfazem Novidade, Validade Fraca).
5. Taxonomia do Trabalho Existente: Caracteriza formalmente os explicadores existentes dentro desta taxonomia. O artigo constata que quase todos os explicadores locais existentes pertencem à família das Razões Suficientes Crédulas (CSR). Os explicadores globais propostos no trabalho anterior [2] correspondem às Razções Necessárias Globais (GNR). Esta análise revela três tipos anteriormente não reconhecidos (SNR, GSR, SSR).
6. Análise de Complexidade: Analisa a complexidade computacional de gerar essas explicações, distinguindo entre problemas de decisão (verificar se uma explicação é válida) e problemas de busca (gerar uma explicação).

Resultos

• Classificação: Os cinco tipos de contrafatuais são divididos em duas formas fundamentais: Razões Necessárias (o que deve estar ausente para mudar a decisão) e Razões Suficientes (o que deve estar presente para mudar a decisão).
• Existência e Compactação:
  • Razões necessárias (GNR, SNR) e Razões Suficientes Céticas (SSR) não são garantidas a existir para cada consulta.
  • Razões Suficientes Crédulas (CSR) e Razões Suficientes Globais (GSR) são garantidas a existir.
  • Razões necessárias são compactas (transmitem todo o intervalo de mudanças via um conjunto mínimo de literais), enquanto razões suficientes são não compactas (enumeram todas as mudanças possíveis).
• Preferência Humana: O artigo argumenta que as razões necessárias, quando existem, alinham-se melhor com as preferências humanas por explicações curtas e concisas em comparação com as razões suficientes, que costumam ser numerosas e verbosas.
• Complexidade:
  • Para classificadores booleanos, decidir se uma explicação é válida ($DECIDEEXP$) é$O(n)$ para CSRs, SNRs e explicadores baseados em esparsidade, mas co-NP-completo para GNRs, GSRs, SSRs e explicadores baseados em cardinalidade/distância.
  • Encontrar uma explicação ($FINDEXP$) é NP-difícil para a maioria das famílias (incluindo GNR, CSR, SNR, GSR), embora possa ser resolvido com no máximo $n$ chamadas a um oráculo SAT na maioria dos casos.

Significância
O artigo afirma fornecer o primeiro arcabouço axiomático para explicações contrafatuais. Sua significância reside em:

1. Rigor Teórico: Ir além da avaliação empírica para uma comparação principiada e objetiva de explicadores baseada nos axiomas que satisfazem.
2. Unificação e Descoberta: Unificar os explicadores locais existentes sob a família CSR, ao mesmo tempo em que identifica e define formalmente três novos tipos de contrafatuais (SNR, GSR, SSR) que eram anteriormente não reconhecidos.
3. Generalidade Agnóstica ao Modelo: O arcabouço é aplicável em diversos contextos e tipos de classificadores.
4. Fundação para Trabalhos Futuros: Ao caracterizar o espaço de possíveis explicadores, o arcabouço permite o design futuro de explicadores que satisfaçam combinações específicas de propriedades desejáveis (ex: acionabilidade, justiça, diversidade) dentro de um tipo específico de contrafatual.

Os autores concluem que, embora as razões necessárias sejam teoricamente atraentes por sua concisão, as razões suficientes são mais robustas em termos de existência. O arcabouço fornece as ferramentas necessárias para navegar nesses compromissos de forma sistemática.