CausalForge：基于形式化证明、具备自迭代能力的因果推断自动化科研智能体框架

论文原链接：https://arxiv.org/html/2607.22511v1

摘要

当前基于大模型的自动化科研系统存在核心缺陷：仅依靠LLM充当审稿人评判结果真伪，实验证明这类LL评审器极易被伪造论文欺骗，检测准确率接近随机猜测。本文提出CausalForge框架，以Lean4形式化证明器作为底层可信校验内核，实现因果推断领域全自动理论科研。
CausalForge由两大核心组件构成：

1. Causalean：基于人工规范、大模型辅助构建的Lean4因果推理基础库，包含7035条机器核验完备的数学声明，覆盖图因果模型、潜在结果、识别理论、半参数估计、面板计量、实验因果等全领域基础定理；
2. CausalSmith自迭代智能体流水线：自动选题、生成猜想、自然语言命题转形式化代码、机器证明、生成可阅读论文，并支持将证明完毕的通用引理自动回流扩充Causalean库。
   本框架解决单一形式校验的短板：Lean内核仅能证明形式语句在假设下逻辑成立，但无法保证形式代码与人类原始科学命题语义一致。因此流水线额外增加语句一致性审计模块，逐段比对形式化定义与原始自然语言猜想，杜绝“证明正确但命题跑偏”漏洞。
   基于123组完整自动化运行记录开展评测，系统成功填补Zeng等人高维混杂变量ATE极小极大估计理论遗留对数平方阶差距等公开理论空白。全部源码、形式化库、实验运行记录开源开放。

1 引言

大语言模型可快速生成猜想、证明、完整论文，但产出物的核验成本极高。实证领域仅增加审稿工作量，理论因果推断领域风险更致命：错误定理在专家人工核验前难以区分真伪，而人工校验周期漫长、成本高昂。
现有自动化科研方案普遍采用“生成LLM+评审LLM”双模型架构，但已有实验（BadScientist）证明，LLM审稿对伪造论文接受率高达82%，真伪识别效果接近随机，完全无法作为可靠正确性评判依据。

形式化证明提供另一条可信校验路径：在Lean4中完成命题形式化后，内核通过类型检查保证证明逻辑严谨，不受大模型幻觉干扰。但仅靠单一Lean校验存在两大关键障碍：

1. 形式化成本极高：从零推导每一条因果定理需要重复实现基础图模型、潜在结果、估计理论，重复造轮子；
2. 语义失配漏洞：即便代码通过类型检查，形式化命题可能与原始科学猜想含义完全不同。例如智能体将复杂引理直接定义为公理、擅自修改原始假设条件，机器证明合法但科学结论失效。

针对两大缺陷，CausalForge提出双层可信保障机制：

1. 构建完备可复用Causalean形式化库，所有基础工具提前机器核验，智能体可直接调用；
2. 在Lean内核证明校验之外，增加语句一致性审计，逐节点对比形式化代码与原始自然语言命题，排查假设篡改、空真定义、公理替代引理等隐蔽漏洞。

流水线完整工作流：智能体自主筛选科研空白→生成自然语言猜想→逻辑图结构化拆解命题→自动转为Lean4形式代码→调用Causalean复用已知定理完成证明→审计语义匹配度→生成配套学术论文，同时支持将通用新引理回流入库持续扩充基础库。

本文四大核心贡献

1. Causalean开源Lean4因果库：包含7035条机器核验声明（4616条定理+2015条定义），覆盖图因果、潜在结果、识别、半参数估计、面板、随机实验全领域，提供语义检索API供智能体调用；
2. CausalSmith端到端自迭代智能体流水线：全自动选题、命题、形式化、证明、论文生成，具备库回流闭环，持续扩充基础形式化工具；
3. 双层可信验证机制：Lean内核保证证明逻辑完备，语句审计保证形式代码与科学命题语义等价，解决纯形式化语义漂移问题；
4. 大规模实证评测：123组完整自动化运行记录，成功解决高维混杂ATE极小极大估计公开理论缺口，系统存在明显能力边界（纯原创因果识别猜想成功率极低，技术补全类问题效果优异）。

2 相关工作

2.1 LLM自动化科研与形式化发现

