CausalForge：一个基于形式化基础、自我改进的智能体框架，用于因果推断的自动化研究

arXiv 2026 73.5 method

TLDR

CausalForge利用Lean证明助手和自我改进的智能体流水线实现因果推断的自动化理论研究。

评分理由

The paper presents a novel framework that combines a formal library (Causalean) with an agentic pipeline (CausalSmith) for automated theorem proving and research. Strengths include formal verification via Lean and a self-improving loop, while weaknesses are the narrow focus on causal inference and potential subjectivity in the statement audit step.

Read-first 评分解释

综合优先阅读分 73.5，由主题、引用、图谱、方法、可复现性和近期性等信号加权得到。原始总分保留为 69。

近期性 8%

100

使用温和的时间衰减，让近期论文更容易浮现，同时保留较早基础工作的价值。年份：2026

可复现性 25%

检查链接和可见文本中的论文、代码、数据集、工件与仓库信号。论文：有；代码：有；数据：无；命中信号：工件、代码、GitHub

方法质量 25%

检查可见的摘要与分析字段，寻找实验、数据集、基线、指标和局限性等方法证据。命中信号：评估、指标、结果

主题相关性 42%

57.5

使用现有 LLM 关键词相关性评分，并归一化到 0-100。关键词：AI scientist、automated scientific discovery、autonomous research agent、automated research、literature review agent、survey generation、automated experimentation、experiment design agent、AI for scientific research、paper writing agent、research automation、scientific discovery agent

研究版图角色

前沿论文方法锚点复现锚点

排序敏感性

稳定性：volatile；排名波动范围：37。

关键词评分

automated research

research automation

AI scientist

automated scientific discovery

autonomous research agent

AI for scientific research

scientific discovery agent

paper writing agent

literature review agent

automated experimentation

survey generation

experiment design agent

深度分析

创新点

CausalForge：一个基于Lean证明助手的因果推断自动化理论研究框架，具有形式化基础
Causalean：在人工设计与审查下借助LLM辅助开发的、包含7,035个机器验证声明的因果推断基础Lean库
CausalSmith：一个自我改进的智能体流水线，能够自主选择研究主题、提出结果、形式化陈述、构建证明，并输出产物供人工审查
陈述审计：一种将形式化定理与它们意图表达的非形式化主张进行比对的机制，以弥合形式证明与科学意义之间的差距

方法

CausalForge结合了Causalean库和CausalSmith流水线。CausalSmith选择主题、生成结果、在Lean中形式化、构建机器验证的证明并呈现产物；随后通过陈述审计检查形式化定理与非形式化主张之间的对齐。系统通过完成自主研究运行后产生的产物进行评估。

关键结果

该系统生成自主研究运行的产物，形式化验证确保证明的正确性，陈述审计缓解了形式化与预期科学主张之间的差距。

局限性

机器验证的证明仅保证形式化假设下的正确性，无法保证形式化忠实反映了预期的科学主张，且陈述审计可能无法完全消除这一差距。
该流水线依赖人工审查最终产物，限制了完全自主性。
评估仅限于自主运行产生的产物，摘要中未报告定量指标。

技术栈

Lean proof assistantLLMPython

资源

论文代码