📈 economics

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

CausalForge est un cadre agentique auto-amélioré et formellement fondé qui automatise la recherche en inférence causale en combinant la bibliothèque Causalean basée sur Lean avec un pipeline qui génère, formalise et audite des preuves afin de garantir la fiabilité des résultats vérifiés par machine.

Auteurs originaux : Jiyuan Tan, Vasilis Syrgkanis

Publié 2026-07-27

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Jiyuan Tan, Vasilis Syrgkanis

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous soyez un détective essayant de résoudre un mystère sur la cause et l'effet. Vous voulez savoir : « Si je prends ce médicament, est-ce que je vais guérir ? » ou « Est-ce que cette pluie a réellement causé l'inondation ? ». Dans le monde de la science, cela s'appelle l'inférence causale. Il ne s'agit pas seulement d'observer des choses qui se produisent ; il s'agit de comprendre ce qui se passerait si nous changions quelque chose. Pendant longtemps, les scientifiques ont utilisé les mathématiques pour prouver que ces histoires de cause à effet sont vraies. Mais les mathématiques sont difficiles, et une seule petite erreur dans une preuve peut rendre toute l'histoire fausse.

Récemment, les ordinateurs sont devenus très doués pour écrire des histoires et résoudre des énigmes en utilisant ce qu'on appelle les Grands Modèles de Langage (LLM). Ce sont comme des robots super intelligents capables de lire presque tout ce qui a été écrit, puis d'écrire leurs propres articles, preuves et théories. Mais il y a un piège : ces robots sont excellents pour paraître confiants, mais ils sont terribles pour vérifier leur propre travail. Ils inventent souvent des faits, inventent des chiffres ou écrivent des preuves qui semblent parfaites mais qui sont en réalité absurdes. Si nous laissons un robot écrire un article scientifique, puis demandons à un autre robot de le vérifier, ils pourraient simplement hocher la tête l'un vers l'autre et dire : « Oui, c'est vrai ! », même quand c'est complètement faux. C'est un gros problème car, en science, se tromper peut conduire à de mauvaises décisions.

C'est là qu'intervient un nouveau projet appelé CausalForge. Voyez cela comme un « robot scientifique auto-améliorant » conçu spécifiquement pour faire de la recherche en inférence causale, mais avec un filet de sécurité très strict. Au lieu de simplement faire confiance à un robot pour vérifier le devoir d'un autre robot, CausalForge utilise un outil mathématique magique et incassable appelé Lean (un assistant de preuve). Lean est comme un professeur super strict qui n'acceptera jamais une réponse à moins que chaque étape ne soit logiquement parfaite. Si les mathématiques ne concordent pas, Lean dit « Non ! » et refuse de valider.

Mais il y a un second problème : même si les mathématiques sont parfaites, le robot pourrait être en train de prouver la mauvaise chose. Imaginez un robot prouvant que « Tous les chats sont des chiens » avec une logique parfaite. Les mathématiques sont solides, mais l'affirmation est absurde. CausalForge résout cela en ajoutant un « Audit de Déclaration » (Statement Audit). C'est comme un traducteur qui vérifie : « Le robot a-t-il réellement prouvé ce qu'il disait vouloir prouver ? ».

Alors, qu'a réellement fait CausalForge ? L'équipe a construit deux parties principales. Premièrement, ils ont créé une immense bibliothèque appelée Causalean, qui contient plus de 7 000 faits mathématiques pré-vérifiés et parfaits sur la cause et l'effet. C'est comme une boîte à outils géante où chaque outil a déjà été testé pour s'assurer qu'il fonctionne. Deuxièmement, ils ont construit un pipeline de robot appelé CausalSmith. Ce robot peut choisir un sujet de recherche, essayer d'inventer un nouveau théorème, écrire la preuve dans le langage Lean, puis faire en sorte que le système vérifie si la preuve est réelle et si l'affirmation correspond aux mathématiques.

Les résultats sont un mélange de succès et de rappels à la réalité. Sur les 123 tentatives de découverte faites par le système, 9 ont été pleinement acceptées comme étant correctes, novatrices et vérifiées par machine. Le système s'est montré étonnamment doué pour trouver de petites lacunes techniques dans la recherche existante (comme corriger une minuscule erreur dans une formule), mais il a eu du mal lorsqu'on lui a demandé de concevoir de toutes pièces des idées entièrement nouvelles et de grande envergure. L'article montre que, bien que nous ne puissions pas encore faire entièrement confiance aux robots pour juger leur propre créativité, nous pouvons leur faire confiance pour effectuer le travail lourd de rédaction et de vérification des mathématiques, tant que nous avons un « professeur magique » strict (Lean) et un « traducteur » attentif (l'audit) pour les surveiller. Ce n'est pas une baguette magique qui résout tous les problèmes scientifiques, mais c'est une nouvelle façon puissante de s'assurer que nos récits scientifiques sont réellement vrais.

