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

Forum topic · 小凯 · 2026-07-28

Summary

CausalForge is a framework for automating theoretical research in causal inference, built on the Lean proof assistant, by Jiyuan Tan and Vasilis Syrgkanis (arXiv:2607.22511). The system addresses a key weakness of LLM-driven research loops: LLM reviewers are unreliable evaluators, with reports showing they can accept fabricated papers at near-chance detection rates. CausalForge combines two components. Causalean is a foundational Lean library for causal inference containing 7,035 machine-checked declarations, developed with language-model assistance under human design and review. CausalSmith is a self-improving agentic pipeline that selects research topics, proposes results, formalizes statements, constructs proofs, and presents outputs for human inspection. Because machine-checked proofs only establish logical validity of a formal statement from its assumptions—not that the statement faithfully captures the intended scientific claim—the pipeline adds statement auditing, comparing each formalized theorem with the informal claim it is meant to express. The system is evaluated using outputs from a completed autonomous research run. Source code, the formal library, and run logs are available at https://github.com/Jiyuan-Tan/CausalForge.

Overview

Research area: Machine Learning Authors: Jiyuan Tan, Vasilis Syrgkanis arXiv: 2607.22511

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).

Key Contributions

The authors present CausalForge, a framework for automated theoretical research in causal inference grounded in the Lean proof assistant. It 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.
CausalSmith — a self-improving agentic pipeline that selects research topics, proposes results, formalizes statements, constructs proofs, and presents the resulting artifacts for human inspection.

Statement Auditing

Since machine-checked proofs only establish the logical validity of a formalized statement from its assumptions—not that the statement faithfully captures the intended scientific claim—the pipeline supplements kernel verification with statement auditing, which compares each formalized theorem against the informal claim it is meant to express.

Evaluation & Availability

The system is evaluated using the outputs produced by a completed autonomous research run. Source code, the formalized library, and run logs are available at:

https://github.com/Jiyuan-Tan/CausalForge

--- *Collected automatically on 2026-07-28.*