A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

Resumo Técnico: Uma Formalização Cubical de Independência Condicional, Condicionamento Bayesiano e a Correção da D-Separação de Pearl

Enunciado do Problema
O artigo aborda uma lacuna fundamental na verificação formal do raciocínio probabilístico: o axioma de intercâmbio de álgebra convexa padrão, comum às formalizações de monoides de probabilidade desde Stone, é provadamente fraco demais para suportar o condicionamento Bayesiano completo. Enquanto as formalizações clássicas (ex: em Coq) tratam a independência condicional (IC) como uma igualdade proposicional entre probabilidades de valores reais, elas dependem da lógica clássica e da extensionalidade, muitas vezes exigindo hipóteses de positividade e divisão por probabilidades não nulas para derivar resultados estruturais como o axioma da interseção. Além disso, elevar o condicionamento Bayesiano recursivo para uma representação de Tipo Indutivo Superior (HIT) de distribuições revela um descompassio estrutural: o axioma de intercâmbio padrão assume um único peso interno compartilhado para misturas rearranjadas, enquanto o condicionamento Bayesiano produz naturalmente misturas com pesos internos distintos relacionados pela fórmula de Bayes.

Metodologia
O autor desenvolve uma formalização construtiva em Cubical Agda, utilizando Teoria de Tipos Cubica e Tipos Indutivos Superiores (HITs). A metodologia baseia-se em três mudanças estruturais em relação às abordagens clássicas:

1. Monoide de Probabilidade como um HIT: Distribuições finitas (FDist) são definidas como um HIT gerado por massas pontuais e uma operação de mistura ponderada binária. As leis algébricas convexas padrão (idempotência, comutatividade assimétrica, casos de fronteira, intercâmbio e associatividade assimétrica) são impostas como construtores de caminho (path constructors). Isso permite que igualdades distributivas sejam tratadas como transformações executáveis (caminhos) em vez de igualdades proposicionais opacas.
2. Independência Condicional Estrutural: A IC é definida como um caminho entre núcleos de distribuição (kXY z ≡ kX z ⊗D kY z) em vez de uma igualdade ponto a ponto de números reais. Isso permite o raciocínio composicional onde testemunhas de IC podem ser transportadas através de operações monádicas.
3. Tratamento Construtivo de Pesos: O desenvolvimento é polimórfico sobre uma assinatura de Peso abstrata (um corpo ordenado com ordem decidível), instanciada concretamente nos racionais ($\mathbb{Q}$). Isso evita a indecidibilidade da igualdade nos reais construtivos e permite o tratamento explícito de positividade e divisão.

Principais Contribuições e Resultados

• O Descompasso do Intercâmbio e Generalização: A principal descoberta técnica é que o axioma de intercâmbio padrão (lei medial) é insuficiente para o condicionamento Bayesiano completo. Condicionar uma mistura de 4 folhas cria duas metades internas com pesos distintos ($q_1$ e $q_2$) relacionados pela fórmula de Bayes, enquanto o axioma padrão exige que eles sejam idênticos ($q_1 = q_2$). O autor introduz um axioma de intercâmbio generalizado (mix-bayes-interchange) que permite pesos internos distintos. Prova-se que a forma padrão é o caso degenerado onde esses pesos coincidem.
• Axioma de Interseção Construtivo: O artigo fornece uma prova construtiva do axioma da interseção (que classicamente requer positividade) reduzindo-o à contração. Em vez da extração Bayesiana via divisão, a prova utiliza testemunhas estruturais de tipos $\Sigma$ de fatoração e hipóteses de habitação para variáveis de condicionamento. Isso recupera o conteúdo total da interseção para qualquer modelo de distribuição positiva concreta sem postulados.
• Verificação do Do-Calculus de Pearl: Todas as três regras do do-calculus de Pearl são verificadas ao nível do núcleo em pequenos modelos causais estruturais (SCMs):
  • Regras 1 e 3: Verificadas como corolários das leis do monoide e do lema constBind (intervenção em variáveis independentes deixa as marginais inalteradas).
  • Regra 2: Verificada em SCMs confundidos usando uma testemunha de IC estrutural de que a priori conjunta fatora. Isso estabelece a equivalência entre intervenção e condicionamento sob independência.
• Condicionamento Bayesiano Recursivo: Uma função total para o condicionamento Bayesiano recursivo é definida em um fragmento de suporte total do HIT. O autor liquida todas as seis obrigações de coerência necessárias para elevar esta função ao HIT completo. A quinta coerência (intercâmbio) exige o axioma generalizado mencionado acima.
• Alinhamento com Categorias de Markov: O monoide FDist é verificado como uma instância concreta de uma categoria de Markov (no sentido de Fritz e Cho–Jacobs). O axioma não trivial de delete-naturality (preservação da massa total) é provado via indução de HIT, confirmando que os construtores de caminho capturam corretamente a normalização estocástica.
• Correção da D-Separação: A correção do teorema da d-separação de Pearl é verificada construtivamente para quaisquer Grafos Acíclicos Dirigidos (DAGs) finitos. Isso cobre tanto formas intervencionais (para conjuntos multi-elemento $X, Y, Z$) quanto formas Bayesianas (para padrões elementares), derivadas via fatoração ancestral sem redução por caminho.

Significância e Alegações
O artigo afirma fornecer a primeira formalização computacional verificada por máquina da direção da correção do teorema da d-separação de Pearl neste nível de generalidade, inteiramente dentro de um arcabouço de teoria de tipos.

• Conteúdo Computacional: Diferente das formalizações clássicas onde a IC é uma asserção, a abordagem cubica produz conteúdo computacional. Testemunhas de IC são transformações executáveis; distribuições posteriores são termos executáveis computados pelo normalizador do Agda.
• Correção Fundamental: O trabalho identifica que a fundação algébrica padrão para monoides de probabilidade é "fraca demais" para o condicionamento Bayesiano. A generalização proposta do axioma de intercâmbio é apresentada como um refinamento estrutural necessário para qualquer arcabouço que pretenda suportar inferência Bayesiana completa dentro de um ambiente monádico.
• Verificação da Pilha de Mahadevan: O artigo verifica a "camada inferior" da estrutura de Modelo Causal de Topos (TCM) de Mahadevan. Ele confirma que as identidades de núcleo do do-calculus e o monoide de distribuição comutativa de fato ocorrem construtivamente, servindo como um substrato verificado sobre o qual a maquinaria topológica (feixes, semântica de forcing) pode ser construída.
• Zero Postulados: Todo o desenvolvimento, incluindo a correção da d-separação e o condicionamento Bayesiano, é verificado com zero postulados acima da interface de campo ordenado abstrato (instanciada em $\mathbb{Q}$). Isso inclui a remoção de limites anteriormente usados e a substituição da divisão clássica por operações construtivas guardadas por positividade.

O artigo conclui que o conteúdo construtivo da independência condicional e do condicionamento é melhor capturado não pela lógica clássica mais extensionalidade, mas pelo raciocínio estrutural e baseado em caminhos da teoria de tipos cúbica, onde as leis algébricas da probabilidade são intrínsecas à definição do tipo.