📈 economics

CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference

CausalForge é um framework de agentes formalmente fundamentado e de autoaperfeiçoamento que automatiza a pesquisa em inferência causal ao combinar a biblioteca Causalean baseada em Lean com um pipeline que gera, formaliza e audita provas para garantir a confiabilidade de resultados verificados por máquina.

Autores originais: Jiyuan Tan, Vasilis Syrgkanis

Publicado 2026-07-27

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Jiyuan Tan, Vasilis Syrgkanis

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

Imagine que você é um detetive tentando resolver um mistério sobre causa e efeito. Você quer saber: "Se eu tomar este remédio, vou melhorar?" ou "Será que aquela chuva realmente causou a inundação?". No mundo da ciência, isso é chamado de inferência causal. É diferente de apenas observar as coisas acontecendo; trata-se de descobrir o que aconteceria se mudássemos algo. Por muito tempo, os cientistas usaram a matemática para provar que essas histórias de causa e efeito são verdadeiras. Mas a matemática é difícil, e um único erro minúsculo em uma prova pode tornar toda a história falsa.

Recentemente, os computadores ficaram muito bons em escrever histórias e resolver quebra-cabeças usando algo chamado Modelos de Linguagem de Grande Escala (LLMs). Estes são como robôs superinteligentes que podem ler quase tudo o que já foi escrito e então escrever seus próprios artigos, provas e teorias. Mas há um porém: esses robôs são ótimos em parecer confiantes, mas são terríveis em verificar o próprio trabalho. Eles frequentemente inventam fatos, criam números ou escrevem provas que parecem perfeitas, mas que são, na verdade, sem sentido. Se deixarmos um robô escrever um artigo científico e depois pedirmos a outro robô para checá-lo, eles podem apenas acenar um para o outro e dizer: "Sim, isso é verdade!", mesmo quando está completamente errado. Isso é um grande problema porque, na ciência, estar errado pode levar a decisões ruins.

É aqui que entra um novo projeto chamado CausalForge. Pense nele como um "robô cientista de autoaperfeiçoamento" projetado especificamente para fazer pesquisas em inferência causal, mas com uma rede de segurança muito rigorosa. Em vez de apenas confiar que um robô verifique o dever de casa de outro robô, o CausalForge usa uma ferramenta matemática mágica e inquebrável chamada Lean (um assistente de prova). O Lean é como um professor superrigoroso que nunca aceitará uma resposta a menos que cada passo seja logicamente perfeito. Se a matemática não bater, o Lean diz: "Não!" e se recusa a dar o visto.

Mas há um segundo problema: mesmo que a matemática seja perfeita, o robô pode estar provando a coisa errada. Imagine um robô provando que "Todos os gatos são cachorros" com uma lógica perfeita. A matemática é sólida, mas a afirmação é absurda. O CausalForge resolve isso adicionando uma "Auditoria de Declaração". É como um tradutor que verifica: "O robô realmente provou o que ele disse que iria provar?".

Então, o que o CausalForge realmente fez? A equipe construiu duas partes principais. Primeiro, criaram uma biblioteca massiva chamada Causalean, que contém mais de 7.000 fatos matemáticos pré-verificados e perfeitos sobre causa e efeito. É como uma caixa de ferramentas gigante onde cada ferramenta já foi testada para garantir que funciona. Segundo, construíram um pipeline de robô chamado CausalSmith. Este robô pode escolher um tópico de pesquisa, tentar inventar um novo teorema, escrever a prova na linguagem Lean e, em seguida, fazer com que o sistema verifique se a prova é real e se a afirmação corresponde à matemática.

Os resultados são uma mistura de sucesso e choques de realidade. Das 123 tentativas que o sistema fez para descobrir coisas novas, 9 foram totalmente aceitas como corretas, inéditas e verificadas por máquina. O sistema foi surpreendentemente bom em encontrar pequenas lacunas técnicas em pesquisas existentes (como corrigir um erro minúsculo em uma fórmula), mas teve dificuldades quando solicitado a criar ideias inteiramente novas e grandiosas do zero. O artigo mostra que, embora não possamos confiar totalmente em robôs para julgar sua própria criatividade ainda, podemos confiar neles para fazer o trabalho pesado de escrever e verificar a matemática, desde que tenhamos um "professor mágico" rigoroso (Lean) e um "tradutor" cuidadoso (a auditoria) vigiando. Não é uma varinha mágica que resolve todos os problemas científicos, mas é uma nova e poderosa maneira de garantir que nossas histórias científicas sejam realmente verdadeiras.

