|
斯坦福人工智能实验室（SAIL）于2026年10月13日介绍 CausalSmith，一套面向因果推断理论研究的智能体流程。研究者 Jiyuan Tan 与 Vasilis Syrgkanis 将大语言模型用于提出研究思路、撰写自然语言定理与证明，再由另一代理审阅正确性和新颖性，随后把数学陈述形式化到 Lean 4 中验证。项目还构建了因果推断库 Causalean，供后续运行复用并扩展已验证的定义与定理。
SAIL称，截至2026年10月，系统累计运行1732次，其中41次（2.4%）被列为通过：结果需正确、完整通过Lean证明，并达到由语言模型评审的新颖性门槛；1388次被判为数学正确但贡献偏增量，303次失败。失败和通过的运行都会保存到run bank，供之后筛选与改进。
这类工具的潜在用途是帮助因果推断理论研究者探索候选结果、复核形式证明并复用领域引理，也可能让应用研究人员更方便地查阅可审计的理论工作。
边界不能忽略：形式化证明只证明Lean中的命题成立，并不自动保证它忠实表达论文中的自然语言主张，因此项目另设逐项审计；是否有趣或有用仍需人类判断。作者表示，目前只人工审查了生成论文中的一小部分，整体质量尚不清楚；“通过”是系统筛选结果，不等于同行评审或广泛验证。
官方介绍（Stanford AI Lab）：https://ai.stanford.edu/blog/causalsmith/ |
0