CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
stat.ML, cs.AI, cs.LG, econ.EM
Submitted: 2026-07-24
Updated: 2026-09-15
Code: https://github.com/Jiyuan-Tan/CausalForge
Project page: https://jiyuan-tan.github.io/CausalForge
License: http://creativecommons.org/licenses/by/4.0/
The gist: Automating theoretical research is constrained not only by the generation of candidate results, but also by their reliable evaluation.
Terminology
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.
Sources
- Faithful Autoformalization via Roundtrip Verification and Repair
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
- Evaluating Sakana's AI Scientist: Bold Claims, Mixed Results, and a Promising Future?
- ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
- Causal Evaluation of Language Models
- ORCA: ORchestrating Causal Agent
- The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization
- Baldur: Whole-Proof Generation and Repair with Large Language Models
- Is ChatGPT a Good Causal Reasoner? A Comprehensive Evaluation
- EconCSLib: AI-Assisted Lean Formalization for Economics & Computation research
- Accelerating scientific discovery with Co-Scientist
- Mining Causality: AI-Assisted Search for Instrumental Variables
- Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
- BadScientist: Can a Research Agent Write Convincing but Unsound Papers that Fool LLM Reviewers?
- LLMs Are Prone to Fallacies in Causal Inference
- Causal Reasoning and Large Language Models: Opening a New Frontier for Causality
- HyperTree Proof Search for Neural Theorem Proving
- Formalization of Optimality Conditions for Smooth Constrained Optimization Problems
- Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
- Are LLMs Capable of Data-based Statistical and Causal Reasoning? Benchmarking Advanced Quantitative Reasoning with Data
Related papers
- Behavior of prediction performance metrics with rare events
- Optimal Estimation of Generic Dynamics by Path-Dependent Neural Jump ODEs
- A Posterior-Dynamics Framework for Imaging Inverse Problems with Pretrained Diffusion Priors
- Efficient quadratic entropy with distance sketches
- Embedding-Bias in Conditional Independence Testing
- From Log-Odds to Shapley Values: An Explanatory Geometry for the Weighted Naive Bayes Classifier