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

Introduction

Language models generate research artifacts more rapidly than they can be evaluated. Formal verification provides a different basis for evaluation.

A proof accepted by the Lean 4 kernel is guaranteed to be correct relative to its trusted core.

This guarantee removes proof soundness from an LLM reviewer’s judgment.

Research Question

Vacuity covers a concept defined as True, an unsatisfiable hypothesis, and a witness with no real obstruction. In the Lean 4 development this borrowed bound appears as an explicit hypothesis.

Methodology

A third strand builds agents that do causal analysis without correctness guarantees. Mathlib supplies the analysis, probability, and measure theory for causal-inference development.

Study Design

The task it poses is narrower than open-ended review, and frontier models performed well on it in our observations, but a model can still err when auditing a statement, and we do not estimate how often it does.

Results & Findings

This primarily increases the burden of review in empirical fields. Incorrect theorems in theoretical work present a direct risk because expert verification is slow and costly.

• This primarily increases the burden of review in empirical fields.
• Incorrect theorems in theoretical work present a direct risk because expert verification is slow and costly.
• Many automated research systems delegate evaluation to a reviewing language model.
• Empirical evaluations show defects in LLM reviewers.
• Independent evaluations report hallucinated numbers, coding failures, and little novelty in AI-Scientist systems.

Practical Applications

A researcher may supply a topic anchor, or the orchestrator may invoke the causalsmith-topics module. The orchestrator writes a stage’s completion marker only after the stage returns, so a stopped run resumes from its recorded state, and a stage may return a checkpoint or an escalation instead of an advance.

The first scaffold may contain proof obligations; a subsequent revision edits only the flagged declarations and their necessary dependents, preserving already valid proof bodies.

Explicit re-entry may re-run an earlier stage after a correction; the corrected stage then runs forward through its dependent gates.

Related Work

This section reviews existing literature on autoformalization and theorem proving, emphasizing the limitations of current systems that rely on language models for evaluation. It discusses the need for explicit assessment of formal statements against intended claims.

Background

The background section explains the concepts of causal inference, including structural causal models and potential outcomes. It also describes Lean 4 as a proof checker and its relevance in providing a trusted evaluation framework.

Figures Explained

The paper’s visual material highlights the workflow and the main system components.

• Figure 1 :: Figure1: Causalean in layers: graphical and measure-theoretic foundations support the model languages, which support identification, which supports the estimation and design methods on top. A retrieval index over all 7,035 declarations spans the stack and is the interface the pipeline queries.
• Figure 2: two DAGs have the same skeleton and immoralities markovEquiv iff sameSkeleton sameImmoralities Rule 2 of do-calculus under its graphical condition do rule2 kernel Backdoor adjustment identifies an interventional distribution almost everywhere backdoor identifiable ae Frontdoor adjustment identifies an interventional distribution almost everywhere frontdoor identifiable ae Soundness of the graphical ID algorithm on the discrete positive class id sound discrete Causal discovery LiNGAM identifiability from nonzero source kurtosis lingam identifiability kurtosis Soundness of invariant causal prediction icp sound Completeness of invariant prediction for linear-Gaussian models icp complete linearGaussian Identifiability in linear causal disentanglement disentanglement identifiability Potential outcomes, exact identification, and partial identification Wald-ratio identification of the local average treatment effect late wald Difference-in-differences identification of the ATT att did Callaway-Sant’Anna group-time ATT identification att csdid Sharp regression-discontinuity identification rdd identification Fuzzy regression-discontinuity identification frd identification Wald identification for dynamic treatment timing whenToTreat wald Manski worst-case ATE bounds manski bounds ATE Sharpness of the Balke-Pearl bounds for a binary instrument balkePearl sharp Lee bounds for the ATT under selection lee bounds ATT AS Pointwise Imbens-Manski coverage for partially identified parameters imbensManski pointwise coverage Estimation and statistical theory Asymptotic normality of the debiased-ML ATE estimator dml ATE tendstoNormal Attainment of the Hahn efficiency bound by debiased-ML ATE dml ATE attains hahn bound Asymptotic linearity of debiased-ML ATT estimation dml ATT isAsymLinear Asymptotic normality of partially linear DML plr dml tendstoNormal Asymptotic linearity of sequential doubly robust DTR estimation seqDR dml isAsymLinear Structure-agnostic minimax lower bound for ATE estimation minimax lower bound var causal Optimal weighting for generalized method of moments gmm efficiency.
• Figure 2 :: Figure2: The CausalSmith pipeline. Discovery includes topic selection: when a researcher does not supply a topic, a dedicated selector searches and ranks candidate directions, screens them against the run record, and admits a topic only after an adversarial quality gate. The resulting claim moves left to right through discovery, formalization, proof, and presentation, clearing a gate between stages (novelty and mathematical soundness; statement matching; and a final convergence review). The kernel establishes proof soundness during the proof stage. The convergence review is an independent dual-model review of the full frozen graph, including nodes previously marked as matched; the presentation stage then assembles the reviewed result into a paper. Two feedback channels grow the system (Section 5.4). Stages reuse Causalean through retrieval, and when a run needs a new load-bearing lemma, study mode proves it and promotes it back into Causalean. In parallel, every run-accepted, downgraded, or failed-is recorded in the run record, whose entries are consulted during screening before the next proposal is drafted. The logic graph is the object that moves through the diagram: Discovery creates it from the selected or supplied topic, formalization maps it to Lean 4, proof construction updates it, the statement-match and convergence gates review it, and presentation writes from it. See Sections C to F for the operational stage flow (Figure4), run record and recovery, graph-controlled proof loop, and presentation pipeline.
• Figure 3 :: Figure 3: A logic graph (schematic). Nodes are statements; fill encodes review status (matched, drift, unreviewed); a dashed blue border marks a cited node, borrowed and off the critical path. Solid edges are statement-uses, dashed edges proof-uses. The green underlay traces the critical path of gated nodes the review must clear before final recording.