CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
Abstract
Automating theoretical research requires generating candidate results and evaluating them reliably. Models keep getting better at the first, while the second remains hard. A common approach asks one large language model (LLM) to review what another produced, yet such reviewers are empirically unreliable: they may accept fabricated papers and catch the fabrication at close to chance rates~\citep{badscientist2025}. We present \textsc{CausalSmith}, a framework for automated theoretical research in causal inference built on the Lean proof assistant, where a proof is checked by a program rather than read by a referee. \textsc{CausalSmith} rests on \textsc{Causalean}, a foundational Lean library for causal inference holding 8,179 machine-checked definitions and theorems, developed with language-model assistance under human design and review. Around it, we build a self-improving agentic pipeline that selects research topics, proposes results, formalizes statements, constructs proofs, and presents the resulting artifacts for human inspection. Moreover, the pipeline pairs Lean verification with a statement audit that compares each formal theorem against the informal claim behind it. 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/CausalSmith.
Related
- Automated, Efficient, and Model-Free Inference for Randomized Clinical Trials via Data-Driven Covariate Adjustment
- Improving ecological inference and uncertainty quantification from camera trap data through the fusion of AI confidences and manual annotations
- Automated loop invariant inference through learning-guided program structure analysis
- Stability for a formally determined Lorentzian inverse problem
- Genus of quaternion algebras over formally real fields
BibTeX
@misc{tan2026causalsmith,
title = {{CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference}},
author = {Jiyuan Tan and Vasilis Syrgkanis},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2607.22511},
eprint = {2607.22511},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2607.22511},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
AU - Jiyuan Tan
AU - Vasilis Syrgkanis
PY - 2026
DA - 2026/09/15
PB - arXiv
DO - 10.48550/arxiv.2607.22511
UR - https://arxiv.org/abs/2607.22511
AB - Automating theoretical research requires generating candidate results and evaluating them reliably. Models keep getting better at the first, while the second remains hard. A common approach asks one large language model (LLM) to review what another produced, yet such reviewers are empirically unreliable: they may accept fabricated papers and catch the fabrication at close to chance rates~\citep{badscientist2025}. We present \textsc{CausalSmith}, a framework for automated theoretical research in causal inference built on the Lean proof assistant, where a proof is checked by a program rather than read by a referee. \textsc{CausalSmith} rests on \textsc{Causalean}, a foundational Lean library for causal inference holding 8,179 machine-checked definitions and theorems, developed with language-model assistance under human design and review. Around it, we build a self-improving agentic pipeline that selects research topics, proposes results, formalizes statements, constructs proofs, and presents the resulting artifacts for human inspection. Moreover, the pipeline pairs Lean verification with a statement audit that compares each formal theorem against the informal claim behind it. 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/CausalSmith.
ER -