Resumo Técnico: CausalForge

Declaração do Problema

A automação da pesquisa teórica em inferência causal enfrenta um gargalo crítico: a avaliação confiável dos resultados gerados. Embora os Grandes Modelos de Linguagem (LLMs) possam gerar conjecturas, provas e artigos rapidamente, eles têm dificuldade em avaliar sua própria correção. Estudos empíricos indicam que revisores baseados em LLM são pouco confiáveis, aceitando frequentemente artigos fabricados a taxas próximas ao acaso e falhando em distinguir entre teoremas corretos e incorretos.

Confiar exclusivamente na verificação formal (por exemplo, via assistente de prova Lean 4) é insuficiente por duas razões:

Custo: A formalização de resultados a partir de primeiros princípios é laboriosa. A descoberta automatizada requer uma biblioteca reutilizável e verificada de teoremas causais para evitar a reconstrução da teoria padrão a cada execução.
Fidelidade (Faithfulness): Uma prova verificada por máquina garante que uma afirmação formal decorre de suas premissas, mas não garante que a afirmação formal capture fielmente a reivindicação científica pretendida. Um LLM pode produzir uma prova de verificação de tipo para uma definição vazia, um teorema com hipóteses contraditórias ou um resultado onde um passo não provado foi substituído por um axioma.

Metodologia: O Framework CausalForge

O CausalForge é um framework de agentes de autoaperfeiçoamento projetado para automatizar a pesquisa teórica em inferência causal. Ele integra uma biblioteca formal fundamental com um pipeline de múltiplos estágios que enfatiza tanto a solidez da prova quanto a fidelidade da afirmação.

Componentes Principais

Causalean (A Biblioteca):
- Uma biblioteca fundamental em Lean 4 contendo 7.035 declarações verificadas por máquina que abrangem modelos gráficos, modelos causais estruturais (SCMs), resultados potenciais, identificação, estimação e estatística assintótica.
- Construída com assistência de LLM sob design e revisão humana, ela fornece uma interface de recuperação para que os agentes reutilizem primitivas verificadas (ex: ajuste de backdoor, estimadores de aprendizado de máquina duplo).
- Ela impõe uma separção estrita entre a biblioteca principal e os lemas específicos do pipeline, permitindo que a biblioteca cresça através de um ciclo de feedback.
CausalSmith (O Pipeline):
- Uma máquina de estados determinística executando quatro estágios: Descoberta (Discovery), Formalização (Formalization), Construção de Prova (Proof Construction) e Apresentação (Presentation).
- Grafo de Lógica: O artefato central é um grafo de lógica onde os nós representam afirmações (definições, lemas, teoremas) e as arestas representam dependências. Este grafo rastreia o "caminho crítico" de nós com portões (substrato não provado) versus nós citados (resultados emprestados).
- Descoberta: Seleciona tópicos de pesquisa (fornecidos pelo usuário ou selecionados autonomamente a partir de lacunas na literatura) e propõe resultados em linguagem natural.
- Formalização & Prova: Mapeia o grafo de lógica para declarações em Lean 4, preenche as obrigações de prova usando a recuperação do Causalean e constrói as provas.
- Auditoria de Afirmação (A Inovação Central): Um portão dedicado de "correspondência de afirmação" que verifica se a declaração formal em Lean 4 corresponde logicamente à reivindicação pretendida em linguagem natural. Isso envolve:
  - Verificar por "atalhos não provados" (ex: sorry, admit, axiomas ocultos).
  - Detectar "vacuidade" (definições que reduzem a True, hipóteses insatisfatórias).
  - Garantir a "fidelidade" via retrotradução: converter a reivindicação pretendida em uma lista de hipótese/conclusão com formato Lean e compará-la contra a declaração formal para garantir equivalência lógica (nem mais forte, nem mais fraca).