Résumé technique : CausalForge

Énoncé du problème

L'automatisation de la recherche théorique en inférence causale est confrontée à un goulot d'étranglement critique : l'évaluation fiable des résultats générés. Bien que les modèles de langage de grande taille (LLM) puissent générer rapidement des conjectures, des preuves et des articles, ils peinent à évaluer leur propre exactitude. Des études empiriques indiquent que les réviseurs basés sur les LLM sont peu fiables, acceptant souvent des articles fabriqués à un taux proche du hasard et échouant à distinguer les théorèmes corrects des incorrects.

S'appuyer uniquement sur la vérification formelle (par exemple, via l'assistant de preuve Lean 4) est insuffisant pour deux raisons :

Coût : La formalisation des résultats à partir de principes fondamentaux est laborieuse. La découverte automatisée nécessite une bibliothèque de théorèmes causaux réutilisable et vérifiée pour éviter de reconstruire la théorie standard à chaque exécution.
Fidélité : Une preuve vérifiée par machine garantit qu'une proposition formelle découle de ses hypothèses, mais elle ne garantit pas que la proposition formelle capture fidèlement l'affirmation scientifique voulue. Un LLM peut produire une preuve de vérification de type pour une définition vacueuse, un théorème avec des hypothèses contradictoires, ou un résultat où une étape non prouvée a été substituée par un axiome.

Méthodologie : Le cadre CausalForge

CausalForge est un cadre agentique auto-améliorable conçu pour automatiser la recherche théorique en inférence causale. Il intègre une bibliothèque formelle fondamentale avec un pipeline multi-étapes qui met l'accent à la fois sur la solidité de la preuve et sur la fidélité de l'énoncé.

Composants principaux

Causalean (La Bibliothèque) :
- Une bibliothèque fondamentale en Lean 4 contenant 7 035 déclarations vérifiées par machine couvrant les modèles graphiques, les modèles causaux structurels (SCM), les potentiels de résultats, l'identification, l'estimation et les statistiques asymptotiques.
- Construite avec l'assistance de LLM sous conception et revue humaines, elle fournit une interface de récupération pour que les agents puissent réutiliser des primitives vérifiées (ex. : ajustement par la méthode du backdoor, estimateurs de double apprentissage automatique).
- Elle impose une séparation stricte entre la bibliothèque de base et les lemmes spécifiques au pipeline, permettant à la bibliothèque de croître via une boucle de rétroaction.
CausalSmith (Le Pipeline) :
- Une machine à états déterministe exécutant quatre étapes : Découverte, Formalisation, Construction de preuve et Présentation.
- Graphe de logique : L'artéfact central est un graphe de logique où les nœuds représentent des énoncés (définitions, lemmes, théorèmes) et les arêtes représentent les dépendances. Ce graphe suit le « chemin critique » des nœuds à seuil (substrat non prouvé) par rapport aux nœuds cités (résultats empruntés).
- Découverte : Sélectionne des sujets de recherche (soit fournis par l'utilisateur, soit sélectionnés de manière autonome à partir des lacunes de la littérature) et propose des résultats en langage naturel.
- Formalisation et Preuve : Mappe le graphe de logique vers des déclarations Lean 4, remplit les obligations de preuve via la récupération dans Causalean, et construit les preuves.
- Audit d'Énoncé (L'innovation centrale) : Une étape dédiée de « correspondance d'énoncé » qui vérifie si la déclaration formelle en Lean 4 correspond logiquement à l'affirmation en langage naturel. Cela implique de :
  - Rechercher les « raccourcis non prouvés » (ex. : sorry, adict, axiomes cachés).
  - Détecter la « vacuité » (définitions se réduisant à True, hypothèses insatisfaisables).
  - Assurer la « fidélité » via une rétro-traduction : convertir l'affirmation voulue en une liste d'hypothèses/conclusions de forme Lean et la comparer à la déclaration formelle pour s'assurer de l'équivalence logique (ni plus forte, ni plus faible).
