Resumo Técnico: ExplAIner: Uma Linguagem de Consulta Declarativa para Explicar Modelos de Classificação

1. Declaração do Problema

O campo da IA Explicável (XAI) produziu uma proliferação de noções, pontuações e consultas de explicação distintas (ex: abdutiva, contrastiva, necessidade de características, contrafatuais). Do ponto de vista da gestão de dados, essa diversidade carece de um framework unificado. As abordagens atuais frequentemente exigem o design de algoritmos separados para cada tarefa de explicação. O artigo postula que é necessária uma linguagem de consulta declarativa para especificar, combinar e analisar essas noções de forma uniforme.

No entanto, as linguagens fundamentais existentes enfrentam duas limitações críticas:

1. Expressividade: Elas frequentemente falham em capturar noções centrais de explicação baseadas em otimalidade (ex: explicações abdutivas mínimas).
2. Complexidade: Seus problemas de avaliação podem ser intratáveis, atingindo altos níveis da hierarquia polinomial (PH), tornando-os impraticáveis para implementação utilizando motores baseados em SAT padrão.

O desafio central é projetar uma lógica que equilibre expressividade suficiente para capturar uma ampla família de consultas de explicação com complexidade de avaliação controlada (especificamente, tratabilidade via solvers SAT, correspondente à hierarquia booleana sobre NP).

2. Metodologia e Framework

Os autores desenvolvem um framework para explicar modelos booleanos (funções $M: \{0, 1\}^n \to \{0, 1\}$) tratando os modelos como estruturas sobre as quais as consultas são avaliadas. A metodologia procede em três estágios:

2.1 Análise de FOIL

O artigo revisita o FOIL (First-Order Interpretability Logic), uma lógica agnóstica ao modelo que trata modelos como caixas-pretas com acesso a instâncias positivas e à relação de inclusão ($\subseteq$) sobre instâncias parciais.

• Limitação de Expressividade: Os autores provam que o FOIL não consegue expressar a consulta para explicações abdutivas mínimas (mAXp), mesmo quando restrito a árvores de decisão. Isso é demonstrado usando jogos de Ehrenfeucht-Fraïssé para mostrar que o FOIL não consegue distinguir entre modelos onde uma explicação mínima existe e aqueles onde ela não existe, baseando-se apenas na inclusão.
• Limitação de Complexidade: A avaliação do FOIL sobre árvores de decisão é mostrada como sendo difícil para cada nível da hierarquia polinomial ($\Sigma^P_k$-hard). Isso implica que o FOIL não pode ser avaliado com um número polinomial de chamadas a um oráculo NP, tornando-o inadequado para avaliação prática baseada em SAT.

2.2 Introdução do ExplAIner

Para abordar essas limitações, os autores introduzem o ExplAIner, uma lógica de primeira ordem em camadas com um vocabulário estendido.

• Extensão de Vocabulário: O ExplAIner adiciona uma relação binária $\preceq$ que compara instâncias parciais com base no número de características definidas (cardinalidade). Os autores provam que $\subseteq$ e $\preceq$ são independentes; nenhum pode ser definido em termos do outro sobre árvores de decisão.
• Estrutura em Camadas:
  1. Camada Atômica: Fórmulas sobre $\{\subseteq, \preceq\}$. Elas dependem apenas da estrutura das instâncias parciais, não do modelo. A avaliação está em P (tempo polinomial) e a validade é decidível via redução para aritmética de Presburger.
  2. Camada Quantificada: Estende a camada atômica com predicados AllPos e AllNeg (verificando se todas as complementações de uma instância parcial são classificadas positivamente/negativamente) e quantificadores guardados. Quantificadores guardados restringem a quantificação universal a instâncias parciais com exatamente uma característica definida. Se AllPos e AllNeg forem tratáveis (em P) para uma classe de modelos, a avaliação desta camada está em NP.
  3. Camada Completa do ExplAIner: Permite combinações booleanas de fórmulas da camada quantificada. Esta camada captura toda a Hierarquia Booleana (BH) sobre NP.

2.3 Introdução do Opt-FOIL

Reconhecendo que a avaliação (verificar se uma instância é uma explicação) difere da computação (encontrar uma explicação), os autores definem o Opt-FOIL.

