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

CausalForge基于形式化证明、具备自迭代能力的因果推断自动化科研智能体框架论文原链接https://arxiv.org/html/2607.22511v1摘要当前基于大模型的自动化科研系统存在核心缺陷仅依靠LLM充当审稿人评判结果真伪实验证明这类LL评审器极易被伪造论文欺骗检测准确率接近随机猜测。本文提出CausalForge框架以Lean4形式化证明器作为底层可信校验内核实现因果推断领域全自动理论科研。CausalForge由两大核心组件构成Causalean基于人工规范、大模型辅助构建的Lean4因果推理基础库包含7035条机器核验完备的数学声明覆盖图因果模型、潜在结果、识别理论、半参数估计、面板计量、实验因果等全领域基础定理CausalSmith自迭代智能体流水线自动选题、生成猜想、自然语言命题转形式化代码、机器证明、生成可阅读论文并支持将证明完毕的通用引理自动回流扩充Causalean库。本框架解决单一形式校验的短板Lean内核仅能证明形式语句在假设下逻辑成立但无法保证形式代码与人类原始科学命题语义一致。因此流水线额外增加语句一致性审计模块逐段比对形式化定义与原始自然语言猜想杜绝“证明正确但命题跑偏”漏洞。基于123组完整自动化运行记录开展评测系统成功填补Zeng等人高维混杂变量ATE极小极大估计理论遗留对数平方阶差距等公开理论空白。全部源码、形式化库、实验运行记录开源开放。1 引言大语言模型可快速生成猜想、证明、完整论文但产出物的核验成本极高。实证领域仅增加审稿工作量理论因果推断领域风险更致命错误定理在专家人工核验前难以区分真伪而人工校验周期漫长、成本高昂。现有自动化科研方案普遍采用“生成LLM评审LLM”双模型架构但已有实验BadScientist证明LLM审稿对伪造论文接受率高达82%真伪识别效果接近随机完全无法作为可靠正确性评判依据。形式化证明提供另一条可信校验路径在Lean4中完成命题形式化后内核通过类型检查保证证明逻辑严谨不受大模型幻觉干扰。但仅靠单一Lean校验存在两大关键障碍形式化成本极高从零推导每一条因果定理需要重复实现基础图模型、潜在结果、估计理论重复造轮子语义失配漏洞即便代码通过类型检查形式化命题可能与原始科学猜想含义完全不同。例如智能体将复杂引理直接定义为公理、擅自修改原始假设条件机器证明合法但科学结论失效。针对两大缺陷CausalForge提出双层可信保障机制构建完备可复用Causalean形式化库所有基础工具提前机器核验智能体可直接调用在Lean内核证明校验之外增加语句一致性审计逐节点对比形式化代码与原始自然语言命题排查假设篡改、空真定义、公理替代引理等隐蔽漏洞。流水线完整工作流智能体自主筛选科研空白→生成自然语言猜想→逻辑图结构化拆解命题→自动转为Lean4形式代码→调用Causalean复用已知定理完成证明→审计语义匹配度→生成配套学术论文同时支持将通用新引理回流入库持续扩充基础库。本文四大核心贡献Causalean开源Lean4因果库包含7035条机器核验声明4616条定理2015条定义覆盖图因果、潜在结果、识别、半参数估计、面板、随机实验全领域提供语义检索API供智能体调用CausalSmith端到端自迭代智能体流水线全自动选题、命题、形式化、证明、论文生成具备库回流闭环持续扩充基础形式化工具双层可信验证机制Lean内核保证证明逻辑完备语句审计保证形式代码与科学命题语义等价解决纯形式化语义漂移问题大规模实证评测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 因果推断两大主流框架结构因果模型SCM图模型有向无环图DAGdo干预算子核心工具后门/前门调整、ID图形识别算法、d分离判定潜在结果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马尔可夫等价充要条件骨架无向三角冲突完全一致do演算三条规则图形完备证明后门/前门调整识别性定理离散正分布下ID图形算法完备性证明潜在结果识别Wald估计识别LATE局部平均处理效应Callaway-Santanna分组双重差分ATT识别Manski最坏情况ATE识别界、Balke-Pearl二元工具尖锐界半参数估计去偏机器学习DML估计ATE渐近正态性DML达到Hahn效率下界极小极大证明双重稳健序贯DTR估计渐近线性面板与实验交错TWFE双向固定效应因果分解网络干扰下Horvitz-Thompson估计一致性因果发现非高斯LiNGAM可识别证明、不变预测ICP完备性4.4 检索引擎三大工作模式概念检索自然语言查询扩展因果领域同义词匹配类型模式检索输入定理假设/结论类型匹配同结构已有证明目标定向检索针对当前证明目标排序最优可复用引理。所有检索融合语义嵌入向量打分支持模块过滤缩小范围。4.5 公理安全校验规范全库无sorry、无人工新增公理仅有限图判定、极小极大数值计算由native_decide生成编译器内置临时公理全部自动扫描记录来源外部依赖仅OptSuite优化KKT条件、lean-rademacher拉德马赫复杂度两个开源库适配版本无未核验外部假设。5 CausalSmith自迭代全自动科研流水线整体四段式流水线发现选题→形式化规划→机器证明语义审计→论文生成附带两条闭环反馈实验运行记录沉淀、新通用引理回流Causalean库。核心数据结构逻辑依赖图Logic Graph每条猜想拆解为定义、假设、引理、顶层定理节点记录自然语言原始命题与对应Lean4代码、审计状态未审核/匹配/语义漂移。5.1 逻辑图核心设计每条完整科研成果对应一张有向无环逻辑图节点类型前置设定、定义、假设、中间引理、顶层主定理边分为两类语句依赖定义/假设构成命题、证明依赖证明需要前置引理节点审核状态unreviewed未审核 /matched语义等价 /drift语义漂移区分关键负载节点必须完整证明、引用节点直接复用库中已有结论流水线全程基于逻辑图推进一旦某节点形式代码修改所有依赖节点自动重置审核状态重新审计语义匹配。5.2 阶段1选题与猜想发现两种输入模式人类给定研究主题 / 智能体自主检索学术空白自主选题自主选题流程检索近年因果论文、引用文献筛选学界未解决技术缺口对抗性选题门限校验要求问题定义清晰、存在明确下游应用价值剔除空洞猜想生成自然语言完整猜想区分两类问题技术补全类识别框架、估计量已有仅需填补界、收敛速率等数学缺口原创识别类需要全新图/反事实识别逻辑系统成功率极低。猜想生成后构建初始逻辑图标记所有前置假设、待证引理。5.3 阶段2形式化规划读取逻辑图每个自然语言节点生成Lean4目标代码框架分配对应库模块检索Causalean匹配可复用结论标记引用节点无现成工具则标记为待证明负载节点生成证明义务清单。5.4 阶段3证明构建语句一致性审计核心双层校验第一层Lean内核机器证明调度证明填充智能体调用检索接口复用库定理迭代完成证明编译校验无语法、推导错误。第二层语义一致性审计解决形式漂移漏洞内核仅保证推导合法审计模块校验形式代码与原始自然命题逻辑等价四大类内核通过但无效漏洞全部拦截命题错误形式语句与人类猜想完全不符空洞命题定义恒为真、假设矛盾无可行样本未证明捷径用axiom/sorry/admit替代完整推导范围收窄擅自删减原始假设、固定常数缩小适用场景。审计流程将Lean代码反向翻译回自然语言命题与原始猜想双向等价比对不采用简单文本相似度匹配规避表层文字欺骗。完成单轮证明审计后执行全局收敛复审遍历整张逻辑图所有节点二次核验。5.5 阶段4成果生成与双反馈闭环反馈1运行记录沉淀每一条选题无论成功/降级/失败完整存档包含猜想原文、逻辑图、审计记录后续选题阶段检索历史记录避免重复尝试无解方向。反馈2通用引理回流入库证明完成、审计通过的负载节点若具备通用性启动库升级流程快照当前Causalean库新引理并入对应模块重建索引、文档、完整性校验编译失败自动回滚快照仅完整通过才永久入库。论文生成读取审核通过的逻辑图生成标准学术论文每条定理附带对应Lean源码跳转链接清晰区分库复用结论与本次新证明成果。6 实验评测123组完整自动化运行记录6.1 整体运行分布总运行记录123组三类结果Accepted9组证明完备、语义匹配、达到预设创新等级Downgraded证明合法但创新不足结论可简化为已知构造Failed猜想本身数学不成立、形式化无法闭合。9组成功成果全部属于技术补全类渐近界、估计收敛速率无全新因果识别原创定理。6.2 按领域分组成功率六大选题领域运行统计渐近统计/随机实验/面板高接受率8组成功SCM图模型、精确识别、部分识别94组仅1组成功大量降级案例降级核心原因推导完成后发现新结论等价于已有Manski/Balke标准界无实质创新。6.3 标杆完整成功案例高维离散混杂ATE极小极大界填补Zeng等人2024工作给出高离散混杂变量ATE极小极大下界R≍1n(dnlog⁡n)2R \asymp \frac{1}{n}\left(\frac{d}{n\log n}\right)^2R≍n1​(nlognd​)2但仅证明下界上下界存在log⁡2n\log^2 nlog2n对数阶差距。CausalSmith自主完成猜想、形式化、完整机器证明设计混合分层估计量填补该理论缺口高样本单元格使用插层比率估计稀疏单元格采用无偏阶乘多项式近似统一校准常数不依赖混杂重叠参数完整26个Lean模块机器核验无自定义公理下界作为引用假设清晰标注无隐藏推导捷径。6.4 机器完备性核验对9组Accepted成果逐条执行#print axioms扫描无sorry/opaque/自定义公理所有负载节点均完整推导外部文献下界仅作为定理显式假设不混入证明内核。6.5 库回流实例剂量反应反向定理证明过程缺少Bretagnolle-Huber亲和界流水线自动启动Study模式证明该引理并入Causalean.Stat模块后续其他ATE收敛定理直接复用该库结论。7 讨论与局限性7.1 三层可信度分离核心理论贡献Lean内核客观判定证明推导是否合法完全可信、无主观偏差语句审计判定形式代码与原始科学命题语义匹配降低漏洞但依赖LLM辅助存在极小误判概率成果学术价值/创新性只能由人类专家最终判定LLM打分仅作流水线门限参考不可作为结论依据。7.2 系统局限仅针对因果推断领域迁移至其他学科需要重建对应形式化基础库语义审计依赖大模型双向翻译比对无法做到100%零失误评测样本总量偏少仅123组运行原创因果识别类猜想几乎无法产出合格创新成果无完整量化审计精确率、召回率基准数据集缺少人类专家双盲对照实验。7.3 未来研究方向构建语义审计标准基准量化审计正误精度消融实验对比纯LLM评审、仅Lean内核、CausalForge双层校验三类方案漏洞率拓展多学科专用形式库将流水线迁移至计量、生物统计等领域优化自主选题模块提升全新因果识别猜想产出质量。8 结论现有LLM自动化科研依靠大模型评审存在严重正确性隐患。本文提出CausalForge框架结合Lean4机器形式证明内核语句语义双层审计构建可信因果自动化科研体系开源完备因果形式库Causalean大幅降低定理形式化重复成本CausalSmith流水线全自动选题、形式化、证明、论文生成支持通用引理自迭代扩充基础库双层校验同时解决证明逻辑漏洞、形式语义漂移两类关键缺陷基于123组完整自动化运行记录验证系统有效性成功填补公开因果理论数学缺口。系统清晰区分证明严谨性、命题匹配度、学术价值三层独立评判标准为可信AI理论科研提供全新范式。附录A 标志性定理Lean源码文件路径完整库固定工具链leanprover/lean4:v4.29.0-rc3节选核心定理文件映射定理名称Lean文件路径do演算第二条规则SCM/Do/DoCalculus.lean后门调整识别SCM/ID/Backdoor.leanLATE Wald识别PO/ID/Exact/LATE.leanManski ATE界PO/ID/Partial/Manski/NonAsp.leanDML渐近正态估计Estimation/ATE/DML.lean交错TWFE因果分解Panel/TWFE/Decomposition.lean附录B 逻辑图存储规范每条成果独立存储FormalizationGraph对象节点属性类型、自然语言原文、Lean代码、审核状态、假设标签边区分语句依赖、证明依赖内置结构校验器拦截重复节点、非法依赖环路所有图表可导出用于论文可视化。附录C CausalSmith流水线完整操作流程全阶段有序执行序列D-1.1 文献勘探检索未解决科研缺口D-1.2 生成猜想与数学核心D0 数学推导生成初始逻辑图D0-max 最大化人工校验点可暂停人工介入D0.5 猜想创新度门限过滤ckpt D/F 分支决策是否启动高成本形式化流程F1 形式化规划检索库可复用结论F2 生成Lean代码脚手架F2.5 脚手架与原始命题首轮匹配审计F3 迭代填充证明内核编译校验F3.5 漏洞扫描sorry/非法公理/未使用假设F4 全局逻辑图收敛复审F5 论文素材整理等待人工终审流程跳转规则审计发现语义漂移退回F2重写形式代码猜想推导发现无创新直接标记Downgraded存档证明无解/命题数学错误标记Failed全部审计通过进入成果归档可启动库回流流程。附录D 实验运行记录与复现规范所有123组运行完整目录存放于仓库CausalSmith/doc/research/_bank/区分accepted/downgraded/failed三类文件夹每组包含state状态文件、完整逻辑图、所有LLM交互日志、审计报告复现环境固定Lean4版本提供一键执行脚本run_pipeline.sh统计指标全部由库索引自动生成无人工修改数据。附录E 库回流完整执行脚本引理入库自动化流程Study模式# 1. 检测逻辑图中无可用库的负载节点python pipeline_scan.py--graph./result/graph.json--outputgap_list.txt# 2. 为缺失引理生成Lean脚手架python formalize.py--targetgap_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跳转链接。开源资源总清单项目主仓库https://github.com/Jiyuan-Tan/CausalForge可视化文档站https://jiyuan-tan.github.io/CausalForge/论文PDFhttps://arxiv.org/pdf/2607.22511全套流水线执行脚本仓库scripts/目录Causalean形式化完整源码仓库Causalean/123组实验原始运行记录CausalSmith/doc/research/_bank/复现环境配置文件lakefile.lean、environment.yml所有图表、实验统计绘图代码仓库analysis/