- Revisão de Convergência: Uma revisão por modelo duplo de todo o grafo congelado antes da apresentação para capturar qualquer derivação no significado da afirmação.
Mecanismo de Autoaperfeiçoamento:
- Registro de Execução (Run Record): Cada execução (aceita, rebaixada ou falha) é registrada. Execuções falhas impedem que agentes futuros repitam caminhos sem saída; execuções rebaixadas refinam os alvos de novidade.
- Feedback da Biblioteca: Quando uma execução requer um novo lema de carga estrutural não presente no Causalean, o sistema entra em "modo de estudo" para prová-lo. Uma vez verificado e revisado para reusabilidade, o lema é promovido para o Causalean, expandindo a biblioteca para execuções futuras.

Contribuições Principais

Biblioteca Causalean: Uma formalização ampla e verificada por máquina do conjunto de ferramentas de inferência causal (7.035 declarações) que serve como uma base verificada para a descoberta automatizada.
Pipeline CausalSmith: Um sistema de ponta a ponta que seleciona tópicos autonomamente, propõe resultados, formaliza-os, prova-os em Lean 4 e audita a fidelidade das afirmações.
Mecanismo de Auditoria de Afirmação: Uma abordagem inovadora para preencher a lacuna entre a verificação formal e a intenção científica. Ao auditar o grafo de lógica nó a nó, o sistema garante que uma prova aceita pelo kernel corresponda à reivindicação científica específica sendo feita, em vez de apenas um teorema sintaticamente válido.
Avaliação Empírica: Um catálogo de 123 execuções de pesquisa autônomas registradas, incluindo 9 resultados aceitos que fecham lacunas técnicas na literatura existente.

Resultados

O sistema foi avaliado usando 123 execuções registradas:

Resultados: 9 execuções foram aceitas, 44 foram rebaixadas (sólidas, mas carecendo de novidade) e 70 falharam (rejeitadas na proposta ou derivação matemática).
Padrões de Desempenho: O sistema destaca-se em Teoria Estatística, Experimentação e Métodos de Painel, onde sucedeu em fechar lacunas técnicas (ex: correspondendo limites superiores a limites inferiores conhecidos). Teve dificuldades nos clusters de Identificação Exata, Identificação Parcial e SCM, onde a contribuição exige uma ideia conceitual nova em vez de refinamento técnico. Nessas áreas, o sistema frequentemente produziu resultados que eram matematicamente sólidos, mas reduziam-se a construções conhecidas (ex: "contenção externa genérica do estilo Manski").
Resultado Emblemático: O sistema fechou com sucesso um gap minimax na estimação do Efeito de Tratamento Médio (ATE) sob confusão discreta de alta dimensão. Construiu um estimador computável que fechou um gap de fator $\log^2$ entre os limites superior e inferior estabelecidos por Zeng et al. [54]. Este resultado foi verificado por máquina, auditado para fidelidade de afirmação e formalmente vinculado ao desenvolvimento em Lean 4.
Crescimento da Biblioteca: O ciclo de feedback promoveu com sucesso 13 novos lemas (ex: limites de afinidade de Bretagnolle–Huber, desigualdade de Fano) de execuções específicas para a biblioteca geral Causalean.

Significância e Alegações

O artigo postula que o CausalForge oferece um novo modelo de confiança para a pesquisa teórica automatizada ao separar três questões distintas:

Solidez da Prova: Garantida pelo kernel do Lean 4.
Fidelidade da Afirmação: Verificada pela auditoria de afirmação (comparando reivindicações formais vs. pretendidas).
Significância Científica: Permanece um julgamento humano, informado, mas não determinado pelo pipeline de níveis de novidade.

Os autores alegam que este framework aborda a falta de confiabilidade dos revisores de LLM ao fundamentar a avaliação na verificação formal, enquanto reconhece explicitamente os limites da automação em relação ao significado dos teoremas. O sistema demonstra que agentes autônomos podem produzir teoremas causais fiéis e verificados por máquina, particularmente em domínios onde as lacunas técnicas são bem definidas. No entanto, o artigo nota modestamente que o sistema atual é limitado na geração de ideias conceituais verdadeiramente novas e que a confiabilidade das auditorias de novidade e fidelidade baseadas em LLM requer estudos mais rigorosos. O trabalho não pretende substituir pesquisadores humanos, mas fornecer uma ferramenta de autoaperfeiçoamento formalmente fundamentada para explorar as fronteiras da teoria da inferência causal.