🤖 AI

A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus

Este artigo apresenta a primeira formalização verificada por máquina em Cubical Agda de modelos causais de topos, verificando conceitos centrais como intervenção como mapas característicos e colagem de feixes (sheaf gluing), ao mesmo tempo em que identifica e repara uma lacuna nos axiomas de Lawvere-Tierney para estabelecer a estabilidade das regras de Pearl e demonstra uma obstrução de contextualidade dentro de um arcabouço seguro e livre de axiomas.

Autores originais: Karen Sargsyan

Publicado 2026-07-20

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Karen Sargsyan

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

O Dilema do Detetive: Por que a Causalidade Precisa de um Novo Mapa

Imagine que você é um detetive tentando resolver um mistério. Você tem uma lista de pistas: "Choveu", "A grama está molhada" e "O regador estava ligado". No passado, os cientistas tratavam essas pistas como uma simples lista de fatos. Se a grama estivesse molhada, eles poderiam supor que choveu. Mas a vida real é mais complexa. E se você deixasse a grama molhada ao ligar o regador? Isso muda o fato de que choveu? Este é o cerne da inferência causal: descobrir não apenas o que acontece junto, mas o que causa o quê, especialmente quando intervimos e mudamos as regras do jogo.

Por décadas, especialistas usaram diagramas e matemática para rastrear essas cadeias de causa e efeito. Mas recentemente, uma nova ideia surgiu: e se tratarmos todo o mundo das causas não como uma imagem estática, mas como uma paisagem mutável que muda dependendo de onde você está olhando? Este é o domínio da Teoria dos Topos, um ramo da matemática que estuda como formas e estruturas se encaixam. Pense nisso como uma linguagem universal para "colar" peças de informação. Se você tem um quebra-cabeça onde as peças se encaixam perfeitamente em suas mãos, mas não formam uma imagem completa quando você tenta montá-las sobre a mesa, esse é o problema que esta nova matemática tenta resolver. A grande questão é: podemos usar essa matemática de alto nível para construir um sistema infalível para entender a causa e o efeito, mesmo quando estamos mudando o mundo ao testar coisas?

A Jornada do Artigo: Construindo um Lego Causal

Este artigo é um projeto de construção massivo, verificado por computador. Os autores, liderados por Karen Sargsyan, pegaram uma teoria ousada chamada "Modelos Causais de Topos" e a reconstruíram do zero dentro de um programa de computador chamado Cubical Agda. Pense neste programa como um mestre de Lego super rigoroso que se recusa a deixar você encaixar dois blocos a menos que a conexão seja matematicamente perfeita. O objetivo era verificar uma teoria proposta por um pesquisador chamado Mahadevan, que sugere que podemos descrever todo o universo de causa e efeito usando as regras de um "Topos" (um universo matemático).

Os autores não apenas copiaram a teoria; eles a testaram, consertaram e encontraram coisas que o autor original deixou passar. Aqui está o que eles descobriram, explicado através de seu canteiro de obras digital.

1. O "Botão de Fazer" e o Filtro de Verdade

Na teoria original, uma intervenção (como forçar uma variável a ter um valor específico, escrito como do(X = x)) é descrita como um "mapa característico" especial. Imagine que você tem um mapa gigante de uma cidade (o mundo causal). Se você quiser forçar o fechamento de uma rua específica, você não apenas apaga a rua; você desenha um "filtro de verdade" especial sobre o mapa. Esse filtro destaca exatamente onde a rua está fechada e em nenhum outro lugar.

Os autores construíram este filtro em seu código de computador. Eles provaram que este filtro funciona exatamente como prometido: ele identifica perfeitamente a "rua fechada" e nada mais. Eles mostraram que isso não é apenas um truque inteligente; é uma regra fundamental deste universo matemático. Se você tentar forçar um valor que não se ajusta ao fluxo natural do mapa, o sistema o rejeita. Isso confirma que o "Botão de Fazer" é uma ferramenta sólida e confiável neste novo framework.

2. A Cola que Às Vezes Falha

