CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
CausalSmith：以形式化验证为基础的自我改进因果推断研究代理框架AI 解读 ↓
← 返回论文列表与筛选
阅读说明
本页整理公开书目信息，不生成学术质量评分。AI 解读根据题名及所注明的摘要或原文片段生成，未完成全文核验，可能有误；具体假设、证明与结论请核对原文。摘要保留来源文本，未经模型改写。
DOI 首次登记不等于接收或发表日期。部分更正、评论等条目没有独立摘要；缺少可靠材料时保留待补状态。
本页为预印本版本；arXiv 收录、作者填写的期刊信息以及作者既有发表经历，都不单独证明本篇已接收。作者发表记录按 OpenAlex 身份与完整姓名、本站覆盖期刊 ISSN 及正式卷期核对，只展示已核实例，档案仍可能误合并。
引用量采用 OpenAlex 单条关联记录，不合计多个记录；关联记录可能包含正式发表版本，不等于此版本单独引用。缺失不视为零，引用指标不代表论文质量。
关注作者按书目中的完整姓名匹配，同名和姓名变体需人工辨别。相关论文先按共享细分方向和具体方法排列，再参考通用方法与发表日期。
分类依据与纠错
AI 根据所提供的论文材料归类：摘要明确以因果推断基础库与因果理论研究为对象，形式验证和代理流程是其研究工具。
反馈分类问题
正在核对关联版本…
代码、数据与补充材料
正在核对对应版本的资源…
关注这篇论文的作者
CausalSmith：以形式化验证为基础的自我改进因果推断研究代理框架
- 研究问题
- 自动化因果理论研究中，如何可靠检验语言模型提出的结果，并确保机器验证的形式定理对应其宣称的非形式化结论？
- 方法与思路
- 作者以 Lean 因果推断基础库支撑选题、命题、形式化和证明流程，并将程序验证与形式命题对照非形式主张的审计结合。
- 材料陈述的贡献
- 摘要称，框架整合机器检查的基础库、研究代理流程及命题审计，并提供自主研究运行产物、源代码与运行记录供检查。
- 阅读关注点
- 应核对基础库所编码的因果概念与假设、命题审计的实现及评价方式，并检查自主运行的成功定义和人工设计审查的作用。
- 阅读边界
- 本资料为 arXiv 预印本，同行评审及期刊接收未核实；摘要未说明评价细节，机器证明通过不等于非形式主张或现实假设正确。
原文摘要
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.