AI-Scientist、FunSearch等系统依靠LLM打分/任务指标评判产出，但LLM评审不可靠；AlphaProof等自动定理证明工具仅负责证明，不具备自主命题能力。CausalForge创新结合自主科研命题+机器形式证明+语义双重审计，同时配套领域专用可复用数学库。

2. 大模型因果推理评测

CLadder、Causal-Copilot等因果LLM基准仅做问答打分，无机器核验的定理证明流程，无法产出严谨数学结论。本文框架可自动生成带完备机器证明的因果理论成果。

2. Lean领域专用形式库

现有Lean数学库Mathlib覆盖通用测度、概率，EconCSLib覆盖经济学，无完整因果推断形式化体系。Causalean填补该空白，且专为自动化智能体设计检索接口。

3 前置基础：因果推断与Lean4证明器

3.1 因果推断两大主流框架

1. 结构因果模型SCM（图模型）：有向无环图DAG+do干预算子，核心工具后门/前门调整、ID图形识别算法、d分离判定；
2. 潜在结果PO框架：每个样本对应不同处理下反事实结果，核心估计量ATE、ATT、LATE、双重差分、Manski部分识别界、Balke-Pearl二元工具界。
   两类框架全部在Causalean中完成完备形式化证明。

3.2 Lean4形式化可信原理

Lean4将数学命题编码为类型，证明是对应类型的合法项，仅极小内核负责类型校验，所有上层tactic、LLM生成代码均不可信，仅内核输出具备严谨保证。
关键局限：内核仅校验证明推导合法，无法判断形式语句是否等价于人类原始猜想，这是本文审计模块需要解决的核心痛点。常见内核通过但语义失效场景：

• 定义化简恒为True（空洞命题）；
• 假设条件矛盾，任意结论均可证明；
• 将待证引理直接声明为公理绕过推导。

4 Causalean：因果推断专用Lean4形式化基础库

4.1 设计规范与分层架构

Causalean仅存储通用领域基础数学结论，单篇论文专属一次性引理放在CausalSmith运行目录，通过持续集成隔离，仅经人工审核的通用结论允许回流入库。
构建分工：人类划定覆盖范围、标准化定义；LLM负责定义、证明、注释初稿；人工终审每条声明语义匹配度，无sorry、自定义公理才允许入库。

库整体分层（自底向上）

底层：图论、基础测度/概率（复用轻量化Mathlib子集）
中层：SCM图模型、潜在结果形式化
上层：识别理论、半参数估计、面板、随机实验、因果发现
配套检索引擎：支持自然语言概念检索、类型模式检索、证明目标定向检索，内置1024维句子嵌入向量索引，7035条声明全量可检索。

4.2 库完整规模统计

总文件973个，代码总行261940行，共7035条机器核验声明：

• 定理/引理：4616条
• 数学定义：2015条
• 结构/归纳类型/实例：404条
  十大模块内容规模：
  | 模块 | 文件数 | 代码行数 | 定义 | 定理引理 | 结构实例 |
  |------|--------|----------|------|----------|----------|
  | 估计理论 | 168 | 54246 | 298 | 621 | 100 |
  | 渐近统计 | 202 | 47165 | 213 | 894 | 38 |
  | 潜在结果PO | 138 | 41415 | 592 | 947 | 80 |
  | SCM图模型 | 88 | 36342 | 208 | 523 | 67 |
  | 轻量化Mathlib | 113 | 24778 | 104 | 500 | 11 |
  | 面板方法 | 68 | 18382 | 258 | 389 | 44 |
  | 随机实验 | 101 | 16095 | 172 | 370 | 12 |
  | 基础图论 | 21 | 10866 | 70 | 160 | 28 |
  | 机器学习辅助工具 | 50 | 6330 | 56 | 100 | 13 |
  | 因果发现 | 24 | 6321 | 44 | 112 | 10 |

4.3 核心标志性形式化定理

库内置大量学界经典完备机器证明，节选代表结论：

图因果SCM

1. 马尔可夫等价充要条件：骨架+无向三角冲突完全一致
2. do演算三条规则图形完备证明
3. 后门/前门调整识别性定理
4. 离散正分布下ID图形算法完备性证明

潜在结果识别

1. Wald估计识别LATE局部平均处理效应
2. Callaway-Santanna分组双重差分ATT识别
3. Manski最坏情况ATE识别界、Balke-Pearl二元工具尖锐界

半参数估计