• Mecanismo: O Opt-FOIL é um fragmento do ExplAIner aumentado com um operador de minimização (min) sobre ordens parciais estritas definíveis.
• Sintaxe: Uma fórmula $\Psi = \min[\varphi, \rho]$ computa uma instância $x$ que satisfaz uma especificação lógica $\varphi$ que é mínima em relação a uma ordem parcial estrita $\rho$.
• Decidibilidade de Sintaxe: O artigo fornece um algoritmo (baseado em aritmética de Presburger) para verificar se uma determinada fórmula atômica define uma ordem parcial estrita, garantindo que o Opt-FOIL possua uma sintaxe decidível.

3. Contribuições Principais e Resultados

3.1 Limitações do FOIL

• Teorema 3.1: Nenhuma fórmula FOIL pode definir a consulta de explicação abdutiva mínima sobre árvores de decisão.
• Teorema 3.4: Para cada nível $k$ da hierarquia polinomial, existe uma fórmula FOIL fixa cuja avaliação sobre árvores de decisão é $\Sigma^P_k$-hard.

3.2 Expressividade e Complexidade do ExplAIner

• Expressividade: O ExplAIner codifica com sucesso uma ampla gama de noções de explicação, incluindo:
  • Explicações Fracas/Abdutivas/Abdutivas Mínimas (wAXp, AXp, mAXp).
  • Explicações Fracas/Contrastivas/Contrastivas Máximas (wCXp, CXp, mCXp).
  • Mudança Mínima Requerida (MCR) e Mudança Máxima Permitida (MCA).
  • Características Necessárias e Relevantes (NF, RF).
• Limites de Complexidade:
  • Camada Atômica: A avaliação está em P.
  • Camada Quantificada: Se AllPos e AllNeg estiverem em P, a avaliação está em NP. Existem consultas nesta camada que são NP-completas sobre árvores de decisão.
  • Camada Completa: Se AllPos e AllNeg estiverem em P, a avaliação está na Hierarquia Booleana (BH). Especificamente, para cada nível $BH_k$, há uma consulta ExplAIner que é $BH_k$-hard sobre árvores de decisão.
  • Aplicabilidade: Esses limites valem para árvores de decisão, circuitos d-DNNF (de forma normal disjuntiva negada decomponível determinística), 2CNF e Horn CNF.

3.3 Garantias Computacionais do Opt-FOIL

• Teorema 5.3: Se AllPos e AllNeg estiverem em P, o problema de computação para qualquer fórmula Opt-FOIL está em FPNP (funções computáveis em tempo polinomial com um número polinomial de chamadas a um oráculo NP).
• Algoritmo: A computação envolve a construção de um caminho na ordem parcial estrita. Como o comprimento de tais caminhos é polinomialmente limitado (Lema 5.5), o algoritmo termina com um número polinomial de chamadas ao solver SAT.
• Contenção Estrita: Assumindo que a hierarquia polinomial não colapse, o Opt-FOIL está estritamente contido no ExplAIner, que está estritamente contido no FOIL (com predicados estendidos). Isso confirma que o Opt-FOIL sacrifica parte do poder expressivo (ex: não pode expressar certas consultas de não-otimalidade que o ExplAiner pode) para ganhar tratabilidade computacional para encontrar respostas.

4. Significância e Alegações

O artigo alega que o ExplAIner e o Opt-FOIL fornecem uma base declarativa e principista para a XAI formal.

• Uniformidade: Eles oferecem uma linguagem única para especificar diversas noções de explicação, permitindo a combinação de critérios (ex: encontrar uma explicação comum para múltiplas instâncias).
• Tratabilidade: Ao restringir a lógica para camadas onde a avaliação está na hierarquia booleana e a computação está em FPNP, o framework alinha-se com as capacidades dos solvers SAT modernos. Isso é crucial porque a XAI formal frequentemente depende de codificações SAT para modelos como árvores de decisão e circuitos d-DNNF.
• Separação de Preocupações: O framework separa a especificação lógica das consultas de explicação da complexidade dependente da representação da avaliação. Isso permite que a mesma linguagem de consulta seja aplicada a diferentes classes de modelos (árvores, circuitos), desde que suportem verificações de consistência eficientes (AllPos/AllNeg).

Os autores concluem que, embora o FOIL sirva como uma ferramenta teórica fundamental, ele é inadequado para implementação prática devido à sua alta complexidade e expressividade limitada em relação à otimalidade. O ExplAIner e o Opt-FOIL resolvem esses problemas, permitindo a especificação e computação eficiente de explicações para modelos booleanos.