Uma das promessas mais empolgantes da teoria original era a Colagem de Sheaves (Sheaf Gluing). Imagine que você tem três detetives diferentes olhando para uma cena de crime de três ângulos diferentes. Se o Detetive A concorda com o Detetive B, e o Detetive B concorda com o Detetive C, você pode assumir que todos concordam com a imagem completa. Nesta matemática, "colar" significa pegar essas visões locais e encaixá-las em uma verdade global gigante.

Os autores provaram que, para dois detetives, isso sempre funciona. Se suas visões se sobrepõem e coincidem, elas podem ser coladas perfeitamente. No entanto, eles encontraram uma falha quando três ou mais detetives estão envolvidos. Eles construíram um cenário (um "triângulo de Specker") onde cada par de detetives concorda perfeitamente, mas quando você tenta combinar todos os três, a imagem desmorona. Não existe uma única história global que se ajuste a todas as pistas locais. Isso é uma "obstrução de contextualidade". É como ter três peças de um quebra-cabeça que se encaixam em pares, mas quando você tenta colocá-las todas na mesa, elas formam um buraco no meio. Os autores provaram que isso não é um erro em seu código; é um recurso real da matemática. Significa que, em sistemas causais complexos, só porque as partes locais concordam, não significa que uma solução global exista. Você precisa de uma verificação global, não apenas de verificações locais.

3. Consertando a "Modalidade Mágica"

A teoria usa uma ferramenta especial chamada topologia de Lawvere-Tierney (vamos chamá-la de "Modalidade Mágica") para decidir quais fatos causais são "estáveis" ou "verdadeiros" através de diferentes situações. O artigo original listou três regras para esta ferramenta mágica. Os autores rodaram os números e descobriram um problema: aquelas três regras não eram suficientes! Eles encontraram uma escada estranha de três degraços onde a ferramenta seguia todas as três regras, mas ainda assim quebrava a lógica (não era "inflacionária", ou seja, não mantinha as coisas iguais ou maiores).

Eles corrigiram isso adicionando uma quarta regra. Com esta nova regra, a ferramenta mágica funciona corretamente. Eles então mostraram que esta ferramenta torna o "Cálculo de Do" (as regras para calcular causa e efeito) estável. Não importa como você fatie o mundo ou mude a perspectiva, as regras centrais da causalidade permanecem firmes. Eles até mostraram um exemplo específico desta "magia" em ação: a topologia da "dupla negação", que atua como um filtro que transforma verdades imprecisas e incertas em fatos clássicos claros.

4. Transportando a Verdade Entre Mundos

Finalmente, os autores abordaram a Transportabilidade: Uma regra que aprendemos em um mundo (como um hospital em Tóquio) pode ser confiável em outro (uma clínica em Nova York)? Em seu framework, mover um fato causal de um lugar para outro é o mesmo que verificar se ele é "estável" sob a Modalidade Mágica. Se um fato é estável, ele viaja com segurança. Se não for estável, pode quebrar quando você o mover. Eles provaram que, para certos tipos de fatos (como aqueles envolvendo intervenções), essa estabilidade é garantida. No entanto, observaram que, para cenários do mundo real mais complexos, onde os fatos podem mudar de valores entre mundos, a matemática torna-se mais difícil e requer mais trabalho para ser totalmente resolvida.

A Conclusão

Este artigo é um triunfo da verificação. Ele não disse apenas: "Esta teoria parece legal". Ele construiu a teoria em um computador, forçou-a a seguir regras lógicas estritas e descobriu que:

O "Botão de Fazer" funciona perfeitamente como um filtro de verdade.
Acordos locais podem às vezes falhar em criar uma verdade global (o problema dos "três detetives").
As regras originais para a "Modalidade Mágica" estavam incompletas e precisavam de uma quarta regra para funcionar.
Uma vez corrigido, o sistema prova que as regras causais são estáveis e podem ser transportadas entre diferentes ambientes.

Os autores estão muito seguros sobre esses resultados porque eles são verificados por máquina. Cada passo foi verificado pelo computador, sem suposições ou momentos de "talvez". Eles não apenas simularam isso; eles provaram matematicamente. No entanto, eles são cuidadosos ao dizer que isto é apenas a versão "1-topos" (um tipo específico e mais simples de universo matemático). Eles ainda não resolveram o problema inteiro da causalidade, especialmente as partes que envolvem setas direcionadas (onde A causa B, mas B não causa A) de uma forma totalmente assimétrica. Mas para a parte que abordaram, eles construíram uma base sólida, provando que a matemática por trás dos modelos causais não é apenas uma ideia bonita, mas uma realidade de trabalho verificada.

