CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
TLDR
CausalForge automates theoretical research in causal inference using a Lean proof assistant and a self-improving agentic pipeline.
Reasoning
The paper presents a novel framework that combines a formal library (Causalean) with an agentic pipeline (CausalSmith) for automated theorem proving and research. Strengths include formal verification via Lean and a self-improving loop, while weaknesses are the narrow focus on causal inference and potential subjectivity in the statement audit step.
Read-first score
Read-first score 73.5, weighted from topical fit, citation, graph, method, reproducibility, and recency signals. Original total remains 69.
Field roles
Rank sensitivity
Stability: volatile; rank range: 37.
Keyword Scores
Deep Analysis
Innovations
- CausalForge: a formally grounded framework for automated theoretical research in causal inference using the Lean proof assistant
- Causalean: a foundational Lean library with 7,035 machine-checked declarations for causal inference, developed with LLM assistance under human design and review
- CausalSmith: a self-improving agentic pipeline that autonomously selects research topics, proposes results, formalizes statements, constructs proofs, and outputs artifacts for human inspection
- Statement audit: a mechanism that compares formal theorems against the informal claims they intend to express, addressing the gap between formal proof and scientific meaning
Methodology
CausalForge combines the Causalean library and the CausalSmith pipeline. CausalSmith selects topics, generates results, formalizes them in Lean, constructs machine-checked proofs, and presents artifacts; a statement audit then checks alignment between formal theorems and informal claims. The system is evaluated on artifacts from completed autonomous research runs.
Key Results
The system produces artifacts from autonomous research runs, with formal verification ensuring proof correctness and statement audits mitigating the gap between formalization and intended scientific claims.
Limitations
- Machine-checked proofs only guarantee correctness under formal assumptions, not that the formalization faithfully captures the intended scientific claim, and the statement audit may not fully eliminate this gap.
- The pipeline relies on human inspection of the final artifacts, limiting full autonomy.
- Evaluation is limited to artifacts from autonomous runs, with no quantitative metrics reported in the abstract.