- Revue de Convergence : Une revue par un modèle dual de l'ensemble du graphe gelé avant la présentation pour détecter tout décalage dans le sens de l'énoncé.
Mécanisme d'Auto-amélioration :
- Registre d'Exécution : Chaque exécution (acceptée, déclassée ou échouée) est enregistrée. Les exécutions échouées empêchent les futurs agents de répéter des impasses ; les exécutions déclassées affinent les cibles de nouveauté.
- Rétroaction de la Bibliothèque : Lorsqu'une exécution nécessite un nouveau lemme structurel absent de Causalean, le système entre en « mode étude » pour le prouver. Une fois vérifié et examiné pour sa réutilisabilité, le lemme est promu dans Causalean, élargissant la bibliothèque pour les exécutions futures.

Contributions Clés

Bibliothèque Causalean : Une large formalisation vérifiée par machine de la boîte à outils de l'inférence causale (7 035 déclarations) servant de fondation vérifiée pour la découverte automatisée.
Pipeline CausalSmith : Un système de bout en bout qui sélectionne de manière autonome des sujets, propose des résultats, les formalise, les prouve dans Lean 4 et audite la fidélité des énoncés formels.
Mécanisme d'Audit d'Énoncé : Une approche novatrice pour combler le fossé entre la vérification formelle et l'intention scientifique. En auditant le graphe de logique nœud par nœud, le système garantit qu'une preuve acceptée par le noyau correspond à l'affirmation scientifique spécifique faite, plutôt qu'à un simple théorème syntaxiquement valide.
Évaluation Empirique : Un catalogue de 123 exécutions de recherche autonomes enregistrées, incluant 9 résultats acceptés qui comblent des lacunes techniques dans la littérature existante.

Résultats

Le système a été évalué à l'aide de 123 exécutions enregistrées :

Résultats : 9 exécutions ont été acceptées, 44 ont été déclassées (solides mais manquant de nouveauté), et 70 ont échoué (rejetées lors de la proposition ou de la dérivation mathématique).
Modèles de Performance : Le système excelle dans la Théorie Statistique, l'Expérimentation et les Méthodes de Panel, où il a réussi à combler des lacunes techniques (ex. : faire correspondre des bornes supérieures à des bornes inférieures connues). Il a éprouvé des difficultés dans les clusters d'Identification Exacte, d'Identification Partielle et de SCM, où la contribution nécessite une nouvelle idée conceptuelle plutôt qu'un raffinement technique. Dans ces domaines, le système a fréquemment produit des résultats mathématiquement solides mais se réduisant à des constructions connues (ex. : « l'enveloppement extérieur générique de style Manski »).
Résultat Phare : Le système a réussi à combler un écart minimax dans l'estimation de l'Effet de Traitement Moyen (ATE) sous confusion discrète de haute dimension. Il a construit un estimateur calculable qui a comblé un écart de facteur $\log^2$ entre les bornes supérieures et inférieures connues établies par Zeng et al. [54]. Ce résultat a été vérifié par machine, audité pour la fidélité de l'énoncé et formellement lié au développement de Lean 4.
Croissance de la Bibliothèque : La boucle de rétroaction a réussi à promouvoir 13 nouveaux lemmes (ex. : bornes d'affinité de Bretagnolle–Huber, inégalité de Fano) de la part des exécutions spécifiques vers la bibliothèque générale Causalean.

Signification et Revendications

L'article pose que CausalForge offre un nouveau modèle de confiance pour la recherche théorique automatisée en séparant trois questions distinctes :

Solidité de la Preuve : Garantie par le noyau de Lean 4.
Fidélité de l'Énoncé : Vérifiée par l'audit d'énoncé (comparaison entre les affirmations formelles et voulues).
Signification Scientifique : Reste un jugement humain, informé mais non déterminé par le pipeline de nouveauté.

Les auteurs affirment que ce cadre répond à l'imprévisibilité des réviseurs LLM en ancrant l'évaluation dans la vérification formelle tout en reconnaissant explicitement les limites de l'automatisation concernant la signification des théorèmes. Le système démontre que des agents autonomes peuvent produire des théorèmes causaux fidèles et vérifiés par machine, particulièrement dans les domaines où les lacunes techniques sont bien définies. Cependant, l'article note modestement que le système actuel est limité dans la génération d'idées conceptuelles véritablement nouvelles et que la fiabilité des audits de nouveauté et de fidélité basés sur les LLM nécessite une étude plus rigoureuse. Le travail ne prétend pas remplacer les chercheurs humains, mais fournir un outil auto-améliorable et formellement ancré pour explorer les frontières de la théorie de l'inférence causale.