Resumo Técnico: Uma Formalização Cubical de Modelos Causais de Topos

Problema e Motivação
O artigo aborda a verificação de "Modelos Causais de Topos" (TCMs), um framework proposto por Mahadevan [Mah25c, Mah25b, Mah25a] que recastea a inferência causal dentro da categoria de um topos. Neste framework, um mundo causal é um presheaf, intervenções são mapas característicos para o classificador de subobjetos $\Omega$ , e o raciocínio ocorre na linguagem interna intuicionista. Embora o material de origem forneça uma reformulação conceitual onde a maquinaria causal padrão (intervenção, montagem de mecanismos, contrafatuais) corresponde a propriedades universais de topos, trata-se de um desenvolvimento baseado em papel. As principais afirmações centrais na fonte são enunciadas sem prova, e alguns axiomas são deixados abstratos ou potencialmente incompletos. O problema é fornecer uma verificação verificada por máquina deste núcleo de 1-topos, garantindo a consistência lógica do framework e identificando quaisquer lacunas na apresentação axiomática original.

Metodologia
Os autores implementam a formalização em Cubical Agda, um assistente de prova baseado em teoria de tipos cubica. O desenvolvimento é uma sequência direta de um artigo complementar [Sar26] que verificou um monad de probabilidade e as regras do cálculo do-de Pearl.

Fundamentos: O trabalho opera sobre o topos de presheaves $\mathbf{PSh}(\mathcal{C}) = \mathbf{Set}^{\mathcal{C}^{op}}$ sobre uma categoria base abstrata $\mathcal{C}$ de contextos.
Segurança e Axiomas: Todo o desenvolvimento passa no flag --safe do Agda, o que significa que não contém postulados, buracos ou recursos inseguros. O corpo de números ordenados é concretamente instanciado como os números racionais $\mathbb{Q}$ , evitando postulados abstratos.
Estrutura: A formalização constrói o classificador de subobjetos $\Omega$ como um presheaf de sieves, define a linguagem interna via forcing de Kripke-Joyal e constrói uma topologia de Lawvere-Tierney para modelar a modalidade $j$ -do-calculus.

Principais Contribuições e Resultados

O Classificador de Intervenção (Seção 3):
Os autores constroem $\Omega$ como o presheaf de sieves e realizam a intervenção $do(X := x_0)$ como um mapa característico $\chi: X \to \Omega$ . Eles provam o teorema de classificação em ambas as direções: $\chi_c(b) = \top \iff b = x_0^c$ . Crucialmente, eles estabelecem que, para a construção ser interna ao topos, o valor fixo $x_0$ deve ser um elemento global natural (um valor natural no contexto), não meramente uma família indexada por contexto. Isso prova que $\Omega$ é o classificador de subobjetos, satisfazendo a propriedade universal de que todo sub-presheaf fechado sob restrição é unicamente classificado por um mapa para $\Omega$ .
Colagem de Mecanismos Independentes via Sheaf (Seção 4):
O material de origem afirma que mecanismos locais que concordam em sobreposições podem ser "colados" em um mecanismo global único, mas não fornece prova. Os autores provam isso como um limite de pullback no topos de presheaves. Eles demonstram que, para dois mecanismos $p: X \to Z$ e $q: Y \to Z$ , o pullback $X \times_Z Y$ existe por contexto, e qualquer cone de mecanismos concordantes fatora unicamente através deste pullback. Isso confirma a propriedade de "colagem" (gluing) sem exigir uma topologia de Grothendieck ou sheafification, pois ela se mantém para todos os presheaves.
A Linguagem Interna (Seção 5):
O artigo define o forcing de Kripke-Joyal para a lógica interna e verifica mecanicamente as cláusulas para todos os conectivos ( $\top, \bot, \land, \lor, \Rightarrow$ ) e quantificadores ( $\forall, \exists$ ). Eles verificam a propriedade de localidade (monotonicidade), garantindo que o forcing é estável sob restrição, que é a característica definidora da semântica de Kripke.
Correção dos Axiomas de Lawvere-Tierney (Seção 6):
Uma descoberta significativa é uma lacuna na definição padrão de uma topologia de Lawvere-Tierney fornecida na fonte. Os três axiomas padrão (preservação de $\top$ , preservação de $\land$ , e idempotência) não implicam inflacionariedade ( $S \leq j(S)$ ). Os autores fornecem um contra-modelo (uma cadeia de três elementos) que satisfaz os três axiomas onde a inflacionariedade falha, o que significa que o operador não é necessariamente um operador de fechamento. Eles adicionam a inflacionariedade como um quarto axioma para garantir que $j$ seja um operador de fechamento (núcleo).

