A homotopy-type-theoretic generalization of neurosymbolic inference

Resumo Técnico: Uma Generalização da Inferência Neurosimbólica via Teoria de Tipos Homotópicos

Enunciado do Problema
Os sistemas neurosimbólicos (NeSy) atuais dependem amplamente de um funcional unificado definido como uma soma ponderada por crença de uma quantidade lógica sobre um espaço de $\sigma$-estruturas (atribuições de valores a símbolos lógicos). Este funcional, frequentemente instanciado como contagem de modelos ponderados (WMC), lógica probabilística ou lógica difusa, opera sobre conjuntos. Os autores argumentam que os conjuntos são objetos "deliberadamente esquecidos" que descartam duas informações críticas essenciais para a NeSy estruturada:

1. Simetria: Eles falham em distinguir entre $\sigma$-estruturas que são idênticas até uma simetria da teoria (ex: trocar indivíduos intercambiáveis). Consequentemente, o funcional padrão supercontabiliza estruturas simétricas.
2. Multiplicidade de Prova: Eles colapsam múltiplas derivações distintas que testemunham uma consulta em um único número, ignorando o "de quantas formas" um fato é provado.

Este decategorificação gera um modo de falha específico conhecido como atalhos de raciocínio (reasoning shortcuts). Quando um modelo é treinado apenas em saídas lógicas, ele pode convergir para uma percepção que atribui o significado errado a conceitos latentes (um "atalho") enquanto preserva a saída. Métodos padrão têm dificuldade em identificar o posterior "consciente do atalho" (uma distribuição uniforme sobre o conjunto de confusão de conceitos equivalentes) sem recorrer a ensembles complexos ou estimativa de densidade expressiva.

Metodologia
O artigo propõe substituir os conjuntos subjacentes da inferência NeSy por tipos da Teoria de Tipos Homotópicos (HoTT). Neste arcabouço, um tipo lembra não apenas seus elementos, mas as maneiras pelas quais os elementos podem ser identificados (isomorfismos).

Os autores "elevam" os quatro ingredientes do funcional NeSy padrão (Eq. 1) um nível acima:

1. Espaço de Estrutura ($\Omega$): Substituído por um tipo onde tipos de identidade registram simetrias (renomeações de indivíduos). O conjunto clássico de estruturas é o caso de truncamento 0.
2. Função Lógica ($\ell$): Substituída por uma família de provas $P: \Omega \to \mathcal{U}$. O nível de truncamento de $P$ é um parâmetro de design: uma proposição (nível -1) verifica satisfação; um conjunto (nível 0) conta derivações; um grupóide (nível 1) identifica derivações simétricas.
3. Inferência: Substituída pela cardinalidade homotópica ponderada por crença. Em vez de uma simples soma, o valor da inferência é computado como:
   $$N(P, b) = \left\| \sum_{\omega:\Omega} P(\omega) \right\|_{V,b}$$
   Isso conta cada elemento ponderado pelo inverso do tamanho de seu grupo de simetria ($1/|Aut(x)|$), garantindo que estruturas simétricas contribuam menos que as assimétricas.
4. Valoração: A escolha do semiring comutativo (ex: $(+, \times)$ para probabilidade, $(\max, +)$ para tropical) determina qual invariante numérico é lido da cardinalidade homotópica.

Contribuições Principais

1. Arcabouço Teórico: Os autores formalizam a inferência NeSy como uma cardinalidade homotópica ponderada por crença. Este arcabouço introduz dois parâmetros explícitos ausentes em formulações clássicas: um parâmetro de simetria (definindo o grupo de renomeações permitidas) e um nível de truncamento (definindo a granularidade do rastreamento de provas).
2. Teorema de Conservatividade: Um teorema verificado por máquina (verificado em Lean 4) prova que, quando as simetrias são triviais (o grupo é a identidade) ou o semiring é idempotente, a cardinalidade homotópica colapsa exatamente para o funcional clássico baseado em conjuntos. Isso garante que o novo arcabouço seja uma generalização fiel.
3. Atalhos de Raciocínio como Órbitas: O artigo identifica o "conjunto de confusão" (o conjunto de atribuições de conceitos que geram a mesma saída) como uma órbita sob o grupo de simetria da teoria.
   • O posterior de conceito "consciente do atalho" é identificado como o único ponto invariante de simetria: a distribuição uniforme sobre a órbita.
   • Isso leva à Média de Órbita (Orbit-Averaging), um método de forma fechada para computar este posterior:
     $$\bar{p}(c | x) = \frac{1}{|G|} \sum_{g \in G} p_\theta(g^{-1} \cdot c | x)$$
   • Este método simetriza um único modelo base sobre o grupo $G$ que preserva a saída, sem exigir um ensemble ou estimativa de densidade.
4. Funções Geradoras: Para modelos permutáveis (exchangeable models), o arcabouço produz naturalmente funções geradoras exponenciais (via cardinalidade homotópica) em vez de funções geradoras ordinárias, alinhando-se com a teoria das espécies combinatórias.

Resultados Experimentais
Os autores avaliaram o método de média de órbita em benchmarks de atalhos de raciocínio do MNIST (especificamente tarefas com grupos de simetria conhecidos e verdade fundamental para identificabilidade de conceitos).

• Configuração: Uma única rede neural foi treinada para prever rótulos fundidos. A tarefa consistia em distinguir dígitos identificáveis (tamanho da órbita 1) de dígitos confundíveis (tamanho da órbita > 1).
• Comparação: Um wrapper de média de órbita de modelo único foi comparado contra um modelo base e um ensemble de 5 modelos treinado para diversidade (Bears).
• Descobertas:
  • O modelo base foi excessivamente confiante em dígitos confundíveis (alto Erro de Calibração Esperada, ECE).
  • A média de órbita reduziu o ECE em dígitos confundíveis de 0,614 para 0,010 enquanto preservava a acurácia dos rótulos e a calibração de conceitos identificáveis.
  • O ensemble treinado para diversidade alcançou melhorias de calibração semelhantes apenas sacrificando a acurácia dos rótulos ou descalibrando conceitos identificáveis, destacando um compromisso (trade-off) que o wrapper de modelo único evita.

Significância e Alegações
O artigo afirma que ler a inferência NeSy através da lente da HoTT fornece um "benefício concreto" ao expor a estrutura de simetria responsável pelos atalhos de raciocínio.

• Unificação Teórica: Unifica várias abordagens NeSy (probabilísticas, difusas, de proveniência) sob uma visão decategorificada de um objeto mais rico e estruturado.
• Eficiência Prática: Demonstra que o posterior "consciente do atalho", anteriormente considerado dependente de ensembles caros, pode ser computado em forma fechada ao tirar a média de um único modelo sobre o grupo de simetria.
• Calibração: O método melhora a calibração em conceitos não identificáveis sem degradar o desempenho em conceitos identificáveis, resolvendo um modo de falha específico do aprendizado NeSy.
• Limitações: Os autores observam que o arcabouço atual depende de tipos finitos ($\pi$-finitude). Estender a cardinalidade homotópica para domínios contínuos via "coesão" permanece um problema em aberto.

O trabalho é apresentado como uma mudança fundamental de um raciocínio baseado em conjuntos para um baseado em tipos, onde o "esquecimento" dos conjuntos é substituído pela memória estrutural dos tipos, abordando diretamente as causas raízes dos atalhos de raciocínio.