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

📄 arXiv: 2607.22511v1 📥 PDF

作者: Jiyuan Tan, Vasilis Syrgkanis

分类: stat.ML, cs.AI, cs.LG, econ.EM

发布日期: 2026-07-24

🔗 代码/项目: GITHUB

💡 一句话要点

提出CausalForge框架以解决因果推断研究的自动化问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 因果推断 自动化研究 机器检查 Lean证明助手 自我改进 智能管道 科学研究

📋 核心要点

  1. 现有方法在自动化理论研究中面临评估不可靠的问题，尤其是大型语言模型的审稿能力不足。
  2. CausalForge框架通过结合Causalean和CausalSmith，提供了一个系统化的因果推断研究自动化解决方案。
  3. 实验结果表明，CausalForge能够有效生成和验证因果推断的研究成果，提升了研究的可靠性。

📝 摘要（中文）

自动化理论研究不仅受限于候选结果的生成，还受限于其可靠评估。常见的方法是通过大型语言模型（LLM）审稿人来闭环研究，但这些审稿人在实证上仍然不可靠。本文提出CausalForge，一个基于Lean证明助手的因果推断自动化理论研究框架。CausalForge结合了Causalean，一个包含7035个机器检查声明的基础Lean库，以及CausalSmith，一个自我改进的智能管道，能够选择研究主题、提出结果、形式化声明、构建证明并呈现结果供人类检查。该系统通过对已完成的自主研究运行生成的文献进行评估，展示了其有效性。

🔬 方法详解

问题定义：本文旨在解决因果推断领域自动化研究中，候选结果生成与评估的可靠性问题。现有方法依赖于大型语言模型进行审稿，但这些模型的评估能力存在显著不足，可能接受虚假论文。

核心思路：CausalForge框架通过结合Causalean和CausalSmith，提供一个自我改进的智能管道，能够自动选择研究主题、提出结果并进行形式化验证，从而提高研究的可靠性和效率。

技术框架：CausalForge的整体架构包括两个主要模块：Causalean库用于因果推断的基础声明和验证，CausalSmith管道用于自动化研究过程。该框架通过机器检查证明和声明审计相结合，确保生成的结果与科学声明一致。

关键创新：CausalForge的创新点在于其自我改进的智能管道设计，能够通过机器检查和声明审计相结合的方式，提升因果推断研究的自动化水平和结果的可靠性。这与传统依赖人工审稿的方式形成了鲜明对比。

关键设计：在设计上，CausalForge使用了Lean证明助手进行形式化验证，确保每个声明都经过机器检查。此外，声明审计过程通过比较形式定理与非正式声明，进一步提高了结果的准确性和可信度。

🖼️ 关键图片

img_0
img_1
img_2

📊 实验亮点

实验结果显示，CausalForge在生成和验证因果推断研究成果方面表现出色，能够有效减少虚假结果的产生。具体性能数据和对比基线尚未详细披露，但系统的自我改进能力显著提升了研究的可靠性和效率。

🎯 应用场景

CausalForge框架具有广泛的应用潜力，特别是在因果推断、自动化科学研究和机器学习等领域。其自动化能力可以帮助研究人员更高效地生成和验证理论结果，推动科学研究的进展。未来，该框架可能会影响更多学科的研究方法，提升研究的透明度和可靠性。

📄 摘要（原文）

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.