1. 去偏机器学习DML估计ATE渐近正态性
2. DML达到Hahn效率下界极小极大证明
3. 双重稳健序贯DTR估计渐近线性

面板与实验

1. 交错TWFE双向固定效应因果分解
2. 网络干扰下Horvitz-Thompson估计一致性

因果发现

1. 非高斯LiNGAM可识别证明、不变预测ICP完备性

4.4 检索引擎三大工作模式

1. 概念检索：自然语言查询扩展因果领域同义词匹配；
2. 类型模式检索：输入定理假设/结论类型，匹配同结构已有证明；
3. 目标定向检索：针对当前证明目标排序最优可复用引理。
   所有检索融合语义嵌入向量打分，支持模块过滤缩小范围。

4.5 公理安全校验规范

全库无sorry、无人工新增公理，仅有限图判定、极小极大数值计算由native_decide生成编译器内置临时公理，全部自动扫描记录来源；外部依赖仅OptSuite优化KKT条件、lean-rademacher拉德马赫复杂度两个开源库适配版本，无未核验外部假设。

5 CausalSmith：自迭代全自动科研流水线

整体四段式流水线：发现选题→形式化规划→机器证明+语义审计→论文生成，附带两条闭环反馈：实验运行记录沉淀、新通用引理回流Causalean库。
核心数据结构：逻辑依赖图Logic Graph，每条猜想拆解为定义、假设、引理、顶层定理节点，记录自然语言原始命题与对应Lean4代码、审计状态（未审核/匹配/语义漂移）。

5.1 逻辑图核心设计

每条完整科研成果对应一张有向无环逻辑图：

• 节点类型：前置设定、定义、假设、中间引理、顶层主定理
• 边分为两类：语句依赖（定义/假设构成命题）、证明依赖（证明需要前置引理）
• 节点审核状态：unreviewed未审核 / matched语义等价 / drift语义漂移
• 区分关键负载节点（必须完整证明）、引用节点（直接复用库中已有结论）
  流水线全程基于逻辑图推进，一旦某节点形式代码修改，所有依赖节点自动重置审核状态，重新审计语义匹配。

5.2 阶段1：选题与猜想发现

两种输入模式：人类给定研究主题 / 智能体自主检索学术空白自主选题
自主选题流程：

1. 检索近年因果论文、引用文献，筛选学界未解决技术缺口；
2. 对抗性选题门限校验：要求问题定义清晰、存在明确下游应用价值，剔除空洞猜想；
3. 生成自然语言完整猜想，区分两类问题：
   • 技术补全类：识别框架、估计量已有，仅需填补界、收敛速率等数学缺口；
   • 原创识别类：需要全新图/反事实识别逻辑（系统成功率极低）。
     猜想生成后构建初始逻辑图，标记所有前置假设、待证引理。

5.3 阶段2：形式化规划

读取逻辑图每个自然语言节点，生成Lean4目标代码框架，分配对应库模块；检索Causalean匹配可复用结论，标记引用节点；无现成工具则标记为待证明负载节点，生成证明义务清单。

5.4 阶段3：证明构建+语句一致性审计（核心双层校验）

第一层：Lean内核机器证明

调度证明填充智能体，调用检索接口复用库定理迭代完成证明，编译校验无语法、推导错误。

第二层：语义一致性审计（解决形式漂移漏洞）

内核仅保证推导合法，审计模块校验形式代码与原始自然命题逻辑等价，四大类内核通过但无效漏洞全部拦截：

1. 命题错误：形式语句与人类猜想完全不符；
2. 空洞命题：定义恒为真、假设矛盾无可行样本；
3. 未证明捷径：用axiom/sorry/admit替代完整推导；
4. 范围收窄：擅自删减原始假设、固定常数缩小适用场景。
   审计流程：将Lean代码反向翻译回自然语言命题，与原始猜想双向等价比对，不采用简单文本相似度匹配，规避表层文字欺骗。
   完成单轮证明审计后执行全局收敛复审，遍历整张逻辑图所有节点二次核验。

5.5 阶段4：成果生成与双反馈闭环

反馈1：运行记录沉淀

每一条选题无论成功/降级/失败完整存档，包含猜想原文、逻辑图、审计记录，后续选题阶段检索历史记录，避免重复尝试无解方向。

反馈2：通用引理回流入库

