Paper: 2607.22511 Authors: Jiyuan Tan, Vasilis Syrgkanis Categories: stat.ML, cs.AI, cs.LG, econ.EM
The Gap
Here’s the problem: people have been trying to automate theoretical research by closing the loop—LLM generates a paper, another LLM reviews it, iterate. Sounds elegant. The catch? The reviewer LLM is essentially useless. Cited work (Bad Scientist, 2025) shows LLM reviewers accept fabricated papers at rates close to random chance. So you’ve built an engine with no brakes. The whole pipeline’s credibility rests on a reviewer that can’t distinguish real from fake.
Prior approaches either (a) rely on LLM self-review, which is unreliable, or (b) use formal verification but only for narrow, pre-specified tasks. Nobody has built a full autonomous research pipeline in a scientific domain grounded in a proof assistant with a large, reusable formal library.
CausalForge fills this by: (1) building Causalean, a massive Lean library for causal inference (7,035 declarations), and (2) wrapping it in CausalSmith, an agentic pipeline where Lean’s kernel is the trust anchor, augmented by a statement audit that checks formal-informal alignment.
LLM-based research automation
|
v
LLM reviewer as quality gate
|
v
Reviewer unreliable (accepts fabrications ~randomly)
|
v
Need: mechanical trust anchor
|
v
CausalForge approach:
Causalean (7035 Lean declarations)
+ CausalSmith (agentic pipeline)
+ Lean kernel verification
+ statement audit (formal <-> informal)
|
v
Autonomous research runs produce
machine-checked artifacts
|
v
Conclusion: formal grounding makes
automated theoretical research credible
The Increment
One sentence: Before this paper, automated theoretical research relied on LLM self-judgment (unreliable); after, it has a Lean-verified pipeline with 7,000+ causal inference declarations and a statement audit ensuring formal theorems actually mean what they claim.
Core Mechanism
CausalForge has two main components that work in tandem. Causalean is a foundational Lean 4 library containing 7,035 machine-checked declarations covering core concepts in causal inference—potential outcomes, DAGs, do-calculus, identification results, and more. It was built with LLM assistance but under human design and review, meaning every declaration has been verified by Lean’s kernel and curated by experts. This library serves as both the knowledge base and the formal substrate.
CausalSmith is the agentic pipeline that uses Causalean to do research. It operates in stages: (1) topic selection—picking a research question in causal inference; (2) result proposal—generating candidate theorems or lemmas; (3) formalization—translating informal claims into Lean statements; (4) proof construction—building formal proofs using Lean tactics and Causalean’s existing declarations; (5) presentation—packaging artifacts for human inspection. The pipeline loops, learns from failures, and improves over runs.
The critical safety layer is the statement audit. A Lean proof only guarantees that a formal statement follows from assumptions—it says nothing about whether that formal statement faithfully captures the intended scientific claim. A theorem about “average treatment effect” in Lean might formally prove something subtly different from what a causal inference researcher means. The statement audit compares each formal theorem against the informal claim it’s supposed to express, catching semantic mismatches that kernel verification alone cannot.
CausalSmith (Agentic Pipeline)
|
+--> [Topic Selection]
| |
| v
+--> [Result Proposal] ---> candidate theorem (informal)
| |
| v
+--> [Formalization] -----> Lean statement (formal)
| |
| v
+--> [Proof Construction] -> Lean proof object
| |
| v
+--> [Statement Audit] ---> compare formal vs informal
| |
| v
+--> [Presentation] ------> artifact for human review
Causalean (Lean Library, 7035 declarations)
|
+-- used during Formalization
+-- used during Proof Construction
+-- verified by Lean kernel (always)
Structural Metaphor
Think of CausalForge as a constitutional court system for automated research.
Causalean is the constitution—a large, carefully written body of 7,035 articles (declarations) that define what’s legally valid in the domain of causal inference. These articles were drafted with help from assistants (LLMs) but ratified by human legislators (the authors). Every article has been reviewed and is binding law.
CausalSmith is the legislature—it proposes new laws (theorems), drafts them in proper legal language (formalizes into Lean), and argues for their passage (constructs proofs). It works autonomously, but it can only propose laws that are consistent with the constitution.
Lean’s kernel is the constitutional court—it reviews every proposed law and checks: is this consistent with the constitution? Does the logical chain hold? If not, it strikes it down (proof fails). This is the mechanical trust anchor that replaces the unreliable LLM reviewer.
The statement audit is the ombudsman—it asks a different question: “Did the legislature actually write the law they intended to write?” Sometimes a bill passes constitutional review but doesn’t match the original policy intent. The ombudsman catches these semantic gaps—cases where the formal theorem is valid but doesn’t mean what the researcher thought it meant.
Without the ombudsman (statement audit), you’d have a system where laws pass court review but might be about something entirely different from what was proposed. With it, you get both procedural correctness and semantic fidelity.
Key Concepts
-
Statement audit (formal-informal alignment): Suppose a causal inference researcher wants to prove “the backdoor criterion identifies the average treatment effect.” They write this in English (informal claim). A system translates it into Lean (formal statement). Lean proves the formal statement. Great—but did the Lean statement actually capture “average treatment effect” or something subtly different, like “conditional average treatment effect”? The statement audit is a systematic check that compares the informal intent against the formal expression. It’s like a translator who, after converting a speech from English to French, has a bilingual person verify the French version says the same thing as the English original. Without this, you can have mathematically valid proofs of the wrong thing.
-
Machine-checked declaration: In Lean, a “declaration” is a formally defined concept—like a function, a theorem, or a type. “Machine-checked” means Lean’s kernel has verified it: the type system is satisfied, the proof is valid, the definition is well-formed. This is unlike a paper theorem, which a human might have checked (or not). Causalean’s 7,035 declarations are all machine-checked, meaning they carry a mechanical guarantee of correctness. Think of it like the difference between a handwritten IOU and a notarized contract—both might be legitimate, but one carries institutional verification.
-
Self-improving agentic pipeline: “Agentic” means the system acts autonomously—selects topics, generates hypotheses, formalizes, proves, iterates. “Self-improving” means it learns from its own failures across runs. When a proof attempt fails, the system incorporates that feedback into future attempts. This is different from a one-shot LLM call that generates a paper; it’s a persistent agent that accumulates knowledge about what works. Like a researcher who keeps a lab notebook and actually reads it before designing the next experiment.
Framework Shift
Before (mainstream): After (this paper):
+-----------------------+
+----------+ +----------+ | CausalSmith Pipeline |
| LLM |-->| LLM | | |
| Generator| | Reviewer | | [Topic] --> [Propose] |
+----------+ +----------+ | | |
| | | v |
v v | [Formalize] |
"Paper" "Accept/Reject" | | |
| | | v |
+---+----------+ | [Lean Kernel Verify] |
| | | |
v | v |
Trust? (no mechanical | [Statement Audit] |
guarantee) | | |
| v |
| [Artifact + Proof] |
+-----------------------+
|
v
Machine-checked
(mechanical guarantee)
From “LLM reviews LLM’s work” to “Lean kernel verifies formal proofs with semantic audit,” the core shift is replacing probabilistic self-judgment with mechanical trust anchored in a proof assistant.
Expert Assessment
Problem choice: Real gap, well-motivated. The failure of LLM reviewers as quality gates is a genuine bottleneck for automated research. Causal inference is a good domain choice—rich enough to be interesting, structured enough for formalization, and practically important. The problem sits at the intersection of formal methods, AI agents, and scientific automation, which is a hot trajectory. Not manufactured.
Method maturity: This is more “ambitious engineering” than “clever insight.” The key ideas—formal library + agentic pipeline + kernel verification + statement audit—are individually known; the contribution is assembling them into a working system for a real domain. The 7,035-declaration library is genuine labor. The statement audit is the most interesting piece, but the paper doesn’t deeply evaluate its effectiveness—how often does it catch mismatches? How reliable is the audit itself? There’s a risk the audit is just another LLM call dressed up differently.
Experimental integrity: This is where I have concerns. The paper evaluates using “artifacts produced by completed autonomous research runs”—but how many? What’s the success rate? What fraction of attempted theorems are actually novel and correct? The abstract doesn’t give numbers, which is a yellow flag. Comparing against “LLM reviewer baseline” is a low bar. I’d want to see: how often does CausalSmith produce a genuinely new, non-trivial result vs. reproving known facts? The absence of concrete numbers in the abstract is concerning.
Writing quality: The abstract is dense and well-structured—it names the problem clearly, cites the LLM reviewer failure, introduces both components, and acknowledges the formal-informal alignment challenge. Good. However, the “evaluates using artifacts produced by completed autonomous research runs” is suspiciously vague. Section 4 (presumably experiments) is where I’d invest rewriting effort—make the evaluation concrete and quantitative.
Verdict: weak accept — The framework is novel and well-motivated, the formal library is a real contribution, but the evaluation is opaque and the statement audit’s reliability is unproven. The system is interesting; the evidence that it works is thin.
Takeaways
Three concrete things to steal:
-
The statement audit pattern: Any time you use an LLM to formalize something (code, math, legal language), add a separate check that the formal output matches the informal intent. This is a general pattern: generate formally, then audit semantic alignment. You can apply this to code generation (does the function spec match the natural language requirement?), to legal AI (does the formal clause match the policy intent?), to specification writing generally.
-
Domain-specific formal libraries as agent infrastructure: If you want an AI agent to do credible work in a domain, build a formal library first. Causalean (7,035 declarations) is the enabler. For other domains—say, mechanism design, or statistical theory—the same pattern applies: formalize the core concepts in a proof assistant, then let agents build on top. The library is the investment; the agent is the return.
-
Kernel-as-trust-anchor over LLM-as-reviewer: Whenever you need quality assurance in an automated pipeline, ask: can I replace the LLM reviewer with a mechanical check? For math and code, the answer is often yes (Lean, Coq, property-based testing). The insight is that you don’t need the reviewer to be intelligent—you need it to be *correct. Formal verification is the extreme version of this, but even lighter-weight mechanical checks (type systems, linters, formal specifications) beat LLM self-review.
论文: 2607.22511 作者: Jiyuan Tan, Vasilis Syrgkanis 分类: stat.ML, cs.AI, cs.LG, econ.EM
缺口
自动化学术研究一直有个尴尬的问题：你让 LLM 生成论文，再让另一个 LLM 审稿，听起来很美。 但 LLM 审稿人基本是摆设——引用的研究（Bad Scientist, 2025）表明，LLM 审稿人接受造假论文的概率接近随机。 你造了一台没有刹车的引擎。
此前的方案要么 (a) 依赖 LLM 自我审稿（不可靠），要么 (b) 用形式化验证但只在预设的狭窄任务上。 没有人把完整的研究流程——选题、猜想、形式化、证明、展示——建在一个定理证明器和大型形式化库之上。
CausalForge 的解法：先建 Causalean（7035 条 Lean 机器检查声明的因果推断库）， 再用 CausalSmith（自改进行为体流水线）跑通全流程，Lean 内核作为信任锚， 加上”陈述审计”检查形式定理和非形式声明的语义对齐。
LLM 驱动的研究自动化
|
v
LLM 审稿人作为质量关卡
|
v
审稿人不可靠（接受造假论文 ~随机）
|
v
需要：机械化的信任锚
|
v
CausalForge 方案：
Causalean（7035 条 Lean 声明）
+ CausalSmith（行为体流水线）
+ Lean 内核验证
+ 陈述审计（形式 <--> 非形式）
|
v
自主研究运行产出机器检查的制品
|
v
结论：形式化基础让自动化学术研究变得可信
增量
一句话: 这篇论文之前，自动化学术研究靠 LLM 自我判断（不可靠）；之后，有了一条 Lean 验证管道，配上 7000 多条因果推断形式化声明和陈述审计，确保形式定理真正表达它声称的意思。
核心机制
CausalForge 由两个主要组件协同工作。 Causalean 是一个 Lean 4 基础库，包含 7035 条机器检查声明，覆盖因果推断的核心概念：潜在结果、DAG、do-演算、识别结果等。 它在 LLM 辅助下构建，但由人类设计和审查——每条声明都经过 Lean 内核验证和专家筛选。 这个库既是知识库，也是形式化基底。
CausalSmith 是使用 Causalean 做研究的行为体流水线。 它分阶段运行：(1) 选题——挑选因果推断中的研究问题；(2) 结果提议——生成候选定理或引理； (3) 形式化——把非形式声明翻译成 Lean 语句；(4) 证明构造——利用 Lean 策略和 Causalean 已有声明构建形式证明； (5) 展示——把制品打包供人类检查。 流水线会循环运行，从失败中学习，跨运行自我改进。
最关键的安全层是陈述审计。 Lean 证明只保证形式语句能从前提推出——它不保证这个形式语句忠实捕捉了原初的科学声明。 一个关于”平均处理效应”的 Lean 定理可能形式上证明了某个微妙不同的东西。 陈述审计把每个形式定理与它要表达的非形式声明做对比，捕捉内核验证发现不了的语义错位。
CausalSmith（行为体流水线）
|
+--> [选题]
| |
| v
+--> [结果提议] ---> 候选定理（非形式）
| |
| v
+--> [形式化] -----> Lean 语句（形式）
| |
| v
+--> [证明构造] -> Lean 证明对象
| |
| v
+--> [陈述审计] ---> 对比形式 vs 非形式
| |
| v
+--> [展示] ------> 制品供人类审查
Causalean（Lean 库，7035 条声明）
|
+-- 形式化阶段使用
+-- 证明构造阶段使用
+-- 始终由 Lean 内核验证
结构性比喻
把 CausalForge 想象成一个宪政体系。
Causalean 是宪法——一部精心编纂的 7035 条条款（声明），定义了因果推断领域什么合法。 这些条款在助手（LLM）帮助下起草，但由人类立法者（作者）批准。 每条条款都经过审查，具有约束力。
CausalSmith 是立法机构——它提出新法律（定理），用规范法律语言起草（形式化为 Lean）， 论证通过（构建证明）。它自主运作，但只能提出与宪法一致的法律。
Lean 内核是宪法法院——审查每条新法律：这与宪法一致吗？逻辑链条成立吗？ 不成立就否决（证明失败）。这是取代不可靠 LLM 审稿人的机械化信任锚。
陈述审计是监察专员——它问一个不同的问题： “立法机构真的写出了他们想写的法律吗？” 有时一部法案通过了宪法审查，但与原初的政策意图不符。 监察专员捕捉这些语义偏差——形式定理有效但意思偏了的案例。
没有监察专员（陈述审计），你的法律通过了法院审查，但可能根本不是你想立的法。 有了它，程序正确性和语义忠实性都有了保障。
关键概念
-
陈述审计（形式-非形式对齐）: 假设一位因果推断研究者想证明”后门准则识别平均处理效应”。 用英文写下（非形式声明）。系统翻译成 Lean（形式语句）。Lean 证明了形式语句。 很好——但 Lean 语句真的捕捉了”平均处理效应”还是某种微妙不同的东西，比如”条件平均处理效应”？ 陈述审计就是系统地对比非形式意图和形式表达。 好比一个翻译把演讲从英文译成法文后，让一个双语者验证法文版和英文原意一致。 没有这一步，你可能得到数学上有效但证明了错误东西的证明。
-
机器检查声明: 在 Lean 中，“声明”是一个形式定义的概念——函数、定理或类型。 “机器检查”意味着 Lean 内核已验证：类型系统满足，证明有效，定义良构。 这和论文定理不同，论文定理可能被人检查过也可能没有。 Causalean 的 7035 条声明全部机器检查，携带着机械正确性保证。 好比手写借条和公证合同的区别——两者都可能合法，但一个有机构验证。
-
自改进行为体流水线: “行为体”意味着系统自主行动——选题、生成假设、形式化、证明、迭代。 “自改进”意味着它从跨运行的失败中学习。证明尝试失败时，系统把反馈融入后续尝试。 这和一次性 LLM 调用生成论文不同；它是一个持久行为体，积累什么管用的知识。 好比一个研究者保持实验笔记本，并且真的在设计下一个实验前读了它。
框架转变
之前（主流方法）： 之后（本文方法）：
+----------+ +----------+ +-------------------------+
| LLM |->| LLM | | CausalSmith 流水线 |
| 生成器 | | 审稿人 | | |
+----------+ +----------+ | [选题] --> [提议] |
| | | | |
v v | v |
"论文" "接受/拒绝" | [形式化] |
| | | | |
+--+---------+ | v |
| | [Lean 内核验证] |
v | | |
信任？（无机械保证） | v |
| [陈述审计] |
| | |
| v |
| [制品 + 证明] |
+-------------------------+
|
v
机器检查（机械保证）
从”LLM 审 LLM 的活”到”Lean 内核验证形式证明加语义审计”，核心转变是用机械化的信任锚替代概率性的自我判断。
专家评审
选题眼光: 真缺口，动机充分。LLM 审稿人作为质量关卡失败是自动化学术研究的真实瓶颈。 因果推断是不错的领域选择——足够丰富有趣，结构化程度适合形式化，且有实际重要性。 问题处于形式化方法、AI 行为体和科学自动化的交叉地带，是热门方向。不是人造问题。
方法成熟度: 更像”雄心勃勃的工程”而非”巧妙洞见”。 关键思想——形式化库 + 行为体流水线 + 内核验证 + 陈述审计——单独看都不新； 贡献在于把它们组装成一个在真实领域可工作的系统。 7035 声明库是真功夫。 陈述审计是最有趣的部分，但论文没有深入评估其有效性——多久捕捉一次错位？审计本身有多可靠？ 有风险是审计只是另一次 LLM 调用换了件衣服。
实验诚意: 这是我有顾虑的地方。 论文用”完成的自主研究运行产出的制品”来评估——但多少次运行？成功率多少？ 尝试的定理中有多少比例是真正新颖且正确的？ 摘要里不给数字，这是黄灯。 和”LLM 审稿人基线”比是低标准。 我想看到：CausalSmith 多常产出真正新的、非平凡的结果，而不是重新证明已知事实？ 摘要中缺乏具体数字让人担忧。
写作功力: 摘要写得紧凑清晰——命名问题明确，引用 LLM 审稿人失败，介绍两个组件， 还坦承形式-非形式对齐挑战。不错。 但”用完成的自主研究运行产出的制品评估”这句含糊得可疑。 第 4 节（大概是实验）是我会重点重写的地方——让评估具体、量化。
判决: 弱接收 —— 框架新颖且动机充分，形式化库是真正贡献，但评估不透明，陈述审计的可靠性未得到证明。系统有意思；证据太薄。
要点总结
三个可以偷的具体做法：
-
陈述审计模式: 任何时候你用 LLM 把东西形式化（代码、数学、法律语言），加一个独立检查确保形式输出匹配非形式意图。这是通用模式：形式生成，然后审计语义对齐。可以用在代码生成（函数规格是否匹配自然语言需求？）、法律 AI（形式条款是否匹配政策意图？）、规格书写作。陈述审计是 CausalForge 最具迁移价值的设计模式。
-
领域特定形式库作为行为体基础设施: 如果你想让 AI 行为体在某个领域做可信工作，先建形式化库。Causalean（7035 声明）是使能器。其他领域——机制设计、统计理论——同样适用：在定理证明器中形式化核心概念，然后让行为体在其上构建。库是投资，行为体是回报。
-
内核作信任锚，替代 LLM 审稿: 在自动化流水线中需要质量保证时问自己：我能用机械检查替代 LLM 审稿吗？对数学和代码，答案通常是”可以”（Lean、Coq、基于属性的测试）。关键洞见是审稿人不需要聪明——需要正确。形式化验证是这思路的极端版本，但更轻量的机械检查（类型系统、linter、形式规格）也比 LLM 自审稿强。