Instância Concreta: Eles exibem a topologia da dupla negação ( $\neg\neg$ ) como uma instância concreta não degenerada.
Estabilidade: Eles provam que as intervenções e as três regras do do-calculus de Pearl são $j$ -fechadas (estáveis) para cada topologia. No entanto, observam que isso é trivial para regras cujas conclusões são provadas como igualdades (valor de verdade $\top$ ). O resultado substantivo refere-se a alegações contingentes (por exemplo, independências condicionais que ocorrem em alguns regimes mas não em outros), mostrando que seus valores de verdade são $j$ -fechados sob a topologia da dupla negação.

Obstrução de Contextualidade (Seção 7):
Os autores introduzem um fenômeno não considerado no programa original: uma obstrução cohomológica à colagem. Embora dois mecanismos sempre se colem, três contextos podem falhar em admitir um modelo global mesmo sendo pairwise consistentes. Eles verificam mecanicamente o triângulo de Specker (três observáveis booleanos com anti-correlações par a par) como uma testemunha mínima.

Eles formalizam a obstrução como uma classe não nula na primeira cohomologia de Čech ( $H^1$ ) da cobertura com coeficientes em $\mathbb{Z}_2$ .
Provam que uma seção global existe se, e somente se, a holonomia do cociclo for trivial. O triângulo de Specker possui holonomia não trivial, confirmando a ausência de um modelo global.

Transportabilidade como Invariância (Seção 8):
O artigo identifica a transportabilidade de um contrafactual através de uma cobertura de regimes como $j$ -estabilidade (invariância). Um contrafactual ocorre globalmente (é transportável) se, e somente se, seu valor de verdade interno for $j$ -fechado. Eles provam a correção: se um contrafatual é $j$ -estável e ocorre em um ambiente $j$ -denso, ele ocorre globalmente.

Significância e Alegações
O artigo reivindica significância em duas áreas primárias:

Garantia: As alegações centrais do framework TCM agora são certificadas em vez de apenas assertadas. Isso é crítico para automação, pois um núcleo verificado é necessário para verificar modelos causais gerados por máquina.
Descobertas Práticas: A mecanização revelou dois insights práticos:
- As garantias da camada modal dependem de $j$ ser um operador de fechamento; os axiomas originais eram insuficientes.
- A montagem modular de mecanismos causais (estilo map-reduce) não é garantida apenas pela concordância par a par; uma verificação de consistência global é necessária para detectar obstruções cohomológicas (contextualidade).

Escopo e Limitações
Os autores limitam explicitamente o escopo ao fragmento do 1-topos (presheaf).

Eles não formalizam a sheafification de nível de tipo (o refletor de associado-sheaf em todo o topos).
Eles não abordam a elevação para o nível de categoria direcionada ou $\infty$ -categórica, que exigiria uma teoria de tipos direcionada para modelar a assimetria da causalidade (as setas causais são simétricas no atual modelo de presheaf).
O resultado de transportabilidade é estabelecido como uma equivalência com uma hipótese de densidade específica, mas a equivalência de completude com o critério de $s$ -hedge gráfico permanece como um trabalho futuro.

O desenvolvimento está disponível abertamente e representa o primeiro relato verificado por máquina do núcleo de 1-topos dos modelos causais de topos, corrigindo os axiomas modais e provando propriedades de colagem e obstrução anteriormente não verificadas.