证明完成、审计通过的负载节点若具备通用性，启动库升级流程：

1. 快照当前Causalean库；
2. 新引理并入对应模块，重建索引、文档、完整性校验；
3. 编译失败自动回滚快照，仅完整通过才永久入库。

论文生成

读取审核通过的逻辑图，生成标准学术论文，每条定理附带对应Lean源码跳转链接，清晰区分库复用结论与本次新证明成果。

6 实验评测（123组完整自动化运行记录）

6.1 整体运行分布

总运行记录123组，三类结果：

1. Accepted（9组）：证明完备、语义匹配、达到预设创新等级；
2. Downgraded：证明合法但创新不足，结论可简化为已知构造；
3. Failed：猜想本身数学不成立、形式化无法闭合。
   9组成功成果全部属于技术补全类（渐近界、估计收敛速率），无全新因果识别原创定理。

6.2 按领域分组成功率

六大选题领域运行统计：

1. 渐近统计/随机实验/面板：高接受率，8组成功；
2. SCM图模型、精确识别、部分识别：94组仅1组成功，大量降级案例；
   降级核心原因：推导完成后发现新结论等价于已有Manski/Balke标准界，无实质创新。

6.3 标杆完整成功案例：高维离散混杂ATE极小极大界填补

Zeng等人2024工作给出高离散混杂变量ATE极小极大下界：
$$R\asymp \frac{1}{n}+{\left(\frac{d}{n\log n}\right)}^2$$
但仅证明下界，上下界存在${\log }^{2}n$对数阶差距。
CausalSmith自主完成猜想、形式化、完整机器证明，设计混合分层估计量填补该理论缺口：

• 高样本单元格使用插层比率估计；
• 稀疏单元格采用无偏阶乘多项式近似；
• 统一校准常数不依赖混杂重叠参数；
  完整26个Lean模块机器核验，无自定义公理，下界作为引用假设清晰标注，无隐藏推导捷径。

6.4 机器完备性核验

对9组Accepted成果逐条执行#print axioms扫描，无sorry/opaque/自定义公理，所有负载节点均完整推导，外部文献下界仅作为定理显式假设，不混入证明内核。

6.5 库回流实例

剂量反应反向定理证明过程缺少Bretagnolle-Huber亲和界，流水线自动启动Study模式证明该引理，并入Causalean.Stat模块，后续其他ATE收敛定理直接复用该库结论。

7 讨论与局限性

7.1 三层可信度分离（核心理论贡献）

1. Lean内核：客观判定证明推导是否合法（完全可信、无主观偏差）；
2. 语句审计：判定形式代码与原始科学命题语义匹配（降低漏洞，但依赖LLM辅助，存在极小误判概率）；
3. 成果学术价值/创新性：只能由人类专家最终判定，LLM打分仅作流水线门限参考，不可作为结论依据。

7.2 系统局限

1. 仅针对因果推断领域，迁移至其他学科需要重建对应形式化基础库；
2. 语义审计依赖大模型双向翻译比对，无法做到100%零失误；
3. 评测样本总量偏少，仅123组运行，原创因果识别类猜想几乎无法产出合格创新成果；
4. 无完整量化审计精确率、召回率基准数据集，缺少人类专家双盲对照实验。

7.3 未来研究方向

1. 构建语义审计标准基准，量化审计正误精度；
2. 消融实验对比纯LLM评审、仅Lean内核、CausalForge双层校验三类方案漏洞率；
3. 拓展多学科专用形式库，将流水线迁移至计量、生物统计等领域；
4. 优化自主选题模块，提升全新因果识别猜想产出质量。

8 结论

现有LLM自动化科研依靠大模型评审存在严重正确性隐患。本文提出CausalForge框架，结合Lean4机器形式证明内核+语句语义双层审计，构建可信因果自动化科研体系：

1. 开源完备因果形式库Causalean，大幅降低定理形式化重复成本；
2. CausalSmith流水线全自动选题、形式化、证明、论文生成，支持通用引理自迭代扩充基础库；
3. 双层校验同时解决证明逻辑漏洞、形式语义漂移两类关键缺陷；
   基于123组完整自动化运行记录验证系统有效性，成功填补公开因果理论数学缺口。
   系统清晰区分证明严谨性、命题匹配度、学术价值三层独立评判标准，为可信AI理论科研提供全新范式。

