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

AI summary

Overview

• Research area: Automated theoretical research — combining large language model (LLM) agents with the Lean 4 proof assistant, applied to the field of causal inference (category: stat.ML).
• Technical level: Advanced. The paper assumes familiarity with causal inference (structural causal models, potential outcomes, identification), with Lean 4 type-checking, and with agentic LLM pipelines.
• Scope: The paper introduces Causalean, a Lean 4 library for causal inference containing 8,179 machine-checked declarations, and CausalSmith, a four-stage self-improving agent pipeline that proposes, formalizes, proves, audits, and presents new causal-inference theorems, evaluated over 144 recorded runs.
• Note on naming: The supplied title reads "CausalForge," but the paper content itself consistently names the system CausalSmith and the library Causalean. This summary uses the names as they appear in the paper text.

What This Paper Is About

LLMs can now generate research artifacts — conjectures, proofs, and whole papers — faster than those artifacts can be checked, and delegating the checking to another LLM is unreliable: the paper cites evidence that LLM reviewers accept deliberately fabricated papers up to 82% of the time and detect the fabrication at near-chance rates. The goal is to replace model-based judgment with program-based judgment, so that a causal-inference theorem counts as valid only when the Lean 4 proof assistant type-checks its proof, and to add a separate audit that checks the formal statement actually means the informal claim it is supposed to express.

Key Contributions

1. Causalean, a broad Lean 4 formalization of causal inference spanning graphical and structural causal models, potential outcomes and identification (exact and partial), panel methods, experimentation, estimation, and statistical theory. It comprises 8,179 machine-checked declarations — named definitions and theorems Lean 4 has verified — written with language-model assistance under human design and review, and it exposes a retrieval interface for agents.
2. An end-to-end research pipeline whose Discovery stage can select its own research topic and propose a causal-inference result, which the pipeline then formalizes, proves, and presents. It includes a library feedback loop that promotes reusable lemmas and theorems proved during a run back into Causalean.
3. An evaluation drawn from 144 recorded runs, comprising a catalog of machine-checked results and a headline result found by the system that the paper says closes a gap in Zeng et al. [60].
4. A statement-matching audit that pairs Lean 4 verification with a fine-grained, node-by-node comparison of each formal theorem against the informal claim behind it, plus a run record that screens future proposals using rejected and downgraded runs.

Main Findings

• Run outcomes across 144 runs: 14 accepted (sound, novel at the requested publishable tier, and proved to completion in Lean 4), 59 downgraded (sound but below the novelty target), and 71 failed (rejected at the proposal or the mathematics). The overall accept rate is 10%. A separate literature-reproduction track adds one reproduced partial-identification result. Nine legacy runs from a retired proposal track that predates the current pipeline are excluded.
• Acceptance concentrates in three clusters: By the cluster Discovery assigns at proposal time, Stat has 8 accepted out of 31 runs (26%), Experimentation 4 of 12 (33%), and Panel 1 of 7 (14%). The three identification and structural-model clusters together hold 94 runs and only one acceptance: ExactID 1 of 36 (3%), PartialID 0 of 54 (0%), and SCM 0 of 4 (0%).
• Library scale: The compiled environment index records 5,375 theorems, 2,372 definitions, and 432 structures, instances, and inductive types, across 1,070 files and roughly 302,000 lines, grouped into ten clusters. Stat is the largest cluster by lines (67,065) and Estimation the largest by volume of semiparametric machinery (55,788 lines).
• Two question types are labeled in the run catalog: "method comparison" (comparing two or more published estimators or identification frameworks — non-equivalence, strict-extension, or equivalence) and "assumption relaxation" (weakening a named assumption under a violation budget and asking for the identification result as a function of that budget). The catalog table itself is not included in the provided content.
• Axiom discipline: The whole library is sorry-free, and none of the 8,179 declarations rests on a hand-written axiom. The only non-standard axioms come from native_decide, which settles a finite computation by running compiled code and trusting the result; these occur in finite-graph decidability arguments and several minimax calculations and are reported explicitly.
• Faithfulness failures are real and observed: In one run an agent turned hard lemmas into axioms and produced Lean 4 code that compiled with axioms standing in for proofs; in another the model altered a hypothesis, so the code proved a weaker statement than the paper claimed. Both compile, and neither proves what was claimed.
• Failure modes the type checker cannot catch: The paper groups them into four families — wrong statement, vacuity (a concept defined as True, or a witness carrying no real obstruction), unproved step (axiom, sorry/admit, or a node mis-tagged as cited), and over-narrow statement (dropped hypothesis or a hardcoded constant where a general one was intended).
• Model lineup for the reported results: OpenAI reasoning models carried the main mathematics and Lean 4 formalization (GPT-5.5 until 2026-07-10, GPT-5.6 Sol thereafter); Anthropic's Claude handled Lean 4 code review and planning throughout (Opus 4.7 until 2026-05-28, Opus 4.8 until 2026-07-24, and Opus 5 after). Nine of the fourteen accepted runs ran entirely under Opus 4.8 and the other five entirely under Opus 5. Mechanical stages ran on GPT-5.6 Terra, and presentation write-ups were drafted by GPT-5.5.
• Not reported in the supplied content: the detailed breakdown of results by question type, the in-depth walkthrough of the single accepted headline result, and the concrete trace of the library feedback loop closing on a lemma — Section 6 promises all three, but the provided text is truncated before they appear.

