Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

Título: Interpretabilidade Mecanística Formal: Descoberta Automatizada de Circuitos com Garantias Prováveis

1. O Problema

A Interpretabilidade Mecanística (MI) visa decompor redes neurais em componentes e módulos funcionais compreensíveis por humanos. Um desafio central neste campo é a descoberta de circuitos: identificar subgrafos dentro da rede que são responsáveis por comportamentos específicos do modelo.

Apesar dos avanços recentes, a maioria dos métodos atuais de descoberta de circuitos é heurística ou aproximada. Eles dependem de:

• Amostragem discreta de inputs.
• Técnicas de "patching" (substituição de ativações) baseadas em valores fixos (como zero ou média) ou amostras aleatórias.

Limitações Críticas:

• Falta de Garantias Contínuas: Um circuito pode parecer fiel em pontos de amostragem, mas falhar sob pequenas perturbações contínuas no espaço de entrada ou nas ativações de patching.
• Insegurança para Segurança: Como a interpretabilidade está ligada a questões de segurança e confiabilidade, a falta de garantias rigorosas sobre domínios contínuos é preocupante. Pequenas perturbações podem quebrar a fidelidade do circuito descoberto.

2. Metodologia

Os autores propõem um novo framework que integra a Interpretabilidade Mecanística com os avanços recentes em Verificação de Redes Neurais. O objetivo é derivar circuitos com garantias matemáticas rigorosas sobre domínios contínuos.

Componentes Principais da Metodologia:

• Codificação Siamesa (Siamese Encoding):
  Para verificar propriedades que envolvem tanto o modelo completo quanto um subconjunto (circuito), os autores utilizam uma codificação siamesa. Eles duplicam o circuito e o "empilham" com o modelo original, criando um modelo combinado. Isso permite que verificadores formais (como o $\alpha$-$\beta$-CROWN) certifiquem diretamente a distância entre as saídas do modelo e do circuito sobre todo um domínio contínuo.

• Três Famílias de Garantias Prováveis:

  1. Robustez ao Domínio de Entrada (Input-Domain Robustness): Garante que o circuito seja fiel ao modelo em toda uma região contínua de entrada (ex: uma bola $\ell_p$ em torno de um ponto), não apenas em pontos amostrados.
  2. Robustez ao Domínio de Patching (Patching-Domain Robustness): Garante que a fidelidade do circuito seja mantida mesmo quando as ativações dos componentes não pertencentes ao circuito são perturbadas dentro de um domínio contínuo de ativações viáveis, em vez de serem fixadas em valores constantes arbitrários.
  3. Minimalidade (Minimality): Formalização de diferentes graus de "succintude" do circuito, desde a minimalidade quase (quasi-minimal) até a minimalidade cardinal (o menor conjunto possível).

• Algoritmos de Descoberta:

  • Algoritmo Ganancioso (Greedy): Remove componentes iterativamente enquanto a fidelidade (definida pelas garantias acima) é mantida.
  • Busca Binária: Uma variante mais rápida para encontrar circuitos "quase-minimais".
  • Método de Conjuntos de Bloqueio (Blocking-sets) e MHS: Utiliza uma dualidade teórica entre circuitos e "conjuntos de bloqueio" (subgrafos cuja remoção quebra a fidelidade). O algoritmo calcula o Conjunto de Atingimento Mínimo (Minimum Hitting Set - MHS) desses conjuntos de bloqueio para aproximar ou encontrar circuitos cardinalmente mínimos (globalmente ótimos).

• Propriedade de Monotonicidade:
  Os autores provam que, sob certas condições (onde o domínio de patching engloba o domínio de entrada e o espaço de ativação é fechado sob concatenação), o predicado de fidelidade torna-se monotônico. Isso é crucial, pois garante que algoritmos gananciosos convergem para circuitos subset-minimais (nenhum subconjunto próprio é fiel), evitando mínimos locais "ruins".

3. Contribuições Chave

Teóricas:

• Formalização de Garantias: Definição rigorosa de robustez de entrada e de patching sobre domínios contínuos, superando a dependência de amostragem.
• Conexões Teóricas: Descoberta de conexões profundas entre robustez de entrada, robustez de patching e minimalidade. A prova de que a monotonicidade do predicado de fidelidade é a chave para garantir minimalidade de subconjunto.
• Dualidade Circuito-Bloqueio: Estabelecimento de uma dualidade entre circuitos fiéis e conjuntos de bloqueio, permitindo o uso de solvers de SAT/MILP para encontrar circuitos minimalmente cardinais de forma eficiente.

Empíricas:

• Framework de Codificação Siamesa: Uma técnica técnica para codificar redes neurais e seus circuitos em um único modelo para verificação formal.
• Algoritmos Automatizados: Implementação de algoritmos que convergem para circuitos com garantias de minimalidade e robustez.
• Avaliação Extensiva: Experimentos realizados em modelos de visão (MNIST, CIFAR-10, GTSRB, TaxiNet) utilizando o verificador de ponta $\alpha$-$\beta$-CROWN.

4. Resultados Experimentais

Os experimentos compararam a abordagem proposta (provável) com métodos baseados em amostragem (padrão na literatura):

• Robustez de Entrada:

  • O método baseado em amostragem atingiu taxas de robustez baixas (ex: 46,5% no CIFAR-10, 19,2% no MNIST).
  • O método provável alcançou 100% de robustez em todos os conjuntos de dados, garantindo que o circuito funciona corretamente em toda a vizinhança contínua, embora com um custo computacional maior (tempo de verificação).
  • O tamanho dos circuitos foi comparável entre os dois métodos.

• Robustez de Patching:

  • Circuitos descobertos com patching zero ou médio falharam drasticamente quando testados sob perturbações contínuas de patching (robustez < 60% em muitos casos).
  • O método provável garantiu 100% de robustez contra perturbações contínuas no domínio de patching.

• Minimalidade:

  • Os algoritmos de busca iterativa e binária encontraram circuitos menores que os métodos padrão.
  • O método baseado em MHS (Minimum Hitting Set) conseguiu aproximar ou encontrar circuitos cardinalmente mínimos (os menores possíveis), demonstrando que a busca exata é viável para redes de tamanho moderado através da exploração da dualidade.

5. Significado e Impacto

Este trabalho representa um marco fundamental na área de Interpretabilidade Mecanística:

1. Transição de Heurística para Formal: Move a descoberta de circuitos de uma abordagem baseada em "tentativa e erro" e amostragem para uma base matemática rigorosa com garantias de correção.
2. Segurança e Confiabilidade: Ao garantir que os circuitos descobertos são robustos a perturbações contínuas, o trabalho fornece uma base mais segura para confiar nas explicações geradas por IA, essencial para aplicações críticas.
3. Ponte entre Áreas: Integra bem-sucedida a teoria de Verificação Formal de Redes Neurais (tradicionalmente usada para robustez adversarial) com a Interpretabilidade, criando um novo subcampo de "Interpretabilidade Formal".
4. Futuro: Estabelece as fundações teóricas e algorítmicas para futuras pesquisas em descoberta de circuitos prováveis, abrindo caminho para métodos que podem escalar para modelos maiores à medida que as técnicas de verificação evoluem.

Em resumo, o artigo demonstra que é possível descobrir circuitos internos de redes neurais que não apenas explicam o comportamento do modelo, mas que são matematicamente garantidos para serem fiéis e mínimos sob condições contínuas, superando as limitações fundamentais dos métodos atuais.