附录A 标志性定理Lean源码文件路径

完整库固定工具链：leanprover/lean4:v4.29.0-rc3
节选核心定理文件映射：

定理名称	Lean文件路径
do演算第二条规则	SCM/Do/DoCalculus.lean
后门调整识别	SCM/ID/Backdoor.lean
LATE Wald识别	PO/ID/Exact/LATE.lean
Manski ATE界	PO/ID/Partial/Manski/NonAsp.lean
DML渐近正态估计	Estimation/ATE/DML.lean
交错TWFE因果分解	Panel/TWFE/Decomposition.lean

附录B 逻辑图存储规范

每条成果独立存储FormalizationGraph对象：
节点属性：类型、自然语言原文、Lean代码、审核状态、假设标签；
边区分语句依赖、证明依赖；
内置结构校验器，拦截重复节点、非法依赖环路，所有图表可导出用于论文可视化。

附录C CausalSmith流水线完整操作流程

全阶段有序执行序列

1. D-1.1 文献勘探：检索未解决科研缺口
2. D-1.2 生成猜想与数学核心
3. D0 数学推导，生成初始逻辑图
4. D0-max 最大化人工校验点（可暂停人工介入）
5. D0.5 猜想创新度门限过滤
6. ckpt D/F 分支决策：是否启动高成本形式化流程
7. F1 形式化规划，检索库可复用结论
8. F2 生成Lean代码脚手架
9. F2.5 脚手架与原始命题首轮匹配审计
10. F3 迭代填充证明+内核编译校验
11. F3.5 漏洞扫描（sorry/非法公理/未使用假设）
12. F4 全局逻辑图收敛复审
13. F5 论文素材整理，等待人工终审

流程跳转规则

• 审计发现语义漂移：退回F2重写形式代码；
• 猜想推导发现无创新：直接标记Downgraded存档；
• 证明无解/命题数学错误：标记Failed；
• 全部审计通过：进入成果归档，可启动库回流流程。

附录D 实验运行记录与复现规范

1. 所有123组运行完整目录存放于仓库CausalSmith/doc/research/_bank/；
2. 区分accepted/downgraded/failed三类文件夹，每组包含state状态文件、完整逻辑图、所有LLM交互日志、审计报告；
3. 复现环境固定Lean4版本，提供一键执行脚本run_pipeline.sh；
4. 统计指标全部由库索引自动生成，无人工修改数据。

附录E 库回流完整执行脚本

引理入库自动化流程（Study模式）

# 1. 检测逻辑图中无可用库的负载节点
python pipeline_scan.py --graph ./result/graph.json --output gap_list.txt
# 2. 为缺失引理生成Lean脚手架
python formalize.py --target gap_list.txt
# 3. 批量执行机器证明
lake build ./temp_lemmas
# 4. 漏洞扫描：禁止sorry/自定义公理
python lint_check.py ./temp_lemmas
# 5. 快照当前Causalean库
cp -r ./Causalean ./Causalean_backup
# 6. 合并引理至对应模块，重建索引
python lib_merge.py --source ./temp_lemmas --target ./Causalean
# 7. 全库重编译，失败自动回滚快照
lake build ./Causalean || cp -r ./Causalean_backup ./Causalean
# 8. 重新生成在线文档嵌入向量索引
python build_docs.py

脚本存放路径：仓库scripts/lib_upgrade.sh

附录F 论文生成完整脚本

# 输入审核通过逻辑图，生成带代码锚定TeX论文
python paper_gen.py \
  --graph ./final/graph.json \
  --output ./output_main.tex \
  --crosswalk ./code_mapping.csv

输出文件：论文Tex、定理-源码映射对照表，每条结论附带GitHub跳转链接。

开源资源总清单

1. 项目主仓库：https://github.com/Jiyuan-Tan/CausalForge
2. 可视化文档站：https://jiyuan-tan.github.io/CausalForge/
3. 论文PDF：https://arxiv.org/pdf/2607.22511
4. 全套流水线执行脚本：仓库scripts/目录
5. Causalean形式化完整源码：仓库Causalean/
6. 123组实验原始运行记录：CausalSmith/doc/research/_bank/
7. 复现环境配置文件：lakefile.lean、environment.yml
8. 所有图表、实验统计绘图代码：仓库analysis/