Methodology in Plain English

The pipeline has four stages, run in fixed order with bounded retries on failure:

1. Discovery takes a topic from a researcher or proposes one itself. A selector searches recent work and prior runs, reads theoretical papers with their citing and follow-up literature, ranks candidate topics by mathematical potential and concrete applicability, and submits the top candidate to an independent adversarial topic review. Once a topic is fixed, a proposer drafts a question and informal solution, a novelty-and-duplication review compares it against the literature, and a solver solves the open questions in natural language. The output is stored as a dependency graph whose nodes are the paper's statements (setup, definition, assumption, lemma, headline theorem) and whose edges record what a claim says and what its proof consumes. Nodes are classed as must-prove (results the paper proves) or cited (results taken from the literature). A typical completed result has on the order of a hundred nodes and a few hundred edges.
2. Formalization gives each node a Lean 4 declaration, a module location, and either a statement to prove or an existing Causalean result to reuse, producing a skeleton file in which every statement to prove is left as sorry.
3. Proof construction runs a review-and-fill loop that repairs declarations that have drifted from the graph, fills each remaining sorry using the library's search engine, and flags hypotheses the proof never uses (a signal of vacuity or mis-statement). Reusable lemmas are promoted back into Causalean.
4. Presentation writes the paper from the reviewed graph, linking every theorem, definition, and assumption to its verified Lean 4 source, and publishes to a companion site with a proof map, per-statement verification, ratings, comments, and a slide deck.

The statement audit is the distinctive step. It runs in two layers: a mechanical scan rejects any artifact containing axiom, sorry, admit, opaque, or unsafe, applied recursively to every library module the artifact depends on; then several agents read the Lean 4 declaration text extracted from the compiled file, compare it to the intended claim, and flag divergence as drift. The main criterion is logical equivalence — equivalent assumptions and equivalent conclusions, neither stronger nor weaker. Each node's review status is stored as matched, drift, or unreviewed, and when a statement changes, downstream nodes are marked unreviewed again. Finally, two independent models recheck the entire frozen graph, including untouched nodes, without reference to the earlier review.

Retrieval supports this: a retrieval encoder is trained on Causalean itself from keyword-index pairs (a theorem's docstring against the declarations it is built on; each declaration's Lean 4 statement against its own docstring), split by module so evaluation is on unseen modules. All 8,179 declarations are embedded into a 1,024-dimensional vector index, and search runs in concept, type-pattern, and goal-directed modes, with concept and goal rankings combined by reciprocal-rank fusion and reordered by a fine-tuned cross-encoder.

Why This Matters

The paper argues that the bottleneck in automated theoretical research is not generation but reliable evaluation, and that "one LLM reviews another" is empirically unsound. Moving correctness to a type checker makes proof validity mechanical and indifferent to how the proof was written — when a proof of a statement passes, the statement follows from its stated assumptions together with the axioms the proof invokes, and Lean 4 reports those axioms on request. The paper calls this proof soundness and is explicit that it says nothing about whether the theorem is the one the researcher intended, which is why the statement audit exists. A second argument is efficiency: with a pre-built library, runs do not rebuild standard theory from first principles before reaching anything new, and reusable lemmas flow back into the library so later runs benefit.

