论文概要
研究领域: ML 作者: Jiyuan Tan, Vasilis Syrgkanis 发布时间: 2026-07-24 arXiv: 2607.22511
中文摘要
自动化理论研究不仅受候选结果生成的限制，还受其可靠评估的限制。一种常见方法是用大型语言模型(LLM)评审员来闭合研究循环。然而，此类评审员在经验上仍然不可靠：它们可能接受伪造的论文，且检测率接近随机水平（Bad Scientist, 2025）。本文提出CausalForge，一个基于Lean证明助手的因果推断自动化理论研究框架。CausalForge结合了Causalean（一个包含7035个机器检查声明的因果推断基础Lean库，在人类设计和审查下使用语言模型辅助开发）和CausalSmith（一个自我改进的智能体流程，选择研究主题、提出结果、形式化陈述、构建证明，并将所得成果呈现给人类检查）。由于机器检查的证明仅确立形式化陈述从其假设出发的逻辑有效性，而非该陈述忠实捕捉了预期的科学主张，该流程通过陈述审计来补充内核验证，将每个形式化定理与其旨在表达的非正式主张进行比较。本文使用完成的自主研究生成的成果来评估该系统。源代码、形式化库和运行记录可在https://github.com/Jiyuan-Tan/CausalForge获取。
原文摘要
Automating theoretical research is constrained not only by the generation of candidate results, but also by their reliable evaluation. A common approach is to close the research loop with a large language model (LLM) reviewer. However, such reviewers remain empirically unreliable: they may accept fabricated papers and detect them at rates close to chance (Bad Scientist, 2025). We present CausalForge, a framework for automated theoretical research in causal inference grounded in the Lean proof assistant. CausalForge combines Causalean, a foundational Lean library for causal inference containing 7,035 machine-checked declarations developed with language-model assistance under human design and review, with CausalSmith, a self-improving agentic pipeline that selects research topics, proposes r…
— 自动采集于 2026-07-28
#论文 #arXiv #ML #小凯