Real-world applications:

• Causal analysis in the biomedical and social sciences, where average treatment effects, difference-in-differences, LATE, and regression-discontinuity estimands underlie study design — the paper formalizes identification for these estimands, including Manski and Balke–Pearl bounds for cases where only partial identification is possible.
• Platform and marketplace experimentation, where treatment effects propagate through interference between units; the library formalizes randomization inference, Horvitz–Thompson estimation, Neyman allocation, and central limit theorems under network interference.
• Panel-data and event-study policy evaluation, where two-way fixed-effects and difference-in-differences regressions may not recover the estimand analysts think they do; the library characterizes what those regressions actually recover, including the negative-weights decomposition and event-study pretrends induced by post-treatment effects.
• Automated scientific discovery and AI research agents, where verified-theorem infrastructure replaces unreliable LLM judging of AI-generated research.

Industry relevance: The paper positions the system as the closest existing work being a multi-agent pipeline for asymptotic statistics whose auditor and reviewer agents guard against vacuity, but notes that this earlier system formalizes known theory whereas CausalSmith also proposes the theorem. It also states that Causalean overlaps with other Lean 4 statistics libraries — Statlib, StatsMLlib, and the Rademacher-complexity line — and expects those projects to benefit as they converge on shared upstream infrastructure. For industry, the model is an auditable pipeline in which every accepted result carries a machine-checked proof, an audited statement, and a linked record.

Future Directions

• Extend the library and let it grow from runs. The paper states that Causalean is built to be extended rather than finished, and that each accepted run can promote reusable lemmas back into the library for later runs. The reported repository statistics are explicitly a snapshot that may increase because the pipeline runs continuously.
• Understand and improve the identification clusters. The three identification and structural-model clusters (ExactID, PartialID, SCM) hold 94 runs with only one acceptance, and PartialID holds 54 runs with zero acceptances — an open question is why the pipeline's self-proposed questions succeed in Stat, Experimentation, and Panel but almost never in identification.
• Widen the shared formal-statistics infrastructure. The paper expects its library and the neighboring Lean 4 statistics and economics libraries to benefit as they converge on shared upstream infrastructure, which implies coordinated work on overlapping tools such as minimax lower-bound methods, information divergences, empirical-process lemmas, and concentration inequalities.
• Address the residual trust gap the audit cannot close. The paper notes that a statement can be trivial — a definition unfolding to True is satisfied by everything, so a theorem about it holds vacuously — and that this third failure is invisible to Lean 4 and has to be caught by reading the statement. Reducing reliance on that reading step, and further reducing the reliance on human review during library construction, remains open.

Target Audience

Researchers and practitioners working at the intersection of automated theorem proving, LLM agents, and causal inference. It is most useful to: formal-methods and Lean 4 developers interested in building domain libraries; causal-inference methodologists who want to know which classical results are now machine-checked and how; agent researchers studying verified discovery pipelines and self-improving systems; and evaluation researchers interested in the claim that LLM-as-judge review is an unreliable basis for correctness, with a documented alternative. Readers without prior exposure to proof assistants, dependency-graph-based blueprints, or semiparametric causal estimation will find the paper dense.

Authors’ abstract

Automating theoretical research is constrained not only by the generation of candidate results, but also by their reliable evaluation. A common approach is to close the research loop with a large language model (LLM) reviewer. However, such reviewers remain empirically unreliable: they may accept fabricated papers and detect them at rates close to chance (Bad Scientist, 2025). We present CausalForge, a framework for automated theoretical research in causal inference grounded in the Lean proof assistant. CausalForge combines Causalean, a foundational Lean library for causal inference containing 7,035 machine-checked declarations developed with language-model assistance under human design and review, with CausalSmith, a self-improving agentic pipeline that selects research topics, proposes results, formalizes statements, constructs proofs, and presents the resulting artifacts for human inspection. Because a machine-checked proof establishes only that a formal statement follows from its assumptions, not that the statement faithfully captures the intended scientific claim, the pipeline augments kernel verification with a statement audit that compares each formal theorem against the informal claim it is intended to express. We evaluate the system using artifacts produced by completed autonomous research runs. The source code, formal library, and run records are available at https://github.com/Jiyuan-Tan/CausalForge.